浏览代码

Move candidate generator classes to a separate module. Add script for rendering graph of transition priorities.

Joeri Exelmans 4 年之前
父节点
当前提交
348c04e397

+ 667 - 0
examples/chatclient/model_chatclient_priorities.svg

@@ -0,0 +1,667 @@
+<?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: priorities Pages: 1 -->
+<svg width="3259pt" height="548pt"
+ viewBox="0.00 0.00 3259.30 548.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 544)">
+<title>priorities</title>
+<polygon fill="#ffffff" stroke="transparent" points="-4,4 -4,-544 3255.2978,-544 3255.2978,4 -4,4"/>
+<!-- 3. Connected&#45;&gt;Connecting -->
+<g id="node1" class="node">
+<title>3. Connected&#45;&gt;Connecting</title>
+<ellipse fill="none" stroke="#000000" cx="1627.2978" cy="-522" rx="106.6812" ry="18"/>
+<text text-anchor="middle" x="1627.2978" y="-518.3" font-family="Times,serif" font-size="14.00" fill="#000000">3. Connected&#45;&gt;Connecting</text>
+</g>
+<!-- 4. NotJoined&#45;&gt;GettingRoomNumber -->
+<g id="node2" class="node">
+<title>4. NotJoined&#45;&gt;GettingRoomNumber</title>
+<ellipse fill="none" stroke="#000000" cx="1589.2978" cy="-234" rx="141.8751" ry="18"/>
+<text text-anchor="middle" x="1589.2978" y="-230.3" font-family="Times,serif" font-size="14.00" fill="#000000">4. NotJoined&#45;&gt;GettingRoomNumber</text>
+</g>
+<!-- 3. Connected&#45;&gt;Connecting&#45;&gt;4. NotJoined&#45;&gt;GettingRoomNumber -->
+<g id="edge1" class="edge">
+<title>3. Connected&#45;&gt;Connecting&#45;&gt;4. NotJoined&#45;&gt;GettingRoomNumber</title>
+<path fill="none" stroke="#000000" d="M1624.9207,-503.9843C1618.4963,-455.2939 1600.75,-320.7961 1592.9998,-262.0573"/>
+<polygon fill="#000000" stroke="#000000" points="1596.4521,-261.4651 1591.6739,-252.0089 1589.5122,-262.3808 1596.4521,-261.4651"/>
+</g>
+<!-- 5. GettingRoomNumber&#45;&gt;GettingRoomNumber -->
+<g id="node3" class="node">
+<title>5. GettingRoomNumber&#45;&gt;GettingRoomNumber</title>
+<ellipse fill="none" stroke="#000000" cx="2863.2978" cy="-450" rx="183.0677" ry="18"/>
+<text text-anchor="middle" x="2863.2978" y="-446.3" font-family="Times,serif" font-size="14.00" fill="#000000">5. GettingRoomNumber&#45;&gt;GettingRoomNumber</text>
+</g>
+<!-- 3. Connected&#45;&gt;Connecting&#45;&gt;5. GettingRoomNumber&#45;&gt;GettingRoomNumber -->
+<g id="edge2" class="edge">
+<title>3. Connected&#45;&gt;Connecting&#45;&gt;5. GettingRoomNumber&#45;&gt;GettingRoomNumber</title>
+<path fill="none" stroke="#000000" d="M1728.1827,-516.1232C1940.3021,-503.7667 2434.3878,-474.985 2695.1826,-459.7931"/>
+<polygon fill="#000000" stroke="#000000" points="2695.7294,-463.2673 2705.5089,-459.1916 2695.3223,-456.2791 2695.7294,-463.2673"/>
+</g>
+<!-- 6. GettingRoomNumber&#45;&gt;JoiningOrJoined -->
+<g id="node4" class="node">
+<title>6. GettingRoomNumber&#45;&gt;JoiningOrJoined</title>
+<ellipse fill="none" stroke="#000000" cx="2292.2978" cy="-378" rx="163.5712" ry="18"/>
+<text text-anchor="middle" x="2292.2978" y="-374.3" font-family="Times,serif" font-size="14.00" fill="#000000">6. GettingRoomNumber&#45;&gt;JoiningOrJoined</text>
+</g>
+<!-- 3. Connected&#45;&gt;Connecting&#45;&gt;6. GettingRoomNumber&#45;&gt;JoiningOrJoined -->
+<g id="edge3" class="edge">
+<title>3. Connected&#45;&gt;Connecting&#45;&gt;6. GettingRoomNumber&#45;&gt;JoiningOrJoined</title>
+<path fill="none" stroke="#000000" d="M1723.6688,-514.2622C1838.7918,-504.4106 2024.2455,-486.4436 2091.2978,-468 2149.4395,-452.0074 2212.231,-421.5608 2251.8755,-400.5397"/>
+<polygon fill="#000000" stroke="#000000" points="2253.5427,-403.6171 2260.7053,-395.8102 2250.2376,-397.4465 2253.5427,-403.6171"/>
+</g>
+<!-- 7. GettingRoomNumber&#45;&gt;GettingRoomNumber -->
+<g id="node5" class="node">
+<title>7. GettingRoomNumber&#45;&gt;GettingRoomNumber</title>
+<ellipse fill="none" stroke="#000000" cx="2292.2978" cy="-306" rx="183.0677" ry="18"/>
+<text text-anchor="middle" x="2292.2978" y="-302.3" font-family="Times,serif" font-size="14.00" fill="#000000">7. GettingRoomNumber&#45;&gt;GettingRoomNumber</text>
+</g>
+<!-- 3. Connected&#45;&gt;Connecting&#45;&gt;7. GettingRoomNumber&#45;&gt;GettingRoomNumber -->
+<g id="edge4" class="edge">
+<title>3. Connected&#45;&gt;Connecting&#45;&gt;7. GettingRoomNumber&#45;&gt;GettingRoomNumber</title>
+<path fill="none" stroke="#000000" d="M1717.9534,-512.4944C1803.4967,-502.6613 1925.0345,-486.2108 1969.2978,-468 2045.2683,-436.7442 2045.8084,-396.7118 2119.2978,-360 2137.5264,-350.8939 2181.595,-337.179 2220.6899,-325.85"/>
+<polygon fill="#000000" stroke="#000000" points="2221.8616,-329.1549 2230.5034,-323.0254 2219.9254,-322.428 2221.8616,-329.1549"/>
+</g>
+<!-- 8. GettingRoomNumber&#45;&gt;GettingRoomNumber -->
+<g id="node6" class="node">
+<title>8. GettingRoomNumber&#45;&gt;GettingRoomNumber</title>
+<ellipse fill="none" stroke="#000000" cx="2812.2978" cy="-234" rx="183.0677" ry="18"/>
+<text text-anchor="middle" x="2812.2978" y="-230.3" font-family="Times,serif" font-size="14.00" fill="#000000">8. GettingRoomNumber&#45;&gt;GettingRoomNumber</text>
+</g>
+<!-- 3. Connected&#45;&gt;Connecting&#45;&gt;8. GettingRoomNumber&#45;&gt;GettingRoomNumber -->
+<g id="edge5" class="edge">
+<title>3. Connected&#45;&gt;Connecting&#45;&gt;8. GettingRoomNumber&#45;&gt;GettingRoomNumber</title>
+<path fill="none" stroke="#000000" d="M1732.0813,-518.4112C1893.6306,-510.2047 2211.4143,-483.3706 2465.2978,-396 2580.0437,-356.5117 2707.5612,-290.9807 2771.3082,-256.6165"/>
+<polygon fill="#000000" stroke="#000000" points="2773.1145,-259.6186 2780.2416,-251.7793 2769.7814,-253.4631 2773.1145,-259.6186"/>
+</g>
+<!-- 9. Leaving&#45;&gt;NotJoined -->
+<g id="node7" class="node">
+<title>9. Leaving&#45;&gt;NotJoined</title>
+<ellipse fill="none" stroke="#000000" cx="2328.2978" cy="-234" rx="92.8835" ry="18"/>
+<text text-anchor="middle" x="2328.2978" y="-230.3" font-family="Times,serif" font-size="14.00" fill="#000000">9. Leaving&#45;&gt;NotJoined</text>
+</g>
+<!-- 3. Connected&#45;&gt;Connecting&#45;&gt;9. Leaving&#45;&gt;NotJoined -->
+<g id="edge6" class="edge">
+<title>3. Connected&#45;&gt;Connecting&#45;&gt;9. Leaving&#45;&gt;NotJoined</title>
+<path fill="none" stroke="#000000" d="M1656.4202,-504.6468C1728.9897,-462.0693 1924.6888,-351.3042 2100.2978,-288 2148.6827,-270.558 2204.8902,-257.1727 2249.3905,-248.0916"/>
+<polygon fill="#000000" stroke="#000000" points="2250.1632,-251.5063 2259.2779,-246.1051 2248.7844,-244.6435 2250.1632,-251.5063"/>
+</g>
+<!-- 10. Joining&#45;&gt;H -->
+<g id="node8" class="node">
+<title>10. Joining&#45;&gt;H</title>
+<ellipse fill="none" stroke="#000000" cx="1852.2978" cy="-234" rx="64.9885" ry="18"/>
+<text text-anchor="middle" x="1852.2978" y="-230.3" font-family="Times,serif" font-size="14.00" fill="#000000">10. Joining&#45;&gt;H</text>
+</g>
+<!-- 3. Connected&#45;&gt;Connecting&#45;&gt;10. Joining&#45;&gt;H -->
+<g id="edge7" class="edge">
+<title>3. Connected&#45;&gt;Connecting&#45;&gt;10. Joining&#45;&gt;H</title>
+<path fill="none" stroke="#000000" d="M1641.3725,-503.9843C1679.898,-454.6717 1787.1848,-317.3446 1832.108,-259.8429"/>
+<polygon fill="#000000" stroke="#000000" points="1835.1172,-261.6762 1838.5156,-251.6412 1829.601,-257.3667 1835.1172,-261.6762"/>
+</g>
+<!-- 11. Initial&#45;&gt;EnteringMessage -->
+<g id="node9" class="node">
+<title>11. Initial&#45;&gt;EnteringMessage</title>
+<ellipse fill="none" stroke="#000000" cx="1446.2978" cy="-306" rx="115.0796" ry="18"/>
+<text text-anchor="middle" x="1446.2978" y="-302.3" font-family="Times,serif" font-size="14.00" fill="#000000">11. Initial&#45;&gt;EnteringMessage</text>
+</g>
+<!-- 3. Connected&#45;&gt;Connecting&#45;&gt;11. Initial&#45;&gt;EnteringMessage -->
+<g id="edge8" class="edge">
+<title>3. Connected&#45;&gt;Connecting&#45;&gt;11. Initial&#45;&gt;EnteringMessage</title>
+<path fill="none" stroke="#000000" d="M1609.0491,-503.9092C1598.8707,-493.6083 1586.1049,-480.3342 1575.2978,-468 1534.626,-421.5812 1490.4961,-364.5737 1465.8332,-332.0495"/>
+<polygon fill="#000000" stroke="#000000" points="1468.5266,-329.8083 1459.7042,-323.9418 1462.9426,-334.0296 1468.5266,-329.8083"/>
+</g>
+<!-- 12. Initial&#45;&gt;Leaving -->
+<g id="node10" class="node">
+<title>12. Initial&#45;&gt;Leaving</title>
+<ellipse fill="none" stroke="#000000" cx="1347.2978" cy="-234" rx="82.5854" ry="18"/>
+<text text-anchor="middle" x="1347.2978" y="-230.3" font-family="Times,serif" font-size="14.00" fill="#000000">12. Initial&#45;&gt;Leaving</text>
+</g>
+<!-- 3. Connected&#45;&gt;Connecting&#45;&gt;12. Initial&#45;&gt;Leaving -->
+<g id="edge9" class="edge">
+<title>3. Connected&#45;&gt;Connecting&#45;&gt;12. Initial&#45;&gt;Leaving</title>
+<path fill="none" stroke="#000000" d="M1576.0044,-506.1231C1504.1002,-480.7627 1376.1146,-423.5457 1322.2978,-324 1311.5438,-304.1082 1319.9223,-279.1841 1329.7812,-260.6115"/>
+<polygon fill="#000000" stroke="#000000" points="1332.8958,-262.2155 1334.8199,-251.7968 1326.8186,-258.7416 1332.8958,-262.2155"/>
+</g>
+<!-- 13. EnteringMessage&#45;&gt;EnteringMessage -->
+<g id="node11" class="node">
+<title>13. EnteringMessage&#45;&gt;EnteringMessage</title>
+<ellipse fill="none" stroke="#000000" cx="916.2978" cy="-378" rx="155.1726" ry="18"/>
+<text text-anchor="middle" x="916.2978" y="-374.3" font-family="Times,serif" font-size="14.00" fill="#000000">13. EnteringMessage&#45;&gt;EnteringMessage</text>
+</g>
+<!-- 3. Connected&#45;&gt;Connecting&#45;&gt;13. EnteringMessage&#45;&gt;EnteringMessage -->
+<g id="edge10" class="edge">
+<title>3. Connected&#45;&gt;Connecting&#45;&gt;13. EnteringMessage&#45;&gt;EnteringMessage</title>
+<path fill="none" stroke="#000000" d="M1528.8388,-514.9184C1440.8985,-507.3522 1308.9509,-492.9336 1196.2978,-468 1116.3463,-450.3043 1026.683,-419.46 970.8519,-398.8855"/>
+<polygon fill="#000000" stroke="#000000" points="971.7637,-395.4907 961.1707,-395.2956 969.33,-402.0541 971.7637,-395.4907"/>
+</g>
+<!-- 14. EnteringMessage&#45;&gt;Initial -->
+<g id="node12" class="node">
+<title>14. EnteringMessage&#45;&gt;Initial</title>
+<ellipse fill="none" stroke="#000000" cx="853.2978" cy="-306" rx="115.0796" ry="18"/>
+<text text-anchor="middle" x="853.2978" y="-302.3" font-family="Times,serif" font-size="14.00" fill="#000000">14. EnteringMessage&#45;&gt;Initial</text>
+</g>
+<!-- 3. Connected&#45;&gt;Connecting&#45;&gt;14. EnteringMessage&#45;&gt;Initial -->
+<g id="edge11" class="edge">
+<title>3. Connected&#45;&gt;Connecting&#45;&gt;14. EnteringMessage&#45;&gt;Initial</title>
+<path fill="none" stroke="#000000" d="M1529.5688,-514.6788C1461.0033,-507.554 1367.9059,-493.8485 1289.2978,-468 1189.972,-435.339 1178.327,-396.3678 1080.2978,-360 1035.1084,-343.2352 982.8894,-330.3893 939.9367,-321.4409"/>
+<polygon fill="#000000" stroke="#000000" points="940.5748,-317.999 930.0758,-319.4208 939.1698,-324.8566 940.5748,-317.999"/>
+</g>
+<!-- 15. EnteringMessage&#45;&gt;EnteringMessage -->
+<g id="node13" class="node">
+<title>15. EnteringMessage&#45;&gt;EnteringMessage</title>
+<ellipse fill="none" stroke="#000000" cx="525.2978" cy="-234" rx="155.1726" ry="18"/>
+<text text-anchor="middle" x="525.2978" y="-230.3" font-family="Times,serif" font-size="14.00" fill="#000000">15. EnteringMessage&#45;&gt;EnteringMessage</text>
+</g>
+<!-- 3. Connected&#45;&gt;Connecting&#45;&gt;15. EnteringMessage&#45;&gt;EnteringMessage -->
+<g id="edge12" class="edge">
+<title>3. Connected&#45;&gt;Connecting&#45;&gt;15. EnteringMessage&#45;&gt;EnteringMessage</title>
+<path fill="none" stroke="#000000" d="M1526.3965,-516.1898C1413.8859,-508.8024 1226.7508,-493.8014 1067.2978,-468 925.5311,-445.0605 883.2936,-454.8565 752.2978,-396 672.5965,-360.1902 592.4564,-294.3611 552.1048,-258.6334"/>
+<polygon fill="#000000" stroke="#000000" points="554.3658,-255.96 544.5769,-251.907 549.7018,-261.1799 554.3658,-255.96"/>
+</g>
+<!-- 18. ExpectingAnswer&#45;&gt;Pinging -->
+<g id="node16" class="node">
+<title>18. ExpectingAnswer&#45;&gt;Pinging</title>
+<ellipse fill="none" stroke="#000000" cx="1002.2978" cy="-162" rx="122.6784" ry="18"/>
+<text text-anchor="middle" x="1002.2978" y="-158.3" font-family="Times,serif" font-size="14.00" fill="#000000">18. ExpectingAnswer&#45;&gt;Pinging</text>
+</g>
+<!-- 3. Connected&#45;&gt;Connecting&#45;&gt;18. ExpectingAnswer&#45;&gt;Pinging -->
+<g id="edge35" class="edge">
+<title>3. Connected&#45;&gt;Connecting&#45;&gt;18. ExpectingAnswer&#45;&gt;Pinging</title>
+<path fill="none" stroke="#000000" d="M1524.9928,-516.829C1202.4839,-499.8583 228.2978,-443.1997 228.2978,-378 228.2978,-378 228.2978,-378 228.2978,-306 228.2978,-238.9772 286.5954,-239.674 349.2978,-216 441.3545,-181.2429 707.2107,-168.8014 869.9199,-164.3875"/>
+<polygon fill="#000000" stroke="#000000" points="870.0978,-167.8841 880.0017,-164.1207 869.9125,-160.8866 870.0978,-167.8841"/>
+</g>
+<!-- 19. ExpectingAnswer&#45;&gt;Initial -->
+<g id="node17" class="node">
+<title>19. ExpectingAnswer&#45;&gt;Initial</title>
+<ellipse fill="none" stroke="#000000" cx="1425.2978" cy="-90" rx="116.1796" ry="18"/>
+<text text-anchor="middle" x="1425.2978" y="-86.3" font-family="Times,serif" font-size="14.00" fill="#000000">19. ExpectingAnswer&#45;&gt;Initial</text>
+</g>
+<!-- 3. Connected&#45;&gt;Connecting&#45;&gt;19. ExpectingAnswer&#45;&gt;Initial -->
+<g id="edge36" class="edge">
+<title>3. Connected&#45;&gt;Connecting&#45;&gt;19. ExpectingAnswer&#45;&gt;Initial</title>
+<path fill="none" stroke="#000000" d="M1521.1988,-519.9461C1273.2352,-514.685 661.4126,-498.9111 458.2978,-468 302.0618,-444.2232 114.2978,-536.0348 114.2978,-378 114.2978,-378 114.2978,-378 114.2978,-234 114.2978,-146.9343 204.2123,-166.5849 288.2978,-144 383.797,-118.3494 1024.9874,-99.7993 1300.204,-92.9264"/>
+<polygon fill="#000000" stroke="#000000" points="1300.328,-96.4245 1310.2379,-92.6769 1300.154,-89.4266 1300.328,-96.4245"/>
+</g>
+<!-- 16. Initial&#45;&gt;Pinging -->
+<g id="node19" class="node">
+<title>16. Initial&#45;&gt;Pinging</title>
+<ellipse fill="none" stroke="#000000" cx="2449.2978" cy="-162" rx="81.4863" ry="18"/>
+<text text-anchor="middle" x="2449.2978" y="-158.3" font-family="Times,serif" font-size="14.00" fill="#000000">16. Initial&#45;&gt;Pinging</text>
+</g>
+<!-- 3. Connected&#45;&gt;Connecting&#45;&gt;16. Initial&#45;&gt;Pinging -->
+<g id="edge33" class="edge">
+<title>3. Connected&#45;&gt;Connecting&#45;&gt;16. Initial&#45;&gt;Pinging</title>
+<path fill="none" stroke="#000000" d="M1733.7892,-521.1232C2050.0092,-518.0965 2969.5986,-506.0876 3099.2978,-468 3174.6264,-445.8789 3251.2978,-456.5096 3251.2978,-378 3251.2978,-378 3251.2978,-378 3251.2978,-306 3251.2978,-210.9512 3149.1158,-240.5707 3057.2978,-216 2962.0141,-190.5019 2683.8047,-173.5326 2539.0929,-166.1713"/>
+<polygon fill="#000000" stroke="#000000" points="2539.0723,-162.6659 2528.9087,-165.6579 2538.7198,-169.657 2539.0723,-162.6659"/>
+</g>
+<!-- 17. Pinging&#45;&gt;ExpectingAnswer -->
+<g id="node20" class="node">
+<title>17. Pinging&#45;&gt;ExpectingAnswer</title>
+<ellipse fill="none" stroke="#000000" cx="1701.2978" cy="-162" rx="122.6784" ry="18"/>
+<text text-anchor="middle" x="1701.2978" y="-158.3" font-family="Times,serif" font-size="14.00" fill="#000000">17. Pinging&#45;&gt;ExpectingAnswer</text>
+</g>
+<!-- 3. Connected&#45;&gt;Connecting&#45;&gt;17. Pinging&#45;&gt;ExpectingAnswer -->
+<g id="edge34" class="edge">
+<title>3. Connected&#45;&gt;Connecting&#45;&gt;17. Pinging&#45;&gt;ExpectingAnswer</title>
+<path fill="none" stroke="#000000" d="M1733.4983,-520.2272C2054.3826,-514.5754 2995.636,-495.7122 3055.2978,-468 3104.3748,-445.2043 3137.2978,-432.1128 3137.2978,-378 3137.2978,-378 3137.2978,-378 3137.2978,-306 3137.2978,-242.488 3085.7157,-238.434 3026.2978,-216 2998.6098,-205.5461 2160.0967,-177.0322 1831.5365,-166.227"/>
+<polygon fill="#000000" stroke="#000000" points="1831.6,-162.7273 1821.4904,-165.8969 1831.3701,-169.7235 1831.6,-162.7273"/>
+</g>
+<!-- 4. NotJoined&#45;&gt;GettingRoomNumber&#45;&gt;18. ExpectingAnswer&#45;&gt;Pinging -->
+<g id="edge39" class="edge">
+<title>4. NotJoined&#45;&gt;GettingRoomNumber&#45;&gt;18. ExpectingAnswer&#45;&gt;Pinging</title>
+<path fill="none" stroke="#000000" d="M1487.0502,-221.4586C1380.4496,-208.3832 1214.2296,-187.995 1106.7982,-174.8178"/>
+<polygon fill="#000000" stroke="#000000" points="1106.9409,-171.3091 1096.5891,-173.5655 1106.0886,-178.2571 1106.9409,-171.3091"/>
+</g>
+<!-- 4. NotJoined&#45;&gt;GettingRoomNumber&#45;&gt;19. ExpectingAnswer&#45;&gt;Initial -->
+<g id="edge40" class="edge">
+<title>4. NotJoined&#45;&gt;GettingRoomNumber&#45;&gt;19. ExpectingAnswer&#45;&gt;Initial</title>
+<path fill="none" stroke="#000000" d="M1568.8587,-216.0535C1539.808,-190.5455 1486.4642,-143.7071 1453.6181,-114.8666"/>
+<polygon fill="#000000" stroke="#000000" points="1455.56,-111.914 1445.7362,-107.946 1450.9414,-117.1741 1455.56,-111.914"/>
+</g>
+<!-- 4. NotJoined&#45;&gt;GettingRoomNumber&#45;&gt;16. Initial&#45;&gt;Pinging -->
+<g id="edge37" class="edge">
+<title>4. NotJoined&#45;&gt;GettingRoomNumber&#45;&gt;16. Initial&#45;&gt;Pinging</title>
+<path fill="none" stroke="#000000" d="M1701.7052,-223.0215C1726.9009,-220.6368 1753.5077,-218.1779 1778.2978,-216 1987.7148,-197.6021 2234.1227,-178.398 2362.1451,-168.6041"/>
+<polygon fill="#000000" stroke="#000000" points="2362.5784,-172.0812 2372.2826,-167.8293 2362.0449,-165.1016 2362.5784,-172.0812"/>
+</g>
+<!-- 4. NotJoined&#45;&gt;GettingRoomNumber&#45;&gt;17. Pinging&#45;&gt;ExpectingAnswer -->
+<g id="edge38" class="edge">
+<title>4. NotJoined&#45;&gt;GettingRoomNumber&#45;&gt;17. Pinging&#45;&gt;ExpectingAnswer</title>
+<path fill="none" stroke="#000000" d="M1616.9832,-216.2022C1631.6311,-206.7857 1649.7865,-195.1144 1665.4941,-185.0167"/>
+<polygon fill="#000000" stroke="#000000" points="1667.4117,-187.9448 1673.9308,-179.593 1663.6264,-182.0565 1667.4117,-187.9448"/>
+</g>
+<!-- 5. GettingRoomNumber&#45;&gt;GettingRoomNumber&#45;&gt;6. GettingRoomNumber&#45;&gt;JoiningOrJoined -->
+<g id="edge14" class="edge">
+<title>5. GettingRoomNumber&#45;&gt;GettingRoomNumber&#45;&gt;6. GettingRoomNumber&#45;&gt;JoiningOrJoined</title>
+<path fill="none" stroke="#000000" d="M2750.4865,-435.7751C2652.1351,-423.3735 2509.988,-405.4496 2410.1702,-392.8631"/>
+<polygon fill="#000000" stroke="#000000" points="2410.3985,-389.3642 2400.0392,-391.5856 2409.5228,-396.3092 2410.3985,-389.3642"/>
+</g>
+<!-- 5. GettingRoomNumber&#45;&gt;GettingRoomNumber&#45;&gt;18. ExpectingAnswer&#45;&gt;Pinging -->
+<g id="edge43" class="edge">
+<title>5. GettingRoomNumber&#45;&gt;GettingRoomNumber&#45;&gt;18. ExpectingAnswer&#45;&gt;Pinging</title>
+<path fill="none" stroke="#000000" d="M2692.0406,-443.4981C2540.8499,-436.348 2314.7209,-422.2147 2119.2978,-396 1872.8289,-362.9378 1817.0092,-319.2004 1570.2978,-288 1501.0678,-279.2448 991.2056,-302.7374 943.2978,-252 924.4805,-232.0713 946.6054,-205.4276 968.9275,-186.3095"/>
+<polygon fill="#000000" stroke="#000000" points="971.2503,-188.9312 976.7645,-179.8844 966.8122,-183.5178 971.2503,-188.9312"/>
+</g>
+<!-- 5. GettingRoomNumber&#45;&gt;GettingRoomNumber&#45;&gt;19. ExpectingAnswer&#45;&gt;Initial -->
+<g id="edge44" class="edge">
+<title>5. GettingRoomNumber&#45;&gt;GettingRoomNumber&#45;&gt;19. ExpectingAnswer&#45;&gt;Initial</title>
+<path fill="none" stroke="#000000" d="M2977.9699,-435.9492C3028.9436,-427.3147 3081.28,-414.3309 3098.2978,-396 3193.5496,-293.3984 3045.1314,-177.9002 2909.2978,-144 2779.6318,-111.6391 1886.441,-96.2742 1551.6538,-91.6032"/>
+<polygon fill="#000000" stroke="#000000" points="1551.4773,-88.1005 1541.4297,-91.4614 1551.3802,-95.0998 1551.4773,-88.1005"/>
+</g>
+<!-- 5. GettingRoomNumber&#45;&gt;GettingRoomNumber&#45;&gt;16. Initial&#45;&gt;Pinging -->
+<g id="edge41" class="edge">
+<title>5. GettingRoomNumber&#45;&gt;GettingRoomNumber&#45;&gt;16. Initial&#45;&gt;Pinging</title>
+<path fill="none" stroke="#000000" d="M2969.4158,-435.322C3015.2343,-426.6029 3061.5173,-413.7306 3075.2978,-396 3126.5524,-330.0533 3094.1625,-256.8256 3021.2978,-216 2980.2807,-193.0184 2689.414,-174.5975 2538.9726,-166.4853"/>
+<polygon fill="#000000" stroke="#000000" points="2539.0024,-162.9819 2528.8296,-165.9425 2538.6283,-169.9719 2539.0024,-162.9819"/>
+</g>
+<!-- 5. GettingRoomNumber&#45;&gt;GettingRoomNumber&#45;&gt;17. Pinging&#45;&gt;ExpectingAnswer -->
+<g id="edge42" class="edge">
+<title>5. GettingRoomNumber&#45;&gt;GettingRoomNumber&#45;&gt;17. Pinging&#45;&gt;ExpectingAnswer</title>
+<path fill="none" stroke="#000000" d="M2888.7446,-432.0762C2945.1145,-390.3364 3070.4633,-284.9644 3004.2978,-216 2994.2228,-205.4989 2159.2221,-177.0137 1831.3622,-166.2215"/>
+<polygon fill="#000000" stroke="#000000" points="1831.4466,-162.7225 1821.337,-165.8918 1831.2165,-169.7187 1831.4466,-162.7225"/>
+</g>
+<!-- 6. GettingRoomNumber&#45;&gt;JoiningOrJoined&#45;&gt;7. GettingRoomNumber&#45;&gt;GettingRoomNumber -->
+<g id="edge15" class="edge">
+<title>6. GettingRoomNumber&#45;&gt;JoiningOrJoined&#45;&gt;7. GettingRoomNumber&#45;&gt;GettingRoomNumber</title>
+<path fill="none" stroke="#000000" d="M2292.2978,-359.8314C2292.2978,-352.131 2292.2978,-342.9743 2292.2978,-334.4166"/>
+<polygon fill="#000000" stroke="#000000" points="2295.7979,-334.4132 2292.2978,-324.4133 2288.7979,-334.4133 2295.7979,-334.4132"/>
+</g>
+<!-- 6. GettingRoomNumber&#45;&gt;JoiningOrJoined&#45;&gt;18. ExpectingAnswer&#45;&gt;Pinging -->
+<g id="edge47" class="edge">
+<title>6. GettingRoomNumber&#45;&gt;JoiningOrJoined&#45;&gt;18. ExpectingAnswer&#45;&gt;Pinging</title>
+<path fill="none" stroke="#000000" d="M2193.8405,-363.6135C2055.0726,-343.8195 1793.9042,-308.3332 1570.2978,-288 1500.8031,-281.6806 991.2056,-302.7374 943.2978,-252 924.4805,-232.0713 946.6054,-205.4276 968.9275,-186.3095"/>
+<polygon fill="#000000" stroke="#000000" points="971.2503,-188.9312 976.7645,-179.8844 966.8122,-183.5178 971.2503,-188.9312"/>
+</g>
+<!-- 6. GettingRoomNumber&#45;&gt;JoiningOrJoined&#45;&gt;19. ExpectingAnswer&#45;&gt;Initial -->
+<g id="edge48" class="edge">
+<title>6. GettingRoomNumber&#45;&gt;JoiningOrJoined&#45;&gt;19. ExpectingAnswer&#45;&gt;Initial</title>
+<path fill="none" stroke="#000000" d="M2450.8146,-373.4531C2606.9218,-367.3355 2833.627,-353.5882 2916.2978,-324 2979.3285,-301.4411 3060.4418,-270.3095 3021.2978,-216 2962.1292,-133.9081 2904.8479,-162.1594 2805.2978,-144 2684.07,-121.8863 1867.604,-100.4655 1550.6963,-92.8855"/>
+<polygon fill="#000000" stroke="#000000" points="1550.6315,-89.3831 1540.5508,-92.6435 1550.4645,-96.3811 1550.6315,-89.3831"/>
+</g>
+<!-- 6. GettingRoomNumber&#45;&gt;JoiningOrJoined&#45;&gt;16. Initial&#45;&gt;Pinging -->
+<g id="edge45" class="edge">
+<title>6. GettingRoomNumber&#45;&gt;JoiningOrJoined&#45;&gt;16. Initial&#45;&gt;Pinging</title>
+<path fill="none" stroke="#000000" d="M2449.5597,-372.9238C2637.3668,-363.1645 2934.9298,-334.7216 3004.2978,-252 3014.5786,-239.7401 3015.0497,-227.8489 3004.2978,-216 2973.7725,-182.3606 2689.6858,-169.0211 2540.2447,-164.2973"/>
+<polygon fill="#000000" stroke="#000000" points="2540.2651,-160.7963 2530.1615,-163.9852 2540.0484,-167.793 2540.2651,-160.7963"/>
+</g>
+<!-- 6. GettingRoomNumber&#45;&gt;JoiningOrJoined&#45;&gt;17. Pinging&#45;&gt;ExpectingAnswer -->
+<g id="edge46" class="edge">
+<title>6. GettingRoomNumber&#45;&gt;JoiningOrJoined&#45;&gt;17. Pinging&#45;&gt;ExpectingAnswer</title>
+<path fill="none" stroke="#000000" d="M2221.4336,-361.6457C2184.7122,-352.2795 2139.474,-339.3369 2100.2978,-324 2034.7757,-298.3491 2015.2928,-294.6106 1959.2978,-252 1942.0251,-238.856 1945.0009,-227.0138 1926.2978,-216 1891.344,-195.4167 1848.9584,-182.6696 1810.442,-174.7794"/>
+<polygon fill="#000000" stroke="#000000" points="1810.7032,-171.2642 1800.2171,-172.7784 1809.3587,-178.1339 1810.7032,-171.2642"/>
+</g>
+<!-- 7. GettingRoomNumber&#45;&gt;GettingRoomNumber&#45;&gt;8. GettingRoomNumber&#45;&gt;GettingRoomNumber -->
+<g id="edge16" class="edge">
+<title>7. GettingRoomNumber&#45;&gt;GettingRoomNumber&#45;&gt;8. GettingRoomNumber&#45;&gt;GettingRoomNumber</title>
+<path fill="none" stroke="#000000" d="M2398.4682,-291.2995C2484.8467,-279.3394 2606.5972,-262.4816 2695.6769,-250.1475"/>
+<polygon fill="#000000" stroke="#000000" points="2696.4013,-253.5807 2705.8267,-248.7421 2695.4411,-246.6468 2696.4013,-253.5807"/>
+</g>
+<!-- 7. GettingRoomNumber&#45;&gt;GettingRoomNumber&#45;&gt;18. ExpectingAnswer&#45;&gt;Pinging -->
+<g id="edge51" class="edge">
+<title>7. GettingRoomNumber&#45;&gt;GettingRoomNumber&#45;&gt;18. ExpectingAnswer&#45;&gt;Pinging</title>
+<path fill="none" stroke="#000000" d="M2117.6781,-300.4931C1757.6056,-288.9334 965.242,-262.3539 955.2978,-252 937.4331,-233.3992 955.3401,-206.6628 973.9657,-187.1658"/>
+<polygon fill="#000000" stroke="#000000" points="976.4602,-189.6211 981.0662,-180.0798 971.5155,-184.6662 976.4602,-189.6211"/>
+</g>
+<!-- 7. GettingRoomNumber&#45;&gt;GettingRoomNumber&#45;&gt;19. ExpectingAnswer&#45;&gt;Initial -->
+<g id="edge52" class="edge">
+<title>7. GettingRoomNumber&#45;&gt;GettingRoomNumber&#45;&gt;19. ExpectingAnswer&#45;&gt;Initial</title>
+<path fill="none" stroke="#000000" d="M2461.2205,-298.9127C2665.9403,-289.4857 2986.0332,-271.7022 3004.2978,-252 3015.1753,-240.2663 3014.5246,-228.305 3004.2978,-216 2892.473,-81.4518 2791.1015,-164.0068 2617.2978,-144 2413.7055,-120.5642 1812.7879,-101.098 1550.3265,-93.4646"/>
+<polygon fill="#000000" stroke="#000000" points="1550.0875,-89.9563 1539.9903,-93.165 1549.8846,-96.9533 1550.0875,-89.9563"/>
+</g>
+<!-- 7. GettingRoomNumber&#45;&gt;GettingRoomNumber&#45;&gt;16. Initial&#45;&gt;Pinging -->
+<g id="edge49" class="edge">
+<title>7. GettingRoomNumber&#45;&gt;GettingRoomNumber&#45;&gt;16. Initial&#45;&gt;Pinging</title>
+<path fill="none" stroke="#000000" d="M2439.6215,-295.1957C2499.4379,-287.462 2558.8262,-274.3001 2577.2978,-252 2587.5042,-239.6781 2586.1435,-229.3324 2577.2978,-216 2564.6938,-197.003 2543.9469,-184.6727 2522.7886,-176.6758"/>
+<polygon fill="#000000" stroke="#000000" points="2523.6608,-173.2737 2513.066,-173.2981 2521.3636,-179.886 2523.6608,-173.2737"/>
+</g>
+<!-- 7. GettingRoomNumber&#45;&gt;GettingRoomNumber&#45;&gt;17. Pinging&#45;&gt;ExpectingAnswer -->
+<g id="edge50" class="edge">
+<title>7. GettingRoomNumber&#45;&gt;GettingRoomNumber&#45;&gt;17. Pinging&#45;&gt;ExpectingAnswer</title>
+<path fill="none" stroke="#000000" d="M2183.1348,-291.5406C2114.8513,-281.3733 2034.0287,-266.96 2002.2978,-252 1979.7532,-241.371 1981.7229,-226.8789 1959.2978,-216 1914.5141,-194.2746 1861.211,-181.2623 1814.7124,-173.481"/>
+<polygon fill="#000000" stroke="#000000" points="1815.0221,-169.9859 1804.5928,-171.8513 1813.909,-176.8969 1815.0221,-169.9859"/>
+</g>
+<!-- 8. GettingRoomNumber&#45;&gt;GettingRoomNumber&#45;&gt;18. ExpectingAnswer&#45;&gt;Pinging -->
+<g id="edge55" class="edge">
+<title>8. GettingRoomNumber&#45;&gt;GettingRoomNumber&#45;&gt;18. ExpectingAnswer&#45;&gt;Pinging</title>
+<path fill="none" stroke="#000000" d="M2648.259,-225.9358C2580.7527,-222.7043 2501.7718,-219.0353 2430.2978,-216 1952.0306,-195.6895 1383.4933,-175.3191 1132.4567,-166.5171"/>
+<polygon fill="#000000" stroke="#000000" points="1132.3181,-163.0102 1122.2016,-166.1578 1132.0729,-170.0059 1132.3181,-163.0102"/>
+</g>
+<!-- 8. GettingRoomNumber&#45;&gt;GettingRoomNumber&#45;&gt;19. ExpectingAnswer&#45;&gt;Initial -->
+<g id="edge56" class="edge">
+<title>8. GettingRoomNumber&#45;&gt;GettingRoomNumber&#45;&gt;19. ExpectingAnswer&#45;&gt;Initial</title>
+<path fill="none" stroke="#000000" d="M2770.6682,-216.3467C2717.9194,-194.903 2623.6941,-159.658 2539.2978,-144 2353.28,-109.4883 1802.1311,-96.1997 1551.6847,-91.8429"/>
+<polygon fill="#000000" stroke="#000000" points="1551.5039,-88.3394 1541.4451,-91.6669 1551.3835,-95.3384 1551.5039,-88.3394"/>
+</g>
+<!-- 8. GettingRoomNumber&#45;&gt;GettingRoomNumber&#45;&gt;16. Initial&#45;&gt;Pinging -->
+<g id="edge53" class="edge">
+<title>8. GettingRoomNumber&#45;&gt;GettingRoomNumber&#45;&gt;16. Initial&#45;&gt;Pinging</title>
+<path fill="none" stroke="#000000" d="M2730.8335,-217.8418C2667.3716,-205.2543 2580.1808,-187.9603 2519.7157,-175.9672"/>
+<polygon fill="#000000" stroke="#000000" points="2520.3645,-172.5278 2509.8746,-174.0152 2519.0025,-179.394 2520.3645,-172.5278"/>
+</g>
+<!-- 8. GettingRoomNumber&#45;&gt;GettingRoomNumber&#45;&gt;17. Pinging&#45;&gt;ExpectingAnswer -->
+<g id="edge54" class="edge">
+<title>8. GettingRoomNumber&#45;&gt;GettingRoomNumber&#45;&gt;17. Pinging&#45;&gt;ExpectingAnswer</title>
+<path fill="none" stroke="#000000" d="M2659.2755,-224.0832C2436.7744,-209.6637 2028.2883,-183.1911 1824.1674,-169.9627"/>
+<polygon fill="#000000" stroke="#000000" points="1824.2117,-166.4584 1814.0062,-169.3042 1823.7589,-173.4437 1824.2117,-166.4584"/>
+</g>
+<!-- 9. Leaving&#45;&gt;NotJoined&#45;&gt;18. ExpectingAnswer&#45;&gt;Pinging -->
+<g id="edge59" class="edge">
+<title>9. Leaving&#45;&gt;NotJoined&#45;&gt;18. ExpectingAnswer&#45;&gt;Pinging</title>
+<path fill="none" stroke="#000000" d="M2262.9099,-221.1586C2250.7782,-219.1472 2238.1843,-217.3054 2226.2978,-216 2119.9252,-204.3183 1424.4358,-177.6338 1131.7574,-166.7521"/>
+<polygon fill="#000000" stroke="#000000" points="1131.6406,-163.2454 1121.5175,-166.3717 1131.3806,-170.2406 1131.6406,-163.2454"/>
+</g>
+<!-- 9. Leaving&#45;&gt;NotJoined&#45;&gt;19. ExpectingAnswer&#45;&gt;Initial -->
+<g id="edge60" class="edge">
+<title>9. Leaving&#45;&gt;NotJoined&#45;&gt;19. ExpectingAnswer&#45;&gt;Initial</title>
+<path fill="none" stroke="#000000" d="M2272.7589,-219.4754C2195.5543,-199.765 2051.1924,-164.6439 1926.2978,-144 1794.7375,-122.2544 1642.2317,-107.2602 1540.3619,-98.6868"/>
+<polygon fill="#000000" stroke="#000000" points="1540.6128,-95.1957 1530.3563,-97.8517 1540.0305,-102.1714 1540.6128,-95.1957"/>
+</g>
+<!-- 9. Leaving&#45;&gt;NotJoined&#45;&gt;16. Initial&#45;&gt;Pinging -->
+<g id="edge57" class="edge">
+<title>9. Leaving&#45;&gt;NotJoined&#45;&gt;16. Initial&#45;&gt;Pinging</title>
+<path fill="none" stroke="#000000" d="M2357.2803,-216.7542C2373.5936,-207.0471 2394.1485,-194.8161 2411.6911,-184.3775"/>
+<polygon fill="#000000" stroke="#000000" points="2413.7478,-187.2265 2420.5517,-179.1051 2410.1683,-181.2109 2413.7478,-187.2265"/>
+</g>
+<!-- 9. Leaving&#45;&gt;NotJoined&#45;&gt;17. Pinging&#45;&gt;ExpectingAnswer -->
+<g id="edge58" class="edge">
+<title>9. Leaving&#45;&gt;NotJoined&#45;&gt;17. Pinging&#45;&gt;ExpectingAnswer</title>
+<path fill="none" stroke="#000000" d="M2261.1953,-221.4487C2249.5813,-219.4797 2237.6068,-217.5774 2226.2978,-216 2086.7369,-196.5343 1925.3897,-180.9683 1818.7975,-171.6415"/>
+<polygon fill="#000000" stroke="#000000" points="1818.9216,-168.1392 1808.6557,-170.7585 1818.3144,-175.1128 1818.9216,-168.1392"/>
+</g>
+<!-- 10. Joining&#45;&gt;H&#45;&gt;18. ExpectingAnswer&#45;&gt;Pinging -->
+<g id="edge63" class="edge">
+<title>10. Joining&#45;&gt;H&#45;&gt;18. ExpectingAnswer&#45;&gt;Pinging</title>
+<path fill="none" stroke="#000000" d="M1797.4567,-224.2172C1779.3082,-221.2391 1758.9787,-218.1805 1740.2978,-216 1526.6887,-191.0671 1276.8689,-175.6515 1129.5378,-167.9676"/>
+<polygon fill="#000000" stroke="#000000" points="1129.7138,-164.4721 1119.5462,-167.4501 1129.3517,-171.4627 1129.7138,-164.4721"/>
+</g>
+<!-- 10. Joining&#45;&gt;H&#45;&gt;19. ExpectingAnswer&#45;&gt;Initial -->
+<g id="edge64" class="edge">
+<title>10. Joining&#45;&gt;H&#45;&gt;19. ExpectingAnswer&#45;&gt;Initial</title>
+<path fill="none" stroke="#000000" d="M1854.083,-215.8701C1855.0117,-195.294 1852.9797,-162.2317 1833.2978,-144 1812.0386,-124.3073 1653.8775,-107.8879 1540.863,-98.5014"/>
+<polygon fill="#000000" stroke="#000000" points="1541.0118,-95.0019 1530.7587,-97.6708 1540.4383,-101.9784 1541.0118,-95.0019"/>
+</g>
+<!-- 10. Joining&#45;&gt;H&#45;&gt;16. Initial&#45;&gt;Pinging -->
+<g id="edge61" class="edge">
+<title>10. Joining&#45;&gt;H&#45;&gt;16. Initial&#45;&gt;Pinging</title>
+<path fill="none" stroke="#000000" d="M1911.9981,-226.8C2019.5672,-213.8268 2246.0336,-186.5143 2367.773,-171.8321"/>
+<polygon fill="#000000" stroke="#000000" points="2368.278,-175.2967 2377.7869,-170.6244 2367.4398,-168.347 2368.278,-175.2967"/>
+</g>
+<!-- 10. Joining&#45;&gt;H&#45;&gt;17. Pinging&#45;&gt;ExpectingAnswer -->
+<g id="edge62" class="edge">
+<title>10. Joining&#45;&gt;H&#45;&gt;17. Pinging&#45;&gt;ExpectingAnswer</title>
+<path fill="none" stroke="#000000" d="M1819.533,-218.3771C1798.1688,-208.1902 1769.9974,-194.7575 1746.5124,-183.5593"/>
+<polygon fill="#000000" stroke="#000000" points="1747.9674,-180.3756 1737.4345,-179.2308 1744.9545,-186.6941 1747.9674,-180.3756"/>
+</g>
+<!-- 11. Initial&#45;&gt;EnteringMessage&#45;&gt;12. Initial&#45;&gt;Leaving -->
+<g id="edge17" class="edge">
+<title>11. Initial&#45;&gt;EnteringMessage&#45;&gt;12. Initial&#45;&gt;Leaving</title>
+<path fill="none" stroke="#000000" d="M1422.0796,-288.3868C1409.2803,-279.0782 1393.3982,-267.5276 1379.5669,-257.4685"/>
+<polygon fill="#000000" stroke="#000000" points="1381.4119,-254.4825 1371.2659,-251.4313 1377.2946,-260.1437 1381.4119,-254.4825"/>
+</g>
+<!-- 11. Initial&#45;&gt;EnteringMessage&#45;&gt;18. ExpectingAnswer&#45;&gt;Pinging -->
+<g id="edge67" class="edge">
+<title>11. Initial&#45;&gt;EnteringMessage&#45;&gt;18. ExpectingAnswer&#45;&gt;Pinging</title>
+<path fill="none" stroke="#000000" d="M1340.6057,-298.8753C1161.6055,-286.5597 817.1942,-261.6813 808.2978,-252 772.2751,-212.7996 837.4692,-189.2771 901.7955,-176.1679"/>
+<polygon fill="#000000" stroke="#000000" points="902.5411,-179.5885 911.6814,-174.2307 901.1949,-172.7191 902.5411,-179.5885"/>
+</g>
+<!-- 11. Initial&#45;&gt;EnteringMessage&#45;&gt;19. ExpectingAnswer&#45;&gt;Initial -->
+<g id="edge68" class="edge">
+<title>11. Initial&#45;&gt;EnteringMessage&#45;&gt;19. ExpectingAnswer&#45;&gt;Initial</title>
+<path fill="none" stroke="#000000" d="M1341.2072,-298.6032C1289.9693,-295.1292 1227.4312,-291.0842 1171.2978,-288 1126.3212,-285.5288 392.4338,-284.5506 361.2978,-252 188.7082,-71.5694 -524.177,-316.7848 713.2978,-144 918.6223,-115.3312 1159.5349,-101.0742 1301.9146,-94.6342"/>
+<polygon fill="#000000" stroke="#000000" points="1302.1601,-98.1268 1311.9939,-94.1839 1301.8476,-91.1338 1302.1601,-98.1268"/>
+</g>
+<!-- 11. Initial&#45;&gt;EnteringMessage&#45;&gt;16. Initial&#45;&gt;Pinging -->
+<g id="edge65" class="edge">
+<title>11. Initial&#45;&gt;EnteringMessage&#45;&gt;16. Initial&#45;&gt;Pinging</title>
+<path fill="none" stroke="#000000" d="M1557.7088,-301.2914C1827.2755,-289.7698 2493.2396,-260.4812 2501.2978,-252 2519.6743,-232.6588 2499.4822,-205.6402 2479.1404,-186.2625"/>
+<polygon fill="#000000" stroke="#000000" points="2481.461,-183.642 2471.7104,-179.4974 2476.7482,-188.8179 2481.461,-183.642"/>
+</g>
+<!-- 11. Initial&#45;&gt;EnteringMessage&#45;&gt;17. Pinging&#45;&gt;ExpectingAnswer -->
+<g id="edge66" class="edge">
+<title>11. Initial&#45;&gt;EnteringMessage&#45;&gt;17. Pinging&#45;&gt;ExpectingAnswer</title>
+<path fill="none" stroke="#000000" d="M1555.6355,-300.2197C1629.1456,-293.7802 1716.7558,-280.2598 1740.2978,-252 1756.0339,-233.1103 1741.6166,-206.9018 1726.0518,-187.6375"/>
+<polygon fill="#000000" stroke="#000000" points="1728.5529,-185.1768 1719.3955,-179.8482 1723.2312,-189.7243 1728.5529,-185.1768"/>
+</g>
+<!-- 12. Initial&#45;&gt;Leaving&#45;&gt;18. ExpectingAnswer&#45;&gt;Pinging -->
+<g id="edge71" class="edge">
+<title>12. Initial&#45;&gt;Leaving&#45;&gt;18. ExpectingAnswer&#45;&gt;Pinging</title>
+<path fill="none" stroke="#000000" d="M1287.5972,-221.5408C1231.0302,-209.7355 1145.645,-191.916 1083.0238,-178.8472"/>
+<polygon fill="#000000" stroke="#000000" points="1083.681,-175.409 1073.1768,-176.7922 1082.2509,-182.2614 1083.681,-175.409"/>
+</g>
+<!-- 12. Initial&#45;&gt;Leaving&#45;&gt;19. ExpectingAnswer&#45;&gt;Initial -->
+<g id="edge72" class="edge">
+<title>12. Initial&#45;&gt;Leaving&#45;&gt;19. ExpectingAnswer&#45;&gt;Initial</title>
+<path fill="none" stroke="#000000" d="M1357.0188,-216.0535C1370.4476,-191.2618 1394.7907,-146.3207 1410.4898,-117.3378"/>
+<polygon fill="#000000" stroke="#000000" points="1413.7689,-118.6327 1415.4542,-108.1727 1407.6138,-115.2986 1413.7689,-118.6327"/>
+</g>
+<!-- 12. Initial&#45;&gt;Leaving&#45;&gt;16. Initial&#45;&gt;Pinging -->
+<g id="edge69" class="edge">
+<title>12. Initial&#45;&gt;Leaving&#45;&gt;16. Initial&#45;&gt;Pinging</title>
+<path fill="none" stroke="#000000" d="M1405.8416,-221.1504C1416.5934,-219.1529 1427.7507,-217.318 1438.2978,-216 1614.9427,-193.9254 2144.9991,-172.9761 2358.609,-165.1914"/>
+<polygon fill="#000000" stroke="#000000" points="2358.9801,-168.6803 2368.8465,-164.8196 2358.726,-161.6849 2358.9801,-168.6803"/>
+</g>
+<!-- 12. Initial&#45;&gt;Leaving&#45;&gt;17. Pinging&#45;&gt;ExpectingAnswer -->
+<g id="edge70" class="edge">
+<title>12. Initial&#45;&gt;Leaving&#45;&gt;17. Pinging&#45;&gt;ExpectingAnswer</title>
+<path fill="none" stroke="#000000" d="M1407.7503,-221.7046C1466.046,-209.8478 1554.7048,-191.8155 1619.3336,-178.6707"/>
+<polygon fill="#000000" stroke="#000000" points="1620.3898,-182.0276 1629.4915,-176.6047 1618.9945,-175.1681 1620.3898,-182.0276"/>
+</g>
+<!-- 13. EnteringMessage&#45;&gt;EnteringMessage&#45;&gt;14. EnteringMessage&#45;&gt;Initial -->
+<g id="edge18" class="edge">
+<title>13. EnteringMessage&#45;&gt;EnteringMessage&#45;&gt;14. EnteringMessage&#45;&gt;Initial</title>
+<path fill="none" stroke="#000000" d="M900.4002,-359.8314C892.8821,-351.2392 883.7775,-340.834 875.5847,-331.4708"/>
+<polygon fill="#000000" stroke="#000000" points="878.1911,-329.1344 868.972,-323.9134 872.9231,-333.744 878.1911,-329.1344"/>
+</g>
+<!-- 13. EnteringMessage&#45;&gt;EnteringMessage&#45;&gt;18. ExpectingAnswer&#45;&gt;Pinging -->
+<g id="edge75" class="edge">
+<title>13. EnteringMessage&#45;&gt;EnteringMessage&#45;&gt;18. ExpectingAnswer&#45;&gt;Pinging</title>
+<path fill="none" stroke="#000000" d="M790.8045,-367.3863C643.9317,-352.0591 414.0079,-318.018 361.2978,-252 351.3147,-239.4965 350.4693,-227.779 361.2978,-216 394.9399,-179.4046 691.8367,-167.5925 869.5371,-163.7921"/>
+<polygon fill="#000000" stroke="#000000" points="869.8234,-167.287 879.7485,-163.5797 869.6778,-160.2885 869.8234,-167.287"/>
+</g>
+<!-- 13. EnteringMessage&#45;&gt;EnteringMessage&#45;&gt;19. ExpectingAnswer&#45;&gt;Initial -->
+<g id="edge76" class="edge">
+<title>13. EnteringMessage&#45;&gt;EnteringMessage&#45;&gt;19. ExpectingAnswer&#45;&gt;Initial</title>
+<path fill="none" stroke="#000000" d="M778.5427,-369.6528C653.222,-360.8955 478.0912,-345.4141 412.2978,-324 351.333,-304.1576 319.3822,-307.5069 287.2978,-252 272.4046,-226.2345 302.4753,-146.3152 305.2978,-144 343.1745,-112.9297 1014.1552,-97.3313 1299.0381,-92.0856"/>
+<polygon fill="#000000" stroke="#000000" points="1299.4866,-95.5781 1309.421,-91.8959 1299.3587,-88.5793 1299.4866,-95.5781"/>
+</g>
+<!-- 13. EnteringMessage&#45;&gt;EnteringMessage&#45;&gt;16. Initial&#45;&gt;Pinging -->
+<g id="edge73" class="edge">
+<title>13. EnteringMessage&#45;&gt;EnteringMessage&#45;&gt;16. Initial&#45;&gt;Pinging</title>
+<path fill="none" stroke="#000000" d="M1046.0906,-368.0797C1426.9717,-338.9319 2515.1732,-255.38 2518.2978,-252 2538.1965,-230.4748 2511.6105,-203.5451 2485.8792,-184.7781"/>
+<polygon fill="#000000" stroke="#000000" points="2487.8134,-181.8598 2477.6149,-178.989 2483.7972,-187.5931 2487.8134,-181.8598"/>
+</g>
+<!-- 13. EnteringMessage&#45;&gt;EnteringMessage&#45;&gt;17. Pinging&#45;&gt;ExpectingAnswer -->
+<g id="edge74" class="edge">
+<title>13. EnteringMessage&#45;&gt;EnteringMessage&#45;&gt;17. Pinging&#45;&gt;ExpectingAnswer</title>
+<path fill="none" stroke="#000000" d="M1015.663,-364.1275C1075.6504,-354.3881 1145.3573,-340.2351 1171.2978,-324 1222.8441,-291.7392 1202.3795,-245.9572 1255.2978,-216 1307.8008,-186.2779 1459.7268,-172.7582 1571.735,-166.7126"/>
+<polygon fill="#000000" stroke="#000000" points="1571.9613,-170.2056 1581.7637,-166.1854 1571.5937,-163.2153 1571.9613,-170.2056"/>
+</g>
+<!-- 14. EnteringMessage&#45;&gt;Initial&#45;&gt;15. EnteringMessage&#45;&gt;EnteringMessage -->
+<g id="edge19" class="edge">
+<title>14. EnteringMessage&#45;&gt;Initial&#45;&gt;15. EnteringMessage&#45;&gt;EnteringMessage</title>
+<path fill="none" stroke="#000000" d="M786.1306,-291.256C734.6097,-279.9465 663.2246,-264.2766 608.1566,-252.1885"/>
+<polygon fill="#000000" stroke="#000000" points="608.5904,-248.7005 598.0725,-249.9749 607.0895,-255.5377 608.5904,-248.7005"/>
+</g>
+<!-- 14. EnteringMessage&#45;&gt;Initial&#45;&gt;18. ExpectingAnswer&#45;&gt;Pinging -->
+<g id="edge79" class="edge">
+<title>14. EnteringMessage&#45;&gt;Initial&#45;&gt;18. ExpectingAnswer&#45;&gt;Pinging</title>
+<path fill="none" stroke="#000000" d="M801.5457,-289.8919C783.6739,-281.568 765.5734,-269.3945 755.2978,-252 747.1598,-238.2242 745.2647,-228.4635 755.2978,-216 772.5326,-194.5902 832.0127,-181.2048 888.2823,-173.1164"/>
+<polygon fill="#000000" stroke="#000000" points="888.9492,-176.5574 898.3733,-171.7161 887.9871,-169.6239 888.9492,-176.5574"/>
+</g>
+<!-- 14. EnteringMessage&#45;&gt;Initial&#45;&gt;19. ExpectingAnswer&#45;&gt;Initial -->
+<g id="edge80" class="edge">
+<title>14. EnteringMessage&#45;&gt;Initial&#45;&gt;19. ExpectingAnswer&#45;&gt;Initial</title>
+<path fill="none" stroke="#000000" d="M739.8915,-302.9157C586.6662,-297.5582 329.2196,-283.8836 300.2978,-252 270.9942,-219.6956 328.0514,-149.9638 337.2978,-144 377.1463,-118.298 1022.4942,-99.721 1300.0236,-92.8826"/>
+<polygon fill="#000000" stroke="#000000" points="1300.2311,-96.3786 1310.1423,-92.6344 1300.0595,-89.3807 1300.2311,-96.3786"/>
+</g>
+<!-- 14. EnteringMessage&#45;&gt;Initial&#45;&gt;16. Initial&#45;&gt;Pinging -->
+<g id="edge77" class="edge">
+<title>14. EnteringMessage&#45;&gt;Initial&#45;&gt;16. Initial&#45;&gt;Pinging</title>
+<path fill="none" stroke="#000000" d="M933.1805,-292.9739C947.8203,-290.9943 962.9917,-289.2112 977.2978,-288 1057.7569,-281.188 2368.2154,-303.632 2430.2978,-252 2447.9676,-237.3045 2451.7753,-210.689 2451.7223,-190.1997"/>
+<polygon fill="#000000" stroke="#000000" points="2455.2184,-190.0202 2451.3956,-180.1391 2448.2221,-190.2474 2455.2184,-190.0202"/>
+</g>
+<!-- 14. EnteringMessage&#45;&gt;Initial&#45;&gt;17. Pinging&#45;&gt;ExpectingAnswer -->
+<g id="edge78" class="edge">
+<title>14. EnteringMessage&#45;&gt;Initial&#45;&gt;17. Pinging&#45;&gt;ExpectingAnswer</title>
+<path fill="none" stroke="#000000" d="M867.251,-287.9946C885.062,-266.5407 918.0646,-231.6376 955.2978,-216 1010.4953,-192.8176 1373.3058,-175.0122 1571.8849,-166.8673"/>
+<polygon fill="#000000" stroke="#000000" points="1572.2424,-170.3558 1582.0915,-166.4513 1571.9572,-163.3616 1572.2424,-170.3558"/>
+</g>
+<!-- 15. EnteringMessage&#45;&gt;EnteringMessage&#45;&gt;18. ExpectingAnswer&#45;&gt;Pinging -->
+<g id="edge83" class="edge">
+<title>15. EnteringMessage&#45;&gt;EnteringMessage&#45;&gt;18. ExpectingAnswer&#45;&gt;Pinging</title>
+<path fill="none" stroke="#000000" d="M620.1079,-219.689C703.1318,-207.1571 823.1924,-189.0348 906.5065,-176.4591"/>
+<polygon fill="#000000" stroke="#000000" points="907.114,-179.9071 916.4796,-174.9537 906.0692,-172.9855 907.114,-179.9071"/>
+</g>
+<!-- 15. EnteringMessage&#45;&gt;EnteringMessage&#45;&gt;19. ExpectingAnswer&#45;&gt;Initial -->
+<g id="edge84" class="edge">
+<title>15. EnteringMessage&#45;&gt;EnteringMessage&#45;&gt;19. ExpectingAnswer&#45;&gt;Initial</title>
+<path fill="none" stroke="#000000" d="M579.3815,-217.0452C646.8133,-196.5691 765.9326,-162.5697 870.2978,-144 1018.5608,-117.6196 1191.5624,-103.3605 1304.4962,-96.2324"/>
+<polygon fill="#000000" stroke="#000000" points="1304.7919,-99.7208 1314.5552,-95.6063 1304.357,-92.7344 1304.7919,-99.7208"/>
+</g>
+<!-- 15. EnteringMessage&#45;&gt;EnteringMessage&#45;&gt;16. Initial&#45;&gt;Pinging -->
+<g id="edge81" class="edge">
+<title>15. EnteringMessage&#45;&gt;EnteringMessage&#45;&gt;16. Initial&#45;&gt;Pinging</title>
+<path fill="none" stroke="#000000" d="M671.0791,-227.6907C754.3297,-224.1395 860.6645,-219.6909 955.2978,-216 1487.1574,-195.2563 2125.6352,-173.094 2358.6028,-165.0977"/>
+<polygon fill="#000000" stroke="#000000" points="2358.8482,-168.5914 2368.7222,-164.7505 2358.6081,-161.5956 2358.8482,-168.5914"/>
+</g>
+<!-- 15. EnteringMessage&#45;&gt;EnteringMessage&#45;&gt;17. Pinging&#45;&gt;ExpectingAnswer -->
+<g id="edge82" class="edge">
+<title>15. EnteringMessage&#45;&gt;EnteringMessage&#45;&gt;17. Pinging&#45;&gt;ExpectingAnswer</title>
+<path fill="none" stroke="#000000" d="M662.7903,-225.5821C893.842,-211.4361 1356.3932,-183.1166 1577.7397,-169.5648"/>
+<polygon fill="#000000" stroke="#000000" points="1578.0056,-173.0552 1587.773,-168.9505 1577.5777,-166.0682 1578.0056,-173.0552"/>
+</g>
+<!-- 1. TryingConnect&#45;&gt;H -->
+<g id="node14" class="node">
+<title>1. TryingConnect&#45;&gt;H</title>
+<ellipse fill="none" stroke="#000000" cx="1074.2978" cy="-306" rx="87.9851" ry="18"/>
+<text text-anchor="middle" x="1074.2978" y="-302.3" font-family="Times,serif" font-size="14.00" fill="#000000">1. TryingConnect&#45;&gt;H</text>
+</g>
+<!-- 2. TryingConnect&#45;&gt;Initial -->
+<g id="node15" class="node">
+<title>2. TryingConnect&#45;&gt;Initial</title>
+<ellipse fill="none" stroke="#000000" cx="1067.2978" cy="-234" rx="102.8821" ry="18"/>
+<text text-anchor="middle" x="1067.2978" y="-230.3" font-family="Times,serif" font-size="14.00" fill="#000000">2. TryingConnect&#45;&gt;Initial</text>
+</g>
+<!-- 1. TryingConnect&#45;&gt;H&#45;&gt;2. TryingConnect&#45;&gt;Initial -->
+<g id="edge13" class="edge">
+<title>1. TryingConnect&#45;&gt;H&#45;&gt;2. TryingConnect&#45;&gt;Initial</title>
+<path fill="none" stroke="#000000" d="M1072.5314,-287.8314C1071.7827,-280.131 1070.8925,-270.9743 1070.0605,-262.4166"/>
+<polygon fill="#000000" stroke="#000000" points="1073.5393,-262.0276 1069.0879,-252.4133 1066.5721,-262.7051 1073.5393,-262.0276"/>
+</g>
+<!-- 1. TryingConnect&#45;&gt;H&#45;&gt;18. ExpectingAnswer&#45;&gt;Pinging -->
+<g id="edge27" class="edge">
+<title>1. TryingConnect&#45;&gt;H&#45;&gt;18. ExpectingAnswer&#45;&gt;Pinging</title>
+<path fill="none" stroke="#000000" d="M1009.356,-293.8442C998.6496,-291.8703 987.6652,-289.8634 977.2978,-288 931.3437,-279.7405 800.3517,-287.7318 770.2978,-252 730.6433,-204.8539 807.1491,-182.306 882.7113,-171.581"/>
+<polygon fill="#000000" stroke="#000000" points="883.4321,-175.0155 892.8728,-170.2068 882.4939,-168.0786 883.4321,-175.0155"/>
+</g>
+<!-- 1. TryingConnect&#45;&gt;H&#45;&gt;19. ExpectingAnswer&#45;&gt;Initial -->
+<g id="edge28" class="edge">
+<title>1. TryingConnect&#45;&gt;H&#45;&gt;19. ExpectingAnswer&#45;&gt;Initial</title>
+<path fill="none" stroke="#000000" d="M1012.1248,-293.2315C1000.5868,-291.2128 988.6075,-289.3497 977.2978,-288 903.8221,-279.2312 363.1877,-305.7194 312.2978,-252 301.2941,-240.3845 304.4146,-229.9232 312.2978,-216 342.9421,-161.8763 372.8308,-162.2243 432.2978,-144 513.1461,-119.2232 1051.7931,-100.7438 1300.2106,-93.4336"/>
+<polygon fill="#000000" stroke="#000000" points="1300.4783,-96.9274 1310.3715,-93.1361 1300.2733,-89.9304 1300.4783,-96.9274"/>
+</g>
+<!-- 1. TryingConnect&#45;&gt;H&#45;&gt;16. Initial&#45;&gt;Pinging -->
+<g id="edge25" class="edge">
+<title>1. TryingConnect&#45;&gt;H&#45;&gt;16. Initial&#45;&gt;Pinging</title>
+<path fill="none" stroke="#000000" d="M1155.7845,-299.2424C1204.1472,-295.4423 1266.6853,-290.8943 1322.2978,-288 1385.6325,-284.7038 2419.1655,-297.5466 2463.2978,-252 2479.0898,-235.7019 2472.7756,-209.3921 2464.1779,-189.4182"/>
+<polygon fill="#000000" stroke="#000000" points="2467.2695,-187.767 2459.8607,-180.1934 2460.9295,-190.7342 2467.2695,-187.767"/>
+</g>
+<!-- 1. TryingConnect&#45;&gt;H&#45;&gt;17. Pinging&#45;&gt;ExpectingAnswer -->
+<g id="edge26" class="edge">
+<title>1. TryingConnect&#45;&gt;H&#45;&gt;17. Pinging&#45;&gt;ExpectingAnswer</title>
+<path fill="none" stroke="#000000" d="M1111.3807,-289.4178C1132.0066,-279.5888 1157.7789,-266.2842 1179.2978,-252 1200.0637,-238.2156 1199.386,-225.8125 1222.2978,-216 1283.5606,-189.7627 1454.0047,-175.2705 1574.0604,-168.0648"/>
+<polygon fill="#000000" stroke="#000000" points="1574.2863,-171.5577 1584.0626,-167.4743 1573.8737,-164.5698 1574.2863,-171.5577"/>
+</g>
+<!-- 2. TryingConnect&#45;&gt;Initial&#45;&gt;18. ExpectingAnswer&#45;&gt;Pinging -->
+<g id="edge31" class="edge">
+<title>2. TryingConnect&#45;&gt;Initial&#45;&gt;18. ExpectingAnswer&#45;&gt;Pinging</title>
+<path fill="none" stroke="#000000" d="M1051.2303,-216.2022C1043.4765,-207.6134 1034.0292,-197.1486 1025.511,-187.7131"/>
+<polygon fill="#000000" stroke="#000000" points="1027.9308,-185.1705 1018.6318,-180.0931 1022.735,-189.8612 1027.9308,-185.1705"/>
+</g>
+<!-- 2. TryingConnect&#45;&gt;Initial&#45;&gt;19. ExpectingAnswer&#45;&gt;Initial -->
+<g id="edge32" class="edge">
+<title>2. TryingConnect&#45;&gt;Initial&#45;&gt;19. ExpectingAnswer&#45;&gt;Initial</title>
+<path fill="none" stroke="#000000" d="M1108.3649,-217.4814C1174.0152,-191.0746 1302.4743,-139.4038 1374.0442,-110.616"/>
+<polygon fill="#000000" stroke="#000000" points="1375.3579,-113.8602 1383.3293,-106.8812 1372.7456,-107.3658 1375.3579,-113.8602"/>
+</g>
+<!-- 2. TryingConnect&#45;&gt;Initial&#45;&gt;16. Initial&#45;&gt;Pinging -->
+<g id="edge29" class="edge">
+<title>2. TryingConnect&#45;&gt;Initial&#45;&gt;16. Initial&#45;&gt;Pinging</title>
+<path fill="none" stroke="#000000" d="M1155.2134,-224.6606C1186.7495,-221.5545 1222.5907,-218.3039 1255.2978,-216 1666.5276,-187.0327 2158.5861,-170.5037 2358.3485,-164.5533"/>
+<polygon fill="#000000" stroke="#000000" points="2358.6093,-168.0472 2368.5012,-164.2525 2358.4019,-161.0502 2358.6093,-168.0472"/>
+</g>
+<!-- 2. TryingConnect&#45;&gt;Initial&#45;&gt;17. Pinging&#45;&gt;ExpectingAnswer -->
+<g id="edge30" class="edge">
+<title>2. TryingConnect&#45;&gt;Initial&#45;&gt;17. Pinging&#45;&gt;ExpectingAnswer</title>
+<path fill="none" stroke="#000000" d="M1143.061,-221.7946C1156.7692,-219.7429 1170.9473,-217.7231 1184.2978,-216 1322.16,-198.2061 1481.2897,-182.2755 1586.1847,-172.4078"/>
+<polygon fill="#000000" stroke="#000000" points="1586.5345,-175.8905 1596.164,-171.472 1585.8808,-168.9211 1586.5345,-175.8905"/>
+</g>
+<!-- 18. ExpectingAnswer&#45;&gt;Pinging&#45;&gt;19. ExpectingAnswer&#45;&gt;Initial -->
+<g id="edge20" class="edge">
+<title>18. ExpectingAnswer&#45;&gt;Pinging&#45;&gt;19. ExpectingAnswer&#45;&gt;Initial</title>
+<path fill="none" stroke="#000000" d="M1082.8565,-148.2879C1155.4636,-135.9292 1262.0138,-117.793 1336.9335,-105.0407"/>
+<polygon fill="#000000" stroke="#000000" points="1337.5566,-108.4851 1346.8275,-103.3566 1336.3819,-101.5844 1337.5566,-108.4851"/>
+</g>
+<!-- 20. Receiving&#45;&gt;Receiving -->
+<g id="node21" class="node">
+<title>20. Receiving&#45;&gt;Receiving</title>
+<ellipse fill="none" stroke="#000000" cx="1497.2978" cy="-18" rx="103.9815" ry="18"/>
+<text text-anchor="middle" x="1497.2978" y="-14.3" font-family="Times,serif" font-size="14.00" fill="#000000">20. Receiving&#45;&gt;Receiving</text>
+</g>
+<!-- 18. ExpectingAnswer&#45;&gt;Pinging&#45;&gt;20. Receiving&#45;&gt;Receiving -->
+<g id="edge87" class="edge">
+<title>18. ExpectingAnswer&#45;&gt;Pinging&#45;&gt;20. Receiving&#45;&gt;Receiving</title>
+<path fill="none" stroke="#000000" d="M1054.9302,-145.6567C1114.3817,-127.3004 1214.0888,-96.8291 1300.2978,-72 1343.4674,-59.5667 1392.1519,-46.2155 1430.3224,-35.8994"/>
+<polygon fill="#000000" stroke="#000000" points="1431.5491,-39.1936 1440.292,-33.2093 1429.7255,-32.4353 1431.5491,-39.1936"/>
+</g>
+<!-- 19. ExpectingAnswer&#45;&gt;Initial&#45;&gt;20. Receiving&#45;&gt;Receiving -->
+<g id="edge88" class="edge">
+<title>19. ExpectingAnswer&#45;&gt;Initial&#45;&gt;20. Receiving&#45;&gt;Receiving</title>
+<path fill="none" stroke="#000000" d="M1443.0955,-72.2022C1451.9226,-63.3752 1462.7309,-52.5669 1472.3671,-42.9307"/>
+<polygon fill="#000000" stroke="#000000" points="1474.859,-45.3885 1479.4552,-35.8425 1469.9092,-40.4388 1474.859,-45.3885"/>
+</g>
+<!-- 0. Initial&#45;&gt;TryingConnect -->
+<g id="node18" class="node">
+<title>0. Initial&#45;&gt;TryingConnect</title>
+<ellipse fill="none" stroke="#000000" cx="2114.2978" cy="-234" rx="102.8821" ry="18"/>
+<text text-anchor="middle" x="2114.2978" y="-230.3" font-family="Times,serif" font-size="14.00" fill="#000000">0. Initial&#45;&gt;TryingConnect</text>
+</g>
+<!-- 0. Initial&#45;&gt;TryingConnect&#45;&gt;18. ExpectingAnswer&#45;&gt;Pinging -->
+<g id="edge23" class="edge">
+<title>0. Initial&#45;&gt;TryingConnect&#45;&gt;18. ExpectingAnswer&#45;&gt;Pinging</title>
+<path fill="none" stroke="#000000" d="M2025.417,-224.8081C1994.1103,-221.7512 1958.6621,-218.4942 1926.2978,-216 1642.0268,-194.0922 1307.9424,-176.6124 1129.6505,-167.9465"/>
+<polygon fill="#000000" stroke="#000000" points="1129.6025,-164.4402 1119.4448,-167.4519 1129.2635,-171.432 1129.6025,-164.4402"/>
+</g>
+<!-- 0. Initial&#45;&gt;TryingConnect&#45;&gt;19. ExpectingAnswer&#45;&gt;Initial -->
+<g id="edge24" class="edge">
+<title>0. Initial&#45;&gt;TryingConnect&#45;&gt;19. ExpectingAnswer&#45;&gt;Initial</title>
+<path fill="none" stroke="#000000" d="M2074.6926,-217.3101C2024.535,-196.8604 1935.0242,-162.6407 1855.2978,-144 1750.9978,-119.6138 1629.7222,-105.6505 1542.6067,-98.0592"/>
+<polygon fill="#000000" stroke="#000000" points="1542.685,-94.5532 1532.4228,-97.1872 1542.0877,-101.5276 1542.685,-94.5532"/>
+</g>
+<!-- 0. Initial&#45;&gt;TryingConnect&#45;&gt;16. Initial&#45;&gt;Pinging -->
+<g id="edge21" class="edge">
+<title>0. Initial&#45;&gt;TryingConnect&#45;&gt;16. Initial&#45;&gt;Pinging</title>
+<path fill="none" stroke="#000000" d="M2179.2864,-220.0323C2237.2936,-207.5651 2321.9526,-189.3697 2380.9584,-176.6879"/>
+<polygon fill="#000000" stroke="#000000" points="2381.8901,-180.0676 2390.9314,-174.5444 2380.4192,-173.2239 2381.8901,-180.0676"/>
+</g>
+<!-- 0. Initial&#45;&gt;TryingConnect&#45;&gt;17. Pinging&#45;&gt;ExpectingAnswer -->
+<g id="edge22" class="edge">
+<title>0. Initial&#45;&gt;TryingConnect&#45;&gt;17. Pinging&#45;&gt;ExpectingAnswer</title>
+<path fill="none" stroke="#000000" d="M2041.4123,-221.2936C1971.3804,-209.0846 1865.4176,-190.6117 1790.4037,-177.5342"/>
+<polygon fill="#000000" stroke="#000000" points="1790.9456,-174.076 1780.4931,-175.8064 1789.7433,-180.972 1790.9456,-174.076"/>
+</g>
+<!-- 16. Initial&#45;&gt;Pinging&#45;&gt;20. Receiving&#45;&gt;Receiving -->
+<g id="edge85" class="edge">
+<title>16. Initial&#45;&gt;Pinging&#45;&gt;20. Receiving&#45;&gt;Receiving</title>
+<path fill="none" stroke="#000000" d="M2381.9757,-151.8168C2213.6854,-126.3612 1774.6864,-59.9579 1585.8108,-31.3885"/>
+<polygon fill="#000000" stroke="#000000" points="1586.3266,-27.9268 1575.9156,-29.8918 1585.2796,-34.8481 1586.3266,-27.9268"/>
+</g>
+<!-- 17. Pinging&#45;&gt;ExpectingAnswer&#45;&gt;20. Receiving&#45;&gt;Receiving -->
+<g id="edge86" class="edge">
+<title>17. Pinging&#45;&gt;ExpectingAnswer&#45;&gt;20. Receiving&#45;&gt;Receiving</title>
+<path fill="none" stroke="#000000" d="M1676.2834,-144.3428C1639.6309,-118.4705 1571.2711,-70.2164 1530.4653,-41.4124"/>
+<polygon fill="#000000" stroke="#000000" points="1532.3855,-38.4837 1522.1974,-35.5762 1528.3487,-44.2025 1532.3855,-38.4837"/>
+</g>
+</g>
+</svg>

