<?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="5 12 774 590" width="774pt" height="590pt" xmlns:dc="http://purl.org/dc/elements/1.1/"><metadata> Produced by OmniGraffle 6.1 <dc:date>2014-12-02 07:14:49 +0000</dc:date></metadata><defs><marker orient="auto" overflow="visible" markerUnits="strokeWidth" id="Arrow_Marker" viewBox="-1 -4 10 8" markerWidth="10" markerHeight="8" color="blue"><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="Courier" font-size="12" units-per-em="1000" underline-position="-144.04297" underline-thickness="91.796875" slope="0" x-height="462.40234" cap-height="594.72656" ascent="753.90625" descent="-246.09375" font-weight="bold"><font-face-src><font-face-name name="Courier-Bold"/></font-face-src></font-face><font-face font-family="Courier" font-size="12" units-per-em="1000" underline-position="-178.22266" underline-thickness="57.617188" slope="0" x-height="462.40234" cap-height="594.72656" ascent="753.90625" descent="-246.09375" font-weight="500"><font-face-src><font-face-name name="Courier"/></font-face-src></font-face><font-face font-family="Helvetica" font-size="12" 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="Helvetica" font-size="12" 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><marker orient="auto" overflow="visible" markerUnits="strokeWidth" id="UMLInheritance_Marker" viewBox="-1 -8 14 16" markerWidth="14" markerHeight="16" color="black"><g><path d="M 12 0 L 0 -7 L 0 7 Z" fill="none" stroke="currentColor" stroke-width="1"/></g></marker><font-face font-family="Helvetica" font-size="12" units-per-em="1000" underline-position="-75.683594" underline-thickness="49.316406" slope="-1e3" 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><font-face font-family="Helvetica" font-size="12" units-per-em="1000" underline-position="-75.683594" underline-thickness="49.316406" slope="-1e3" x-height="539.55078" cap-height="719.72656" ascent="770.01953" descent="-229.98047" font-style="italic" font-weight="bold"><font-face-src><font-face-name name="Helvetica-BoldOblique"/></font-face-src></font-face><marker orient="auto" overflow="visible" markerUnits="strokeWidth" id="FilledArrow_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="currentColor" stroke="currentColor" stroke-width="1"/></g></marker><marker orient="auto" overflow="visible" markerUnits="strokeWidth" id="FilledArrow_Marker_2" viewBox="-1 -4 10 8" markerWidth="10" markerHeight="8" color="blue"><g><path d="M 8 0 L 0 -3 L 0 3 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>Canvas 1</title><rect fill="white" width="768.0188" height="1176.0376"/><g><title>Layer 1</title><path d="M 624 341 L 640 341 L 640 441.1" marker-end="url(#Arrow_Marker)" stroke="blue" stroke-linecap="round" stroke-linejoin="round" stroke-width="1" stroke-dasharray="2,2"/><text transform="translate(42.3333 21.6667)" fill="blue"><tspan font-family="Courier" font-size="12" font-weight="bold" fill="blue" x="0" y="11" textLength="129.62109">initNextTransition</tspan><tspan font-family="Courier" font-size="12" font-weight="500" fill="blue" x="129.62109" y="11" textLength="43.20703">(){...</tspan><tspan font-family="Courier" font-size="12" font-weight="500" fill="blue" x="0" y="25" textLength="115.21875">  curCg = nextCg</tspan><tspan font-family="Courier" font-size="12" font-weight="500" fill="blue" x="0" y="39" textLength="108.01758">  nextCg = null</tspan><tspan font-family="Courier" font-size="12" font-weight="500" fill="blue" x="0" y="53" textLength="122.41992">  curCg.advance()</tspan><tspan font-family="Courier" font-size="12" font-weight="500" fill="blue" x="0" y="67" textLength="144.02344">   ..setExecThread()</tspan><tspan font-family="Courier" font-size="12" font-weight="500" fill="blue" x="0" y="81" textLength="36.00586">  ...</tspan></text><text transform="translate(19.7895 260)" fill="blue"><tspan font-family="Courier" font-size="12" font-weight="bold" fill="blue" x="0" y="11" textLength="122.41992">executeTransition</tspan><tspan font-family="Courier" font-size="12" font-weight="500" fill="blue" x="122.41992" y="11" textLength="36.00586">(){..</tspan><tspan font-family="Courier" font-size="12" font-weight="500" fill="blue" x="0" y="25" textLength="172.82812">  isFirstStepInsn = true</tspan><tspan font-family="Courier" font-size="12" font-weight="500" fill="blue" x="0" y="39" textLength="158.42578">  while (pc != null) {</tspan><tspan font-family="Courier" font-size="12" font-weight="500" fill="blue" x="0" y="53" textLength="237.63867">    nextPc = executeInstruction()</tspan><tspan font-family="Courier" font-size="12" font-weight="500" fill="blue" x="0" y="67" textLength="208.83398">    if (ss.breakTransition())</tspan><tspan font-family="Courier" font-size="12" font-weight="500" fill="blue" x="0" y="81" textLength="79.21289">      break</tspan><tspan font-family="Courier" font-size="12" font-weight="500" fill="blue" x="0" y="95" textLength="57.609375">    else</tspan><tspan font-family="Courier" font-size="12" font-weight="500" fill="blue" x="0" y="109" textLength="122.41992">      pc = nextPc</tspan><tspan font-family="Courier" font-size="12" font-weight="500" fill="blue" x="0" y="123" textLength="194.43164">    isFirstStepInsn = false</tspan></text><text transform="translate(252.667 349.409)" fill="blue"><tspan font-family="Courier" font-size="12" font-weight="bold" fill="blue" x="0" y="11" textLength="64.810547">execute()</tspan><tspan font-family="Courier" font-size="12" font-weight="500" fill="blue" x="64.810547" y="11" textLength="21.603516">{..</tspan><tspan font-family="Courier" font-size="12" font-weight="500" fill="blue" x="0" y="25" textLength="180.0293">  if (!ti.isFirstStepInsn</tspan><tspan font-family="Courier" font-size="12" font-weight="bold" fill="blue" x="180.0293" y="25" textLength="14.402344">()</tspan><tspan font-family="Courier" font-size="12" font-weight="500" fill="blue" x="194.43164" y="25" textLength="21.603516">) {</tspan><tspan font-family="Courier" font-size="12" font-weight="500" fill="blue" x="0" y="39" textLength="180.0293">    ChoiceGenerator cg = </tspan><tspan font-family="Courier" font-size="12" font-weight="500" fill="blue" x="0" y="53" textLength="259.24219">          ..createMonitorEnterCG(..)</tspan><tspan font-family="Courier" font-size="12" font-weight="500" fill="blue" x="0" y="67" textLength="144.02344">    if (cg != null){</tspan><tspan font-family="Courier" font-size="12" font-weight="500" fill="blue" x="0" y="81" textLength="252.04102">      ss.setNextChoiceGenerator(cg)</tspan><tspan font-family="Courier" font-size="12" font-weight="500" fill="blue" x="0" y="95" textLength="194.43164">      return this // repeat</tspan><tspan font-family="Courier" font-size="12" font-weight="500" fill="blue" x="0" y="109" textLength="21.603516">  }</tspan><tspan font-family="Courier" font-size="12" font-weight="500" fill="blue" x="0" y="137" textLength="93.615234">  ei.lock(ti)</tspan><tspan font-family="Courier" font-size="12" font-weight="500" fill="blue" x="0" y="151" textLength="165.62695">  return getNextPc(ti);</tspan></text><rect x="458.041" y="280.5" width="90" height="14" fill="white"/><rect x="458.041" y="280.5" width="90" height="14" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><text transform="translate(463.041 280.5)" fill="black"><tspan font-family="Helvetica" font-size="12" font-weight="500" x="0" y="11" textLength="50.021484">execute()</tspan></text><rect x="458.041" y="266.5" width="90" height="14" fill="white"/><rect x="458.041" y="266.5" width="90" height="14" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><text transform="translate(463.041 266.5)" fill="black"><tspan font-family="Helvetica" font-size="12" font-weight="bold" x="9.0009766" y="11" textLength="61.998047">Instruction</tspan></text><rect x="254" y="65" width="152" height="42" fill="white"/><rect x="254" y="65" width="152" height="42" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><text transform="translate(259 65)" fill="black"><tspan font-family="Helvetica" font-size="12" font-weight="500" x="0" y="11" textLength="47.34375">initNextT</tspan><tspan font-family="Helvetica" font-size="12" font-weight="500" x="46.904297" y="11" textLength="53.34961">ransition()</tspan><tspan font-family="Helvetica" font-size="12" font-weight="500" x="0" y="25" textLength="37.347656">breakT</tspan><tspan font-family="Helvetica" font-size="12" font-weight="500" x="36.908203" y="25" textLength="53.34961">ransition()</tspan><tspan font-family="Helvetica" font-size="12" font-weight="500" x="0" y="39" textLength="140.05664">setNextChoiceGenerator()</tspan></text><rect x="254" y="37" width="152" height="28" fill="white"/><rect x="254" y="37" width="152" height="28" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><text transform="translate(259 37)" fill="black"><tspan font-family="Helvetica" font-size="12" font-weight="500" x="0" y="11" textLength="38.021484">nextCg</tspan><tspan font-family="Helvetica" font-size="12" font-weight="500" x="0" y="25" textLength="32.009766">curCg</tspan></text><rect x="254" y="23" width="152" height="14" fill="white"/><rect x="254" y="23" width="152" height="14" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><text transform="translate(259 23)" fill="black"><tspan font-family="Helvetica" font-size="12" font-weight="bold" x="34.982422" y="11" textLength="72.035156">SystemState</tspan></text><rect x="547.541" y="60" width="113.459" height="28" fill="white"/><rect x="547.541" y="60" width="113.459" height="28" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><text transform="translate(552.541 60)" fill="black"><tspan font-family="Helvetica" font-size="12" font-weight="500" x="0" y="11" textLength="98.033203">hasMoreChoices()</tspan><tspan font-family="Helvetica" font-size="12" font-weight="500" x="0" y="25" textLength="53.361328">advance()</tspan></text><rect x="547.541" y="46" width="113.459" height="14" fill="white"/><rect x="547.541" y="46" width="113.459" height="14" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><text transform="translate(552.541 46)" fill="black"><tspan font-family="Helvetica" font-size="12" font-weight="bold" x="3.0498125" y="11" textLength="97.359375">ChoiceGenerator</tspan></text><rect x="472" y="153" width="101" height="14" fill="white"/><rect x="472" y="153" width="101" height="14" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><text transform="translate(477 153)" fill="black"><tspan font-family="Helvetica" font-size="12" font-weight="500" x="0" y="11" textLength="86.70117">getNextChoice()</tspan></text><rect x="472" y="139" width="101" height="14" fill="white"/><rect x="472" y="139" width="101" height="14" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><text transform="translate(477 139)" fill="black"><tspan font-family="Helvetica" font-size="12" font-weight="500" x="0" y="11" textLength="52.03711">threadSet</tspan></text><rect x="472" y="125" width="101" height="14" fill="white"/><rect x="472" y="125" width="101" height="14" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><text transform="translate(477 125)" fill="black"><tspan font-family="Helvetica" font-size="12" font-weight="bold" x="16.496094" y="11" textLength="58.007812">ThreadCG</tspan></text><rect x="596" y="153" width="101" height="14" fill="white"/><rect x="596" y="153" width="101" height="14" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><text transform="translate(601 153)" fill="black"><tspan font-family="Helvetica" font-size="12" font-weight="500" x="0" y="11" textLength="86.70117">getNextChoice()</tspan></text><rect x="596" y="139" width="101" height="14" fill="white"/><rect x="596" y="139" width="101" height="14" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><text transform="translate(601 139)" fill="black"><tspan font-family="Helvetica" font-size="12" font-weight="500" x="0" y="11" textLength="54.046875">doubleSet</tspan></text><rect x="596" y="125" width="101" height="14" fill="white"/><rect x="596" y="125" width="101" height="14" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><text transform="translate(601 125)" fill="black"><tspan font-family="Helvetica" font-size="12" font-weight="bold" x="16.167969" y="11" textLength="58.664062">DoubleCG</tspan></text><rect x="713.438" y="125" width="54" height="18" fill="white"/><rect x="713.438" y="125" width="54" height="18" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><text transform="translate(718.438 127)" fill="black"><tspan font-family="Helvetica" font-size="12" font-weight="bold" x="16.999023" y="11" textLength="10.001953">...</tspan></text><rect x="495" y="190" width="54" height="18" fill="white"/><rect x="495" y="190" width="54" height="18" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><text transform="translate(500 192)" fill="black"><tspan font-family="Helvetica" font-size="12" font-weight="bold" x="16.999023" y="11" textLength="10.001953">...</tspan></text><rect x="85.4035" y="207" width="118" height="42" fill="white"/><rect x="85.4035" y="207" width="118" height="42" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><text transform="translate(90.4035 207)" fill="black"><tspan font-family="Helvetica" font-size="12" font-weight="500" x="0" y="11" textLength="49.359375">executeT</tspan><tspan font-family="Helvetica" font-size="12" font-weight="500" x="48.919922" y="11" textLength="53.34961">ransition()</tspan><tspan font-family="Helvetica" font-size="12" font-weight="500" x="0" y="25" textLength="105.38086">executeInstruction()</tspan><tspan font-family="Helvetica" font-size="12" font-weight="500" x="0" y="39" textLength="87.35156">isFirstStepInsn()</tspan></text><rect x="85.4035" y="193" width="118" height="14" fill="white"/><rect x="85.4035" y="193" width="118" height="14" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><text transform="translate(90.4035 193)" fill="black"><tspan font-family="Helvetica" font-size="12" font-weight="500" x="0" y="11" textLength="64.04297">{pc, nextPc}</tspan></text><rect x="85.4035" y="179" width="118" height="14" fill="white"/><rect x="85.4035" y="179" width="118" height="14" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><text transform="translate(90.4035 179)" fill="black"><tspan font-family="Helvetica" font-size="12" font-weight="bold" x="23.000977" y="11" textLength="61.998047">ThreadInfo</tspan></text><line x1="609.041" y1="112" x2="609.041" y2="101.5" marker-end="url(#UMLInheritance_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><path d="M 521.57353 125 L 521 112 L 740.403 112 L 740.438 125" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><line x1="646.4202" y1="125" x2="646.3708" y2="112" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><line x1="522" y1="190.257" x2="522" y2="179.757" marker-end="url(#UMLInheritance_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><rect x="366.5" y="327.5" width="90" height="18" fill="white"/><rect x="366.5" y="327.5" width="90" height="18" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><text transform="translate(371.5 329.5)" fill="black"><tspan font-family="Helvetica" font-size="12" font-weight="bold" x="2.6699219" y="11" textLength="74.660156">MonitorEnter</tspan></text><rect x="553.5" y="327.5" width="68" height="18" fill="white"/><rect x="553.5" y="327.5" width="68" height="18" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><text transform="translate(558.5 329.5)" fill="black"><tspan font-family="Helvetica" font-size="12" font-weight="bold" x="6.658203" y="11" textLength="44.683594">Invoke..</tspan></text><rect x="476.703" y="327.5" width="54" height="18" fill="white"/><rect x="476.703" y="327.5" width="54" height="18" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><text transform="translate(481.703 329.5)" fill="black"><tspan font-family="Helvetica" font-size="12" font-weight="bold" x="16.999023" y="11" textLength="10.001953">...</tspan></text><line x1="503.5" y1="318.5" x2="503.5" y2="308" marker-end="url(#UMLInheritance_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><path d="M 411.5 327.5 L 411.5 318.5 L 587.458 318.5 L 587.5 327.5" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><line x1="503.703" y1="327.5" x2="503.87076" y2="318.5" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><rect x="573.5" y="363.833" width="83" height="18" fill="white"/><rect x="573.5" y="363.833" width="83" height="18" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><text transform="translate(578.5 365.833)" fill="black"><tspan font-family="Helvetica" font-size="12" font-weight="bold" x="4.1767578" y="11" textLength="64.646484">MethodInfo</tspan></text><rect x="591.5" y="399.833" width="83" height="18" fill="white"/><rect x="591.5" y="399.833" width="83" height="18" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><text transform="translate(596.5 401.833)" fill="black"><tspan font-family="Helvetica" font-size="12" font-weight="bold" x="5.4804688" y="11" textLength="62.039062">NativePeer</tspan></text><text transform="translate(463.041 446)" fill="red"><tspan font-family="Helvetica" font-size="12" font-style="italic" font-weight="500" fill="red" x="0" y="11" textLength="160.0957">e.g. JPF_gov_nasa_jpf_vm_V</tspan><tspan font-family="Helvetica" font-size="12" font-style="italic" font-weight="500" fill="red" x="159.43945" y="11" textLength="22.669922">erify</tspan><tspan font-family="Helvetica" font-size="12" font-style="italic" font-weight="500" fill="red" x="181.22461" y="11" textLength="91.39453">.getBoolean(env)</tspan></text><line x1="210" y1="469.665" x2="362" y2="469.665" stroke="red" stroke-linecap="round" stroke-linejoin="round" stroke-width="2" stroke-dasharray="8,4,1,4"/><text transform="translate(35 434.665)" fill="red"><tspan font-family="Helvetica" font-size="12" font-style="italic" font-weight="bold" fill="red" x="0" y="11" textLength="43.32422">top half</tspan><tspan font-family="Helvetica" font-size="12" font-style="italic" font-weight="500" fill="red" x="43.32422" y="11" textLength="81.38672">: executed on fi</tspan><tspan font-family="Helvetica" font-size="12" font-style="italic" font-weight="500" fill="red" x="124.71094" y="11" textLength="70.69922">rst invocation</tspan><tspan font-family="Helvetica" font-size="12" font-style="italic" font-weight="500" fill="red" x="0" y="25" textLength="208.78125">optionally sets next CG and reexecutes</tspan></text><text transform="translate(35 475.665)" fill="red"><tspan font-family="Helvetica" font-size="12" font-style="italic" font-weight="bold" fill="red" x="0" y="11" textLength="65.320312">bottom half</tspan><tspan font-family="Helvetica" font-size="12" font-style="italic" font-weight="500" fill="red" x="65.320312" y="11" textLength="124.722656">: executed on revisit (or</tspan><tspan font-family="Helvetica" font-size="12" font-style="italic" font-weight="500" fill="red" x="0" y="25" textLength="187.42969">if no CG created because of policy)</tspan><tspan font-family="Helvetica" font-size="12" font-style="italic" font-weight="500" fill="red" x="0" y="39" textLength="165.43945">does semantic action based on</tspan><tspan font-family="Helvetica" font-size="12" font-style="italic" font-weight="500" fill="red" x="0" y="53" textLength="102.703125">current CGs choice</tspan></text><line x1="585" y1="131" x2="586" y2="246" stroke="red" stroke-linecap="round" stroke-linejoin="round" stroke-width="2" stroke-dasharray="8,4,1,4"/><text transform="translate(468 224)" fill="red"><tspan font-family="Helvetica" font-size="12" font-style="italic" font-weight="500" fill="red" x="0" y="11" textLength="101.396484">scheduling choices</tspan></text><text transform="translate(601.5 224)" fill="red"><tspan font-family="Helvetica" font-size="12" font-style="italic" font-weight="500" fill="red" x="0" y="11" textLength="127.41211">data acquisition choices</tspan></text><path d="M 700 163 L 747 163 L 747 546.1" marker-end="url(#Arrow_Marker)" stroke="blue" stroke-linecap="round" stroke-linejoin="round" stroke-width="1" stroke-dasharray="2,2"/><line x1="406" y1="71" x2="537.641" y2="71" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><path d="M 194 249 C 222 278.6667 258.6663 285.99975 307.333 289.333 C 352.12157 292.40069 408.50888 290.38684 448.14126 290.04641" marker-end="url(#FilledArrow_Marker_2)" stroke="blue" stroke-linecap="round" stroke-linejoin="round" stroke-width="1" stroke-dasharray="2,2"/><circle cx="263.333" cy="171" r="8.000013" stroke="blue" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><text transform="translate(261.933 164)" fill="blue"><tspan font-family="Helvetica" font-size="12" font-weight="500" fill="blue" x="0" y="11" textLength="6.673828">1</tspan></text><circle cx="314.667" cy="277.333" r="8.000013" stroke="blue" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><text transform="translate(313.267 270.333)" fill="blue"><tspan font-family="Helvetica" font-size="12" font-weight="500" fill="blue" x="0" y="11" textLength="6.673828">2</tspan></text><circle cx="374.5" cy="207.333" r="8.000013" stroke="blue" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><text transform="translate(373.1 200.333)" fill="blue"><tspan font-family="Helvetica" font-size="12" font-weight="500" fill="blue" x="0" y="11" textLength="6.673828">3</tspan></text><line x1="426.041" y1="531.45" x2="585" y2="531.45" stroke="red" stroke-linecap="round" stroke-linejoin="round" stroke-width="2" stroke-dasharray="8,4,1,4"/><text transform="translate(424.333 511.333)" fill="red"><tspan font-family="Helvetica" font-size="12" font-style="italic" font-weight="500" fill="red" x="0" y="11" textLength="39.363281">top half</tspan></text><text transform="translate(423.667 536.333)" fill="red"><tspan font-family="Helvetica" font-size="12" font-style="italic" font-weight="500" fill="red" x="0" y="11" textLength="36.685547">bottom</tspan><tspan font-family="Helvetica" font-size="12" font-style="italic" font-weight="500" fill="red" x="0" y="25" textLength="19.347656">half</tspan></text><text transform="translate(465 466.95)" fill="blue"><tspan font-family="Courier" font-size="12" font-weight="500" fill="blue" x="0" y="11" textLength="194.43164">if (!ti.isFirstStepInsn()){</tspan><tspan font-family="Courier" font-size="12" font-weight="500" fill="blue" x="0" y="25" textLength="158.42578">  cg = new BooleanCG()</tspan><tspan font-family="Courier" font-size="12" font-weight="500" fill="blue" x="0" y="39" textLength="223.23633">  ss.setNextChoiceGenerator(cg)</tspan><tspan font-family="Courier" font-size="12" font-weight="500" fill="blue" x="0" y="53" textLength="194.43164">  env.repeatInvocation() ..</tspan><tspan font-family="Courier" font-size="12" font-weight="500" fill="blue" x="0" y="81" textLength="57.609375">} else {</tspan><tspan font-family="Courier" font-size="12" font-weight="500" fill="blue" x="0" y="95" textLength="216.03516">  cg = ss.getChoiceGenerator()</tspan><tspan font-family="Courier" font-size="12" font-weight="500" fill="blue" x="0" y="109" textLength="288.04688">  return ((BooleanCG)cg).getNextChoice()</tspan><tspan font-family="Courier" font-size="12" font-weight="500" fill="blue" x="0" y="123" textLength="7.201172">}</tspan></text><text transform="translate(56 126.333)" fill="blue"><tspan font-family="Courier" font-size="12" font-weight="bold" fill="blue" x="0" y="11" textLength="108.01758">breakTransition</tspan><tspan font-family="Courier" font-size="12" font-weight="500" fill="blue" x="108.01758" y="11" textLength="43.20703">(){...</tspan><tspan font-family="Courier" font-size="12" font-weight="500" fill="blue" x="0" y="25" textLength="165.62695">  return nextCg != null</tspan></text><path d="M 301.333 106 C 299.99966 155.3333 295.3337 164.6667 280.667 179 C 267.09314 192.2653 251.8064 204.10311 213.1948 210.54982" marker-end="url(#FilledArrow_Marker_2)" stroke="blue" stroke-linecap="round" stroke-linejoin="round" stroke-width="1" stroke-dasharray="2,2"/><path d="M 458.041 277.333 C 382.6786 281.99966 361.33353 214.0001 353 187.667 C 345.40257 163.6599 344.73164 148.240585 344.60825 115.9" marker-end="url(#FilledArrow_Marker_2)" stroke="blue" stroke-linecap="round" stroke-linejoin="round" stroke-width="1" stroke-dasharray="2,2"/></g></g></svg>