SCCD/test_files/day_atlee/statechart_fig20_invar.svg

<?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">
<!-- Generated by graphviz version 2.40.1 (20161225.0304)
 -->
<!-- Title: state transitions Pages: 1 -->
<svg width="307pt" height="578pt"
 viewBox="0.00 0.00 306.56 578.00" xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink">
<g id="graph0" class="graph" transform="scale(1 1) rotate(0) translate(4 574)">
<title>state transitions</title>
<polygon fill="#ffffff" stroke="transparent" points="-4,4 -4,-574 302.561,-574 302.561,4 -4,4"/>
<g id="clust1" class="cluster">
<title>cluster__Invar</title>
<path fill="none" stroke="#000000" stroke-width="2" d="M20,-74C20,-74 221,-74 221,-74 227,-74 233,-80 233,-86 233,-86 233,-519 233,-519 233,-525 227,-531 221,-531 221,-531 20,-531 20,-531 14,-531 8,-525 8,-519 8,-519 8,-86 8,-86 8,-80 14,-74 20,-74"/>
<text text-anchor="start" x="107.1644" y="-512.2" font-family="Helvetica,sans-Serif" font-size="12.00" fill="#000000">Invar</text>
</g>
<g id="clust2" class="cluster">
<title>cluster__Invar_I2</title>
<polygon fill="none" stroke="#000000" stroke-dasharray="5,2" points="136,-82 136,-493 225,-493 225,-82 136,-82"/>
<text text-anchor="start" x="175.4972" y="-474.2" font-family="Helvetica,sans-Serif" font-size="12.00" fill="#000000">I2</text>
</g>
<g id="clust3" class="cluster">
<title>cluster__Invar_I1</title>
<polygon fill="none" stroke="#000000" stroke-dasharray="5,2" points="24,-82 24,-493 128,-493 128,-82 24,-82"/>
<text text-anchor="start" x="70.9972" y="-474.2" font-family="Helvetica,sans-Serif" font-size="12.00" fill="#000000">I1</text>
</g>
<!-- __initial -->
<g id="node1" class="node">
<title>__initial</title>
<ellipse fill="#000000" stroke="#000000" stroke-width="2" cx="16" cy="-564.5" rx="5.5" ry="5.5"/>
</g>
<!-- _Invar -->
<!-- __initial&#45;&gt;_Invar -->
<g id="edge1" class="edge">
<title>__initial&#45;&gt;_Invar</title>
<path fill="none" stroke="#000000" d="M16,-558.9533C16,-554.7779 16,-548.5043 16,-541.0332"/>
<polygon fill="#000000" stroke="#000000" points="19.5001,-540.9971 16,-530.9971 12.5001,-540.9972 19.5001,-540.9971"/>
<text text-anchor="middle" x="17.3895" y="-542" font-family="Helvetica,sans-Serif" font-size="10.00" fill="#000000"> </text>
</g>
<!-- _Done -->
<g id="node2" class="node">
<title>_Done</title>
<polygon fill="transparent" stroke="transparent" stroke-width="2" points="219,-46 125,-46 125,0 219,0 219,-46"/>
<text text-anchor="start" x="157.6624" y="-29.2" font-family="Helvetica,sans-Serif" font-size="12.00" fill="#000000">Done</text>
<text text-anchor="start" x="130.501" y="-9.2" font-family="Helvetica,sans-Serif" font-size="12.00" fill="#000000">enter ^out.done</text>
<polygon fill="#000000" stroke="#000000" points="125,-23 125,-23 219,-23 219,-23 125,-23"/>
<path fill="none" stroke="#000000" stroke-width="2" d="M138,-1C138,-1 206,-1 206,-1 212,-1 218,-7 218,-13 218,-13 218,-33 218,-33 218,-39 212,-45 206,-45 206,-45 138,-45 138,-45 132,-45 126,-39 126,-33 126,-33 126,-13 126,-13 126,-7 132,-1 138,-1"/>
</g>
<!-- _Invar_I2 -->
<!-- _Invar_I2_initial -->
<g id="node5" class="node">
<title>_Invar_I2_initial</title>
<ellipse fill="#000000" stroke="#000000" stroke-width="2" cx="172" cy="-449.5" rx="5.5" ry="5.5"/>
</g>
<!-- _Invar_I2_S4 -->
<g id="node8" class="node">
<title>_Invar_I2_S4</title>
<polygon fill="transparent" stroke="transparent" stroke-width="2" points="200,-362 144,-362 144,-326 200,-326 200,-362"/>
<text text-anchor="start" x="164.6632" y="-340.2" font-family="Helvetica,sans-Serif" font-size="12.00" fill="#000000">S4</text>
<path fill="none" stroke="#000000" stroke-width="2" d="M156.3333,-327C156.3333,-327 187.6667,-327 187.6667,-327 193.3333,-327 199,-332.6667 199,-338.3333 199,-338.3333 199,-349.6667 199,-349.6667 199,-355.3333 193.3333,-361 187.6667,-361 187.6667,-361 156.3333,-361 156.3333,-361 150.6667,-361 145,-355.3333 145,-349.6667 145,-349.6667 145,-338.3333 145,-338.3333 145,-332.6667 150.6667,-327 156.3333,-327"/>
</g>
<!-- _Invar_I2_initial&#45;&gt;_Invar_I2_S4 -->
<g id="edge2" class="edge">
<title>_Invar_I2_initial&#45;&gt;_Invar_I2_S4</title>
<path fill="none" stroke="#000000" d="M172,-443.8288C172,-439.1736 172,-432.4097 172,-426.5 172,-426.5 172,-426.5 172,-379.5 172,-377.1079 172,-374.6252 172,-372.1342"/>
<polygon fill="#000000" stroke="#000000" points="175.5001,-372.0597 172,-362.0598 168.5001,-372.0598 175.5001,-372.0597"/>
<text text-anchor="middle" x="173.3895" y="-400" font-family="Helvetica,sans-Serif" font-size="10.00" fill="#000000"> </text>
</g>
<!-- _Invar_I2_S6 -->
<g id="node6" class="node">
<title>_Invar_I2_S6</title>
<polygon fill="transparent" stroke="transparent" stroke-width="2" points="200,-126 144,-126 144,-90 200,-90 200,-126"/>
<text text-anchor="start" x="164.6632" y="-104.2" font-family="Helvetica,sans-Serif" font-size="12.00" fill="#000000">S6</text>
<path fill="none" stroke="#000000" stroke-width="2" d="M156.3333,-91C156.3333,-91 187.6667,-91 187.6667,-91 193.3333,-91 199,-96.6667 199,-102.3333 199,-102.3333 199,-113.6667 199,-113.6667 199,-119.3333 193.3333,-125 187.6667,-125 187.6667,-125 156.3333,-125 156.3333,-125 150.6667,-125 145,-119.3333 145,-113.6667 145,-113.6667 145,-102.3333 145,-102.3333 145,-96.6667 150.6667,-91 156.3333,-91"/>
</g>
<!-- _Invar_I2_S6&#45;&gt;_Done -->
<g id="edge3" class="edge">
<title>_Invar_I2_S6&#45;&gt;_Done</title>
<path fill="none" stroke="#000000" d="M172,-89.9737C172,-80.1983 172,-67.8024 172,-56.3399"/>
<polygon fill="#000000" stroke="#000000" points="175.5001,-56.1774 172,-46.1775 168.5001,-56.1775 175.5001,-56.1774"/>
<text text-anchor="start" x="172" y="-57" font-family="Helvetica,sans-Serif" font-size="10.00" fill="#000000">[INSTATE([&quot;/Invar/I1/S3&quot;])] &#160;&#160;</text>
</g>
<!-- _Invar_I2_S5 -->
<g id="node7" class="node">
<title>_Invar_I2_S5</title>
<polygon fill="transparent" stroke="transparent" stroke-width="2" points="200,-244 144,-244 144,-208 200,-208 200,-244"/>
<text text-anchor="start" x="164.6632" y="-222.2" font-family="Helvetica,sans-Serif" font-size="12.00" fill="#000000">S5</text>
<path fill="none" stroke="#000000" stroke-width="2" d="M156.3333,-209C156.3333,-209 187.6667,-209 187.6667,-209 193.3333,-209 199,-214.6667 199,-220.3333 199,-220.3333 199,-231.6667 199,-231.6667 199,-237.3333 193.3333,-243 187.6667,-243 187.6667,-243 156.3333,-243 156.3333,-243 150.6667,-243 145,-237.3333 145,-231.6667 145,-231.6667 145,-220.3333 145,-220.3333 145,-214.6667 150.6667,-209 156.3333,-209"/>
</g>
<!-- _Invar_I2_S5&#45;&gt;_Invar_I2_S6 -->
<g id="edge4" class="edge">
<title>_Invar_I2_S5&#45;&gt;_Invar_I2_S6</title>
<path fill="none" stroke="#000000" d="M169.1785,-207.9844C168.5166,-202.3957 168,-196.206 168,-190.5 168,-190.5 168,-190.5 168,-143.5 168,-141.0928 168.0919,-138.5995 168.248,-136.1015"/>
<polygon fill="#000000" stroke="#000000" points="171.7449,-136.2949 169.1785,-126.0156 164.7745,-135.6517 171.7449,-136.2949"/>
<text text-anchor="start" x="168" y="-164" font-family="Helvetica,sans-Serif" font-size="10.00" fill="#000000">/a = 3 * a &#160;&#160;</text>
</g>
<!-- _Invar_I2_S4&#45;&gt;_Invar_I2_S5 -->
<g id="edge5" class="edge">
<title>_Invar_I2_S4&#45;&gt;_Invar_I2_S5</title>
<path fill="none" stroke="#000000" d="M167.7033,-325.6741C166.7416,-320.1833 166,-314.1255 166,-308.5 166,-308.5 166,-308.5 166,-261.5 166,-259.2146 166.1224,-256.8579 166.3322,-254.4969"/>
<polygon fill="#000000" stroke="#000000" points="169.8359,-254.7039 167.7033,-244.3259 162.8986,-253.7687 169.8359,-254.7039"/>
<text text-anchor="start" x="166" y="-282" font-family="Helvetica,sans-Serif" font-size="10.00" fill="#000000">/a = a + b &#160;&#160;</text>
</g>
<!-- _Invar_I1 -->
<!-- _Invar_I1_initial -->
<g id="node10" class="node">
<title>_Invar_I1_initial</title>
<ellipse fill="#000000" stroke="#000000" stroke-width="2" cx="60" cy="-449.5" rx="5.5" ry="5.5"/>
</g>
<!-- _Invar_I1_S1 -->
<g id="node13" class="node">
<title>_Invar_I1_S1</title>
<polygon fill="transparent" stroke="transparent" stroke-width="2" points="88,-362 32,-362 32,-326 88,-326 88,-362"/>
<text text-anchor="start" x="52.6632" y="-340.2" font-family="Helvetica,sans-Serif" font-size="12.00" fill="#000000">S1</text>
<path fill="none" stroke="#000000" stroke-width="2" d="M44.3333,-327C44.3333,-327 75.6667,-327 75.6667,-327 81.3333,-327 87,-332.6667 87,-338.3333 87,-338.3333 87,-349.6667 87,-349.6667 87,-355.3333 81.3333,-361 75.6667,-361 75.6667,-361 44.3333,-361 44.3333,-361 38.6667,-361 33,-355.3333 33,-349.6667 33,-349.6667 33,-338.3333 33,-338.3333 33,-332.6667 38.6667,-327 44.3333,-327"/>
</g>
<!-- _Invar_I1_initial&#45;&gt;_Invar_I1_S1 -->
<g id="edge6" class="edge">
<title>_Invar_I1_initial&#45;&gt;_Invar_I1_S1</title>
<path fill="none" stroke="#000000" d="M60,-443.8288C60,-439.1736 60,-432.4097 60,-426.5 60,-426.5 60,-426.5 60,-379.5 60,-377.1079 60,-374.6252 60,-372.1342"/>
<polygon fill="#000000" stroke="#000000" points="63.5001,-372.0597 60,-362.0598 56.5001,-372.0598 63.5001,-372.0597"/>
<text text-anchor="middle" x="61.3895" y="-400" font-family="Helvetica,sans-Serif" font-size="10.00" fill="#000000"> </text>
</g>
<!-- _Invar_I1_S3 -->
<g id="node11" class="node">
<title>_Invar_I1_S3</title>
<polygon fill="transparent" stroke="transparent" stroke-width="2" points="88,-126 32,-126 32,-90 88,-90 88,-126"/>
<text text-anchor="start" x="52.6632" y="-104.2" font-family="Helvetica,sans-Serif" font-size="12.00" fill="#000000">S3</text>
<path fill="none" stroke="#000000" stroke-width="2" d="M44.3333,-91C44.3333,-91 75.6667,-91 75.6667,-91 81.3333,-91 87,-96.6667 87,-102.3333 87,-102.3333 87,-113.6667 87,-113.6667 87,-119.3333 81.3333,-125 75.6667,-125 75.6667,-125 44.3333,-125 44.3333,-125 38.6667,-125 33,-119.3333 33,-113.6667 33,-113.6667 33,-102.3333 33,-102.3333 33,-96.6667 38.6667,-91 44.3333,-91"/>
</g>
<!-- _Invar_I1_S2 -->
<g id="node12" class="node">
<title>_Invar_I1_S2</title>
<polygon fill="transparent" stroke="transparent" stroke-width="2" points="88,-244 32,-244 32,-208 88,-208 88,-244"/>
<text text-anchor="start" x="52.6632" y="-222.2" font-family="Helvetica,sans-Serif" font-size="12.00" fill="#000000">S2</text>
<path fill="none" stroke="#000000" stroke-width="2" d="M44.3333,-209C44.3333,-209 75.6667,-209 75.6667,-209 81.3333,-209 87,-214.6667 87,-220.3333 87,-220.3333 87,-231.6667 87,-231.6667 87,-237.3333 81.3333,-243 75.6667,-243 75.6667,-243 44.3333,-243 44.3333,-243 38.6667,-243 33,-237.3333 33,-231.6667 33,-231.6667 33,-220.3333 33,-220.3333 33,-214.6667 38.6667,-209 44.3333,-209"/>
</g>
<!-- _Invar_I1_S2&#45;&gt;_Invar_I1_S3 -->
<g id="edge7" class="edge">
<title>_Invar_I1_S2&#45;&gt;_Invar_I1_S3</title>
<path fill="none" stroke="#000000" d="M55.7033,-207.6741C54.7416,-202.1833 54,-196.1255 54,-190.5 54,-190.5 54,-190.5 54,-143.5 54,-141.2146 54.1224,-138.8579 54.3322,-136.4969"/>
<polygon fill="#000000" stroke="#000000" points="57.8359,-136.7039 55.7033,-126.3259 50.8986,-135.7687 57.8359,-136.7039"/>
<text text-anchor="start" x="54" y="-164" font-family="Helvetica,sans-Serif" font-size="10.00" fill="#000000">/b = 2 * a + b &#160;&#160;</text>
</g>
<!-- _Invar_I1_S1&#45;&gt;_Invar_I1_S2 -->
<g id="edge8" class="edge">
<title>_Invar_I1_S1&#45;&gt;_Invar_I1_S2</title>
<path fill="none" stroke="#000000" d="M60,-325.9402C60,-320.3497 60,-314.1701 60,-308.5 60,-308.5 60,-308.5 60,-261.5 60,-259.1079 60,-256.6252 60,-254.1342"/>
<polygon fill="#000000" stroke="#000000" points="63.5001,-254.0597 60,-244.0598 56.5001,-254.0598 63.5001,-254.0597"/>
<text text-anchor="start" x="60" y="-282" font-family="Helvetica,sans-Serif" font-size="10.00" fill="#000000">/b = 2 * b &#160;&#160;</text>
</g>
</g>
</svg>