文件差异内容过多而无法显示
+ 295 - 303
examples/digitalwatch/model_digitalwatch.svg


文件差异内容过多而无法显示
+ 1477 - 0
examples/digitalwatch/model_digitalwatch_priorities.svg


+ 150 - 0
examples/stove/statechart_stove.svg

@@ -0,0 +1,150 @@
+<?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="632pt" height="823pt"
+ viewBox="0.00 0.00 632.00 823.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 819)">
+<title>state transitions</title>
+<polygon fill="#ffffff" stroke="transparent" points="-4,4 -4,-819 628,-819 628,4 -4,4"/>
+<g id="clust1" class="cluster">
+<title>cluster__p</title>
+<path fill="none" stroke="#000000" stroke-width="2" d="M20,-8C20,-8 604,-8 604,-8 610,-8 616,-14 616,-20 616,-20 616,-764 616,-764 616,-770 610,-776 604,-776 604,-776 20,-776 20,-776 14,-776 8,-770 8,-764 8,-764 8,-20 8,-20 8,-14 14,-8 20,-8"/>
+<text text-anchor="start" x="308.6646" y="-757.2" font-family="Helvetica,sans-Serif" font-size="12.00" fill="#000000">p</text>
+</g>
+<g id="clust2" class="cluster">
+<title>cluster__p_burner_select</title>
+<polygon fill="none" stroke="#000000" stroke-dasharray="5,2" points="291,-563 291,-738 608,-738 608,-563 291,-563"/>
+<text text-anchor="start" x="413.1586" y="-719.2" font-family="Helvetica,sans-Serif" font-size="12.00" fill="#000000">burner_select</text>
+</g>
+<g id="clust3" class="cluster">
+<title>cluster__p_heat</title>
+<polygon fill="none" stroke="#000000" stroke-dasharray="5,2" points="24,-16 24,-738 283,-738 283,-16 24,-16"/>
+<text text-anchor="start" x="142.3264" y="-719.2" font-family="Helvetica,sans-Serif" font-size="12.00" fill="#000000">heat</text>
+</g>
+<g id="clust4" class="cluster">
+<title>cluster__p_heat_Pushed</title>
+<path fill="none" stroke="#000000" stroke-width="2" d="M52,-24C52,-24 255,-24 255,-24 261,-24 267,-30 267,-36 267,-36 267,-469 267,-469 267,-475 261,-481 255,-481 255,-481 52,-481 52,-481 46,-481 40,-475 40,-469 40,-469 40,-36 40,-36 40,-30 46,-24 52,-24"/>
+<text text-anchor="start" x="133.657" y="-462.2" font-family="Helvetica,sans-Serif" font-size="12.00" fill="#000000">Pushed</text>
+<text text-anchor="start" x="110.329" y="-442.2" font-family="Helvetica,sans-Serif" font-size="12.00" fill="#000000">enter /increase()</text>
+<polygon fill="#000000" stroke="#000000" points="106.5,-456 106.5,-456 201.5,-456 201.5,-456 106.5,-456"/>
+</g>
+<!-- __initial -->
+<g id="node1" class="node">
+<title>__initial</title>
+<ellipse fill="#000000" stroke="#000000" stroke-width="2" cx="16" cy="-809.5" rx="5.5" ry="5.5"/>
+</g>
+<!-- _p -->
+<!-- __initial&#45;&gt;_p -->
+<g id="edge1" class="edge">
+<title>__initial&#45;&gt;_p</title>
+<path fill="none" stroke="#000000" d="M16,-803.9533C16,-799.7779 16,-793.5043 16,-786.0332"/>
+<polygon fill="#000000" stroke="#000000" points="19.5001,-785.9971 16,-775.9971 12.5001,-785.9972 19.5001,-785.9971"/>
+<text text-anchor="middle" x="17.3895" y="-787" font-family="Helvetica,sans-Serif" font-size="10.00" fill="#000000"> </text>
+</g>
+<!-- _p_burner_select -->
+<!-- _p_burner_select_initial -->
+<g id="node4" class="node">
+<title>_p_burner_select_initial</title>
+<ellipse fill="#000000" stroke="#000000" stroke-width="2" cx="345" cy="-694.5" rx="5.5" ry="5.5"/>
+</g>
+<!-- _p_burner_select_BurnerSelect -->
+<g id="node5" class="node">
+<title>_p_burner_select_BurnerSelect</title>
+<polygon fill="transparent" stroke="transparent" stroke-width="2" points="390.5,-607 299.5,-607 299.5,-571 390.5,-571 390.5,-607"/>
+<text text-anchor="start" x="310.8266" y="-585.2" font-family="Helvetica,sans-Serif" font-size="12.00" fill="#000000">BurnerSelect</text>
+<path fill="none" stroke="#000000" stroke-width="2" d="M311.8333,-572C311.8333,-572 378.1667,-572 378.1667,-572 383.8333,-572 389.5,-577.6667 389.5,-583.3333 389.5,-583.3333 389.5,-594.6667 389.5,-594.6667 389.5,-600.3333 383.8333,-606 378.1667,-606 378.1667,-606 311.8333,-606 311.8333,-606 306.1667,-606 300.5,-600.3333 300.5,-594.6667 300.5,-594.6667 300.5,-583.3333 300.5,-583.3333 300.5,-577.6667 306.1667,-572 311.8333,-572"/>
+</g>
+<!-- _p_burner_select_initial&#45;&gt;_p_burner_select_BurnerSelect -->
+<g id="edge2" class="edge">
+<title>_p_burner_select_initial&#45;&gt;_p_burner_select_BurnerSelect</title>
+<path fill="none" stroke="#000000" d="M345,-688.8288C345,-684.1736 345,-677.4097 345,-671.5 345,-671.5 345,-671.5 345,-624.5 345,-622.1079 345,-619.6252 345,-617.1342"/>
+<polygon fill="#000000" stroke="#000000" points="348.5001,-617.0597 345,-607.0598 341.5001,-617.0598 348.5001,-617.0597"/>
+<text text-anchor="middle" x="346.3895" y="-645" font-family="Helvetica,sans-Serif" font-size="10.00" fill="#000000"> </text>
+</g>
+<!-- _p_burner_select_BurnerSelect&#45;&gt;_p_burner_select_BurnerSelect -->
+<g id="edge3" class="edge">
+<title>_p_burner_select_BurnerSelect&#45;&gt;_p_burner_select_BurnerSelect</title>
+<path fill="none" stroke="#000000" d="M390.7453,-593.839C403.1005,-593.5837 412.5,-591.9707 412.5,-589 412.5,-586.9112 407.853,-585.4937 400.7991,-584.7474"/>
+<polygon fill="#000000" stroke="#000000" points="400.9322,-581.2493 390.7453,-584.161 400.5245,-588.2374 400.9322,-581.2493"/>
+<text text-anchor="start" x="412.5" y="-586" font-family="Helvetica,sans-Serif" font-size="10.00" fill="#000000">select_next/selected = (selected + 1) % 4 &#160;&#160;</text>
+</g>
+<!-- _p_heat -->
+<!-- _p_heat_initial -->
+<g id="node7" class="node">
+<title>_p_heat_initial</title>
+<ellipse fill="#000000" stroke="#000000" stroke-width="2" cx="113" cy="-694.5" rx="5.5" ry="5.5"/>
+</g>
+<!-- _p_heat_Released -->
+<g id="node8" class="node">
+<title>_p_heat_Released</title>
+<polygon fill="transparent" stroke="transparent" stroke-width="2" points="149,-607 77,-607 77,-571 149,-571 149,-607"/>
+<text text-anchor="start" x="87.6602" y="-585.2" font-family="Helvetica,sans-Serif" font-size="12.00" fill="#000000">Released</text>
+<path fill="none" stroke="#000000" stroke-width="2" d="M89.3333,-572C89.3333,-572 136.6667,-572 136.6667,-572 142.3333,-572 148,-577.6667 148,-583.3333 148,-583.3333 148,-594.6667 148,-594.6667 148,-600.3333 142.3333,-606 136.6667,-606 136.6667,-606 89.3333,-606 89.3333,-606 83.6667,-606 78,-600.3333 78,-594.6667 78,-594.6667 78,-583.3333 78,-583.3333 78,-577.6667 83.6667,-572 89.3333,-572"/>
+</g>
+<!-- _p_heat_initial&#45;&gt;_p_heat_Released -->
+<g id="edge4" class="edge">
+<title>_p_heat_initial&#45;&gt;_p_heat_Released</title>
+<path fill="none" stroke="#000000" d="M113,-688.8288C113,-684.1736 113,-677.4097 113,-671.5 113,-671.5 113,-671.5 113,-624.5 113,-622.1079 113,-619.6252 113,-617.1342"/>
+<polygon fill="#000000" stroke="#000000" points="116.5001,-617.0597 113,-607.0598 109.5001,-617.0598 116.5001,-617.0597"/>
+<text text-anchor="middle" x="114.3895" y="-645" font-family="Helvetica,sans-Serif" font-size="10.00" fill="#000000"> </text>
+</g>
+<!-- _p_heat_Pushed -->
+<!-- _p_heat_Released&#45;&gt;_p_heat_Pushed -->
+<g id="edge9" class="edge">
+<title>_p_heat_Released&#45;&gt;_p_heat_Pushed</title>
+<path fill="none" stroke="#000000" d="M76.9799,-576.1642C64.6961,-569.3166 54,-559.3715 54,-545.5 54,-545.5 54,-545.5 54,-498.5 54,-478.4508 76.5664,-490.0574 94.925,-485.2591"/>
+<polygon fill="#000000" stroke="#000000" points="96.4344,-488.4171 104,-481 93.4604,-482.0802 96.4344,-488.4171"/>
+<text text-anchor="start" x="54" y="-519" font-family="Helvetica,sans-Serif" font-size="10.00" fill="#000000">pressed_increase &#160;&#160;</text>
+</g>
+<!-- _p_heat_Pushed&#45;&gt;_p_heat_Released -->
+<g id="edge8" class="edge">
+<title>_p_heat_Pushed&#45;&gt;_p_heat_Released</title>
+<path fill="none" stroke="#000000" d="M182.9122,-480.9974C184.2276,-486.7913 185,-492.674 185,-498.5 185,-545.5 185,-545.5 185,-545.5 185,-560.7147 173.0761,-570.7501 158.9332,-577.302"/>
+<polygon fill="#000000" stroke="#000000" points="157.3958,-574.1477 149.4219,-581.1239 160.0058,-580.6429 157.3958,-574.1477"/>
+<text text-anchor="start" x="185" y="-519" font-family="Helvetica,sans-Serif" font-size="10.00" fill="#000000">released_increase &#160;&#160;</text>
+</g>
+<!-- _p_heat_Pushed_initial -->
+<g id="node10" class="node">
+<title>_p_heat_Pushed_initial</title>
+<ellipse fill="#000000" stroke="#000000" stroke-width="2" cx="87" cy="-417.5" rx="5.5" ry="5.5"/>
+</g>
+<!-- _p_heat_Pushed_Waiting -->
+<g id="node12" class="node">
+<title>_p_heat_Pushed_Waiting</title>
+<polygon fill="transparent" stroke="transparent" stroke-width="2" points="117.5,-258 56.5,-258 56.5,-222 117.5,-222 117.5,-258"/>
+<text text-anchor="start" x="67.5002" y="-236.2" font-family="Helvetica,sans-Serif" font-size="12.00" fill="#000000">Waiting</text>
+<path fill="none" stroke="#000000" stroke-width="2" d="M68.8333,-223C68.8333,-223 105.1667,-223 105.1667,-223 110.8333,-223 116.5,-228.6667 116.5,-234.3333 116.5,-234.3333 116.5,-245.6667 116.5,-245.6667 116.5,-251.3333 110.8333,-257 105.1667,-257 105.1667,-257 68.8333,-257 68.8333,-257 63.1667,-257 57.5,-251.3333 57.5,-245.6667 57.5,-245.6667 57.5,-234.3333 57.5,-234.3333 57.5,-228.6667 63.1667,-223 68.8333,-223"/>
+</g>
+<!-- _p_heat_Pushed_initial&#45;&gt;_p_heat_Pushed_Waiting -->
+<g id="edge5" class="edge">
+<title>_p_heat_Pushed_initial&#45;&gt;_p_heat_Pushed_Waiting</title>
+<path fill="none" stroke="#000000" d="M87,-411.8288C87,-407.1736 87,-400.4097 87,-394.5 87,-394.5 87,-394.5 87,-275.5 87,-273.1079 87,-270.6252 87,-268.1342"/>
+<polygon fill="#000000" stroke="#000000" points="90.5001,-268.0597 87,-258.0598 83.5001,-268.0598 90.5001,-268.0597"/>
+<text text-anchor="middle" x="88.3895" y="-332" font-family="Helvetica,sans-Serif" font-size="10.00" fill="#000000"> </text>
+</g>
+<!-- _p_heat_Pushed_Increasing -->
+<g id="node11" class="node">
+<title>_p_heat_Pushed_Increasing</title>
+<polygon fill="transparent" stroke="transparent" stroke-width="2" points="125.5,-68 48.5,-68 48.5,-32 125.5,-32 125.5,-68"/>
+<text text-anchor="start" x="59.8268" y="-46.2" font-family="Helvetica,sans-Serif" font-size="12.00" fill="#000000">Increasing</text>
+<path fill="none" stroke="#000000" stroke-width="2" d="M60.8333,-33C60.8333,-33 113.1667,-33 113.1667,-33 118.8333,-33 124.5,-38.6667 124.5,-44.3333 124.5,-44.3333 124.5,-55.6667 124.5,-55.6667 124.5,-61.3333 118.8333,-67 113.1667,-67 113.1667,-67 60.8333,-67 60.8333,-67 55.1667,-67 49.5,-61.3333 49.5,-55.6667 49.5,-55.6667 49.5,-44.3333 49.5,-44.3333 49.5,-38.6667 55.1667,-33 60.8333,-33"/>
+</g>
+<!-- _p_heat_Pushed_Increasing&#45;&gt;_p_heat_Pushed_Increasing -->
+<g id="edge6" class="edge">
+<title>_p_heat_Pushed_Increasing&#45;&gt;_p_heat_Pushed_Increasing</title>
+<path fill="none" stroke="#000000" d="M125.6945,-54.8723C137.8838,-54.7979 147.5,-53.1738 147.5,-50 147.5,-47.7684 142.7459,-46.303 135.686,-45.6037"/>
+<polygon fill="#000000" stroke="#000000" points="135.8497,-42.1076 125.6945,-45.1277 135.5166,-49.0997 135.8497,-42.1076"/>
+<text text-anchor="start" x="147.5" y="-47" font-family="Helvetica,sans-Serif" font-size="10.00" fill="#000000">after(200 ms)/increase() &#160;&#160;</text>
+</g>
+<!-- _p_heat_Pushed_Waiting&#45;&gt;_p_heat_Pushed_Increasing -->
+<g id="edge7" class="edge">
+<title>_p_heat_Pushed_Waiting&#45;&gt;_p_heat_Pushed_Increasing</title>
+<path fill="none" stroke="#000000" d="M87,-221.9402C87,-216.3497 87,-210.1701 87,-204.5 87,-204.5 87,-204.5 87,-85.5 87,-83.1079 87,-80.6252 87,-78.1342"/>
+<polygon fill="#000000" stroke="#000000" points="90.5001,-78.0597 87,-68.0598 83.5001,-78.0598 90.5001,-78.0597"/>
+<text text-anchor="start" x="87" y="-142" font-family="Helvetica,sans-Serif" font-size="10.00" fill="#000000">after(1 s) &#160;&#160;</text>
+</g>
+</g>
+</svg>

