SCCD/test/test_files/day_atlee/statechart_fig1_redialer.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="777pt" height="394pt"
 viewBox="0.00 0.00 777.00 394.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 390)">
<title>state transitions</title>
<polygon fill="#ffffff" stroke="transparent" points="-4,4 -4,-390 773,-390 773,4 -4,4"/>
<g id="clust1" class="cluster">
<title>cluster__Dialing</title>
<path fill="none" stroke="#000000" stroke-width="2" d="M20,-8C20,-8 749,-8 749,-8 755,-8 761,-14 761,-20 761,-20 761,-335 761,-335 761,-341 755,-347 749,-347 749,-347 20,-347 20,-347 14,-347 8,-341 8,-335 8,-335 8,-20 8,-20 8,-14 14,-8 20,-8"/>
<text text-anchor="start" x="366.1682" y="-328.2" font-family="Helvetica,sans-Serif" font-size="12.00" fill="#000000">Dialing</text>
</g>
<g id="clust2" class="cluster">
<title>cluster__Dialing_Redialer</title>
<polygon fill="none" stroke="#000000" stroke-dasharray="5,2" points="461,-16 461,-309 753,-309 753,-16 461,-16"/>
<text text-anchor="start" x="584.6668" y="-290.2" font-family="Helvetica,sans-Serif" font-size="12.00" fill="#000000">Redialer</text>
</g>
<g id="clust3" class="cluster">
<title>cluster__Dialing_Dialer</title>
<polygon fill="none" stroke="#000000" stroke-dasharray="5,2" points="24,-16 24,-309 453,-309 453,-16 24,-16"/>
<text text-anchor="start" x="223.3376" y="-290.2" font-family="Helvetica,sans-Serif" font-size="12.00" fill="#000000">Dialer</text>
</g>
<!-- __initial -->
<g id="node1" class="node">
<title>__initial</title>
<ellipse fill="#000000" stroke="#000000" stroke-width="2" cx="16" cy="-380.5" rx="5.5" ry="5.5"/>
</g>
<!-- _Dialing -->
<!-- __initial&#45;&gt;_Dialing -->
<g id="edge1" class="edge">
<title>__initial&#45;&gt;_Dialing</title>
<path fill="none" stroke="#000000" d="M16,-374.9533C16,-370.7779 16,-364.5043 16,-357.0332"/>
<polygon fill="#000000" stroke="#000000" points="19.5001,-356.9971 16,-346.9971 12.5001,-356.9972 19.5001,-356.9971"/>
<text text-anchor="middle" x="17.3895" y="-358" font-family="Helvetica,sans-Serif" font-size="10.00" fill="#000000"> </text>
</g>
<!-- _Dialing_Redialer -->
<!-- _Dialing_Redialer_initial -->
<g id="node4" class="node">
<title>_Dialing_Redialer_initial</title>
<ellipse fill="#000000" stroke="#000000" stroke-width="2" cx="572" cy="-265.5" rx="5.5" ry="5.5"/>
</g>
<!-- _Dialing_Redialer_WaitForRedial -->
<g id="node6" class="node">
<title>_Dialing_Redialer_WaitForRedial</title>
<polygon fill="transparent" stroke="transparent" stroke-width="2" points="627.5,-178 516.5,-178 516.5,-142 627.5,-142 627.5,-178"/>
<text text-anchor="start" x="527.8342" y="-156.2" font-family="Helvetica,sans-Serif" font-size="12.00" fill="#000000">WaitForRedial ✓</text>
<path fill="none" stroke="#000000" stroke-width="2" d="M528.8333,-143C528.8333,-143 615.1667,-143 615.1667,-143 620.8333,-143 626.5,-148.6667 626.5,-154.3333 626.5,-154.3333 626.5,-165.6667 626.5,-165.6667 626.5,-171.3333 620.8333,-177 615.1667,-177 615.1667,-177 528.8333,-177 528.8333,-177 523.1667,-177 517.5,-171.3333 517.5,-165.6667 517.5,-165.6667 517.5,-154.3333 517.5,-154.3333 517.5,-148.6667 523.1667,-143 528.8333,-143"/>
</g>
<!-- _Dialing_Redialer_initial&#45;&gt;_Dialing_Redialer_WaitForRedial -->
<g id="edge2" class="edge">
<title>_Dialing_Redialer_initial&#45;&gt;_Dialing_Redialer_WaitForRedial</title>
<path fill="none" stroke="#000000" d="M572,-259.8288C572,-255.1736 572,-248.4097 572,-242.5 572,-242.5 572,-242.5 572,-195.5 572,-193.1079 572,-190.6252 572,-188.1342"/>
<polygon fill="#000000" stroke="#000000" points="575.5001,-188.0597 572,-178.0598 568.5001,-188.0598 575.5001,-188.0597"/>
<text text-anchor="middle" x="573.3895" y="-216" font-family="Helvetica,sans-Serif" font-size="10.00" fill="#000000"> </text>
</g>
<!-- _Dialing_Redialer_RedialDigits -->
<g id="node5" class="node">
<title>_Dialing_Redialer_RedialDigits</title>
<polygon fill="transparent" stroke="transparent" stroke-width="2" points="588.5,-60 503.5,-60 503.5,-24 588.5,-24 588.5,-60"/>
<text text-anchor="start" x="514.5026" y="-38.2" font-family="Helvetica,sans-Serif" font-size="12.00" fill="#000000">RedialDigits</text>
<path fill="none" stroke="#000000" stroke-width="2" d="M515.8333,-25C515.8333,-25 576.1667,-25 576.1667,-25 581.8333,-25 587.5,-30.6667 587.5,-36.3333 587.5,-36.3333 587.5,-47.6667 587.5,-47.6667 587.5,-53.3333 581.8333,-59 576.1667,-59 576.1667,-59 515.8333,-59 515.8333,-59 510.1667,-59 504.5,-53.3333 504.5,-47.6667 504.5,-47.6667 504.5,-36.3333 504.5,-36.3333 504.5,-30.6667 510.1667,-25 515.8333,-25"/>
</g>
<!-- _Dialing_Redialer_RedialDigits&#45;&gt;_Dialing_Redialer_RedialDigits -->
<g id="edge3" class="edge">
<title>_Dialing_Redialer_RedialDigits&#45;&gt;_Dialing_Redialer_RedialDigits</title>
<path fill="none" stroke="#000000" d="M588.7986,-46.856C601.0518,-46.6655 610.5,-45.0469 610.5,-42 610.5,-39.8577 605.8289,-38.4214 598.7961,-37.6913"/>
<polygon fill="#000000" stroke="#000000" points="598.9749,-34.1959 588.7986,-37.144 598.5923,-41.1855 598.9749,-34.1959"/>
<text text-anchor="start" x="610.5" y="-39" font-family="Helvetica,sans-Serif" font-size="10.00" fill="#000000">[c &lt; numdigits(p)]^dial &#160;&#160;</text>
</g>
<!-- _Dialing_Redialer_RedialDigits&#45;&gt;_Dialing_Redialer_WaitForRedial -->
<g id="edge4" class="edge">
<title>_Dialing_Redialer_RedialDigits&#45;&gt;_Dialing_Redialer_WaitForRedial</title>
<path fill="none" stroke="#000000" d="M503.4804,-56.5685C496.2377,-61.7041 491,-68.5217 491,-77.5 491,-124.5 491,-124.5 491,-124.5 491,-130.0837 497.5386,-135.3603 506.9003,-140.0534"/>
<polygon fill="#000000" stroke="#000000" points="505.6262,-143.3174 516.1849,-144.1915 508.4759,-136.9237 505.6262,-143.3174"/>
<text text-anchor="start" x="491" y="-98" font-family="Helvetica,sans-Serif" font-size="10.00" fill="#000000">[c == numdigits(p)] &#160;&#160;</text>
</g>
<!-- _Dialing_Redialer_WaitForRedial&#45;&gt;_Dialing_Redialer_RedialDigits -->
<g id="edge5" class="edge">
<title>_Dialing_Redialer_WaitForRedial&#45;&gt;_Dialing_Redialer_RedialDigits</title>
<path fill="none" stroke="#000000" d="M618.0321,-141.7223C622.8326,-137.125 626,-131.456 626,-124.5 626,-124.5 626,-124.5 626,-77.5 626,-69.8242 613.5399,-62.6778 598.4545,-56.8384"/>
<polygon fill="#000000" stroke="#000000" points="599.405,-53.461 588.8104,-53.3785 597.0411,-60.0498 599.405,-53.461"/>
<text text-anchor="start" x="626" y="-98" font-family="Helvetica,sans-Serif" font-size="10.00" fill="#000000">redial [c == 0]/p = lp ^dial &#160;&#160;</text>
</g>
<!-- _Dialing_Dialer -->
<!-- _Dialing_Dialer_initial -->
<g id="node8" class="node">
<title>_Dialing_Dialer_initial</title>
<ellipse fill="#000000" stroke="#000000" stroke-width="2" cx="80" cy="-265.5" rx="5.5" ry="5.5"/>
</g>
<!-- _Dialing_Dialer_WaitForDial -->
<g id="node10" class="node">
<title>_Dialing_Dialer_WaitForDial</title>
<polygon fill="transparent" stroke="transparent" stroke-width="2" points="128.5,-178 31.5,-178 31.5,-142 128.5,-142 128.5,-178"/>
<text text-anchor="start" x="42.505" y="-156.2" font-family="Helvetica,sans-Serif" font-size="12.00" fill="#000000">WaitForDial ✓</text>
<path fill="none" stroke="#000000" stroke-width="2" d="M43.8333,-143C43.8333,-143 116.1667,-143 116.1667,-143 121.8333,-143 127.5,-148.6667 127.5,-154.3333 127.5,-154.3333 127.5,-165.6667 127.5,-165.6667 127.5,-171.3333 121.8333,-177 116.1667,-177 116.1667,-177 43.8333,-177 43.8333,-177 38.1667,-177 32.5,-171.3333 32.5,-165.6667 32.5,-165.6667 32.5,-154.3333 32.5,-154.3333 32.5,-148.6667 38.1667,-143 43.8333,-143"/>
</g>
<!-- _Dialing_Dialer_initial&#45;&gt;_Dialing_Dialer_WaitForDial -->
<g id="edge6" class="edge">
<title>_Dialing_Dialer_initial&#45;&gt;_Dialing_Dialer_WaitForDial</title>
<path fill="none" stroke="#000000" d="M80,-259.8288C80,-255.1736 80,-248.4097 80,-242.5 80,-242.5 80,-242.5 80,-195.5 80,-193.1079 80,-190.6252 80,-188.1342"/>
<polygon fill="#000000" stroke="#000000" points="83.5001,-188.0597 80,-178.0598 76.5001,-188.0598 83.5001,-188.0597"/>
<text text-anchor="middle" x="81.3895" y="-216" font-family="Helvetica,sans-Serif" font-size="10.00" fill="#000000"> </text>
</g>
<!-- _Dialing_Dialer_DialDigits -->
<g id="node9" class="node">
<title>_Dialing_Dialer_DialDigits</title>
<polygon fill="transparent" stroke="transparent" stroke-width="2" points="140,-60 68,-60 68,-24 140,-24 140,-60"/>
<text text-anchor="start" x="78.6734" y="-38.2" font-family="Helvetica,sans-Serif" font-size="12.00" fill="#000000">DialDigits</text>
<path fill="none" stroke="#000000" stroke-width="2" d="M80.3333,-25C80.3333,-25 127.6667,-25 127.6667,-25 133.3333,-25 139,-30.6667 139,-36.3333 139,-36.3333 139,-47.6667 139,-47.6667 139,-53.3333 133.3333,-59 127.6667,-59 127.6667,-59 80.3333,-59 80.3333,-59 74.6667,-59 69,-53.3333 69,-47.6667 69,-47.6667 69,-36.3333 69,-36.3333 69,-30.6667 74.6667,-25 80.3333,-25"/>
</g>
<!-- _Dialing_Dialer_DialDigits&#45;&gt;_Dialing_Dialer_DialDigits -->
<g id="edge7" class="edge">
<title>_Dialing_Dialer_DialDigits&#45;&gt;_Dialing_Dialer_DialDigits</title>
<path fill="none" stroke="#000000" d="M140.25,-46.875C152.3333,-46.875 162,-45.25 162,-42 162,-39.7656 157.431,-38.2993 150.6489,-37.6011"/>
<polygon fill="#000000" stroke="#000000" points="150.3996,-34.0861 140.25,-37.125 150.0794,-41.0788 150.3996,-34.0861"/>
<text text-anchor="start" x="162" y="-39" font-family="Helvetica,sans-Serif" font-size="10.00" fill="#000000">dial(d:int) [c &lt; 10]/lp = lp * 10 + d⁏ c = c + 1⁏ &#160;^out.out &#160;&#160;</text>
</g>
<!-- _Dialing_Dialer_DialDigits&#45;&gt;_Dialing_Dialer_WaitForDial -->
<g id="edge8" class="edge">
<title>_Dialing_Dialer_DialDigits&#45;&gt;_Dialing_Dialer_WaitForDial</title>
<path fill="none" stroke="#000000" d="M74.4875,-60.3273C70.0916,-65.167 67,-70.9124 67,-77.5 67,-124.5 67,-124.5 67,-124.5 67,-126.9367 67.2734,-129.4132 67.7409,-131.8668"/>
<polygon fill="#000000" stroke="#000000" points="64.4295,-133.0164 70.5523,-141.6629 71.1579,-131.0853 64.4295,-133.0164"/>
<text text-anchor="start" x="67" y="-98" font-family="Helvetica,sans-Serif" font-size="10.00" fill="#000000">[c == 10] &#160;&#160;</text>
</g>
<!-- _Dialing_Dialer_WaitForDial&#45;&gt;_Dialing_Dialer_DialDigits -->
<g id="edge10" class="edge">
<title>_Dialing_Dialer_WaitForDial&#45;&gt;_Dialing_Dialer_DialDigits</title>
<path fill="none" stroke="#000000" d="M128.5115,-146.0105C144.3736,-139.9675 158,-132.4599 158,-124.5 158,-124.5 158,-124.5 158,-77.5 158,-69.8638 154.1829,-63.7787 148.5785,-58.9596"/>
<polygon fill="#000000" stroke="#000000" points="150.2577,-55.8692 140.0188,-53.1463 146.3249,-61.66 150.2577,-55.8692"/>
<text text-anchor="start" x="158" y="-98" font-family="Helvetica,sans-Serif" font-size="10.00" fill="#000000">redial ∧ dial(d:int) [c == 0]/lp = d⁏ c = 1⁏ &#160;^out.out &#160;&#160;</text>
</g>
<!-- _Dialing_Dialer_WaitForDial&#45;&gt;_Dialing_Dialer_WaitForDial -->
<g id="edge9" class="edge">
<title>_Dialing_Dialer_WaitForDial&#45;&gt;_Dialing_Dialer_WaitForDial</title>
<path fill="none" stroke="#000000" d="M128.7649,-164.8167C141.1797,-164.5001 150.5,-162.8945 150.5,-160 150.5,-157.9648 145.8922,-156.5668 138.8407,-155.8061"/>
<polygon fill="#000000" stroke="#000000" points="138.9618,-152.307 128.7649,-155.1833 138.5299,-159.2937 138.9618,-152.307"/>
<text text-anchor="start" x="150.5" y="-157" font-family="Helvetica,sans-Serif" font-size="10.00" fill="#000000">dial(d:int) ∧ ¬redial [c &lt; 10]/c = c + 1⁏ lp = lp * 10 + d⁏ &#160;^out.out &#160;&#160;</text>
</g>
</g>
</svg>