<?xml version="1.0" encoding="utf-8" standalone="no"?>
<!DOCTYPE svg PUBLIC "-//W3C//DTD SVG 1.1//EN" "http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd">
<svg xmlns="http://www.w3.org/2000/svg" xmlns:xl="http://www.w3.org/1999/xlink" version="1.1" viewBox="20 24 747 537" width="747pt" height="537pt" xmlns:dc="http://purl.org/dc/elements/1.1/"><metadata> Produced by OmniGraffle 6.1 <dc:date>2015-01-05 22:17:29 +0000</dc:date></metadata><defs><filter id="Shadow" filterUnits="userSpaceOnUse"><feGaussianBlur in="SourceAlpha" result="blur" stdDeviation="1.308"/><feOffset in="blur" result="offset" dx="0" dy="2"/><feFlood flood-color="black" flood-opacity=".5" result="flood"/><feComposite in="flood" in2="offset" operator="in"/></filter><filter id="Shadow_2" filterUnits="userSpaceOnUse"><feGaussianBlur in="SourceAlpha" result="blur" stdDeviation="1.308"/><feOffset in="blur" result="offset" dx="0" dy="2"/><feFlood flood-color="black" flood-opacity=".5" result="flood"/><feComposite in="flood" in2="offset" operator="in" result="color"/><feMerge><feMergeNode in="color"/><feMergeNode in="SourceGraphic"/></feMerge></filter><marker orient="auto" overflow="visible" markerUnits="strokeWidth" id="Arrow_Marker" viewBox="-1 -4 10 8" markerWidth="10" markerHeight="8" color="black"><g><path d="M 8 0 L 0 -3 L 0 3 Z" fill="none" stroke="currentColor" stroke-width="1"/></g></marker><marker orient="auto" overflow="visible" markerUnits="strokeWidth" id="Arrow_Marker_2" viewBox="-9 -4 10 8" markerWidth="10" markerHeight="8" color="black"><g><path d="M -8 0 L 0 3 L 0 -3 Z" fill="none" stroke="currentColor" stroke-width="1"/></g></marker><font-face font-family="Helvetica" font-size="11" units-per-em="1000" underline-position="-75.683594" underline-thickness="49.316406" slope="0" x-height="532.22656" cap-height="719.72656" ascent="770.01953" descent="-229.98047" font-weight="bold"><font-face-src><font-face-name name="Helvetica-Bold"/></font-face-src></font-face><font-face font-family="Helvetica" font-size="11" units-per-em="1000" underline-position="-75.683594" underline-thickness="49.316406" slope="0" x-height="522.94922" cap-height="717.28516" ascent="770.01953" descent="-229.98047" font-weight="500"><font-face-src><font-face-name name="Helvetica"/></font-face-src></font-face><font-face font-family="Lucida Grande" font-size="11" panose-1="2 11 6 0 4 5 2 2 2 4" units-per-em="1000" underline-position="-97.65625" underline-thickness="48.828125" slope="0" x-height="530.27344" cap-height="722.65625" ascent="966.7969" descent="-210.9375" font-weight="500"><font-face-src><font-face-name name="LucidaGrande"/></font-face-src></font-face><font-face font-family="Helvetica" font-size="15" units-per-em="1000" underline-position="-75.683594" underline-thickness="49.316406" slope="-800" x-height="522.94922" cap-height="717.28516" ascent="770.01953" descent="-229.98047" font-style="italic" font-weight="500"><font-face-src><font-face-name name="Helvetica-Oblique"/></font-face-src></font-face><marker orient="auto" overflow="visible" markerUnits="strokeWidth" id="FilledArrow_Marker" viewBox="-1 -4 8 8" markerWidth="8" markerHeight="8" color="black"><g><path d="M 5.5999994 0 L 0 -2.0999998 L 0 2.0999998 Z" fill="currentColor" stroke="currentColor" stroke-width="1"/></g></marker><font-face font-family="Helvetica" font-size="10" units-per-em="1000" underline-position="-75.683594" underline-thickness="49.316406" slope="0" x-height="522.94922" cap-height="717.28516" ascent="770.01953" descent="-229.98047" font-weight="500"><font-face-src><font-face-name name="Helvetica"/></font-face-src></font-face><font-face font-family="Times New Roman" font-size="20" panose-1="2 2 8 3 7 5 5 2 3 4" units-per-em="1000" underline-position="-108.88672" underline-thickness="95.214844" slope="0" x-height="456.54297" cap-height="662.10938" ascent="891.1133" descent="-216.3086" font-weight="bold"><font-face-src><font-face-name name="TimesNewRomanPS-BoldMT"/></font-face-src></font-face><marker orient="auto" overflow="visible" markerUnits="strokeWidth" id="FilledArrow_Marker_2" viewBox="-1 -2 4 4" markerWidth="4" markerHeight="4" color="black"><g><path d="M 1.6 0 L 0 -.6 L 0 .6 Z" fill="currentColor" stroke="currentColor" stroke-width="1"/></g></marker></defs><g stroke="none" stroke-opacity="1" stroke-dasharray="none" fill="none" fill-opacity="1"><title>App Types</title><rect fill="white" width="768.0188" height="588.0188"/><g><title>Layer 1</title><g><xl:use xl:href="#id50_Graphic" filter="url(#Shadow)"/><xl:use xl:href="#id65_Graphic" filter="url(#Shadow)"/></g><g filter="url(#Shadow_2)"><path d="M 327.333 77.9986 L 474.333 77.9986 C 480.40813 77.9986 485.333 82.92347 485.333 88.9986 L 485.333 311.5916 C 485.333 317.66673 480.40813 322.5916 474.333 322.5916 L 327.333 322.5916 C 321.25787 322.5916 316.333 317.66673 316.333 311.5916 L 316.333 88.9986 C 316.333 82.92347 321.25787 77.9986 327.333 77.9986 Z" stroke="red" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/></g><g id="id50_Graphic"><path d="M 282.2563 114.6481 C 282.2563 109.43795 281.63467 108.79335 277.09383 103.6371 L 277.04586 103.58375 C 272.48103 98.3736 272.43356 98.3736 267.74881 98.3736 C 261.51097 98.3736 233.309 98.3736 233.309 98.3736 L 233.309 153.3736 L 282.2563 153.3736 L 282.2563 114.6481 Z" fill="white"/><path d="M 282.2563 114.6481 C 282.2563 109.43795 281.63467 108.79335 277.09383 103.6371 L 277.04586 103.58375 C 272.48103 98.3736 272.43356 98.3736 267.74881 98.3736 C 261.51097 98.3736 233.309 98.3736 233.309 98.3736 L 233.309 153.3736 L 282.2563 153.3736 L 282.2563 114.6481 Z M 282.2563 114.3797 C 282.2563 109.43795 282.20833 109.43795 272.43356 109.43795 L 272.43356 109.43795 C 272.43356 98.4275 272.43356 98.3736 268.03564 98.3736" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/></g><line x1="31.2632" y1="385.317" x2="755.896" y2="385.317" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1" stroke-dasharray="16,9,1,9"/><line x1="300.567" y1="128.5" x2="506.433" y2="128.5" marker-end="url(#Arrow_Marker)" marker-start="url(#Arrow_Marker_2)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><text transform="translate(118.333 406.626)" fill="black"><tspan font-family="Helvetica" font-size="11" font-weight="bold" x="0" y="10" textLength="133.21924">non-functional properties</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" x="0" y="24" textLength="6.1123047">  </tspan><tspan font-family="Lucida Grande" font-size="11" font-weight="500" x="6.1123047" y="24" textLength="5.961914">■</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" x="12.074219" y="24" textLength="110.08594"> unhandled exceptions</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" x="0" y="37" textLength="41.561523">     (incl. </tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" x="40.95996" y="37" textLength="73.95996">AssertionError)</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" x="0" y="51" textLength="6.1123047">  </tspan><tspan font-family="Lucida Grande" font-size="11" font-weight="500" x="6.1123047" y="51" textLength="5.961914">■</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" x="12.074219" y="51" textLength="52.58838"> deadlocks</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" x="0" y="65" textLength="6.1123047">  </tspan><tspan font-family="Lucida Grande" font-size="11" font-weight="500" x="6.1123047" y="65" textLength="5.961914">■</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" x="12.074219" y="65" textLength="29.95459"> races</tspan></text><text transform="translate(118.333 318.229)" fill="black"><tspan font-family="Helvetica" font-size="11" font-weight="bold" x="0" y="10" textLength="119.8291">restricted choice types</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" x="0" y="24" textLength="6.1123047">  </tspan><tspan font-family="Lucida Grande" font-size="11" font-weight="500" x="6.1123047" y="24" textLength="5.961914">■</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" x="12.074219" y="24" textLength="111.91211"> scheduling sequences</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" x="0" y="38" textLength="6.1123047">  </tspan><tspan font-family="Lucida Grande" font-size="11" font-weight="500" x="6.1123047" y="38" textLength="5.961914">■</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" x="12.074219" y="38" textLength="88.04297"> java.util.Random </tspan></text><text transform="translate(118.333 478.959)" fill="black"><tspan font-family="Helvetica" font-size="11" font-weight="bold" x="0" y="10" textLength="107.572266">improved inspection</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" x="0" y="24" textLength="6.1123047">  </tspan><tspan font-family="Lucida Grande" font-size="11" font-weight="500" x="6.1123047" y="24" textLength="5.961914">■</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" x="12.074219" y="24" textLength="93.5376"> coverage statistics</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" x="0" y="38" textLength="6.1123047">  </tspan><tspan font-family="Lucida Grande" font-size="11" font-weight="500" x="6.1123047" y="38" textLength="5.961914">■</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" x="12.074219" y="38" textLength="97.22217"> exact object counts</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" x="0" y="52" textLength="6.1123047">  </tspan><tspan font-family="Lucida Grande" font-size="11" font-weight="500" x="6.1123047" y="52" textLength="5.961914">■</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" x="12.074219" y="52" textLength="78.87451"> execution costs</tspan></text><text transform="translate(36.33314 309.333) rotate(-90)" fill="black"><tspan font-family="Helvetica" font-size="15" font-style="italic" font-weight="500" x="0" y="15" textLength="72.53174">constraints</tspan></text><text transform="translate(38.9582 487.959) rotate(-90)" fill="black"><tspan font-family="Helvetica" font-size="15" font-style="italic" font-weight="500" x="0" y="15" textLength="40.86914">benefi</tspan><tspan font-family="Helvetica" font-size="15" font-style="italic" font-weight="500" x="40.86914" y="15" textLength="11.6674805">ts</tspan></text><text transform="translate(527.5 202)" fill="black"><tspan font-family="Helvetica" font-size="11" font-weight="bold" x="0" y="10" textLength="152.81836">restricted application models</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" x="0" y="24" textLength="6.1123047">  </tspan><tspan font-family="Lucida Grande" font-size="11" font-weight="500" x="6.1123047" y="24" textLength="5.961914">■</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" x="12.074219" y="24" textLength="26.280762"> UML</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" x="37.952148" y="24" textLength="73.981445"> statemachines</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" x="0" y="38" textLength="6.1123047">  </tspan><tspan font-family="Lucida Grande" font-size="11" font-weight="500" x="6.1123047" y="38" textLength="5.961914">■</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" x="12.074219" y="38" textLength="151.620605"> does not run w/o JPF libraries </tspan></text><text transform="translate(118.666 200.667)" fill="black"><tspan font-family="Helvetica" font-size="11" font-weight="bold" x="0" y="10" textLength="72.12842">runtime costs</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" x="0" y="24" textLength="6.1123047">  </tspan><tspan font-family="Lucida Grande" font-size="11" font-weight="500" x="6.1123047" y="24" textLength="5.961914">■</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" x="12.074219" y="24" textLength="130.23291"> order of magnitude slower</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" x="0" y="38" textLength="6.1123047">  </tspan><tspan font-family="Lucida Grande" font-size="11" font-weight="500" x="6.1123047" y="38" textLength="5.961914">■</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" x="12.074219" y="38" textLength="109.430664"> state storage memory</tspan></text><text transform="translate(118.333 244.97)" fill="black"><tspan font-family="Helvetica" font-size="11" font-weight="bold" x="0" y="10" textLength="127.13379">standard library support</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" x="0" y="24" textLength="6.1123047">  </tspan><tspan font-family="Lucida Grande" font-size="11" font-weight="500" x="6.1123047" y="24" textLength="5.961914">■</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" x="12.074219" y="24" textLength="116.77832"> java.net, javax.swing, ..</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" x="0" y="37" textLength="151.01367">     (needs abstraction models) </tspan></text><text transform="translate(528.197 437.293)" fill="black"><tspan font-family="Helvetica" font-size="11" font-weight="bold" x="0" y="10" textLength="158.89307">functional (domain) properties</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" x="0" y="24" textLength="6.1123047">  </tspan><tspan font-family="Lucida Grande" font-size="11" font-weight="500" x="6.1123047" y="24" textLength="5.961914">■</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" x="12.074219" y="24" textLength="120.430664"> built-in into JPF libraries</tspan></text><text transform="translate(118.666 288.728)" fill="black"><tspan font-family="Helvetica" font-size="11" font-weight="bold" x="0" y="10" textLength="160.74072">functional property impl. costs</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" x="0" y="24" textLength="6.1123047">  </tspan><tspan font-family="Lucida Grande" font-size="11" font-weight="500" x="6.1123047" y="24" textLength="5.961914">■</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" x="12.074219" y="24" textLength="123.49756"> listeners, MJI knowledge</tspan></text><text transform="translate(528.197 467.96)" fill="black"><tspan font-family="Helvetica" font-size="11" font-weight="bold" x="0" y="10" textLength="6.7192383">fl</tspan><tspan font-family="Helvetica" font-size="11" font-weight="bold" x="6.7192383" y="10" textLength="94.166016">exible state space</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" x="0" y="24" textLength="6.1123047">  </tspan><tspan font-family="Lucida Grande" font-size="11" font-weight="500" x="6.1123047" y="24" textLength="5.961914">■</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" x="12.074219" y="24" textLength="73.36914"> domain specifi</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" x="85.44336" y="24" textLength="45.853027">c choices</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" x="0" y="37" textLength="63.572266">     (e.g. UML</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" x="63.169434" y="37" textLength="91.58789"> &quot;enabling events&quot;)</tspan></text><text transform="translate(528.864 511.294)" fill="black"><tspan font-family="Helvetica" font-size="11" font-weight="bold" x="0" y="10" textLength="163.80762">runtime costs &amp; library support</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" x="0" y="24" textLength="6.1123047">  </tspan><tspan font-family="Lucida Grande" font-size="11" font-weight="500" x="6.1123047" y="24" textLength="5.961914">■</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" x="12.074219" y="24" textLength="149.80518"> usually not a problem, domain</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" x="0" y="37" textLength="147.96289">     libs can control state space</tspan></text><text transform="translate(142 114.334)" fill="black"><tspan font-family="Helvetica" font-size="11" font-weight="500" x="0" y="10" textLength="57.481445">runs on any</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" x="0" y="23" textLength="22">JVM</tspan></text><text transform="translate(597.018 112.38)" fill="black"><tspan font-family="Helvetica" font-size="11" font-weight="500" x="0" y="10" textLength="44.63379">runs only</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" x="0" y="23" textLength="50.746094">under JPF</tspan></text><text transform="translate(528.197 406.626)" fill="black"><tspan font-family="Helvetica" font-size="11" font-weight="bold" x="0" y="10" textLength="102.066895">low modeling costs</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" x="0" y="24" textLength="6.1123047">  </tspan><tspan font-family="Lucida Grande" font-size="11" font-weight="500" x="6.1123047" y="24" textLength="5.961914">■</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" x="12.074219" y="24" textLength="165.08594"> statemachine w/o layout hassle,..</tspan></text><text transform="translate(527.833 247.333)" fill="black"><tspan font-family="Helvetica" font-size="11" font-weight="bold" x="0" y="10" textLength="131.40918">initial domain impl. costs</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" x="0" y="24" textLength="6.1123047">  </tspan><tspan font-family="Lucida Grande" font-size="11" font-weight="500" x="6.1123047" y="24" textLength="5.961914">■</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" x="12.074219" y="24" textLength="126.55371"> domain libs can be tricky </tspan></text><text transform="translate(408 85.8125)" fill="black"><tspan font-family="Lucida Grande" font-size="11" font-weight="500" x="0" y="11" textLength="65.5542">&quot;sweet spot&quot;</tspan></text><text transform="translate(345.41 172.334)" fill="red"><tspan font-family="Helvetica" font-size="11" font-weight="bold" fill="red" x="0" y="10" textLength="93.51074">annotate program</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" fill="red" x="0" y="24" textLength="6.1123047">  </tspan><tspan font-family="Lucida Grande" font-size="11" font-weight="500" fill="red" x="6.1123047" y="24" textLength="5.961914">■</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" fill="red" x="12.074219" y="24" textLength="67.251465"> requirements</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" fill="red" x="0" y="38" textLength="6.1123047">  </tspan><tspan font-family="Lucida Grande" font-size="11" font-weight="500" fill="red" x="6.1123047" y="38" textLength="5.961914">■</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" fill="red" x="12.074219" y="38" textLength="89.86914"> sequences (UML)</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" fill="red" x="0" y="52" textLength="6.1123047">  </tspan><tspan font-family="Lucida Grande" font-size="11" font-weight="500" fill="red" x="6.1123047" y="52" textLength="5.961914">■</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" fill="red" x="12.074219" y="52" textLength="79.46533"> contracts (PbC)</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" fill="red" x="0" y="66" textLength="6.1123047">  </tspan><tspan font-family="Lucida Grande" font-size="11" font-weight="500" fill="red" x="6.1123047" y="66" textLength="5.961914">■</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" fill="red" x="12.074219" y="66" textLength="26.286133"> tests</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" fill="red" x="0" y="79" textLength="23.22461">    …</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" fill="red" x="0" y="92" textLength="3.0561523"> </tspan></text><text transform="translate(345.41 259.291)" fill="red"><tspan font-family="Helvetica" font-size="11" font-weight="bold" fill="red" x="0" y="10" textLength="87.41992">analyze program</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" fill="red" x="0" y="24" textLength="6.1123047">  </tspan><tspan font-family="Lucida Grande" font-size="11" font-weight="500" fill="red" x="6.1123047" y="24" textLength="5.961914">■</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" fill="red" x="12.074219" y="24" textLength="72.13379"> symbolic exec</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" fill="red" x="0" y="38" textLength="15.280762">     </tspan><tspan font-family="Lucida Grande" font-size="11" font-weight="500" fill="red" x="15.280762" y="38" textLength="11">→</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" fill="red" x="26.280762" y="38" textLength="45.251465"> test data</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" fill="red" x="0" y="52" textLength="6.1123047">  </tspan><tspan font-family="Lucida Grande" font-size="11" font-weight="500" fill="red" x="6.1123047" y="52" textLength="5.961914">■</tspan><tspan font-family="Helvetica" font-size="11" font-weight="500" fill="red" x="12.074219" y="52" textLength="105.77295"> thread safety / races </tspan></text><path d="M 443.077 271.319 C 448.50012 269.28287 455.12626 268.07605 459.348 265.21 C 463.56974 262.34395 467.8014 258.03911 468.41 254.121 C 469.0186 250.20289 466.9996 245.38813 463 241.699 C 460.3534 239.25783 455.78244 237.2113 451.19748 235.16785" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><text transform="translate(241.566 140.124)" fill="black"><tspan font-family="Helvetica" font-size="10" font-weight="500" x="0" y="10" textLength="29.453125">*.class</tspan></text><g id="id65_Graphic"><path d="M 424.2383 117.1085 C 424.2383 111.89835 423.61667 111.25375 419.07583 106.0975 L 419.02786 106.04415 C 414.46303 100.834 414.41556 100.834 409.7308 100.834 C 403.49297 100.834 375.291 100.834 375.291 100.834 L 375.291 155.834 L 424.2383 155.834 L 424.2383 117.1085 Z" fill="white"/><path d="M 424.2383 117.1085 C 424.2383 111.89835 423.61667 111.25375 419.07583 106.0975 L 419.02786 106.04415 C 414.46303 100.834 414.41556 100.834 409.7308 100.834 C 403.49297 100.834 375.291 100.834 375.291 100.834 L 375.291 155.834 L 424.2383 155.834 L 424.2383 117.1085 Z M 424.2383 116.8401 C 424.2383 111.89835 424.19033 111.89835 414.41556 111.89835 L 414.41556 111.89835 C 414.41556 100.8879 414.41556 100.834 410.01764 100.834" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/></g><text transform="translate(385.548 142.585)" fill="black"><tspan font-family="Helvetica" font-size="10" font-weight="500" x="0" y="10" textLength="25.014648">*.java</tspan></text><text transform="translate(381.548 115.758)" fill="blue"><tspan font-family="Times New Roman" font-size="20" font-weight="bold" fill="blue" x="0" y="18" textLength="33.046875">@V</tspan></text><path d="M 574.3423 117.1085 C 574.3423 111.89835 573.72067 111.25375 569.17983 106.0975 L 569.13186 106.04415 C 564.56703 100.834 564.51956 100.834 559.8348 100.834 C 553.59697 100.834 525.395 100.834 525.395 100.834 L 525.395 155.834 L 574.3423 155.834 L 574.3423 117.1085 Z" fill="white"/><path d="M 574.3423 117.1085 C 574.3423 111.89835 573.72067 111.25375 569.17983 106.0975 L 569.13186 106.04415 C 564.56703 100.834 564.51956 100.834 559.8348 100.834 C 553.59697 100.834 525.395 100.834 525.395 100.834 L 525.395 155.834 L 574.3423 155.834 L 574.3423 117.1085 Z M 574.3423 116.8401 C 574.3423 111.89835 574.29433 111.89835 564.51956 111.89835 L 564.51956 111.89835 C 564.51956 100.8879 564.51956 100.834 560.12164 100.834" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><ellipse cx="543.737" cy="113.0895" rx="5.3750086" ry="4.0625065" fill="yellow"/><ellipse cx="543.737" cy="113.0895" rx="5.3750086" ry="4.0625065" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><ellipse cx="556.987" cy="126.2145" rx="5.3750086" ry="4.0625065" fill="red"/><ellipse cx="556.987" cy="126.2145" rx="5.3750086" ry="4.0625065" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><ellipse cx="538.987" cy="135.2145" rx="5.3750086" ry="4.0625065" fill="blue"/><ellipse cx="538.987" cy="135.2145" rx="5.3750086" ry="4.0625065" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><path d="M 549.51266 113.920245 C 550.629 114.080814 551.84554 113.92592 552.862 114.402 C 553.87846 114.87808 555.03463 115.563874 555.612 116.777 C 555.80122 117.17458 555.9176 117.662774 555.9969 118.19702" marker-end="url(#FilledArrow_Marker_2)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><path d="M 559.38672 130.37215 C 560.37838 132.09026 562.65776 134.17099 562.362 135.527 C 562.06624 136.88301 560.5531 138.39227 557.612 138.509 C 555.40905 138.596435 551.6817 137.6995 548.14292 136.92421" marker-end="url(#FilledArrow_Marker_2)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><path d="M 538.68525 130.65814 C 538.5775 129.031255 537.41597 126.75709 538.362 125.777 C 539.30803 124.79691 542.22674 124.81438 544.362 124.777 C 545.42796 124.75834 546.5616 124.8872 547.71222 125.05311" marker-end="url(#FilledArrow_Marker_2)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><text transform="translate(535.842 142.467)" fill="black"><tspan font-family="Helvetica" font-size="10" font-weight="500" x="0" y="10" textLength="25.014648">*.java</tspan></text><text transform="translate(198.618 42.3331)" fill="black"><tspan font-family="Helvetica" font-size="15" font-style="italic" font-weight="500" x="0" y="15" textLength="88.374023">JPF unaware</tspan><tspan font-family="Helvetica" font-size="15" font-style="italic" font-weight="500" x="0" y="33" textLength="63.354492">programs</tspan></text><text transform="translate(354.033 33.4506)" fill="black"><tspan font-family="Helvetica" font-size="15" font-style="italic" font-weight="500" x="0" y="15" textLength="84.22119">JPF enabled</tspan><tspan font-family="Helvetica" font-size="15" font-style="italic" font-weight="500" x="0" y="33" textLength="63.354492">programs</tspan></text><text transform="translate(498.368 43.1018)" fill="black"><tspan font-family="Helvetica" font-size="15" font-style="italic" font-weight="500" x="0" y="15" textLength="101.74072">JPF dependent</tspan><tspan font-family="Helvetica" font-size="15" font-style="italic" font-weight="500" x="0" y="33" textLength="63.354492">programs</tspan></text></g></g></svg>