+ 79 - 0
examples/stove/statechart_stove_priorities.svg

@@ -0,0 +1,79 @@
+<?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: priorities Pages: 1 -->
+<svg width="642pt" height="188pt"
+ viewBox="0.00 0.00 641.73 188.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 184)">
+<title>priorities</title>
+<polygon fill="#ffffff" stroke="transparent" points="-4,4 -4,-184 637.7341,-184 637.7341,4 -4,4"/>
+<!-- 1. Pushed&#45;&gt;Released -->
+<g id="node1" class="node">
+<title>1. Pushed&#45;&gt;Released</title>
+<ellipse fill="none" stroke="#000000" cx="306.5917" cy="-162" rx="85.2851" ry="18"/>
+<text text-anchor="middle" x="306.5917" y="-158.3" font-family="Times,serif" font-size="14.00" fill="#000000">1. Pushed&#45;&gt;Released</text>
+</g>
+<!-- 2. Waiting&#45;&gt;Increasing -->
+<g id="node2" class="node">
+<title>2. Waiting&#45;&gt;Increasing</title>
+<ellipse fill="none" stroke="#000000" cx="93.5917" cy="-90" rx="93.6835" ry="18"/>
+<text text-anchor="middle" x="93.5917" y="-86.3" font-family="Times,serif" font-size="14.00" fill="#000000">2. Waiting&#45;&gt;Increasing</text>
+</g>
+<!-- 1. Pushed&#45;&gt;Released&#45;&gt;2. Waiting&#45;&gt;Increasing -->
+<g id="edge1" class="edge">
+<title>1. Pushed&#45;&gt;Released&#45;&gt;2. Waiting&#45;&gt;Increasing</title>
+<path fill="none" stroke="#000000" d="M261.4199,-146.7307C228.8259,-135.713 184.6064,-120.7655 149.7396,-108.9796"/>
+<polygon fill="#000000" stroke="#000000" points="150.7651,-105.6317 140.1709,-105.7451 148.5235,-112.2631 150.7651,-105.6317"/>
+</g>
+<!-- 3. Increasing&#45;&gt;Increasing -->
+<g id="node3" class="node">
+<title>3. Increasing&#45;&gt;Increasing</title>
+<ellipse fill="none" stroke="#000000" cx="306.5917" cy="-90" rx="101.2821" ry="18"/>
+<text text-anchor="middle" x="306.5917" y="-86.3" font-family="Times,serif" font-size="14.00" fill="#000000">3. Increasing&#45;&gt;Increasing</text>
+</g>
+<!-- 1. Pushed&#45;&gt;Released&#45;&gt;3. Increasing&#45;&gt;Increasing -->
+<g id="edge2" class="edge">
+<title>1. Pushed&#45;&gt;Released&#45;&gt;3. Increasing&#45;&gt;Increasing</title>
+<path fill="none" stroke="#000000" d="M306.5917,-143.8314C306.5917,-136.131 306.5917,-126.9743 306.5917,-118.4166"/>
+<polygon fill="#000000" stroke="#000000" points="310.0918,-118.4132 306.5917,-108.4133 303.0918,-118.4133 310.0918,-118.4132"/>
+</g>
+<!-- 4. BurnerSelect&#45;&gt;BurnerSelect -->
+<g id="node5" class="node">
+<title>4. BurnerSelect&#45;&gt;BurnerSelect</title>
+<ellipse fill="none" stroke="#000000" cx="370.5917" cy="-18" rx="120.4791" ry="18"/>
+<text text-anchor="middle" x="370.5917" y="-14.3" font-family="Times,serif" font-size="14.00" fill="#000000">4. BurnerSelect&#45;&gt;BurnerSelect</text>
+</g>
+<!-- 1. Pushed&#45;&gt;Released&#45;&gt;4. BurnerSelect&#45;&gt;BurnerSelect -->
+<g id="edge4" class="edge">
+<title>1. Pushed&#45;&gt;Released&#45;&gt;4. BurnerSelect&#45;&gt;BurnerSelect</title>
+<path fill="none" stroke="#000000" d="M362.1942,-148.2763C382.965,-140.1583 404.4411,-127.5005 416.5917,-108 429.6645,-87.0193 414.4198,-61.8757 398.0646,-43.5042"/>
+<polygon fill="#000000" stroke="#000000" points="400.4717,-40.9551 391.0666,-36.0772 395.377,-45.7556 400.4717,-40.9551"/>
+</g>
+<!-- 2. Waiting&#45;&gt;Increasing&#45;&gt;4. BurnerSelect&#45;&gt;BurnerSelect -->
+<g id="edge5" class="edge">
+<title>2. Waiting&#45;&gt;Increasing&#45;&gt;4. BurnerSelect&#45;&gt;BurnerSelect</title>
+<path fill="none" stroke="#000000" d="M149.3136,-75.5163C192.8244,-64.2067 253.5516,-48.422 300.3838,-36.249"/>
+<polygon fill="#000000" stroke="#000000" points="301.3573,-39.6123 310.1552,-33.7091 299.5963,-32.8374 301.3573,-39.6123"/>
+</g>
+<!-- 3. Increasing&#45;&gt;Increasing&#45;&gt;4. BurnerSelect&#45;&gt;BurnerSelect -->
+<g id="edge6" class="edge">
+<title>3. Increasing&#45;&gt;Increasing&#45;&gt;4. BurnerSelect&#45;&gt;BurnerSelect</title>
+<path fill="none" stroke="#000000" d="M322.4119,-72.2022C330.0465,-63.6134 339.3485,-53.1486 347.7356,-43.7131"/>
+<polygon fill="#000000" stroke="#000000" points="350.4812,-45.8925 354.5089,-36.0931 345.2493,-41.242 350.4812,-45.8925"/>
+</g>
+<!-- 0. Released&#45;&gt;Pushed -->
+<g id="node4" class="node">
+<title>0. Released&#45;&gt;Pushed</title>
+<ellipse fill="none" stroke="#000000" cx="548.5917" cy="-90" rx="85.2851" ry="18"/>
+<text text-anchor="middle" x="548.5917" y="-86.3" font-family="Times,serif" font-size="14.00" fill="#000000">0. Released&#45;&gt;Pushed</text>
+</g>
+<!-- 0. Released&#45;&gt;Pushed&#45;&gt;4. BurnerSelect&#45;&gt;BurnerSelect -->
+<g id="edge3" class="edge">
+<title>0. Released&#45;&gt;Pushed&#45;&gt;4. BurnerSelect&#45;&gt;BurnerSelect</title>
+<path fill="none" stroke="#000000" d="M509.0877,-74.0209C483.4341,-63.6441 449.7359,-50.0134 422.0031,-38.7956"/>
+<polygon fill="#000000" stroke="#000000" points="423.0482,-35.4429 412.4654,-34.9377 420.4233,-41.9321 423.0482,-35.4429"/>
+</g>
+</g>
+</svg>

