|
@@ -4,25 +4,25 @@
|
|
|
<!-- Generated by graphviz version 2.40.1 (20161225.0304)
|
|
|
-->
|
|
|
<!-- Title: state transitions Pages: 1 -->
|
|
|
-<svg width="752pt" height="394pt"
|
|
|
- viewBox="0.00 0.00 752.00 394.00" xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink">
|
|
|
+<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 748,-390 748,4 -4,4"/>
|
|
|
+<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 724,-8 724,-8 730,-8 736,-14 736,-20 736,-20 736,-335 736,-335 736,-341 730,-347 724,-347 724,-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="353.6682" y="-328.2" font-family="Helvetica,sans-Serif" font-size="12.00" fill="#000000">Dialing</text>
|
|
|
+<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="436,-16 436,-309 728,-309 728,-16 436,-16"/>
|
|
|
-<text text-anchor="start" x="559.6668" y="-290.2" font-family="Helvetica,sans-Serif" font-size="12.00" fill="#000000">Redialer</text>
|
|
|
+<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 428,-309 428,-16 24,-16"/>
|
|
|
-<text text-anchor="start" x="210.8376" y="-290.2" font-family="Helvetica,sans-Serif" font-size="12.00" fill="#000000">Dialer</text>
|
|
|
+<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">
|
|
@@ -41,49 +41,49 @@
|
|
|
<!-- _Dialing_Redialer_initial -->
|
|
|
<g id="node4" class="node">
|
|
|
<title>_Dialing_Redialer_initial</title>
|
|
|
-<ellipse fill="#000000" stroke="#000000" stroke-width="2" cx="547" cy="-265.5" rx="5.5" ry="5.5"/>
|
|
|
+<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="602.5,-178 491.5,-178 491.5,-142 602.5,-142 602.5,-178"/>
|
|
|
-<text text-anchor="start" x="502.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="M503.8333,-143C503.8333,-143 590.1667,-143 590.1667,-143 595.8333,-143 601.5,-148.6667 601.5,-154.3333 601.5,-154.3333 601.5,-165.6667 601.5,-165.6667 601.5,-171.3333 595.8333,-177 590.1667,-177 590.1667,-177 503.8333,-177 503.8333,-177 498.1667,-177 492.5,-171.3333 492.5,-165.6667 492.5,-165.6667 492.5,-154.3333 492.5,-154.3333 492.5,-148.6667 498.1667,-143 503.8333,-143"/>
|
|
|
+<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->_Dialing_Redialer_WaitForRedial -->
|
|
|
<g id="edge2" class="edge">
|
|
|
<title>_Dialing_Redialer_initial->_Dialing_Redialer_WaitForRedial</title>
|
|
|
-<path fill="none" stroke="#000000" d="M547,-259.8288C547,-255.1736 547,-248.4097 547,-242.5 547,-242.5 547,-242.5 547,-195.5 547,-193.1079 547,-190.6252 547,-188.1342"/>
|
|
|
-<polygon fill="#000000" stroke="#000000" points="550.5001,-188.0597 547,-178.0598 543.5001,-188.0598 550.5001,-188.0597"/>
|
|
|
-<text text-anchor="middle" x="548.3895" y="-216" font-family="Helvetica,sans-Serif" font-size="10.00" fill="#000000"> </text>
|
|
|
+<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="563.5,-60 478.5,-60 478.5,-24 563.5,-24 563.5,-60"/>
|
|
|
-<text text-anchor="start" x="489.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="M490.8333,-25C490.8333,-25 551.1667,-25 551.1667,-25 556.8333,-25 562.5,-30.6667 562.5,-36.3333 562.5,-36.3333 562.5,-47.6667 562.5,-47.6667 562.5,-53.3333 556.8333,-59 551.1667,-59 551.1667,-59 490.8333,-59 490.8333,-59 485.1667,-59 479.5,-53.3333 479.5,-47.6667 479.5,-47.6667 479.5,-36.3333 479.5,-36.3333 479.5,-30.6667 485.1667,-25 490.8333,-25"/>
|
|
|
+<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->_Dialing_Redialer_RedialDigits -->
|
|
|
<g id="edge3" class="edge">
|
|
|
<title>_Dialing_Redialer_RedialDigits->_Dialing_Redialer_RedialDigits</title>
|
|
|
-<path fill="none" stroke="#000000" d="M563.7986,-46.856C576.0518,-46.6655 585.5,-45.0469 585.5,-42 585.5,-39.8577 580.8289,-38.4214 573.7961,-37.6913"/>
|
|
|
-<polygon fill="#000000" stroke="#000000" points="573.9749,-34.1959 563.7986,-37.144 573.5923,-41.1855 573.9749,-34.1959"/>
|
|
|
-<text text-anchor="start" x="585.5" y="-39" font-family="Helvetica,sans-Serif" font-size="10.00" fill="#000000">[c < numdigits(p)]^dial   </text>
|
|
|
+<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 < numdigits(p)]^dial   </text>
|
|
|
</g>
|
|
|
<!-- _Dialing_Redialer_RedialDigits->_Dialing_Redialer_WaitForRedial -->
|
|
|
<g id="edge4" class="edge">
|
|
|
<title>_Dialing_Redialer_RedialDigits->_Dialing_Redialer_WaitForRedial</title>
|
|
|
-<path fill="none" stroke="#000000" d="M478.4804,-56.5685C471.2377,-61.7041 466,-68.5217 466,-77.5 466,-124.5 466,-124.5 466,-124.5 466,-130.0837 472.5386,-135.3603 481.9003,-140.0534"/>
|
|
|
-<polygon fill="#000000" stroke="#000000" points="480.6262,-143.3174 491.1849,-144.1915 483.4759,-136.9237 480.6262,-143.3174"/>
|
|
|
-<text text-anchor="start" x="466" y="-98" font-family="Helvetica,sans-Serif" font-size="10.00" fill="#000000">[c == numdigits(p)]   </text>
|
|
|
+<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)]   </text>
|
|
|
</g>
|
|
|
<!-- _Dialing_Redialer_WaitForRedial->_Dialing_Redialer_RedialDigits -->
|
|
|
<g id="edge5" class="edge">
|
|
|
<title>_Dialing_Redialer_WaitForRedial->_Dialing_Redialer_RedialDigits</title>
|
|
|
-<path fill="none" stroke="#000000" d="M593.0321,-141.7223C597.8326,-137.125 601,-131.456 601,-124.5 601,-124.5 601,-124.5 601,-77.5 601,-69.8242 588.5399,-62.6778 573.4545,-56.8384"/>
|
|
|
-<polygon fill="#000000" stroke="#000000" points="574.405,-53.461 563.8104,-53.3785 572.0411,-60.0498 574.405,-53.461"/>
|
|
|
-<text text-anchor="start" x="601" y="-98" font-family="Helvetica,sans-Serif" font-size="10.00" fill="#000000">redial [c == 0]/p = lp ^dial   </text>
|
|
|
+<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   </text>
|
|
|
</g>
|
|
|
<!-- _Dialing_Dialer -->
|
|
|
<!-- _Dialing_Dialer_initial -->
|
|
@@ -108,37 +108,37 @@
|
|
|
<!-- _Dialing_Dialer_DialDigits -->
|
|
|
<g id="node9" class="node">
|
|
|
<title>_Dialing_Dialer_DialDigits</title>
|
|
|
-<polygon fill="transparent" stroke="transparent" stroke-width="2" points="141,-60 69,-60 69,-24 141,-24 141,-60"/>
|
|
|
-<text text-anchor="start" x="79.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="M81.3333,-25C81.3333,-25 128.6667,-25 128.6667,-25 134.3333,-25 140,-30.6667 140,-36.3333 140,-36.3333 140,-47.6667 140,-47.6667 140,-53.3333 134.3333,-59 128.6667,-59 128.6667,-59 81.3333,-59 81.3333,-59 75.6667,-59 70,-53.3333 70,-47.6667 70,-47.6667 70,-36.3333 70,-36.3333 70,-30.6667 75.6667,-25 81.3333,-25"/>
|
|
|
+<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->_Dialing_Dialer_DialDigits -->
|
|
|
<g id="edge7" class="edge">
|
|
|
<title>_Dialing_Dialer_DialDigits->_Dialing_Dialer_DialDigits</title>
|
|
|
-<path fill="none" stroke="#000000" d="M141.25,-46.875C153.3333,-46.875 163,-45.25 163,-42 163,-39.7656 158.431,-38.2993 151.6489,-37.6011"/>
|
|
|
-<polygon fill="#000000" stroke="#000000" points="151.3996,-34.0861 141.25,-37.125 151.0794,-41.0788 151.3996,-34.0861"/>
|
|
|
-<text text-anchor="start" x="163" y="-39" font-family="Helvetica,sans-Serif" font-size="10.00" fill="#000000">dial [c < 10]/lp = lp * 10 + d⁏ c = c + 1⁏  ^out.out   </text>
|
|
|
+<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 < 10]/lp = lp * 10 + d⁏ c = c + 1⁏  ^out.out   </text>
|
|
|
</g>
|
|
|
<!-- _Dialing_Dialer_DialDigits->_Dialing_Dialer_WaitForDial -->
|
|
|
<g id="edge8" class="edge">
|
|
|
<title>_Dialing_Dialer_DialDigits->_Dialing_Dialer_WaitForDial</title>
|
|
|
-<path fill="none" stroke="#000000" d="M74.6899,-60.1859C70.1752,-65.0344 67,-70.8191 67,-77.5 67,-124.5 67,-124.5 67,-124.5 67,-126.9367 67.2734,-129.4132 67.7409,-131.8668"/>
|
|
|
+<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]   </text>
|
|
|
</g>
|
|
|
<!-- _Dialing_Dialer_WaitForDial->_Dialing_Dialer_DialDigits -->
|
|
|
<g id="edge10" class="edge">
|
|
|
<title>_Dialing_Dialer_WaitForDial->_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,-70.3568 154.6355,-64.5595 149.602,-59.8834"/>
|
|
|
-<polygon fill="#000000" stroke="#000000" points="151.3797,-56.849 141.2305,-53.8085 147.2684,-62.5145 151.3797,-56.849"/>
|
|
|
-<text text-anchor="start" x="158" y="-98" font-family="Helvetica,sans-Serif" font-size="10.00" fill="#000000">dial ∧ redial [c == 0]/lp = d⁏ c = 1⁏  ^out.out   </text>
|
|
|
+<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">dial(d:int) ∧ redial [c == 0]/lp = d⁏ c = 1⁏  ^out.out   </text>
|
|
|
</g>
|
|
|
<!-- _Dialing_Dialer_WaitForDial->_Dialing_Dialer_WaitForDial -->
|
|
|
<g id="edge9" class="edge">
|
|
|
<title>_Dialing_Dialer_WaitForDial->_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 ∧ ¬redial [c < 10]/c = c + 1⁏ lp = lp * 10 + d⁏  ^out.out   </text>
|
|
|
+<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 < 10]/c = c + 1⁏ lp = lp * 10 + d⁏  ^out.out   </text>
|
|
|
</g>
|
|
|
</g>
|
|
|
</svg>
|