learning_tla/lamport_pluscal/pc2_euclid_liveness.svg

<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<!DOCTYPE svg PUBLIC "-//W3C//DTD SVG 1.1//EN"
 "http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd">
<!-- Generated by graphviz version 12.2.1 (20241206.2353)
 -->
<!-- Title: DiskGraph Pages: 1 -->
<svg width="302pt" height="1877pt"
 viewBox="0.00 0.00 302.00 1877.21" 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 1873.21)">
<title>DiskGraph</title>
<polygon fill="white" stroke="none" points="-4,4 -4,-1873.21 298,-1873.21 298,4 -4,4"/>
<g id="clust1" class="cluster">
<title>cluster_graph</title>
<polygon fill="none" stroke="white" points="8,-8 8,-1861.21 286,-1861.21 286,-8 8,-8"/>
</g>
<!-- &#45;6199414645558391910.0 -->
<g id="node1" class="node">
<title>&#45;6199414645558391910.0</title>
<ellipse fill="lightgrey" stroke="black" cx="138" cy="-1777.55" rx="122.15" ry="75.66"/>
<text text-anchor="middle" x="138" y="-1813.75" font-family="Times,serif" font-size="14.00">/\ u0 = 3</text>
<text text-anchor="middle" x="138" y="-1797.25" font-family="Times,serif" font-size="14.00">/\ v0 = 5</text>
<text text-anchor="middle" x="138" y="-1780.75" font-family="Times,serif" font-size="14.00">/\ u = 3</text>
<text text-anchor="middle" x="138" y="-1764.25" font-family="Times,serif" font-size="14.00">/\ v = 5</text>
<text text-anchor="middle" x="138" y="-1747.75" font-family="Times,serif" font-size="14.00">/\ pc = &quot;LBWhile&quot;</text>
<text text-anchor="middle" x="138" y="-1731.25" font-family="Times,serif" font-size="14.00">#&#45;6199414645558391910.0#</text>
</g>
<!-- &#45;6199414645558391910.0&#45;&gt;&#45;6199414645558391910.0 -->
<g id="edge1" class="edge">
<title>&#45;6199414645558391910.0&#45;&gt;&#45;6199414645558391910.0</title>
<path fill="none" stroke="black" d="M247.74,-1811.22C269.58,-1807.43 285.15,-1796.21 285.15,-1777.55 285.15,-1762.24 274.67,-1751.94 258.85,-1746.64"/>
<polygon fill="black" stroke="black" points="259.76,-1743.26 249.21,-1744.24 258.07,-1750.05 259.76,-1743.26"/>
</g>
<!-- &#45;3468211351142298482.0 -->
<g id="node2" class="node">
<title>&#45;3468211351142298482.0</title>
<ellipse fill="none" stroke="black" cx="138" cy="-1590.23" rx="122.15" ry="75.66"/>
<text text-anchor="middle" x="138" y="-1626.43" font-family="Times,serif" font-size="14.00">/\ u0 = 3</text>
<text text-anchor="middle" x="138" y="-1609.93" font-family="Times,serif" font-size="14.00">/\ v0 = 5</text>
<text text-anchor="middle" x="138" y="-1593.43" font-family="Times,serif" font-size="14.00">/\ u = 5</text>
<text text-anchor="middle" x="138" y="-1576.93" font-family="Times,serif" font-size="14.00">/\ v = 3</text>
<text text-anchor="middle" x="138" y="-1560.43" font-family="Times,serif" font-size="14.00">/\ pc = &quot;LBSubtract&quot;</text>
<text text-anchor="middle" x="138" y="-1543.93" font-family="Times,serif" font-size="14.00">#&#45;3468211351142298482.0#</text>
</g>
<!-- &#45;6199414645558391910.0&#45;&gt;&#45;3468211351142298482.0 -->
<g id="edge2" class="edge">
<title>&#45;6199414645558391910.0&#45;&gt;&#45;3468211351142298482.0</title>
<path fill="none" stroke="black" d="M138,-1701.44C138,-1693.53 138,-1685.44 138,-1677.42"/>
<polygon fill="black" stroke="black" points="141.5,-1677.66 138,-1667.66 134.5,-1677.66 141.5,-1677.66"/>
</g>
<!-- &#45;3468211351142298482.0&#45;&gt;&#45;3468211351142298482.0 -->
<g id="edge4" class="edge">
<title>&#45;3468211351142298482.0&#45;&gt;&#45;3468211351142298482.0</title>
<path fill="none" stroke="black" d="M247.74,-1623.9C269.58,-1620.11 285.15,-1608.89 285.15,-1590.23 285.15,-1574.92 274.67,-1564.62 258.85,-1559.32"/>
<polygon fill="black" stroke="black" points="259.76,-1555.94 249.21,-1556.92 258.07,-1562.73 259.76,-1555.94"/>
</g>
<!-- &#45;6889634394201572634.0 -->
<g id="node3" class="node">
<title>&#45;6889634394201572634.0</title>
<ellipse fill="none" stroke="black" cx="138" cy="-1402.91" rx="122.15" ry="75.66"/>
<text text-anchor="middle" x="138" y="-1439.11" font-family="Times,serif" font-size="14.00">/\ u0 = 3</text>
<text text-anchor="middle" x="138" y="-1422.61" font-family="Times,serif" font-size="14.00">/\ v0 = 5</text>
<text text-anchor="middle" x="138" y="-1406.11" font-family="Times,serif" font-size="14.00">/\ u = 2</text>
<text text-anchor="middle" x="138" y="-1389.61" font-family="Times,serif" font-size="14.00">/\ v = 3</text>
<text text-anchor="middle" x="138" y="-1373.11" font-family="Times,serif" font-size="14.00">/\ pc = &quot;LBWhile&quot;</text>
<text text-anchor="middle" x="138" y="-1356.61" font-family="Times,serif" font-size="14.00">#&#45;6889634394201572634.0#</text>
</g>
<!-- &#45;3468211351142298482.0&#45;&gt;&#45;6889634394201572634.0 -->
<g id="edge3" class="edge">
<title>&#45;3468211351142298482.0&#45;&gt;&#45;6889634394201572634.0</title>
<path fill="none" stroke="black" d="M138,-1514.12C138,-1506.21 138,-1498.12 138,-1490.1"/>
<polygon fill="black" stroke="black" points="141.5,-1490.34 138,-1480.34 134.5,-1490.34 141.5,-1490.34"/>
</g>
<!-- &#45;6889634394201572634.0&#45;&gt;&#45;6889634394201572634.0 -->
<g id="edge5" class="edge">
<title>&#45;6889634394201572634.0&#45;&gt;&#45;6889634394201572634.0</title>
<path fill="none" stroke="black" d="M247.74,-1436.58C269.58,-1432.79 285.15,-1421.57 285.15,-1402.91 285.15,-1387.6 274.67,-1377.3 258.85,-1372"/>
<polygon fill="black" stroke="black" points="259.76,-1368.61 249.21,-1369.6 258.07,-1375.41 259.76,-1368.61"/>
</g>
<!-- &#45;2952376645972590487.0 -->
<g id="node4" class="node">
<title>&#45;2952376645972590487.0</title>
<ellipse fill="none" stroke="black" cx="138" cy="-1215.59" rx="122.15" ry="75.66"/>
<text text-anchor="middle" x="138" y="-1251.79" font-family="Times,serif" font-size="14.00">/\ u0 = 3</text>
<text text-anchor="middle" x="138" y="-1235.29" font-family="Times,serif" font-size="14.00">/\ v0 = 5</text>
<text text-anchor="middle" x="138" y="-1218.79" font-family="Times,serif" font-size="14.00">/\ u = 3</text>
<text text-anchor="middle" x="138" y="-1202.29" font-family="Times,serif" font-size="14.00">/\ v = 2</text>
<text text-anchor="middle" x="138" y="-1185.79" font-family="Times,serif" font-size="14.00">/\ pc = &quot;LBSubtract&quot;</text>
<text text-anchor="middle" x="138" y="-1169.29" font-family="Times,serif" font-size="14.00">#&#45;2952376645972590487.0#</text>
</g>
<!-- &#45;6889634394201572634.0&#45;&gt;&#45;2952376645972590487.0 -->
<g id="edge6" class="edge">
<title>&#45;6889634394201572634.0&#45;&gt;&#45;2952376645972590487.0</title>
<path fill="none" stroke="black" d="M138,-1326.8C138,-1318.89 138,-1310.8 138,-1302.78"/>
<polygon fill="black" stroke="black" points="141.5,-1303.01 138,-1293.01 134.5,-1303.02 141.5,-1303.01"/>
</g>
<!-- &#45;2952376645972590487.0&#45;&gt;&#45;2952376645972590487.0 -->
<g id="edge7" class="edge">
<title>&#45;2952376645972590487.0&#45;&gt;&#45;2952376645972590487.0</title>
<path fill="none" stroke="black" d="M247.74,-1249.26C269.58,-1245.47 285.15,-1234.24 285.15,-1215.59 285.15,-1200.28 274.67,-1189.98 258.85,-1184.68"/>
<polygon fill="black" stroke="black" points="259.76,-1181.29 249.21,-1182.28 258.07,-1188.09 259.76,-1181.29"/>
</g>
<!-- 4160762573541434430.0 -->
<g id="node5" class="node">
<title>4160762573541434430.0</title>
<ellipse fill="none" stroke="black" cx="138" cy="-1028.26" rx="118.97" ry="75.66"/>
<text text-anchor="middle" x="138" y="-1064.46" font-family="Times,serif" font-size="14.00">/\ u0 = 3</text>
<text text-anchor="middle" x="138" y="-1047.96" font-family="Times,serif" font-size="14.00">/\ v0 = 5</text>
<text text-anchor="middle" x="138" y="-1031.46" font-family="Times,serif" font-size="14.00">/\ u = 1</text>
<text text-anchor="middle" x="138" y="-1014.96" font-family="Times,serif" font-size="14.00">/\ v = 2</text>
<text text-anchor="middle" x="138" y="-998.46" font-family="Times,serif" font-size="14.00">/\ pc = &quot;LBWhile&quot;</text>
<text text-anchor="middle" x="138" y="-981.96" font-family="Times,serif" font-size="14.00">#4160762573541434430.0#</text>
</g>
<!-- &#45;2952376645972590487.0&#45;&gt;4160762573541434430.0 -->
<g id="edge8" class="edge">
<title>&#45;2952376645972590487.0&#45;&gt;4160762573541434430.0</title>
<path fill="none" stroke="black" d="M138,-1139.48C138,-1131.56 138,-1123.48 138,-1115.45"/>
<polygon fill="black" stroke="black" points="141.5,-1115.69 138,-1105.69 134.5,-1115.69 141.5,-1115.69"/>
</g>
<!-- 4160762573541434430.0&#45;&gt;4160762573541434430.0 -->
<g id="edge10" class="edge">
<title>4160762573541434430.0&#45;&gt;4160762573541434430.0</title>
<path fill="none" stroke="black" d="M245.05,-1061.99C266.58,-1058.26 281.97,-1047.02 281.97,-1028.26 281.97,-1012.88 271.62,-1002.55 256.01,-997.28"/>
<polygon fill="black" stroke="black" points="257.07,-993.93 246.52,-994.9 255.37,-1000.73 257.07,-993.93"/>
</g>
<!-- &#45;7138927888387593572.0 -->
<g id="node6" class="node">
<title>&#45;7138927888387593572.0</title>
<ellipse fill="none" stroke="black" cx="138" cy="-840.94" rx="122.15" ry="75.66"/>
<text text-anchor="middle" x="138" y="-877.14" font-family="Times,serif" font-size="14.00">/\ u0 = 3</text>
<text text-anchor="middle" x="138" y="-860.64" font-family="Times,serif" font-size="14.00">/\ v0 = 5</text>
<text text-anchor="middle" x="138" y="-844.14" font-family="Times,serif" font-size="14.00">/\ u = 2</text>
<text text-anchor="middle" x="138" y="-827.64" font-family="Times,serif" font-size="14.00">/\ v = 1</text>
<text text-anchor="middle" x="138" y="-811.14" font-family="Times,serif" font-size="14.00">/\ pc = &quot;LBSubtract&quot;</text>
<text text-anchor="middle" x="138" y="-794.64" font-family="Times,serif" font-size="14.00">#&#45;7138927888387593572.0#</text>
</g>
<!-- 4160762573541434430.0&#45;&gt;&#45;7138927888387593572.0 -->
<g id="edge9" class="edge">
<title>4160762573541434430.0&#45;&gt;&#45;7138927888387593572.0</title>
<path fill="none" stroke="black" d="M138,-952.15C138,-944.24 138,-936.16 138,-928.13"/>
<polygon fill="black" stroke="black" points="141.5,-928.37 138,-918.37 134.5,-928.37 141.5,-928.37"/>
</g>
<!-- &#45;7138927888387593572.0&#45;&gt;&#45;7138927888387593572.0 -->
<g id="edge12" class="edge">
<title>&#45;7138927888387593572.0&#45;&gt;&#45;7138927888387593572.0</title>
<path fill="none" stroke="black" d="M247.74,-874.62C269.58,-870.83 285.15,-859.6 285.15,-840.94 285.15,-825.64 274.67,-815.33 258.85,-810.03"/>
<polygon fill="black" stroke="black" points="259.76,-806.65 249.21,-807.64 258.07,-813.45 259.76,-806.65"/>
</g>
<!-- 20890309182309314.0 -->
<g id="node7" class="node">
<title>20890309182309314.0</title>
<ellipse fill="none" stroke="black" cx="138" cy="-653.62" rx="109.42" ry="75.66"/>
<text text-anchor="middle" x="138" y="-689.82" font-family="Times,serif" font-size="14.00">/\ u0 = 3</text>
<text text-anchor="middle" x="138" y="-673.32" font-family="Times,serif" font-size="14.00">/\ v0 = 5</text>
<text text-anchor="middle" x="138" y="-656.82" font-family="Times,serif" font-size="14.00">/\ u = 1</text>
<text text-anchor="middle" x="138" y="-640.32" font-family="Times,serif" font-size="14.00">/\ v = 1</text>
<text text-anchor="middle" x="138" y="-623.82" font-family="Times,serif" font-size="14.00">/\ pc = &quot;LBWhile&quot;</text>
<text text-anchor="middle" x="138" y="-607.32" font-family="Times,serif" font-size="14.00">#20890309182309314.0#</text>
</g>
<!-- &#45;7138927888387593572.0&#45;&gt;20890309182309314.0 -->
<g id="edge11" class="edge">
<title>&#45;7138927888387593572.0&#45;&gt;20890309182309314.0</title>
<path fill="none" stroke="black" d="M138,-764.83C138,-756.92 138,-748.84 138,-740.81"/>
<polygon fill="black" stroke="black" points="141.5,-741.05 138,-731.05 134.5,-741.05 141.5,-741.05"/>
</g>
<!-- 20890309182309314.0&#45;&gt;20890309182309314.0 -->
<g id="edge13" class="edge">
<title>20890309182309314.0&#45;&gt;20890309182309314.0</title>
<path fill="none" stroke="black" d="M236.17,-687.66C257.2,-684.27 272.42,-672.92 272.42,-653.62 272.42,-637.94 262.38,-627.51 247.33,-622.33"/>
<polygon fill="black" stroke="black" points="248.19,-618.94 237.64,-619.95 246.52,-625.74 248.19,-618.94"/>
</g>
<!-- 1911697999759052964.0 -->
<g id="node8" class="node">
<title>1911697999759052964.0</title>
<ellipse fill="none" stroke="black" cx="138" cy="-466.3" rx="118.97" ry="75.66"/>
<text text-anchor="middle" x="138" y="-502.5" font-family="Times,serif" font-size="14.00">/\ u0 = 3</text>
<text text-anchor="middle" x="138" y="-486" font-family="Times,serif" font-size="14.00">/\ v0 = 5</text>
<text text-anchor="middle" x="138" y="-469.5" font-family="Times,serif" font-size="14.00">/\ u = 1</text>
<text text-anchor="middle" x="138" y="-453" font-family="Times,serif" font-size="14.00">/\ v = 1</text>
<text text-anchor="middle" x="138" y="-436.5" font-family="Times,serif" font-size="14.00">/\ pc = &quot;LBSubtract&quot;</text>
<text text-anchor="middle" x="138" y="-420" font-family="Times,serif" font-size="14.00">#1911697999759052964.0#</text>
</g>
<!-- 20890309182309314.0&#45;&gt;1911697999759052964.0 -->
<g id="edge14" class="edge">
<title>20890309182309314.0&#45;&gt;1911697999759052964.0</title>
<path fill="none" stroke="black" d="M138,-577.51C138,-569.6 138,-561.51 138,-553.49"/>
<polygon fill="black" stroke="black" points="141.5,-553.73 138,-543.73 134.5,-553.73 141.5,-553.73"/>
</g>
<!-- 1911697999759052964.0&#45;&gt;1911697999759052964.0 -->
<g id="edge15" class="edge">
<title>1911697999759052964.0&#45;&gt;1911697999759052964.0</title>
<path fill="none" stroke="black" d="M245.05,-500.03C266.58,-496.3 281.97,-485.05 281.97,-466.3 281.97,-450.92 271.62,-440.59 256.01,-435.31"/>
<polygon fill="black" stroke="black" points="257.07,-431.97 246.52,-432.94 255.37,-438.76 257.07,-431.97"/>
</g>
<!-- 8805096738011839814.0 -->
<g id="node9" class="node">
<title>8805096738011839814.0</title>
<ellipse fill="none" stroke="black" cx="138" cy="-278.98" rx="118.97" ry="75.66"/>
<text text-anchor="middle" x="138" y="-315.18" font-family="Times,serif" font-size="14.00">/\ u0 = 3</text>
<text text-anchor="middle" x="138" y="-298.68" font-family="Times,serif" font-size="14.00">/\ v0 = 5</text>
<text text-anchor="middle" x="138" y="-282.18" font-family="Times,serif" font-size="14.00">/\ u = 0</text>
<text text-anchor="middle" x="138" y="-265.68" font-family="Times,serif" font-size="14.00">/\ v = 1</text>
<text text-anchor="middle" x="138" y="-249.18" font-family="Times,serif" font-size="14.00">/\ pc = &quot;LBWhile&quot;</text>
<text text-anchor="middle" x="138" y="-232.68" font-family="Times,serif" font-size="14.00">#8805096738011839814.0#</text>
</g>
<!-- 1911697999759052964.0&#45;&gt;8805096738011839814.0 -->
<g id="edge16" class="edge">
<title>1911697999759052964.0&#45;&gt;8805096738011839814.0</title>
<path fill="none" stroke="black" d="M138,-390.19C138,-382.28 138,-374.19 138,-366.17"/>
<polygon fill="black" stroke="black" points="141.5,-366.41 138,-356.41 134.5,-366.41 141.5,-366.41"/>
</g>
<!-- 8805096738011839814.0&#45;&gt;8805096738011839814.0 -->
<g id="edge18" class="edge">
<title>8805096738011839814.0&#45;&gt;8805096738011839814.0</title>
<path fill="none" stroke="black" d="M245.05,-312.71C266.58,-308.97 281.97,-297.73 281.97,-278.98 281.97,-263.6 271.62,-253.27 256.01,-247.99"/>
<polygon fill="black" stroke="black" points="257.07,-244.65 246.52,-245.62 255.37,-251.44 257.07,-244.65"/>
</g>
<!-- 8133042805049486482.0 -->
<g id="node10" class="node">
<title>8133042805049486482.0</title>
<ellipse fill="none" stroke="black" cx="138" cy="-91.66" rx="118.97" ry="75.66"/>
<text text-anchor="middle" x="138" y="-127.86" font-family="Times,serif" font-size="14.00">/\ u0 = 3</text>
<text text-anchor="middle" x="138" y="-111.36" font-family="Times,serif" font-size="14.00">/\ v0 = 5</text>
<text text-anchor="middle" x="138" y="-94.86" font-family="Times,serif" font-size="14.00">/\ u = 0</text>
<text text-anchor="middle" x="138" y="-78.36" font-family="Times,serif" font-size="14.00">/\ v = 1</text>
<text text-anchor="middle" x="138" y="-61.86" font-family="Times,serif" font-size="14.00">/\ pc = &quot;LBPrintResult&quot;</text>
<text text-anchor="middle" x="138" y="-45.36" font-family="Times,serif" font-size="14.00">#8133042805049486482.0#</text>
</g>
<!-- 8805096738011839814.0&#45;&gt;8133042805049486482.0 -->
<g id="edge17" class="edge">
<title>8805096738011839814.0&#45;&gt;8133042805049486482.0</title>
<path fill="none" stroke="black" d="M138,-202.87C138,-194.96 138,-186.87 138,-178.85"/>
<polygon fill="black" stroke="black" points="141.5,-179.09 138,-169.09 134.5,-179.09 141.5,-179.09"/>
</g>
<!-- 8133042805049486482.0&#45;&gt;8133042805049486482.0 -->
<g id="edge19" class="edge">
<title>8133042805049486482.0&#45;&gt;8133042805049486482.0</title>
<path fill="none" stroke="black" d="M245.05,-125.39C266.58,-121.65 281.97,-110.41 281.97,-91.66 281.97,-76.28 271.62,-65.95 256.01,-60.67"/>
<polygon fill="black" stroke="black" points="257.07,-57.33 246.52,-58.3 255.37,-64.12 257.07,-57.33"/>
</g>
</g>
</svg>