+ 7 - 19
src/sccd/render.py

@@ -6,13 +6,11 @@ import os
 from sccd.util.os_tools import *
 from sccd.util.indenting_writer import *
 from sccd.statechart.parser.xml import *
-import lxml.etree as ET
 
 if __name__ == '__main__':
     parser = argparse.ArgumentParser(
         description="Render statecharts as SVG images.")
     parser.add_argument('path', metavar='PATH', type=str, nargs='*', help="Models to render. Can be a XML file or a directory. If a directory, it will be recursively scanned for XML files.")
-    parser.add_argument('--build-dir', metavar='DIR', type=str, default='build', help="As a first step, input XML files first must be compiled to python files. Directory to store these files. Defaults to 'build'")
     parser.add_argument('--output-dir', metavar='DIR', type=str, default='.', help="Directory for SVG rendered output. Defaults to '.' (putting the SVG files with the XML source files)")
     parser.add_argument('--keep-smcat', action='store_true', help="Whether to NOT delete intermediary SMCAT files after producing SVG output. Default = off (delete files)")
     parser.add_argument('--no-svg', action='store_true', help="Don't produce SVG output. This option only makes sense in combination with the --keep-smcat option. Default = off")
@@ -87,9 +85,9 @@ if __name__ == '__main__':
             self.opt = PseudoState.Opt(name)
         # Used for drawing initial state
         class PseudoTransition:
