fgm/learning_tla
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions
learning_tla/learn_tla/topics/fsm3.svg
Frederic G. MARAND 694cf387ae Learn TLA+ Topics: FSMs.
2025-02-25 17:03:44 +00:00

101 lines
6.8 KiB
XML
Raw Permalink Blame History

<?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 12.2.1 (20241206.2353)
-->
<!-- Title: DiskGraph Pages: 1 -->
<svg width="509pt" height="319pt"
viewBox="0.00 0.00 509.00 318.95" 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 314.95)">
<title>DiskGraph</title>
<polygon fill="white" stroke="none" points="-4,4 -4,-314.95 505,-314.95 505,4 -4,4"/>
<g id="clust1" class="cluster">
<title>cluster_graph</title>
<polygon fill="none" stroke="white" points="8,-8 8,-302.95 493,-302.95 493,-8 8,-8"/>
</g>
<!-- &#45;7999366354808658534 -->
<g id="node1" class="node">
<title>&#45;7999366354808658534</title>
<ellipse fill="lightgrey" stroke="black" cx="259" cy="-265.96" rx="111.02" ry="28.99"/>
<text text-anchor="middle" x="259" y="-269.16" font-family="Times,serif" font-size="14.00">/\ state = &quot;BothOff&quot;</text>
<text text-anchor="middle" x="259" y="-252.66" font-family="Times,serif" font-size="14.00">/\ pc = [SM |&#45;&gt; &quot;Action&quot;]</text>
</g>
<!-- &#45;4735211404992135549 -->
<g id="node2" class="node">
<title>&#45;4735211404992135549</title>
<ellipse fill="none" stroke="black" cx="127" cy="-155.47" rx="111.02" ry="28.99"/>
<text text-anchor="middle" x="127" y="-158.67" font-family="Times,serif" font-size="14.00">/\ state = &quot;LampOff&quot;</text>
<text text-anchor="middle" x="127" y="-142.17" font-family="Times,serif" font-size="14.00">/\ pc = [SM |&#45;&gt; &quot;Action&quot;]</text>
</g>
<!-- &#45;7999366354808658534&#45;&gt;&#45;4735211404992135549 -->
<g id="edge1" class="edge">
<title>&#45;7999366354808658534&#45;&gt;&#45;4735211404992135549</title>
<path fill="none" stroke="#1f78b4" d="M187.47,-243.4C174.58,-237.08 162.12,-229.07 152.25,-218.97 145.81,-212.38 140.94,-203.93 137.29,-195.39"/>
<polygon fill="#1f78b4" stroke="#1f78b4" points="140.59,-194.22 133.81,-186.07 134.03,-196.66 140.59,-194.22"/>
<text text-anchor="middle" x="170.62" y="-205.67" font-family="Times,serif" font-size="14.00" fill="#000000">Action</text>
</g>
<!-- &#45;2849417507403741281 -->
<g id="node3" class="node">
<title>&#45;2849417507403741281</title>
<ellipse fill="none" stroke="black" cx="374" cy="-155.47" rx="111.02" ry="28.99"/>
<text text-anchor="middle" x="374" y="-158.67" font-family="Times,serif" font-size="14.00">/\ state = &quot;WallOff&quot;</text>
<text text-anchor="middle" x="374" y="-142.17" font-family="Times,serif" font-size="14.00">/\ pc = [SM |&#45;&gt; &quot;Action&quot;]</text>
</g>
<!-- &#45;7999366354808658534&#45;&gt;&#45;2849417507403741281 -->
<g id="edge2" class="edge">
<title>&#45;7999366354808658534&#45;&gt;&#45;2849417507403741281</title>
<path fill="none" stroke="#1f78b4" d="M275.47,-237.05C283.05,-225.56 292.71,-212.6 303.25,-202.47 308.24,-197.67 313.8,-193.08 319.55,-188.78"/>
<polygon fill="#1f78b4" stroke="#1f78b4" points="321.33,-191.8 327.45,-183.15 317.27,-186.1 321.33,-191.8"/>
<text text-anchor="middle" x="321.62" y="-205.67" font-family="Times,serif" font-size="14.00" fill="#000000">Action</text>
</g>
<!-- &#45;4735211404992135549&#45;&gt;&#45;7999366354808658534 -->
<g id="edge3" class="edge">
<title>&#45;4735211404992135549&#45;&gt;&#45;7999366354808658534</title>
<path fill="none" stroke="#1f78b4" d="M165.47,-182.98C174.02,-189.18 182.93,-195.9 191,-202.47 201.59,-211.08 212.66,-220.88 222.72,-230.12"/>
<polygon fill="#1f78b4" stroke="#1f78b4" points="220.07,-232.45 229.78,-236.69 224.84,-227.32 220.07,-232.45"/>
<text text-anchor="middle" x="228.67" y="-205.67" font-family="Times,serif" font-size="14.00" fill="#000000">Action</text>
</g>
<!-- &#45;4225438770487961676 -->
<g id="node4" class="node">
<title>&#45;4225438770487961676</title>
<ellipse fill="none" stroke="black" cx="253" cy="-44.99" rx="111.02" ry="28.99"/>
<text text-anchor="middle" x="253" y="-48.19" font-family="Times,serif" font-size="14.00">/\ state = &quot;On&quot;</text>
<text text-anchor="middle" x="253" y="-31.69" font-family="Times,serif" font-size="14.00">/\ pc = [SM |&#45;&gt; &quot;Action&quot;]</text>
</g>
<!-- &#45;4735211404992135549&#45;&gt;&#45;4225438770487961676 -->
<g id="edge4" class="edge">
<title>&#45;4735211404992135549&#45;&gt;&#45;4225438770487961676</title>
<path fill="none" stroke="#1f78b4" d="M133.48,-126.07C137.33,-114.36 143.27,-101.37 152.25,-91.98 158.96,-84.97 166.95,-78.93 175.44,-73.76"/>
<polygon fill="#1f78b4" stroke="#1f78b4" points="176.87,-76.97 183.88,-69.02 173.45,-70.86 176.87,-76.97"/>
<text text-anchor="middle" x="170.62" y="-95.18" font-family="Times,serif" font-size="14.00" fill="#000000">Action</text>
</g>
<!-- &#45;2849417507403741281&#45;&gt;&#45;7999366354808658534 -->
<g id="edge5" class="edge">
<title>&#45;2849417507403741281&#45;&gt;&#45;7999366354808658534</title>
<path fill="none" stroke="#1f78b4" d="M363.89,-184.55C358.67,-196.2 351.41,-209.24 342,-218.97 336.49,-224.66 330.11,-229.84 323.4,-234.5"/>
<polygon fill="#1f78b4" stroke="#1f78b4" points="321.85,-231.33 315.35,-239.7 325.65,-237.21 321.85,-231.33"/>
<text text-anchor="middle" x="372.04" y="-205.67" font-family="Times,serif" font-size="14.00" fill="#000000">Action</text>
</g>
<!-- &#45;2849417507403741281&#45;&gt;&#45;4225438770487961676 -->
<g id="edge6" class="edge">
<title>&#45;2849417507403741281&#45;&gt;&#45;4225438770487961676</title>
<path fill="none" stroke="#1f78b4" d="M329.39,-128.56C320.35,-122.48 311.18,-115.65 303.25,-108.48 294.73,-100.78 286.48,-91.55 279.22,-82.58"/>
<polygon fill="#1f78b4" stroke="#1f78b4" points="282.16,-80.67 273.24,-74.96 276.65,-84.99 282.16,-80.67"/>
<text text-anchor="middle" x="321.62" y="-95.18" font-family="Times,serif" font-size="14.00" fill="#000000">Action</text>
</g>
<!-- &#45;4225438770487961676&#45;&gt;&#45;4735211404992135549 -->
<g id="edge7" class="edge">
<title>&#45;4225438770487961676&#45;&gt;&#45;4735211404992135549</title>
<path fill="none" stroke="#1f78b4" d="M227.69,-73.45C216.8,-84.74 203.67,-97.67 191,-108.48 186,-112.75 180.62,-117.03 175.18,-121.18"/>
<polygon fill="#1f78b4" stroke="#1f78b4" points="173.17,-118.31 167.24,-127.1 177.35,-123.93 173.17,-118.31"/>
<text text-anchor="middle" x="227.25" y="-95.18" font-family="Times,serif" font-size="14.00" fill="#000000">Action</text>
</g>
<!-- &#45;4225438770487961676&#45;&gt;&#45;2849417507403741281 -->
<g id="edge8" class="edge">
<title>&#45;4225438770487961676&#45;&gt;&#45;2849417507403741281</title>
<path fill="none" stroke="#1f78b4" d="M312.07,-69.89C322.86,-76.01 333.41,-83.36 342,-91.98 348.79,-98.8 354.43,-107.35 358.99,-115.92"/>
<polygon fill="#1f78b4" stroke="#1f78b4" points="355.84,-117.44 363.36,-124.9 362.14,-114.38 355.84,-117.44"/>
<text text-anchor="middle" x="372.16" y="-95.18" font-family="Times,serif" font-size="14.00" fill="#000000">Action</text>
</g>
</g>
</svg>
Reference in a new issue View git blame Copy permalink