learning_tla/intro/specs/mutex.svg
Frederic G. MARAND de69f7c399 Intro: examples.
2025-02-22 19:20:33 +01:00

298 lines
20 KiB
XML

<?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="996pt" height="554pt"
viewBox="0.00 0.00 996.00 553.92" 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 549.92)">
<title>DiskGraph</title>
<polygon fill="white" stroke="none" points="-4,4 -4,-549.92 992,-549.92 992,4 -4,4"/>
<g id="clust1" class="cluster">
<title>cluster_graph</title>
<polygon fill="none" stroke="white" points="8,-8 8,-523.91 665,-523.91 665,-8 8,-8"/>
</g>
<g id="clust7" class="cluster">
<title>cluster_legend</title>
<polygon fill="none" stroke="black" points="673,-460.42 673,-537.92 980,-537.92 980,-460.42 673,-460.42"/>
<text text-anchor="middle" x="826.5" y="-520.62" font-family="Times,serif" font-size="14.00">Next State Actions</text>
</g>
<!-- 6305415555724440256 -->
<g id="node1" class="node">
<title>6305415555724440256</title>
<ellipse fill="lightgrey" stroke="black" cx="356" cy="-486.92" rx="132.23" ry="28.99"/>
<text text-anchor="middle" x="356" y="-490.12" font-family="Times,serif" font-size="14.00">/\ flag = &lt;&lt;FALSE, FALSE&gt;&gt;</text>
<text text-anchor="middle" x="356" y="-473.62" font-family="Times,serif" font-size="14.00">/\ turn = 1</text>
</g>
<!-- 6305415555724440256&#45;&gt;6305415555724440256 -->
<g id="edge2" class="edge">
<title>6305415555724440256&#45;&gt;6305415555724440256</title>
<path fill="none" stroke="#b2df8a" d="M481.51,-496.34C500.42,-494.89 513.23,-491.75 513.23,-486.92 513.23,-483.11 505.25,-480.35 492.6,-478.65"/>
<polygon fill="#b2df8a" stroke="#b2df8a" points="493.32,-475.2 483.02,-477.66 492.61,-482.17 493.32,-475.2"/>
<text text-anchor="middle" x="524.48" y="-481.87" font-family="Times,serif" font-size="14.00" fill="#000000">Exit</text>
</g>
<!-- &#45;3613841557933027214 -->
<g id="node2" class="node">
<title>&#45;3613841557933027214</title>
<ellipse fill="none" stroke="black" cx="164" cy="-376.44" rx="127.99" ry="28.99"/>
<text text-anchor="middle" x="164" y="-379.64" font-family="Times,serif" font-size="14.00">/\ flag = &lt;&lt;TRUE, FALSE&gt;&gt;</text>
<text text-anchor="middle" x="164" y="-363.14" font-family="Times,serif" font-size="14.00">/\ turn = 1</text>
</g>
<!-- 6305415555724440256&#45;&gt;&#45;3613841557933027214 -->
<g id="edge1" class="edge">
<title>6305415555724440256&#45;&gt;&#45;3613841557933027214</title>
<path fill="none" stroke="#1f78b4" d="M297.7,-460.49C284.3,-454.16 270.24,-447.11 257.5,-439.93 241.87,-431.13 225.42,-420.59 210.74,-410.71"/>
<polygon fill="#1f78b4" stroke="#1f78b4" points="212.87,-407.92 202.64,-405.18 208.93,-413.7 212.87,-407.92"/>
<text text-anchor="middle" x="267.25" y="-426.63" font-family="Times,serif" font-size="14.00" fill="#000000">Try</text>
</g>
<!-- &#45;1010517958299390782 -->
<g id="node3" class="node">
<title>&#45;1010517958299390782</title>
<ellipse fill="none" stroke="black" cx="485" cy="-376.44" rx="127.46" ry="28.99"/>
<text text-anchor="middle" x="485" y="-379.64" font-family="Times,serif" font-size="14.00">/\ flag = &lt;&lt;FALSE, TRUE&gt;&gt;</text>
<text text-anchor="middle" x="485" y="-363.14" font-family="Times,serif" font-size="14.00">/\ turn = 1</text>
</g>
<!-- 6305415555724440256&#45;&gt;&#45;1010517958299390782 -->
<g id="edge3" class="edge">
<title>6305415555724440256&#45;&gt;&#45;1010517958299390782</title>
<path fill="none" stroke="#1f78b4" d="M384.64,-458.17C396.42,-447.08 410.37,-434.37 423.5,-423.43 428.24,-419.48 433.27,-415.46 438.34,-411.52"/>
<polygon fill="#1f78b4" stroke="#1f78b4" points="440.43,-414.33 446.24,-405.47 436.17,-408.77 440.43,-414.33"/>
<text text-anchor="middle" x="433.25" y="-426.63" font-family="Times,serif" font-size="14.00" fill="#000000">Try</text>
</g>
<!-- &#45;3613841557933027214&#45;&gt;6305415555724440256 -->
<g id="edge6" class="edge">
<title>&#45;3613841557933027214&#45;&gt;6305415555724440256</title>
<path fill="none" stroke="#b2df8a" d="M233.11,-401.15C248.63,-407.54 264.72,-415.05 279,-423.43 292.37,-431.28 305.86,-441.34 317.73,-451.09"/>
<polygon fill="#b2df8a" stroke="#b2df8a" points="315.4,-453.7 325.31,-457.46 319.91,-448.34 315.4,-453.7"/>
<text text-anchor="middle" x="312.85" y="-426.63" font-family="Times,serif" font-size="14.00" fill="#000000">Exit</text>
</g>
<!-- &#45;3613841557933027214&#45;&gt;&#45;3613841557933027214 -->
<g id="edge4" class="edge">
<title>&#45;3613841557933027214&#45;&gt;&#45;3613841557933027214</title>
<path fill="none" stroke="#b2df8a" d="M285.51,-385.91C304.24,-384.48 316.99,-381.32 316.99,-376.44 316.99,-372.63 309.21,-369.86 296.87,-368.16"/>
<polygon fill="#b2df8a" stroke="#b2df8a" points="297.32,-364.69 287.01,-367.13 296.59,-371.65 297.32,-364.69"/>
<text text-anchor="middle" x="328.24" y="-371.39" font-family="Times,serif" font-size="14.00" fill="#000000">Exit</text>
</g>
<!-- 1707807870883049515 -->
<g id="node4" class="node">
<title>1707807870883049515</title>
<ellipse fill="none" stroke="black" cx="144" cy="-265.96" rx="127.99" ry="28.99"/>
<text text-anchor="middle" x="144" y="-269.16" font-family="Times,serif" font-size="14.00">/\ flag = &lt;&lt;TRUE, FALSE&gt;&gt;</text>
<text text-anchor="middle" x="144" y="-252.66" font-family="Times,serif" font-size="14.00">/\ turn = 2</text>
</g>
<!-- &#45;3613841557933027214&#45;&gt;1707807870883049515 -->
<g id="edge5" class="edge">
<title>&#45;3613841557933027214&#45;&gt;1707807870883049515</title>
<path fill="none" stroke="#33a02c" d="M158.8,-347.22C156.5,-334.76 153.76,-319.9 151.27,-306.38"/>
<polygon fill="#33a02c" stroke="#33a02c" points="154.78,-306.1 149.52,-296.9 147.89,-307.37 154.78,-306.1"/>
<text text-anchor="middle" x="168.32" y="-316.15" font-family="Times,serif" font-size="14.00" fill="#000000">Give</text>
</g>
<!-- 7755676910325042800 -->
<g id="node5" class="node">
<title>7755676910325042800</title>
<ellipse fill="none" stroke="black" cx="461" cy="-265.96" rx="123.21" ry="28.99"/>
<text text-anchor="middle" x="461" y="-269.16" font-family="Times,serif" font-size="14.00">/\ flag = &lt;&lt;TRUE, TRUE&gt;&gt;</text>
<text text-anchor="middle" x="461" y="-252.66" font-family="Times,serif" font-size="14.00">/\ turn = 1</text>
</g>
<!-- &#45;3613841557933027214&#45;&gt;7755676910325042800 -->
<g id="edge7" class="edge">
<title>&#45;3613841557933027214&#45;&gt;7755676910325042800</title>
<path fill="none" stroke="#1f78b4" d="M220.2,-350.03C247.49,-338.1 280.93,-324.09 311.5,-312.95 331.29,-305.73 352.81,-298.67 373.19,-292.33"/>
<polygon fill="#1f78b4" stroke="#1f78b4" points="374.09,-295.71 382.61,-289.43 372.03,-289.02 374.09,-295.71"/>
<text text-anchor="middle" x="321.25" y="-316.15" font-family="Times,serif" font-size="14.00" fill="#000000">Try</text>
</g>
<!-- &#45;1010517958299390782&#45;&gt;6305415555724440256 -->
<g id="edge10" class="edge">
<title>&#45;1010517958299390782&#45;&gt;6305415555724440256</title>
<path fill="none" stroke="#b2df8a" d="M471.21,-405.6C464.49,-417.27 455.57,-430.3 445,-439.93 438.99,-445.41 432.21,-450.42 425.14,-454.95"/>
<polygon fill="#b2df8a" stroke="#b2df8a" points="423.42,-451.9 416.65,-460.05 427.03,-457.9 423.42,-451.9"/>
<text text-anchor="middle" x="469.77" y="-426.63" font-family="Times,serif" font-size="14.00" fill="#000000">Exit</text>
</g>
<!-- &#45;1010517958299390782&#45;&gt;&#45;1010517958299390782 -->
<g id="edge9" class="edge">
<title>&#45;1010517958299390782&#45;&gt;&#45;1010517958299390782</title>
<path fill="none" stroke="#33a02c" d="M606.09,-385.91C624.75,-384.48 637.46,-381.32 637.46,-376.44 637.46,-372.63 629.7,-369.86 617.41,-368.16"/>
<polygon fill="#33a02c" stroke="#33a02c" points="617.9,-364.69 607.59,-367.13 617.17,-371.65 617.9,-364.69"/>
<text text-anchor="middle" x="650.58" y="-371.39" font-family="Times,serif" font-size="14.00" fill="#000000">Give</text>
</g>
<!-- &#45;1010517958299390782&#45;&gt;7755676910325042800 -->
<g id="edge8" class="edge">
<title>&#45;1010517958299390782&#45;&gt;7755676910325042800</title>
<path fill="none" stroke="#1f78b4" d="M457.65,-347.88C453.49,-342.2 449.82,-335.95 447.5,-329.45 444.87,-322.07 444.72,-314.01 445.88,-306.21"/>
<polygon fill="#1f78b4" stroke="#1f78b4" points="449.27,-307.07 448.04,-296.55 442.44,-305.54 449.27,-307.07"/>
<text text-anchor="middle" x="457.25" y="-316.15" font-family="Times,serif" font-size="14.00" fill="#000000">Try</text>
</g>
<!-- 1707807870883049515&#45;&gt;1707807870883049515 -->
<g id="edge11" class="edge">
<title>1707807870883049515&#45;&gt;1707807870883049515</title>
<path fill="none" stroke="#b2df8a" d="M265.51,-275.43C284.24,-274 296.99,-270.84 296.99,-265.96 296.99,-262.14 289.21,-259.38 276.87,-257.67"/>
<polygon fill="#b2df8a" stroke="#b2df8a" points="277.32,-254.2 267.01,-256.65 276.59,-261.16 277.32,-254.2"/>
<text text-anchor="middle" x="308.24" y="-260.91" font-family="Times,serif" font-size="14.00" fill="#000000">Exit</text>
</g>
<!-- &#45;8220473948061609319 -->
<g id="node6" class="node">
<title>&#45;8220473948061609319</title>
<ellipse fill="none" stroke="black" cx="148" cy="-155.47" rx="132.23" ry="28.99"/>
<text text-anchor="middle" x="148" y="-158.67" font-family="Times,serif" font-size="14.00">/\ flag = &lt;&lt;FALSE, FALSE&gt;&gt;</text>
<text text-anchor="middle" x="148" y="-142.17" font-family="Times,serif" font-size="14.00">/\ turn = 2</text>
</g>
<!-- 1707807870883049515&#45;&gt;&#45;8220473948061609319 -->
<g id="edge12" class="edge">
<title>1707807870883049515&#45;&gt;&#45;8220473948061609319</title>
<path fill="none" stroke="#b2df8a" d="M123.92,-237.08C118.57,-226.43 115.1,-214.05 118.5,-202.47 119.27,-199.85 120.23,-197.25 121.34,-194.69"/>
<polygon fill="#b2df8a" stroke="#b2df8a" points="124.45,-196.28 125.89,-185.79 118.22,-193.1 124.45,-196.28"/>
<text text-anchor="middle" x="129.75" y="-205.67" font-family="Times,serif" font-size="14.00" fill="#000000">Exit</text>
</g>
<!-- &#45;5635155994047828439 -->
<g id="node7" class="node">
<title>&#45;5635155994047828439</title>
<ellipse fill="none" stroke="black" cx="469" cy="-155.47" rx="123.21" ry="28.99"/>
<text text-anchor="middle" x="469" y="-158.67" font-family="Times,serif" font-size="14.00">/\ flag = &lt;&lt;TRUE, TRUE&gt;&gt;</text>
<text text-anchor="middle" x="469" y="-142.17" font-family="Times,serif" font-size="14.00">/\ turn = 2</text>
</g>
<!-- 1707807870883049515&#45;&gt;&#45;5635155994047828439 -->
<g id="edge13" class="edge">
<title>1707807870883049515&#45;&gt;&#45;5635155994047828439</title>
<path fill="none" stroke="#1f78b4" d="M214.52,-241.42C265.69,-224.34 335.02,-201.2 388.38,-183.38"/>
<polygon fill="#1f78b4" stroke="#1f78b4" points="389.36,-186.75 397.74,-180.26 387.15,-180.11 389.36,-186.75"/>
<text text-anchor="middle" x="335.71" y="-205.67" font-family="Times,serif" font-size="14.00" fill="#000000">Try</text>
</g>
<!-- 7755676910325042800&#45;&gt;&#45;3613841557933027214 -->
<g id="edge17" class="edge">
<title>7755676910325042800&#45;&gt;&#45;3613841557933027214</title>
<path fill="none" stroke="#b2df8a" d="M413.02,-293.05C389.39,-305.21 360.19,-319.21 333,-329.45 310.52,-337.91 285.82,-345.53 262.42,-352.02"/>
<polygon fill="#b2df8a" stroke="#b2df8a" points="261.6,-348.61 252.87,-354.62 263.44,-355.37 261.6,-348.61"/>
<text text-anchor="middle" x="380.31" y="-316.15" font-family="Times,serif" font-size="14.00" fill="#000000">Exit</text>
</g>
<!-- 7755676910325042800&#45;&gt;&#45;1010517958299390782 -->
<g id="edge16" class="edge">
<title>7755676910325042800&#45;&gt;&#45;1010517958299390782</title>
<path fill="none" stroke="#b2df8a" d="M467.21,-295.03C469.99,-307.57 473.3,-322.56 476.32,-336.18"/>
<polygon fill="#b2df8a" stroke="#b2df8a" points="472.85,-336.73 478.43,-345.74 479.69,-335.22 472.85,-336.73"/>
<text text-anchor="middle" x="485.69" y="-316.15" font-family="Times,serif" font-size="14.00" fill="#000000">Exit</text>
</g>
<!-- 7755676910325042800&#45;&gt;7755676910325042800 -->
<g id="edge14" class="edge">
<title>7755676910325042800&#45;&gt;7755676910325042800</title>
<path fill="none" stroke="#33a02c" d="M577.81,-275.5C596.45,-274.1 609.21,-270.92 609.21,-265.96 609.21,-262.08 601.42,-259.29 589.13,-257.59"/>
<polygon fill="#33a02c" stroke="#33a02c" points="589.62,-254.12 579.31,-256.57 588.9,-261.09 589.62,-254.12"/>
<text text-anchor="middle" x="622.34" y="-260.91" font-family="Times,serif" font-size="14.00" fill="#000000">Give</text>
</g>
<!-- 7755676910325042800&#45;&gt;&#45;5635155994047828439 -->
<g id="edge15" class="edge">
<title>7755676910325042800&#45;&gt;&#45;5635155994047828439</title>
<path fill="none" stroke="#33a02c" d="M463.08,-236.74C463.99,-224.4 465.07,-209.72 466.06,-196.3"/>
<polygon fill="#33a02c" stroke="#33a02c" points="469.55,-196.67 466.79,-186.44 462.56,-196.15 469.55,-196.67"/>
<text text-anchor="middle" x="478.6" y="-205.67" font-family="Times,serif" font-size="14.00" fill="#000000">Give</text>
</g>
<!-- &#45;8220473948061609319&#45;&gt;1707807870883049515 -->
<g id="edge18" class="edge">
<title>&#45;8220473948061609319&#45;&gt;1707807870883049515</title>
<path fill="none" stroke="#1f78b4" d="M146.95,-184.93C146.49,-197.29 145.95,-211.98 145.46,-225.38"/>
<polygon fill="#1f78b4" stroke="#1f78b4" points="141.97,-225.1 145.1,-235.23 148.96,-225.36 141.97,-225.1"/>
<text text-anchor="middle" x="155.99" y="-205.67" font-family="Times,serif" font-size="14.00" fill="#000000">Try</text>
</g>
<!-- &#45;8220473948061609319&#45;&gt;&#45;8220473948061609319 -->
<g id="edge19" class="edge">
<title>&#45;8220473948061609319&#45;&gt;&#45;8220473948061609319</title>
<path fill="none" stroke="#b2df8a" d="M273.51,-164.89C292.42,-163.44 305.23,-160.3 305.23,-155.47 305.23,-151.66 297.25,-148.91 284.6,-147.2"/>
<polygon fill="#b2df8a" stroke="#b2df8a" points="285.32,-143.75 275.02,-146.21 284.61,-150.72 285.32,-143.75"/>
<text text-anchor="middle" x="316.48" y="-150.42" font-family="Times,serif" font-size="14.00" fill="#000000">Exit</text>
</g>
<!-- 3140063580371242139 -->
<g id="node8" class="node">
<title>3140063580371242139</title>
<ellipse fill="none" stroke="black" cx="419" cy="-44.99" rx="127.46" ry="28.99"/>
<text text-anchor="middle" x="419" y="-48.19" font-family="Times,serif" font-size="14.00">/\ flag = &lt;&lt;FALSE, TRUE&gt;&gt;</text>
<text text-anchor="middle" x="419" y="-31.69" font-family="Times,serif" font-size="14.00">/\ turn = 2</text>
</g>
<!-- &#45;8220473948061609319&#45;&gt;3140063580371242139 -->
<g id="edge20" class="edge">
<title>&#45;8220473948061609319&#45;&gt;3140063580371242139</title>
<path fill="none" stroke="#1f78b4" d="M210.17,-129.59C250.8,-113.32 304.01,-92.02 346.55,-75"/>
<polygon fill="#1f78b4" stroke="#1f78b4" points="347.73,-78.29 355.71,-71.33 345.13,-71.79 347.73,-78.29"/>
<text text-anchor="middle" x="309.48" y="-95.18" font-family="Times,serif" font-size="14.00" fill="#000000">Try</text>
</g>
<!-- &#45;5635155994047828439&#45;&gt;1707807870883049515 -->
<g id="edge24" class="edge">
<title>&#45;5635155994047828439&#45;&gt;1707807870883049515</title>
<path fill="none" stroke="#b2df8a" d="M377.4,-175.23C326.09,-185.96 270.11,-198.13 258.5,-202.47 237.28,-210.39 215.16,-221.66 196.09,-232.45"/>
<polygon fill="#b2df8a" stroke="#b2df8a" points="194.34,-229.42 187.43,-237.45 197.84,-235.48 194.34,-229.42"/>
<text text-anchor="middle" x="269.75" y="-205.67" font-family="Times,serif" font-size="14.00" fill="#000000">Exit</text>
</g>
<!-- &#45;5635155994047828439&#45;&gt;7755676910325042800 -->
<g id="edge23" class="edge">
<title>&#45;5635155994047828439&#45;&gt;7755676910325042800</title>
<path fill="none" stroke="#33a02c" d="M442.55,-184.14C438.53,-189.81 434.98,-196.03 432.75,-202.47 429.99,-210.43 430.92,-218.77 433.7,-226.67"/>
<polygon fill="#33a02c" stroke="#33a02c" points="430.5,-228.09 437.85,-235.71 436.86,-225.17 430.5,-228.09"/>
<text text-anchor="middle" x="445.88" y="-205.67" font-family="Times,serif" font-size="14.00" fill="#000000">Give</text>
</g>
<!-- &#45;5635155994047828439&#45;&gt;&#45;5635155994047828439 -->
<g id="edge21" class="edge">
<title>&#45;5635155994047828439&#45;&gt;&#45;5635155994047828439</title>
<path fill="none" stroke="#1f78b4" d="M585.81,-165.01C604.45,-163.62 617.21,-160.44 617.21,-155.47 617.21,-151.6 609.42,-148.81 597.13,-147.11"/>
<polygon fill="#1f78b4" stroke="#1f78b4" points="597.62,-143.64 587.31,-146.09 596.9,-150.6 597.62,-143.64"/>
<text text-anchor="middle" x="626.96" y="-150.42" font-family="Times,serif" font-size="14.00" fill="#000000">Try</text>
</g>
<!-- &#45;5635155994047828439&#45;&gt;3140063580371242139 -->
<g id="edge22" class="edge">
<title>&#45;5635155994047828439&#45;&gt;3140063580371242139</title>
<path fill="none" stroke="#b2df8a" d="M455.99,-126.25C450.09,-113.45 443.02,-98.1 436.65,-84.28"/>
<polygon fill="#b2df8a" stroke="#b2df8a" points="439.94,-83.06 432.57,-75.44 433.58,-85.99 439.94,-83.06"/>
<text text-anchor="middle" x="458.24" y="-95.18" font-family="Times,serif" font-size="14.00" fill="#000000">Exit</text>
</g>
<!-- 3140063580371242139&#45;&gt;&#45;1010517958299390782 -->
<g id="edge27" class="edge">
<title>3140063580371242139&#45;&gt;&#45;1010517958299390782</title>
<path fill="none" stroke="#33a02c" d="M531.1,-59.19C572.98,-70.19 616.51,-90.19 642,-126.48 685.03,-187.76 680.25,-231.18 641,-294.95 625.91,-319.46 600.72,-336.85 574.93,-349.02"/>
<polygon fill="#33a02c" stroke="#33a02c" points="573.74,-345.72 566.03,-352.99 576.59,-352.11 573.74,-345.72"/>
<text text-anchor="middle" x="685.52" y="-205.67" font-family="Times,serif" font-size="14.00" fill="#000000">Give</text>
</g>
<!-- 3140063580371242139&#45;&gt;&#45;8220473948061609319 -->
<g id="edge28" class="edge">
<title>3140063580371242139&#45;&gt;&#45;8220473948061609319</title>
<path fill="none" stroke="#b2df8a" d="M321.76,-64.07C294.16,-70.98 264.55,-80.13 238.5,-91.98 221.96,-99.51 205.21,-110.07 190.7,-120.38"/>
<polygon fill="#b2df8a" stroke="#b2df8a" points="188.75,-117.47 182.73,-126.18 192.87,-123.12 188.75,-117.47"/>
<text text-anchor="middle" x="249.75" y="-95.18" font-family="Times,serif" font-size="14.00" fill="#000000">Exit</text>
</g>
<!-- 3140063580371242139&#45;&gt;&#45;5635155994047828439 -->
<g id="edge25" class="edge">
<title>3140063580371242139&#45;&gt;&#45;5635155994047828439</title>
<path fill="none" stroke="#1f78b4" d="M411.85,-74.43C410.47,-85.5 410.69,-98.01 415.5,-108.48 417.24,-112.27 419.46,-115.86 422,-119.24"/>
<polygon fill="#1f78b4" stroke="#1f78b4" points="419.17,-121.32 428.38,-126.55 424.44,-116.72 419.17,-121.32"/>
<text text-anchor="middle" x="425.25" y="-95.18" font-family="Times,serif" font-size="14.00" fill="#000000">Try</text>
</g>
<!-- 3140063580371242139&#45;&gt;3140063580371242139 -->
<g id="edge26" class="edge">
<title>3140063580371242139&#45;&gt;3140063580371242139</title>
<path fill="none" stroke="#fb9a99" d="M540.09,-54.46C558.75,-53.03 571.46,-49.87 571.46,-44.99 571.46,-41.18 563.7,-38.42 551.41,-36.71"/>
<polygon fill="#fb9a99" stroke="#fb9a99" points="551.9,-33.24 541.59,-35.68 551.17,-40.2 551.9,-33.24"/>
<text text-anchor="middle" x="586.08" y="-39.94" font-family="Times,serif" font-size="14.00" fill="#000000">Enter</text>
</g>
<!-- Give -->
<g id="node9" class="node">
<title>Give</title>
<polygon fill="#33a02c" stroke="black" points="681,-468.92 681,-504.92 735,-504.92 735,-468.92 681,-468.92"/>
<text text-anchor="middle" x="707.62" y="-481.87" font-family="Times,serif" font-size="14.00">Give</text>
</g>
<!-- Enter -->
<g id="node10" class="node">
<title>Enter</title>
<polygon fill="#fb9a99" stroke="black" points="760,-468.92 760,-504.92 814,-504.92 814,-468.92 760,-468.92"/>
<text text-anchor="middle" x="786.62" y="-481.87" font-family="Times,serif" font-size="14.00">Enter</text>
</g>
<!-- Try -->
<g id="node11" class="node">
<title>Try</title>
<polygon fill="#1f78b4" stroke="black" points="839,-468.92 839,-504.92 893,-504.92 893,-468.92 839,-468.92"/>
<text text-anchor="middle" x="865.75" y="-481.87" font-family="Times,serif" font-size="14.00">Try</text>
</g>
<!-- Exit -->
<g id="node12" class="node">
<title>Exit</title>
<polygon fill="#b2df8a" stroke="black" points="918,-468.92 918,-504.92 972,-504.92 972,-468.92 918,-468.92"/>
<text text-anchor="middle" x="944.75" y="-481.87" font-family="Times,serif" font-size="14.00">Exit</text>
</g>
</g>
</svg>