-          def __init__(self, source, targets):
+          def __init__(self, source, target):
             self.source = source
-            self.targets = targets
+            self.target = target
             self.guard = None
             self.trigger = None
             self.actions = []
@@ -124,7 +122,7 @@ if __name__ == '__main__':
               w.indent()
             if s.default_state:
               w.write(name_to_name(s.opt.full_name)+'_initial [type=initial],')
-              transitions.append(PseudoTransition(source=PseudoState(s.opt.full_name+'/initial'), targets=[s.default_state]))
+              transitions.append(PseudoTransition(source=PseudoState(s.opt.full_name+'/initial'), target=s.default_state))
             s.children.reverse() # this appears to put orthogonal components in the right order :)
             for i, c in enumerate(s.children):
               write_state(c)
@@ -146,20 +144,10 @@ if __name__ == '__main__':
           if t.actions:
             label += ' '.join(a.render() for a in t.actions)
 
-          if len(t.targets) == 1:
-            w.write(name_to_name(t.source.opt.full_name) + ' -> ' + name_to_name(t.targets[0].opt.full_name))
-            if label:
-              w.extendWrite(': '+label)
-            w.extendWrite(';')
-          else:
-            w.write(name_to_name(t.source.opt.full_name) + ' -> ' + ']split'+str(ctr))
-            if label:
-                w.extendWrite(': '+label)
-            w.extendWrite(';')
-            for tt in t.targets:
-              w.write(']split'+str(ctr) + ' -> ' + name_to_name(tt.opt.full_name))
-              w.extendWrite(';')
-            ctr += 1
+          w.write(name_to_name(t.source.opt.full_name) + ' -> ' + name_to_name(t.target.opt.full_name))
+          if label:
+            w.extendWrite(': '+label)
+          w.extendWrite(';')
 
         f.close()
         if args.keep_smcat:

+ 78 - 0
src/sccd/statechart/cmd/render_priorities.py

@@ -0,0 +1,78 @@
+import argparse
+import sys
+import subprocess
+import os
+from sccd.util.os_tools import *
+from sccd.util.indenting_writer import *
+from sccd.statechart.parser.xml import *
+from sccd.statechart.static import priority
+
+if __name__ == '__main__':
+    parser = argparse.ArgumentParser(
+        description="Render the priorities between transitions in a statechart as a graph.")
+    parser.add_argument('path', metavar='PATH', type=str, nargs='*', help="Models to render. Can be a XML file or a directory. If a directory, it will be recursively scanned for XML files.")
+    args = parser.parse_args()
+
+    srcs = get_files(args.path,
+      filter=lambda file: (file.startswith("statechart_") or file.startswith("test_") or file.startswith("model_")) and file.endswith(".xml"))
+
+    if len(srcs) == 0:
+      print("No input files specified.")
+      print()
+      parser.print_usage()
+      exit()
+
+    try:
+        subprocess.run(["dot", "-?"], capture_output=True)
+    except:
+        print("Could not run command 'dot'. Make sure GraphViz dot is installed.")
+
+    for src in srcs:
+        path = os.path.dirname(src)
+        parse_sc = statechart_parser_rules(Globals(), path, load_external=False)
+
+        def find_statechart(el):
+          def when_done(statechart):
+            return statechart
+          # When parsing <test>, only look for <statechart> node in it.
+          # All other nodes will be ignored.
+          return ({"statechart": parse_sc}, when_done)
+
+        statechart = parse_f(src, {
+          "test": find_statechart,
+          "single_instance_cd": find_statechart,
+          "statechart": parse_sc,
+        }, ignore_unmatched=True)
+
+        assert isinstance(statechart, Statechart)
+
+        if statechart.semantics.has_multiple_variants():
+          print("Skipping statechart from " + src + ". Statechart has multiple semantic variants.")
+          continue
+
+        tree = statechart.tree
+
+        dot_target = dropext(src)+'_priorities.dot'
+        svg_target = dropext(src)+'_priorities.svg'
+
+        with open(dot_target, 'w') as f:
+            w = IndentingWriter(f)
+            w.write("digraph priorities {")
+            w.indent()
+
+            graph = priority.get_graph(tree, statechart.semantics)
+
+            print("Priority graph has", len(graph), "edges")
+
+            def label(t):
+                return '"'+str(tree.transition_list.index(t)) + ". " + t.source.short_name + "->" + t.target.short_name+'"'
+
+            for high, low in graph:
+                w.write(label(high) + " -> " + label(low) + ";")
+
+            w.dedent()
+            w.write("}")
+
+        subprocess.run(["dot", "-Tsvg", dot_target, "-o", svg_target])
+        print("Wrote", svg_target)
+        os.remove(dot_target)

+ 175 - 0
src/sccd/statechart/dynamic/candidate_generator.py

@@ -0,0 +1,175 @@
+from typing import *
+from dataclasses import *
+from abc import *
+from sccd.util import timer
+from sccd.util.bitmap import *
+from sccd.statechart.static.tree import *
+from sccd.statechart.dynamic.event import *
+
+@dataclass
+class CacheCounter:
+    __slots__ = ["cache_hits", "cache_misses"]
+    cache_hits: int
+    cache_misses: int
+
+ctr = CacheCounter(0, 0)
+
+if timer.TIMINGS:
+    import atexit
+    def print_stats():
+        print("\ncache hits: %s, cache misses: %s" %(ctr.cache_hits, ctr.cache_misses))
+    atexit.register(print_stats)
+
+
+class GeneratorStrategy(ABC):
+    __slots__ = ["priority_ordered_transitions"]
+    def __init__(self, priority_ordered_transitions):
+        self.priority_ordered_transitions = priority_ordered_transitions
+
+    @abstractmethod
+    def cache_init(self):
+        pass
+
+    @abstractmethod
+    def key(self, execution, events_bitmap, forbidden_arenas):
+        pass
+
+    @abstractmethod
+    def generate(self, execution, events_bitmap, forbidden_arenas):
+        pass
+
+    @abstractmethod
+    def filter_f(self, execution, enabled_events, events_bitmap):
+        pass
+
+
+# First filter on current state, then filter on current events
+class CurrentConfigStrategy(GeneratorStrategy):
+    __slots__ = []
+    def cache_init(self):
+        return {}
+
+    def key(self, execution, events_bitmap, forbidden_arenas):
+        return (execution.configuration, forbidden_arenas)
+
+    def generate(self, execution, events_bitmap, forbidden_arenas):
+        return [ t for t in self.priority_ordered_transitions
+                      if (t.source.opt.state_id_bitmap & execution.configuration)
+                       and (not forbidden_arenas & t.opt.arena_bitmap) ]
+
+    def filter_f(self, execution, enabled_events, events_bitmap):
+        return lambda t: (not t.trigger or t.trigger.check(events_bitmap)) and execution.check_guard(t, enabled_events)
+
+# First filter based on current events, then filter on current state
+class EnabledEventsStrategy(GeneratorStrategy):
+    __slots__ = ["statechart"]
+    def __init__(self, priority_ordered_transitions, statechart):
+        super().__init__(priority_ordered_transitions)
+        self.statechart = statechart
+
+    def cache_init(self):
+        cache = {}
+        cache[(0, 0)] = self.generate(None, 0, 0)
+        for event_id in bm_items(self.statechart.internal_events):
+            events_bitmap = bit(event_id)
+            cache[(events_bitmap, 0)] = self.generate(None, events_bitmap, 0)
+        return cache
+
+    def key(self, execution, events_bitmap, forbidden_arenas):
+        return (events_bitmap, forbidden_arenas)
+
+    def generate(self, execution, events_bitmap, forbidden_arenas):
+        return [ t for t in self.priority_ordered_transitions
+                      if (not t.trigger or t.trigger.check(events_bitmap))
+                      and (not forbidden_arenas & t.opt.arena_bitmap) ]
+
+    def filter_f(self, execution, enabled_events, events_bitmap):
+        return lambda t: (execution.configuration & t.source.opt.state_id_bitmap) and execution.check_guard(t, enabled_events)
+
+class CurrentConfigAndEnabledEventsStrategy(GeneratorStrategy):
+    __slots__ = ["statechart"]
+    def __init__(self, priority_ordered_transitions, statechart):
+        super().__init__(priority_ordered_transitions)
+        self.statechart = statechart
+
+    def cache_init(self):
+        return {}
+
+    def key(self, execution, events_bitmap, forbidden_arenas):
+        return (execution.configuration, events_bitmap, forbidden_arenas)
+
+    def generate(self, execution, events_bitmap, forbidden_arenas):
+        return [ t for t in self.priority_ordered_transitions
+                      if (not t.trigger or t.trigger.check(events_bitmap))
+                      and (t.source.opt.state_id_bitmap & execution.configuration)
+                      and (not forbidden_arenas & t.opt.arena_bitmap) ]
+
+    def filter_f(self, execution, enabled_events, events_bitmap):
+        return lambda t: execution.check_guard(t, enabled_events)
+
+
+class CandidateGenerator:
+    __slots__ = ["strategy", "cache"]
+    def __init__(self, strategy):
+        self.strategy = strategy
+        self.cache = strategy.cache_init()
+
+    def generate(self, execution, enabled_events: List[InternalEvent], forbidden_arenas: Bitmap) -> List[Transition]:
+        with timer.Context("generate candidates"):
+            events_bitmap = bm_from_list(e.id for e in enabled_events)
+            key = self.strategy.key(execution, events_bitmap, forbidden_arenas)
+
+            try:
+                candidates = self.cache[key]
+                ctr.cache_hits += 1
+            except KeyError:
+                candidates = self.cache[key] = self.strategy.generate(execution, events_bitmap, forbidden_arenas)
+                ctr.cache_misses += 1
+
+            candidates = filter(self.strategy.filter_f(execution, enabled_events, events_bitmap), candidates)
+
+            if DEBUG:
+                candidates = list(candidates) # convert generator to list (gotta do this, otherwise the generator will be all used up by our debug printing
+                if candidates:
+                    print()
+                    if enabled_events:
+                        print("events: " + str(enabled_events))
+                    print("candidates: " + ",  ".join(str(t) for t in candidates))
+                candidates = iter(candidates)
+
+            t = next(candidates, None)
+            if t:
+                return [t]
+            else:
+                return []
+
+
+class ConcurrentCandidateGenerator:
+    __slots__ = ["strategy", "cache", "synchronous"]
+    def __init__(self, strategy, synchronous):
+        self.strategy = strategy
+        self.cache = strategy.cache_init()
+        self.synchronous = synchronous
+
+    def generate(self, execution, enabled_events: List[InternalEvent], forbidden_arenas: Bitmap) -> List[Transition]:
+        with timer.Context("generate candidates"):
+            events_bitmap = bm_from_list(e.id for e in enabled_events)
+            transitions = []
+            while True:
+                key = self.strategy.key(execution, events_bitmap, forbidden_arenas)
+                try:
+                    candidates = self.cache[key]
+                    ctr.cache_hits += 1
+                except KeyError:
+                    candidates = self.cache[key] = self.strategy.generate(execution, events_bitmap, forbidden_arenas)
+                    ctr.cache_misses += 1
+                candidates = filter(self.strategy.filter_f(execution, enabled_events, events_bitmap), candidates)
+                t = next(candidates, None)
+                if t:
+                    transitions.append(t)
+                else:
+                    break
+                if self.synchronous:
+                    events_bitmap |= t.opt.raised_events
+                forbidden_arenas |= t.opt.arena_bitmap
+            return transitions

+ 7 - 207
src/sccd/statechart/dynamic/round.py

@@ -1,180 +1,9 @@
 from typing import *
-from sccd.statechart.static.statechart import Statechart
-from sccd.statechart.dynamic.event import *
-from sccd.util.bitmap import *
-from sccd.statechart.static.tree import *
+from sccd.statechart.dynamic.candidate_generator import *
 from sccd.util.debug import *
 from sccd.common.exceptions import *
 from sccd.util import timer
 
-@dataclass
-class CacheCounter:
-    __slots__ = ["cache_hits", "cache_misses"]
-    cache_hits: int
-    cache_misses: int
-
-ctr = CacheCounter(0, 0)
-
-if timer.TIMINGS:
-    import atexit
-    def print_stats():
-        print("\ncache hits: %s, cache misses: %s" %(ctr.cache_hits, ctr.cache_misses))
-    atexit.register(print_stats)
-
-
-class GeneratorStrategy(ABC):
-    __slots__ = ["priority_ordered_transitions"]
-    def __init__(self, priority_ordered_transitions):
-        self.priority_ordered_transitions = priority_ordered_transitions
-
-    @abstractmethod
-    def cache_init(self):
-        pass
-
-    @abstractmethod
-    def key(self, execution, events_bitmap, forbidden_arenas):
-        pass
-
-    @abstractmethod
-    def generate(self, execution, events_bitmap, forbidden_arenas):
-        pass
-
-    @abstractmethod
-    def filter_f(self, execution, enabled_events, events_bitmap):
-        pass
-
-
-# First filter on current state, then filter on current events
-class CurrentConfigStrategy(GeneratorStrategy):
-    __slots__ = []
-    def cache_init(self):
-        return {}
-
-    def key(self, execution, events_bitmap, forbidden_arenas):
-        return (execution.configuration, forbidden_arenas)
-
-    def generate(self, execution, events_bitmap, forbidden_arenas):
-        return [ t for t in self.priority_ordered_transitions
-                      if (t.source.opt.state_id_bitmap & execution.configuration)
-                       and (not forbidden_arenas & t.opt.arena_bitmap) ]
-
-    def filter_f(self, execution, enabled_events, events_bitmap):
-        return lambda t: (not t.trigger or t.trigger.check(events_bitmap)) and execution.check_guard(t, enabled_events)
-
-# First filter based on current events, then filter on current state
-class EnabledEventsStrategy(GeneratorStrategy):
-    __slots__ = ["statechart"]
-    def __init__(self, priority_ordered_transitions, statechart):
-        super().__init__(priority_ordered_transitions)
-        self.statechart = statechart
-
-    def cache_init(self):
-        cache = {}
-        cache[(0, 0)] = self.generate(None, 0, 0)
-        for event_id in bm_items(self.statechart.internal_events):
-            events_bitmap = bit(event_id)
-            cache[(events_bitmap, 0)] = self.generate(None, events_bitmap, 0)
-        return cache
-
-    def key(self, execution, events_bitmap, forbidden_arenas):
-        return (events_bitmap, forbidden_arenas)
-
-    def generate(self, execution, events_bitmap, forbidden_arenas):
-        return [ t for t in self.priority_ordered_transitions
-                      if (not t.trigger or t.trigger.check(events_bitmap))
-                      and (not forbidden_arenas & t.opt.arena_bitmap) ]
-
-    def filter_f(self, execution, enabled_events, events_bitmap):
-        return lambda t: (execution.configuration & t.source.opt.state_id_bitmap) and execution.check_guard(t, enabled_events)
-
-class CurrentConfigAndEnabledEventsStrategy(GeneratorStrategy):
-    __slots__ = ["statechart"]
-    def __init__(self, priority_ordered_transitions, statechart):
-        super().__init__(priority_ordered_transitions)
-        self.statechart = statechart
-
-    def cache_init(self):
-        return {}
-
-    def key(self, execution, events_bitmap, forbidden_arenas):
-        return (execution.configuration, events_bitmap, forbidden_arenas)
-
-    def generate(self, execution, events_bitmap, forbidden_arenas):
-        return [ t for t in self.priority_ordered_transitions
-                      if (not t.trigger or t.trigger.check(events_bitmap))
-                      and (t.source.opt.state_id_bitmap & execution.configuration)
-                      and (not forbidden_arenas & t.opt.arena_bitmap) ]
-
-    def filter_f(self, execution, enabled_events, events_bitmap):
-        return lambda t: execution.check_guard(t, enabled_events)
-
-
-class CandidateGenerator:
-    __slots__ = ["strategy", "cache"]
-    def __init__(self, strategy):
-        self.strategy = strategy
-        self.cache = strategy.cache_init()
-
-    def generate(self, execution, enabled_events: List[InternalEvent], forbidden_arenas: Bitmap) -> List[Transition]:
-        with timer.Context("generate candidates"):
-            events_bitmap = bm_from_list(e.id for e in enabled_events)
-            key = self.strategy.key(execution, events_bitmap, forbidden_arenas)
-
-            try:
-                candidates = self.cache[key]
-                ctr.cache_hits += 1
-            except KeyError:
-                candidates = self.cache[key] = self.strategy.generate(execution, events_bitmap, forbidden_arenas)
-                ctr.cache_misses += 1
-
-            candidates = filter(self.strategy.filter_f(execution, enabled_events, events_bitmap), candidates)
-
-            if DEBUG:
-                candidates = list(candidates) # convert generator to list (gotta do this, otherwise the generator will be all used up by our debug printing
-                if candidates:
-                    print()
-                    if enabled_events:
-                        print("events: " + str(enabled_events))
-                    print("candidates: " + ",  ".join(str(t) for t in candidates))
-                candidates = iter(candidates)
-
-            t = next(candidates, None)
-            if t:
-                return [t]
-            else:
-                return []
-
-
-class ConcurrentCandidateGenerator:
-    __slots__ = ["strategy", "cache", "synchronous"]
-    def __init__(self, strategy, synchronous):
-        self.strategy = strategy
-        self.cache = strategy.cache_init()
-        self.synchronous = synchronous
-
-    def generate(self, execution, enabled_events: List[InternalEvent], forbidden_arenas: Bitmap) -> List[Transition]:
-        with timer.Context("generate candidates"):
-            events_bitmap = bm_from_list(e.id for e in enabled_events)
-            transitions = []
-            while True:
-                key = self.strategy.key(execution, events_bitmap, forbidden_arenas)
-                try:
-                    candidates = self.cache[key]
-                    ctr.cache_hits += 1
-                except KeyError:
-                    candidates = self.cache[key] = self.strategy.generate(execution, events_bitmap, forbidden_arenas)
-                    ctr.cache_misses += 1
-                candidates = filter(self.strategy.filter_f(execution, enabled_events, events_bitmap), candidates)
-                t = next(candidates, None)
-                if t:
-                    transitions.append(t)
-                else:
-                    break
-                if self.synchronous:
-                    events_bitmap |= t.opt.raised_events
-                forbidden_arenas |= t.opt.arena_bitmap
-            return transitions
-
 # 1st bitmap: arenas covered by transitions fired
 # 2nd bitmap: arenas covered by transitions that had a stable target state
 RoundResult = Tuple[Bitmap, Bitmap]
@@ -256,42 +85,12 @@ class Syntactic(SuperRoundMaximality):
 
 # Examples: Big step, combo step
 class SuperRound(Round):
-    __slots__ = ["subround", "maximality"]
-    def __init__(self, name, subround: Round, maximality: SuperRoundMaximality):
+    __slots__ = ["subround", "maximality", "limit"]
+    def __init__(self, name, subround: Round, maximality: SuperRoundMaximality, limit: Optional[int] = None):
         super().__init__(name)
         self.subround = subround
         subround.parent = self
         self.maximality = maximality
-
-    def __repr__(self):
-        return self.name + " > " + self.subround.__repr__()
-
-    def reset(self):
-        super().reset()
-        self.subround.reset()
-
-    def _run(self, forbidden_arenas: Bitmap) -> RoundResult:
-        arenas_changed = Bitmap()
-        arenas_stabilized = Bitmap()
-
-        while True:
-            changed, stabilized = self.subround.run_and_cycle_events(forbidden_arenas) # no forbidden arenas in subround
-            if not changed:
-                break # no more transitions could be executed, done!
-
-            arenas_changed |= changed
-            arenas_stabilized |= stabilized
-
-            forbidden_arenas |= self.maximality.forbidden_arenas(arenas_changed, arenas_stabilized)
-
-        return (arenas_changed, arenas_stabilized)
-
-# Almost identical to SuperRound, but counts subrounds and raises exception if limit exceeded.
-# Useful for maximality options possibly causing infinite big steps like TakeMany and Syntactic.
-class SuperRoundWithLimit(SuperRound):
-    __slots__ = ["limit"]
-    def __init__(self, name, subround: Round, maximality: SuperRoundMaximality, limit: int):
-        super().__init__(name, subround, maximality)
         self.limit = limit
 
     def _run(self, forbidden_arenas: Bitmap) -> RoundResult:
@@ -304,9 +103,10 @@ class SuperRoundWithLimit(SuperRound):
             if not changed:
                 break # no more transitions could be executed, done!
 
-            subrounds += 1
-            if subrounds >= self.limit:
-                raise ModelRuntimeError("%s: Limit reached! (%d×%s) Possibly a never-ending big step." % (self.name, subrounds, self.subround.name))
+            if self.limit is not None:
+                subrounds += 1
+                if subrounds >= self.limit:
+                    raise ModelRuntimeError("%s: Limit reached! (%d×%s) Possibly a never-ending big step." % (self.name, subrounds, self.subround.name))
 
             arenas_changed |= changed
             arenas_stabilized |= stabilized

+ 14 - 25
src/sccd/statechart/dynamic/statechart_instance.py

@@ -4,7 +4,7 @@ from typing import List, Tuple, Iterable
 from sccd.util.debug import print_debug
 from sccd.util.bitmap import *
 from sccd.statechart.static.statechart import *
-import sccd.statechart.static.priority as priority
+from sccd.statechart.static import priority, concurrency
 from sccd.statechart.dynamic.builtin_scope import *
 from sccd.statechart.dynamic.round import *
 from sccd.statechart.dynamic.statechart_execution import *
@@ -39,26 +39,15 @@ class StatechartInstance(Instance):
         # Priority semantics
 
         with timer.Context("priority"):
-            hierarchical = {
-                HierarchicalPriority.NONE: priority.none,
-                HierarchicalPriority.SOURCE_PARENT: priority.source_parent,
-                HierarchicalPriority.SOURCE_CHILD: priority.source_child,
-                HierarchicalPriority.ARENA_PARENT: priority.arena_parent,
-                HierarchicalPriority.ARENA_CHILD: priority.arena_child,
-            }[semantics.hierarchical_priority]
-
-            same_state = {
-                SameSourcePriority.NONE: priority.none,
-                SameSourcePriority.EXPLICIT: priority.explicit,
-            }[semantics.same_source_priority]
-
-            orthogonal = {
-                OrthogonalPriority.NONE: priority.none,
-                OrthogonalPriority.EXPLICIT: priority.ooss_explicit_ordering,
-            }[semantics.orthogonal_priority]
-
-            priority_ordered_transitions = priority.get_total_ordering(statechart.tree,
-                hierarchical, same_state, orthogonal)
+
+            graph = priority.get_graph(statechart.tree, semantics)
+
+            consistency = {
+                Concurrency.SINGLE: concurrency.NoConcurrency(),
+                Concurrency.MANY: concurrency.ArenaOrthogonal(),
+            }[semantics.concurrency]
+
+            priority_ordered_transitions = priority.generate_total_ordering(statechart.tree, graph, consistency)
 
         # strategy = CurrentConfigStrategy(priority_ordered_transitions)
         strategy = EnabledEventsStrategy(priority_ordered_transitions, statechart)
@@ -90,19 +79,19 @@ class StatechartInstance(Instance):
 
             elif semantics.combo_step_maximality == Maximality.TAKE_MANY:
                 # Add even more layers, basically an onion at this point.
-                combo_step = SuperRoundWithLimit(termcolor.colored("combo_many", 'cyan'), subround=combo_one, maximality=TakeMany(), limit=LIMIT)
+                combo_step = SuperRound(termcolor.colored("combo_many", 'cyan'), subround=combo_one, maximality=TakeMany(), limit=LIMIT)
 
             elif semantics.combo_step_maximality == Maximality.SYNTACTIC:
-                combo_step = SuperRoundWithLimit(termcolor.colored("combo_syntactic", 'cyan'), subround=combo_one, maximality=Syntactic(), limit=LIMIT)
+                combo_step = SuperRound(termcolor.colored("combo_syntactic", 'cyan'), subround=combo_one, maximality=Syntactic(), limit=LIMIT)
 
             else:
                 raise Exception("Unsupported option: %s" % semantics.combo_step_maximality)
 
             if semantics.big_step_maximality == Maximality.TAKE_MANY:
-                self._big_step = SuperRoundWithLimit(termcolor.colored("big_many", 'red'), subround=combo_step, maximality=TakeMany(), limit=LIMIT)
+                self._big_step = SuperRound(termcolor.colored("big_many", 'red'), subround=combo_step, maximality=TakeMany(), limit=LIMIT)
 
             elif semantics.big_step_maximality == Maximality.SYNTACTIC:
-                self._big_step = SuperRoundWithLimit(termcolor.colored("big_syntactic", 'red'), subround=combo_step, maximality=Syntactic(), limit=LIMIT)
+                self._big_step = SuperRound(termcolor.colored("big_syntactic", 'red'), subround=combo_step, maximality=Syntactic(), limit=LIMIT)
 
         else:
             raise Exception("Unsupported option: %s" % semantics.big_step_maximality)

+ 43 - 0
src/sccd/statechart/static/concurrency.py

@@ -0,0 +1,43 @@
+from sccd.common.exceptions import *
+from sccd.statechart.static.tree import *
+from abc import *
+
+class SmallStepConsistency:
+    @abstractmethod
+    def can_fire_together(self, t1: Transition, t2: Transition) -> bool:
+        pass
+
+class NoConcurrency(SmallStepConsistency):
+    def can_fire_together(self, t1: Transition, t2: Transition) -> bool:
+        return False
+
+class ArenaOrthogonal(SmallStepConsistency):
+    def can_fire_together(self, t1: Transition, t2: Transition) -> bool:
+        return not (t1.opt.arena_bitmap & t2.opt.arena_bitmap) # nonoverlapping arenas
+
+class SrcDstOrthogonal(SmallStepConsistency):
+    def __init__(self, tree: StateTree):
+        self.tree = tree
+
+    def can_fire_together(self, t1: Transition, t2: Transition) -> bool:
+        source_lca = self.tree.lca(t1.source, t2.source)
+        target_lca = self.tree.lca(t1.target, t2.target)
+        return isinstance(source_lca, ParallelState) and isinstance(target_lca, ParallelState)
+
+# Raises an exception if the given set of transitions can potentially be enabled simulatenously, wrt. their source states in the state tree.
+def check_nondeterminism(tree: StateTree, transitions: Iterable[Transition], consistency: SmallStepConsistency):
+    pairs = itertools.combinations(transitions, 2)
+    for t1, t2 in pairs:
+        if consistency.can_fire_together(t1, t2):
+            return # It's OK: if they are both enabled, they will fire together in a small step
+
+        # They have the same source:
+        if t1.source is t2.source:
+            raise ModelStaticError("Nondeterminism! No priority between outgoing transitions of same state: %s, %s" % (t1, t2))
+        # Their sources are orthogonal to each other:
+        lca = tree.lca(t1.source, t2.source)
+        if isinstance(lca, ParallelState):
+            raise ModelStaticError("Nondeterminism! No priority between orthogonal transitions: %s, %s" % (t1, t2))
+        # Their source states are ancestors of one another:
+        if is_ancestor(t1.source, t2.source) or is_ancestor(t2.source, t1.source):
+            raise ModelStaticError("Nondeterminism! No priority between ancestral transitions: %s, %s" % (t1, t2))

+ 113 - 109
src/sccd/statechart/static/priority.py

@@ -1,5 +1,6 @@
-from sccd.common.exceptions import *
 from sccd.statechart.static.tree import StateTree, Transition, State, ParallelState
+from sccd.statechart.static.concurrency import check_nondeterminism, SmallStepConsistency
+from sccd.statechart.static.semantic_configuration import *
 from sccd.util.graph import strongly_connected_components
 from typing import *
 from sccd.util.visit_tree import visit_tree
@@ -9,108 +10,128 @@ import itertools
 
 EdgeList = List[Tuple[Transition,Transition]]
 
-# explicit ordering of orthogonal regions
-def ooss_explicit_ordering(tree: StateTree) -> EdgeList:
-    edges: EdgeList = []
-    # get all outgoing transitions of state or one of its descendants
-    def get_transitions(s: State) -> List[Transition]:
-        transitions = []
+# Get the (partial) priority ordering between transitions in the state tree, according to given semantics, as a graph
+def get_graph(tree: StateTree, semantics: SemanticConfiguration) -> EdgeList:
+
+    # explicit ordering of orthogonal regions
+    def explicit_ortho(tree: StateTree) -> EdgeList:
+        edges: EdgeList = []
+        # get all outgoing transitions of state or one of its descendants
+        def get_transitions(s: State) -> List[Transition]:
+            transitions = []
+            def visit_state(s: State, _=None):
+                transitions.extend(s.transitions)
+            visit_tree(s, lambda s: s.children, before_children=[visit_state])
+            return transitions
+        # create edges between transitions in one region to another
+        def visit_parallel_state(s: State, _=None):
+            if isinstance(s, ParallelState):
+                prev = []
+                # s.children are the orthogonal regions in document order
+                for region in s.children:
+                    curr = get_transitions(region)
+                    if len(curr) > 0: # skip empty regions
+                        edges.extend(itertools.product(prev, curr))
+                        prev = curr
+        visit_tree(tree.root, lambda s: s.children,
+            before_children=[visit_parallel_state])
+        return edges
+
+    # explicit ordering of outgoing transitions of the same state
+    def explicit_same_state(tree: StateTree) -> EdgeList:
+        edges: EdgeList = []
         def visit_state(s: State, _=None):
-            transitions.extend(s.transitions)
-        visit_tree(s, lambda s: s.children, before_children=[visit_state])
-        return transitions
-    # create edges between transitions in one region to another
-    def visit_parallel_state(s: State, _=None):
-        if isinstance(s, ParallelState):
-            prev = []
-            # s.children are the orthogonal regions in document order
-            for region in s.children:
-                curr = get_transitions(region)
-                if len(curr) > 0: # skip empty regions
-                    edges.extend(itertools.product(prev, curr))
-                    prev = curr
-    visit_tree(tree.root, lambda s: s.children,
-        before_children=[visit_parallel_state])
-    return edges
+            prev = None
+            # s.transitions are s' outgoing transitions in document order
+            for t in s.transitions:
+                if prev is not None:
+                    edges.append((prev, t))
+                prev = t
+        visit_tree(tree.root, lambda s: s.children,
+            before_children=[visit_state])
+        return edges
 
-# explicit ordering of outgoing transitions of the same state
-def explicit(tree: StateTree) -> EdgeList:
-    edges: EdgeList = []
-    def visit_state(s: State, _=None):
-        prev = None
-        # s.transitions are s' outgoing transitions in document order
-        for t in s.transitions:
-            if prev is not None:
-                edges.append((prev, t))
-            prev = t
-    visit_tree(tree.root, lambda s: s.children,
-        before_children=[visit_state])
-    return edges
+    # hierarchical Source-Parent ordering
+    def source_parent(tree: StateTree) -> EdgeList:
+        edges: EdgeList = []
+        def visit_state(s: State, parent_transitions: List[Transition] = []) -> List[Transition]:
+            if len(s.transitions) > 0: # skip states without transitions
+                edges.extend(itertools.product(parent_transitions, s.transitions))
+                return s.transitions
+            return parent_transitions
+        visit_tree(tree.root, lambda s: s.children, before_children=[visit_state])
+        return edges
 
-# hierarchical Source-Parent ordering
-def source_parent(tree: StateTree) -> EdgeList:
-    edges: EdgeList = []
-    def visit_state(s: State, parent_transitions: List[Transition] = []) -> List[Transition]:
-        if len(s.transitions) > 0: # skip states without transitions
-            edges.extend(itertools.product(parent_transitions, s.transitions))
-            return s.transitions
-        return parent_transitions
-    visit_tree(tree.root, lambda s: s.children, before_children=[visit_state])
-    return edges
+    # hierarchical Source-Child ordering
+    def source_child(tree: StateTree) -> EdgeList:
+        edges: EdgeList = []
+        def visit_state(s: State, ts: List[List[Transition]]) -> List[Transition]:
+            children_transitions = list(itertools.chain.from_iterable(ts))
+            if len(s.transitions) > 0: # skip states without transitions
+                edges.extend(itertools.product(children_transitions, s.transitions))
+                return s.transitions
+            else:
+                return children_transitions
+        visit_tree(tree.root, lambda s: s.children, after_children=[visit_state])
+        return edges
 
-# hierarchical Source-Child ordering
-def source_child(tree: StateTree) -> EdgeList:
-    edges: EdgeList = []
-    def visit_state(s: State, ts: List[List[Transition]]) -> List[Transition]:
-        children_transitions = list(itertools.chain.from_iterable(ts))
-        if len(s.transitions) > 0: # skip states without transitions
-            edges.extend(itertools.product(children_transitions, s.transitions))
-            return s.transitions
-        else:
-            return children_transitions
-    visit_tree(tree.root, lambda s: s.children, after_children=[visit_state])
-    return edges
+    # hierarchical Arena-Parent ordering
+    def arena_parent(tree: StateTree) -> EdgeList:
+        edges: EdgeList = []
+        partitions = collections.defaultdict(list) # mapping of transition's arena depth to list of transitions
+        for t in tree.transition_list:
+            partitions[t.opt.arena.opt.depth].append(t)
+        ordered_partitions = sorted(partitions.items(), key=lambda tup: tup[0])
+        prev = []
+        for depth, curr in ordered_partitions:
+            edges.extend(itertools.product(prev, curr))
+            prev = curr
+        return edges
 
-# hierarchical Arena-Parent ordering
-def arena_parent(tree: StateTree) -> EdgeList:
-    edges: EdgeList = []
-    partitions = collections.defaultdict(list) # mapping of transition's arena depth to list of transitions
-    for t in tree.transition_list:
-        partitions[t.opt.arena.opt.depth].append(t)
-    ordered_partitions = sorted(partitions.items(), key=lambda tup: tup[0])
-    prev = []
-    for depth, curr in ordered_partitions:
-        edges.extend(itertools.product(prev, curr))
-        prev = curr
-    return edges
+    # hierarchical Arena-Child ordering
+    def arena_child(tree: StateTree) -> EdgeList:
+        edges: EdgeList = []
+        partitions = collections.defaultdict(list) # mapping of transition's arena depth to list of transitions
+        for t in tree.transition_list:
+            partitions[t.opt.arena.opt.depth].append(t)
+        ordered_partitions = sorted(partitions.items(), key=lambda tup: -tup[0])
+        prev = []
+        for depth, curr in ordered_partitions:
+            edges.extend(itertools.product(prev, curr))
+            prev = curr
+        return edges
+
+    # no priority
+    def none(tree: StateTree) -> EdgeList:
+        return []
 
-# hierarchical Arena-Child ordering
-def arena_child(tree: StateTree) -> EdgeList:
-    edges: EdgeList = []
-    partitions = collections.defaultdict(list) # mapping of transition's arena depth to list of transitions
-    for t in tree.transition_list:
-        partitions[t.opt.arena.opt.depth].append(t)
-    ordered_partitions = sorted(partitions.items(), key=lambda tup: -tup[0])
-    prev = []
-    for depth, curr in ordered_partitions:
-        edges.extend(itertools.product(prev, curr))
-        prev = curr
-    return edges
 
-# no priority
-def none(tree: StateTree) -> EdgeList:
-    return []
+    hierarchical = {
+        HierarchicalPriority.NONE: none,
+        HierarchicalPriority.SOURCE_PARENT: source_parent,
+        HierarchicalPriority.SOURCE_CHILD: source_child,
+        HierarchicalPriority.ARENA_PARENT: arena_parent,
+        HierarchicalPriority.ARENA_CHILD: arena_child,
+    }[semantics.hierarchical_priority]
 
-# Apply the graph-yielding functions to the given statetree, and merge their results into a single graph
-def get_graph(tree: StateTree, *priorities: Callable[[StateTree], EdgeList]) -> EdgeList:
-    edges = list(itertools.chain.from_iterable(p(tree) for p in priorities))
+    same_state = {
+        SameSourcePriority.NONE: none,
+        SameSourcePriority.EXPLICIT: explicit_same_state,
+    }[semantics.same_source_priority]
+
+    orthogonal = {
+        OrthogonalPriority.NONE: none,
+        OrthogonalPriority.EXPLICIT: explicit_ortho,
+    }[semantics.orthogonal_priority]
+
+    edges = list(itertools.chain.from_iterable(p(tree) for p in [hierarchical, same_state, orthogonal]))
     return edges
 
 # Checks whether the 'priorities' given yield a valid ordering of transitions in the statechart.
 # Returns list of all transitions in statechart, ordered by priority (high -> low).
-def get_total_ordering(tree: StateTree, *priorities: Callable[[StateTree], EdgeList]) -> List[Transition]:
+def generate_total_ordering(tree: StateTree, graph: EdgeList, consistency: SmallStepConsistency) -> List[Transition]:
     # "edges" is a list of pairs (t1, t2) of transitions, where t1 has higher priority than t2.
-    edges = get_graph(tree, *priorities)
+    edges = graph
     scc = strongly_connected_components(edges)
     if len(scc) != len(tree.transition_list):
         # Priority graph contains cycles
@@ -120,23 +141,6 @@ def get_total_ordering(tree: StateTree, *priorities: Callable[[StateTree], EdgeL
 
     total_ordering = []
 
-    # Raises an exception if the given set of transitions can potentially be enabled simulatenously, wrt. their source states in the state tree.
-    def check_unordered(transitions):
-        pairs = itertools.combinations(transitions, 2)
-        for t1, t2 in pairs:
-            # LCA of their sources
-            lca_id = bm_highest_bit(t1.source.opt.ancestors & t2.source.opt.ancestors)
-            lca = tree.state_list[lca_id]
-            # Transitions are orthogonal to each other (LCA is And-state):
-            if isinstance(lca, ParallelState):
-                raise ModelStaticError("Nondeterminism! No priority between orthogonal transitions: %s, %s" % (t1, t2))
-            # They have the same source:
-            if t1.source is t2.source:
-                raise ModelStaticError("Nondeterminism! No priority between outgoing transitions of same state: %s, %s" % (t1, t2))
-            # Their source states are ancestors of one another:
-            if bm_has(t1.source.opt.ancestors, t2.source.opt.state_id) or bm_has(t2.source.opt.ancestors, t1.source.opt.state_id):
-                raise ModelStaticError("Nondeterminism! No priority between ancestral transitions: %s, %s" % (t1, t2))
-
     remaining_transitions = set(tree.transition_list)
     remaining_edges = edges
     while len(remaining_edges) > 0:
@@ -149,7 +153,7 @@ def get_total_ordering(tree: StateTree, *priorities: Callable[[StateTree], EdgeL
             lows.add(low)
         highest_priority = highs - lows
         # 2. Check if the transitions in this set are allowed to have equal priority.
-        check_unordered(highest_priority) # may raise Exception
+        check_nondeterminism(tree, highest_priority, consistency) # may raise Exception
         # 3. All good. Add the transitions in the highest-priority set in any order to the total ordering
         total_ordering.extend(highest_priority)
         # 4. Remove the transitions of the highest-priority set from the graph, and repeat.
@@ -157,7 +161,7 @@ def get_total_ordering(tree: StateTree, *priorities: Callable[[StateTree], EdgeL
         remaining_transitions -= highest_priority
 
     # Finally, there may be transitions that occur in the priority graph only as vertices, e.g. in flat statecharts:
-    check_unordered(remaining_transitions)
+    check_nondeterminism(tree, remaining_transitions, consistency)
     total_ordering.extend(remaining_transitions)
 
     return total_ordering

+ 8 - 4
src/sccd/statechart/static/tree.py

@@ -346,10 +346,7 @@ class StateTree(Freezable):
 
             for t in self.transition_list:
                 # Arena can be computed statically. First compute Lowest-common ancestor:
-                # Intersection between source & target ancestors, last member in depth-first sorted state list.
-                lca_id = bm_highest_bit(t.source.opt.ancestors & t.target.opt.ancestors)
-                lca = self.state_list[lca_id]
-                arena = lca
+                arena = self.lca(t.source, t.target)
                 # Arena must be an Or-state:
                 while isinstance(arena, (ParallelState, HistoryState)):
                     arena = arena.parent
@@ -404,5 +401,12 @@ class StateTree(Freezable):
     def bitmap_to_states_reverse(self, bitmap: Bitmap) -> Iterator[State]:
         return (self.state_list[id] for id in bm_reverse_items(bitmap))
 
+    def lca(self, s1: State, s2: State) -> State:
+        # Intersection between source & target ancestors, last member in depth-first sorted state list.
+        return self.state_list[bm_highest_bit(s1.opt.ancestors & s2.opt.ancestors)]
+
 def states_to_bitmap(states: Iterable[State]) -> Bitmap:
     return bm_from_list(s.opt.state_id for s in states)
+
+def is_ancestor(parent: State, child: State) -> bool:
+    return bm_has(child.opt.ancestors, parent.opt.state_id)

+ 1 - 0
test/test_files/day_atlee/statechart_fig1_redialer.xml

@@ -3,6 +3,7 @@
   <semantics
     big_step_maximality="syntactic"
     concurrency="many"
+    orthogonal_priority="none"
     input_event_lifeline="whole"
     enabledness_memory_protocol="small_step"
     assignment_memory_protocol="small_step"/>