learning_tla/lamport_video/specs/TwoPhase.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="8096pt" height="1478pt"
 viewBox="0.00 0.00 8096.00 1478.06" 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 1474.06)">
<title>DiskGraph</title>
<polygon fill="white" stroke="none" points="-4,4 -4,-1474.06 8092,-1474.06 8092,4 -4,4"/>
<g id="clust1" class="cluster">
<title>cluster_graph</title>
<polygon fill="none" stroke="white" points="8,-8 8,-1462.06 7199,-1462.06 7199,-8 8,-8"/>
</g>
<g id="clust10" class="cluster">
<title>cluster_legend</title>
<polygon fill="none" stroke="black" points="7207,-1375.23 7207,-1452.73 8080,-1452.73 8080,-1375.23 7207,-1375.23"/>
<text text-anchor="middle" x="7643.5" y="-1435.43" font-family="Times,serif" font-size="14.00">Next State Actions</text>
</g>
<!-- &#45;7339139893955513500 -->
<g id="node1" class="node">
<title>&#45;7339139893955513500</title>
<ellipse fill="lightgrey" stroke="black" cx="3141" cy="-1401.73" rx="205.41" ry="52.33"/>
<text text-anchor="middle" x="3141" y="-1421.43" font-family="Times,serif" font-size="14.00">/\ msgs = {}</text>
<text text-anchor="middle" x="3141" y="-1404.93" font-family="Times,serif" font-size="14.00">/\ rmState = (r :&gt; &quot;working&quot; @@ s :&gt; &quot;working&quot;)</text>
<text text-anchor="middle" x="3141" y="-1388.43" font-family="Times,serif" font-size="14.00">/\ tmState = &quot;init&quot;</text>
<text text-anchor="middle" x="3141" y="-1371.93" font-family="Times,serif" font-size="14.00">/\ tmPrepared = {}</text>
</g>
<!-- &#45;8948466169862180932 -->
<g id="node2" class="node">
<title>&#45;8948466169862180932</title>
<ellipse fill="none" stroke="black" cx="3141" cy="-1244.58" rx="205.41" ry="52.33"/>
<text text-anchor="middle" x="3141" y="-1264.28" font-family="Times,serif" font-size="14.00">/\ msgs = {[type |&#45;&gt; &quot;Abort&quot;]}</text>
<text text-anchor="middle" x="3141" y="-1247.78" font-family="Times,serif" font-size="14.00">/\ rmState = (r :&gt; &quot;working&quot; @@ s :&gt; &quot;working&quot;)</text>
<text text-anchor="middle" x="3141" y="-1231.28" font-family="Times,serif" font-size="14.00">/\ tmState = &quot;done&quot;</text>
<text text-anchor="middle" x="3141" y="-1214.78" font-family="Times,serif" font-size="14.00">/\ tmPrepared = {}</text>
</g>
<!-- &#45;7339139893955513500&#45;&gt;&#45;8948466169862180932 -->
<g id="edge1" class="edge">
<title>&#45;7339139893955513500&#45;&gt;&#45;8948466169862180932</title>
<path fill="none" stroke="#1f78b4" d="M3141,-1349.07C3141,-1336.05 3141,-1321.94 3141,-1308.44"/>
<polygon fill="#1f78b4" stroke="#1f78b4" points="3144.5,-1308.8 3141,-1298.8 3137.5,-1308.8 3144.5,-1308.8"/>
<text text-anchor="middle" x="3167.25" y="-1318.11" font-family="Times,serif" font-size="14.00" fill="#000000">TMAbort</text>
</g>
<!-- 5550303892963647981 -->
<g id="node3" class="node">
<title>5550303892963647981</title>
<ellipse fill="none" stroke="black" cx="1965" cy="-1244.58" rx="207.01" ry="52.33"/>
<text text-anchor="middle" x="1965" y="-1264.28" font-family="Times,serif" font-size="14.00">/\ msgs = {[type |&#45;&gt; &quot;Prepared&quot;, rm |&#45;&gt; r]}</text>
<text text-anchor="middle" x="1965" y="-1247.78" font-family="Times,serif" font-size="14.00">/\ rmState = (r :&gt; &quot;prepared&quot; @@ s :&gt; &quot;working&quot;)</text>
<text text-anchor="middle" x="1965" y="-1231.28" font-family="Times,serif" font-size="14.00">/\ tmState = &quot;init&quot;</text>
<text text-anchor="middle" x="1965" y="-1214.78" font-family="Times,serif" font-size="14.00">/\ tmPrepared = {}</text>
</g>
<!-- &#45;7339139893955513500&#45;&gt;5550303892963647981 -->
<g id="edge2" class="edge">
<title>&#45;7339139893955513500&#45;&gt;5550303892963647981</title>
<path fill="none" stroke="#b2df8a" d="M2959.51,-1376.79C2742.43,-1348.15 2380.58,-1300.41 2158.37,-1271.09"/>
<polygon fill="#b2df8a" stroke="#b2df8a" points="2159.11,-1267.66 2148.74,-1269.82 2158.2,-1274.6 2159.11,-1267.66"/>
<text text-anchor="middle" x="2619.76" y="-1318.11" font-family="Times,serif" font-size="14.00" fill="#000000">RMPrepare</text>
</g>
<!-- &#45;1686421403185681449 -->
<g id="node4" class="node">
<title>&#45;1686421403185681449</title>
<ellipse fill="none" stroke="black" cx="3748" cy="-1244.58" rx="202.23" ry="52.33"/>
<text text-anchor="middle" x="3748" y="-1264.28" font-family="Times,serif" font-size="14.00">/\ msgs = {}</text>
<text text-anchor="middle" x="3748" y="-1247.78" font-family="Times,serif" font-size="14.00">/\ rmState = (r :&gt; &quot;aborted&quot; @@ s :&gt; &quot;working&quot;)</text>
<text text-anchor="middle" x="3748" y="-1231.28" font-family="Times,serif" font-size="14.00">/\ tmState = &quot;init&quot;</text>
<text text-anchor="middle" x="3748" y="-1214.78" font-family="Times,serif" font-size="14.00">/\ tmPrepared = {}</text>
</g>
<!-- &#45;7339139893955513500&#45;&gt;&#45;1686421403185681449 -->
<g id="edge3" class="edge">
<title>&#45;7339139893955513500&#45;&gt;&#45;1686421403185681449</title>
<path fill="none" stroke="#33a02c" d="M3284.85,-1363.96C3378.1,-1340.13 3499.47,-1309.11 3594.57,-1284.8"/>
<polygon fill="#33a02c" stroke="#33a02c" points="3595.16,-1288.26 3603.98,-1282.39 3593.42,-1281.48 3595.16,-1288.26"/>
<text text-anchor="middle" x="3517.08" y="-1318.11" font-family="Times,serif" font-size="14.00" fill="#000000">RMChooseToAbort</text>
</g>
<!-- &#45;1185406630426197321 -->
<g id="node5" class="node">
<title>&#45;1185406630426197321</title>
<ellipse fill="none" stroke="black" cx="4642" cy="-1244.58" rx="207.01" ry="52.33"/>
<text text-anchor="middle" x="4642" y="-1264.28" font-family="Times,serif" font-size="14.00">/\ msgs = {[type |&#45;&gt; &quot;Prepared&quot;, rm |&#45;&gt; s]}</text>
<text text-anchor="middle" x="4642" y="-1247.78" font-family="Times,serif" font-size="14.00">/\ rmState = (r :&gt; &quot;working&quot; @@ s :&gt; &quot;prepared&quot;)</text>
<text text-anchor="middle" x="4642" y="-1231.28" font-family="Times,serif" font-size="14.00">/\ tmState = &quot;init&quot;</text>
<text text-anchor="middle" x="4642" y="-1214.78" font-family="Times,serif" font-size="14.00">/\ tmPrepared = {}</text>
</g>
<!-- &#45;7339139893955513500&#45;&gt;&#45;1185406630426197321 -->
<g id="edge4" class="edge">
<title>&#45;7339139893955513500&#45;&gt;&#45;1185406630426197321</title>
<path fill="none" stroke="#b2df8a" d="M3330.34,-1381.16C3614.45,-1351.8 4148.72,-1296.57 4440.04,-1266.46"/>
<polygon fill="#b2df8a" stroke="#b2df8a" points="4440.06,-1269.97 4449.65,-1265.46 4439.34,-1263.01 4440.06,-1269.97"/>
<text text-anchor="middle" x="3968.01" y="-1318.11" font-family="Times,serif" font-size="14.00" fill="#000000">RMPrepare</text>
</g>
<!-- &#45;8368542034928358435 -->
<g id="node6" class="node">
<title>&#45;8368542034928358435</title>
<ellipse fill="none" stroke="black" cx="2639" cy="-1244.58" rx="202.23" ry="52.33"/>
<text text-anchor="middle" x="2639" y="-1264.28" font-family="Times,serif" font-size="14.00">/\ msgs = {}</text>
<text text-anchor="middle" x="2639" y="-1247.78" font-family="Times,serif" font-size="14.00">/\ rmState = (r :&gt; &quot;working&quot; @@ s :&gt; &quot;aborted&quot;)</text>
<text text-anchor="middle" x="2639" y="-1231.28" font-family="Times,serif" font-size="14.00">/\ tmState = &quot;init&quot;</text>
<text text-anchor="middle" x="2639" y="-1214.78" font-family="Times,serif" font-size="14.00">/\ tmPrepared = {}</text>
</g>
<!-- &#45;7339139893955513500&#45;&gt;&#45;8368542034928358435 -->
<g id="edge5" class="edge">
<title>&#45;7339139893955513500&#45;&gt;&#45;8368542034928358435</title>
<path fill="none" stroke="#33a02c" d="M3011.72,-1360.78C2940.15,-1338.66 2851.15,-1311.15 2778.07,-1288.56"/>
<polygon fill="#33a02c" stroke="#33a02c" points="2779.44,-1285.32 2768.85,-1285.71 2777.37,-1292.01 2779.44,-1285.32"/>
<text text-anchor="middle" x="2959.43" y="-1318.11" font-family="Times,serif" font-size="14.00" fill="#000000">RMChooseToAbort</text>
</g>
<!-- &#45;1911478502538603270 -->
<g id="node7" class="node">
<title>&#45;1911478502538603270</title>
<ellipse fill="none" stroke="black" cx="1965" cy="-1087.43" rx="253.14" ry="52.33"/>
<text text-anchor="middle" x="1965" y="-1107.13" font-family="Times,serif" font-size="14.00">/\ msgs = {[type |&#45;&gt; &quot;Abort&quot;], [type |&#45;&gt; &quot;Prepared&quot;, rm |&#45;&gt; r]}</text>
<text text-anchor="middle" x="1965" y="-1090.63" font-family="Times,serif" font-size="14.00">/\ rmState = (r :&gt; &quot;prepared&quot; @@ s :&gt; &quot;working&quot;)</text>
<text text-anchor="middle" x="1965" y="-1074.13" font-family="Times,serif" font-size="14.00">/\ tmState = &quot;done&quot;</text>
<text text-anchor="middle" x="1965" y="-1057.63" font-family="Times,serif" font-size="14.00">/\ tmPrepared = {}</text>
</g>
<!-- &#45;8948466169862180932&#45;&gt;&#45;1911478502538603270 -->
<g id="edge6" class="edge">
<title>&#45;8948466169862180932&#45;&gt;&#45;1911478502538603270</title>
<path fill="none" stroke="#b2df8a" d="M2976.14,-1212.97C2936.21,-1205.87 2893.62,-1198.55 2854,-1192.26 2799.05,-1183.52 2661.4,-1162.92 2606,-1157.76 2439.42,-1142.21 2396.11,-1159.71 2230,-1139.76 2204.03,-1136.64 2176.79,-1132.44 2150.07,-1127.78"/>
<polygon fill="#b2df8a" stroke="#b2df8a" points="2151.01,-1124.39 2140.55,-1126.09 2149.78,-1131.28 2151.01,-1124.39"/>
<text text-anchor="middle" x="2761.67" y="-1160.96" font-family="Times,serif" font-size="14.00" fill="#000000">RMPrepare</text>
</g>
<!-- &#45;1049854520183359729 -->
<g id="node8" class="node">
<title>&#45;1049854520183359729</title>
<ellipse fill="none" stroke="black" cx="4043" cy="-1087.43" rx="202.23" ry="52.33"/>
<text text-anchor="middle" x="4043" y="-1107.13" font-family="Times,serif" font-size="14.00">/\ msgs = {[type |&#45;&gt; &quot;Abort&quot;]}</text>
<text text-anchor="middle" x="4043" y="-1090.63" font-family="Times,serif" font-size="14.00">/\ rmState = (r :&gt; &quot;aborted&quot; @@ s :&gt; &quot;working&quot;)</text>
<text text-anchor="middle" x="4043" y="-1074.13" font-family="Times,serif" font-size="14.00">/\ tmState = &quot;done&quot;</text>
<text text-anchor="middle" x="4043" y="-1057.63" font-family="Times,serif" font-size="14.00">/\ tmPrepared = {}</text>
</g>
<!-- &#45;8948466169862180932&#45;&gt;&#45;1049854520183359729 -->
<g id="edge7" class="edge">
<title>&#45;8948466169862180932&#45;&gt;&#45;1049854520183359729</title>
<path fill="none" stroke="#fb9a99" d="M3323.61,-1220.25C3462.46,-1201.49 3657.94,-1172.84 3828,-1139.76 3847.47,-1135.97 3867.84,-1131.62 3887.95,-1127.09"/>
<polygon fill="#fb9a99" stroke="#fb9a99" points="3888.64,-1130.52 3897.61,-1124.89 3887.09,-1123.69 3888.64,-1130.52"/>
<text text-anchor="middle" x="3766.07" y="-1160.96" font-family="Times,serif" font-size="14.00" fill="#000000">RMRcvAbortMsg</text>
</g>
<!-- 5184528711973156768 -->
<g id="node9" class="node">
<title>5184528711973156768</title>
<ellipse fill="none" stroke="black" cx="4642" cy="-1087.43" rx="253.67" ry="52.33"/>
<text text-anchor="middle" x="4642" y="-1107.13" font-family="Times,serif" font-size="14.00">/\ msgs = {[type |&#45;&gt; &quot;Abort&quot;], [type |&#45;&gt; &quot;Prepared&quot;, rm |&#45;&gt; s]}</text>
<text text-anchor="middle" x="4642" y="-1090.63" font-family="Times,serif" font-size="14.00">/\ rmState = (r :&gt; &quot;working&quot; @@ s :&gt; &quot;prepared&quot;)</text>
<text text-anchor="middle" x="4642" y="-1074.13" font-family="Times,serif" font-size="14.00">/\ tmState = &quot;done&quot;</text>
<text text-anchor="middle" x="4642" y="-1057.63" font-family="Times,serif" font-size="14.00">/\ tmPrepared = {}</text>
</g>
<!-- &#45;8948466169862180932&#45;&gt;5184528711973156768 -->
<g id="edge8" class="edge">
<title>&#45;8948466169862180932&#45;&gt;5184528711973156768</title>
<path fill="none" stroke="#b2df8a" d="M3316.75,-1217.2C3384.23,-1207.96 3462.05,-1198.37 3533,-1192.26 3723.57,-1175.82 3772.11,-1186.41 3963,-1174.26 4048.92,-1168.79 4070.21,-1164.95 4156,-1157.76 4253.32,-1149.6 4278.24,-1152.99 4375,-1139.76 4400.47,-1136.27 4427.19,-1131.95 4453.48,-1127.3"/>
<polygon fill="#b2df8a" stroke="#b2df8a" points="4454,-1130.76 4463.22,-1125.55 4452.76,-1123.87 4454,-1130.76"/>
<text text-anchor="middle" x="4187.5" y="-1160.96" font-family="Times,serif" font-size="14.00" fill="#000000">RMPrepare</text>
</g>
<!-- &#45;7914375883265526011 -->
<g id="node10" class="node">
<title>&#45;7914375883265526011</title>
<ellipse fill="none" stroke="black" cx="2445" cy="-1087.43" rx="202.23" ry="52.33"/>
<text text-anchor="middle" x="2445" y="-1107.13" font-family="Times,serif" font-size="14.00">/\ msgs = {[type |&#45;&gt; &quot;Abort&quot;]}</text>
<text text-anchor="middle" x="2445" y="-1090.63" font-family="Times,serif" font-size="14.00">/\ rmState = (r :&gt; &quot;working&quot; @@ s :&gt; &quot;aborted&quot;)</text>
<text text-anchor="middle" x="2445" y="-1074.13" font-family="Times,serif" font-size="14.00">/\ tmState = &quot;done&quot;</text>
<text text-anchor="middle" x="2445" y="-1057.63" font-family="Times,serif" font-size="14.00">/\ tmPrepared = {}</text>
</g>
<!-- &#45;8948466169862180932&#45;&gt;&#45;7914375883265526011 -->
<g id="edge9" class="edge">
<title>&#45;8948466169862180932&#45;&gt;&#45;7914375883265526011</title>
<path fill="none" stroke="#fb9a99" d="M3056.76,-1196.5C3026.76,-1181.74 2992.17,-1166.92 2959,-1157.76 2880.65,-1136.11 2857.64,-1149.97 2777,-1139.76 2727.64,-1133.51 2674.32,-1125.72 2625.15,-1118.12"/>
<polygon fill="#fb9a99" stroke="#fb9a99" points="2625.99,-1114.71 2615.57,-1116.63 2624.91,-1121.63 2625.99,-1114.71"/>
<text text-anchor="middle" x="3055.74" y="-1160.96" font-family="Times,serif" font-size="14.00" fill="#000000">RMRcvAbortMsg</text>
</g>
<!-- 5550303892963647981&#45;&gt;&#45;1911478502538603270 -->
<g id="edge10" class="edge">
<title>5550303892963647981&#45;&gt;&#45;1911478502538603270</title>
<path fill="none" stroke="#1f78b4" d="M1965,-1191.92C1965,-1178.9 1965,-1164.79 1965,-1151.29"/>
<polygon fill="#1f78b4" stroke="#1f78b4" points="1968.5,-1151.65 1965,-1141.65 1961.5,-1151.65 1968.5,-1151.65"/>
<text text-anchor="middle" x="1991.25" y="-1160.96" font-family="Times,serif" font-size="14.00" fill="#000000">TMAbort</text>
</g>
<!-- &#45;7232903358684417468 -->
<g id="node11" class="node">
<title>&#45;7232903358684417468</title>
<ellipse fill="none" stroke="black" cx="835" cy="-1087.43" rx="207.01" ry="52.33"/>
<text text-anchor="middle" x="835" y="-1107.13" font-family="Times,serif" font-size="14.00">/\ msgs = {[type |&#45;&gt; &quot;Prepared&quot;, rm |&#45;&gt; r]}</text>
<text text-anchor="middle" x="835" y="-1090.63" font-family="Times,serif" font-size="14.00">/\ rmState = (r :&gt; &quot;prepared&quot; @@ s :&gt; &quot;working&quot;)</text>
<text text-anchor="middle" x="835" y="-1074.13" font-family="Times,serif" font-size="14.00">/\ tmState = &quot;init&quot;</text>
<text text-anchor="middle" x="835" y="-1057.63" font-family="Times,serif" font-size="14.00">/\ tmPrepared = {r}</text>
</g>
<!-- 5550303892963647981&#45;&gt;&#45;7232903358684417468 -->
<g id="edge11" class="edge">
<title>5550303892963647981&#45;&gt;&#45;7232903358684417468</title>
<path fill="none" stroke="#e31a1c" d="M1781.85,-1219.96C1623.52,-1199.37 1388.55,-1168.39 1184,-1139.76 1131.87,-1132.46 1075.41,-1124.28 1023.4,-1116.63"/>
<polygon fill="#e31a1c" stroke="#e31a1c" points="1023.93,-1113.17 1013.53,-1115.17 1022.91,-1120.09 1023.93,-1113.17"/>
<text text-anchor="middle" x="1465.39" y="-1160.96" font-family="Times,serif" font-size="14.00" fill="#000000">TMRcvPrepared</text>
</g>
<!-- &#45;4974900985114660661 -->
<g id="node12" class="node">
<title>&#45;4974900985114660661</title>
<ellipse fill="none" stroke="black" cx="3514" cy="-1087.43" rx="301.4" ry="52.33"/>
<text text-anchor="middle" x="3514" y="-1107.13" font-family="Times,serif" font-size="14.00">/\ msgs = {[type |&#45;&gt; &quot;Prepared&quot;, rm |&#45;&gt; r], [type |&#45;&gt; &quot;Prepared&quot;, rm |&#45;&gt; s]}</text>
<text text-anchor="middle" x="3514" y="-1090.63" font-family="Times,serif" font-size="14.00">/\ rmState = (r :&gt; &quot;prepared&quot; @@ s :&gt; &quot;prepared&quot;)</text>
<text text-anchor="middle" x="3514" y="-1074.13" font-family="Times,serif" font-size="14.00">/\ tmState = &quot;init&quot;</text>
<text text-anchor="middle" x="3514" y="-1057.63" font-family="Times,serif" font-size="14.00">/\ tmPrepared = {}</text>
</g>
<!-- 5550303892963647981&#45;&gt;&#45;4974900985114660661 -->
<g id="edge12" class="edge">
<title>5550303892963647981&#45;&gt;&#45;4974900985114660661</title>
<path fill="none" stroke="#b2df8a" d="M2147.55,-1219.56C2231.59,-1209.43 2332.71,-1198.54 2424,-1192.26 2729.16,-1171.24 2808.25,-1210.34 3112,-1174.26 3185.99,-1165.47 3266.5,-1149.57 3335.9,-1133.82"/>
<polygon fill="#b2df8a" stroke="#b2df8a" points="3336.5,-1137.28 3345.47,-1131.64 3334.94,-1130.45 3336.5,-1137.28"/>
<text text-anchor="middle" x="3243.76" y="-1160.96" font-family="Times,serif" font-size="14.00" fill="#000000">RMPrepare</text>
</g>
<!-- 6700361766525303124 -->
<g id="node13" class="node">
<title>6700361766525303124</title>
<ellipse fill="none" stroke="black" cx="1400" cy="-1087.43" rx="203.82" ry="52.33"/>
<text text-anchor="middle" x="1400" y="-1107.13" font-family="Times,serif" font-size="14.00">/\ msgs = {[type |&#45;&gt; &quot;Prepared&quot;, rm |&#45;&gt; r]}</text>
<text text-anchor="middle" x="1400" y="-1090.63" font-family="Times,serif" font-size="14.00">/\ rmState = (r :&gt; &quot;prepared&quot; @@ s :&gt; &quot;aborted&quot;)</text>
<text text-anchor="middle" x="1400" y="-1074.13" font-family="Times,serif" font-size="14.00">/\ tmState = &quot;init&quot;</text>
<text text-anchor="middle" x="1400" y="-1057.63" font-family="Times,serif" font-size="14.00">/\ tmPrepared = {}</text>
</g>
<!-- 5550303892963647981&#45;&gt;6700361766525303124 -->
<g id="edge13" class="edge">
<title>5550303892963647981&#45;&gt;6700361766525303124</title>
<path fill="none" stroke="#33a02c" d="M1826.06,-1205.43C1741.93,-1182.33 1634.66,-1152.87 1548.81,-1129.29"/>
<polygon fill="#33a02c" stroke="#33a02c" points="1549.94,-1125.98 1539.37,-1126.7 1548.09,-1132.73 1549.94,-1125.98"/>
<text text-anchor="middle" x="1753.82" y="-1160.96" font-family="Times,serif" font-size="14.00" fill="#000000">RMChooseToAbort</text>
</g>
<!-- &#45;1686421403185681449&#45;&gt;&#45;1049854520183359729 -->
<g id="edge14" class="edge">
<title>&#45;1686421403185681449&#45;&gt;&#45;1049854520183359729</title>
<path fill="none" stroke="#1f78b4" d="M3836.11,-1197.24C3870.33,-1179.24 3909.67,-1158.55 3944.79,-1140.08"/>
<polygon fill="#1f78b4" stroke="#1f78b4" points="3946.02,-1143.39 3953.24,-1135.64 3942.76,-1137.2 3946.02,-1143.39"/>
<text text-anchor="middle" x="3930.6" y="-1160.96" font-family="Times,serif" font-size="14.00" fill="#000000">TMAbort</text>
</g>
<!-- &#45;3226588047523633907 -->
<g id="node14" class="node">
<title>&#45;3226588047523633907</title>
<ellipse fill="none" stroke="black" cx="5124" cy="-1087.43" rx="203.82" ry="52.33"/>
<text text-anchor="middle" x="5124" y="-1107.13" font-family="Times,serif" font-size="14.00">/\ msgs = {[type |&#45;&gt; &quot;Prepared&quot;, rm |&#45;&gt; s]}</text>
<text text-anchor="middle" x="5124" y="-1090.63" font-family="Times,serif" font-size="14.00">/\ rmState = (r :&gt; &quot;aborted&quot; @@ s :&gt; &quot;prepared&quot;)</text>
<text text-anchor="middle" x="5124" y="-1074.13" font-family="Times,serif" font-size="14.00">/\ tmState = &quot;init&quot;</text>
<text text-anchor="middle" x="5124" y="-1057.63" font-family="Times,serif" font-size="14.00">/\ tmPrepared = {}</text>
</g>
<!-- &#45;1686421403185681449&#45;&gt;&#45;3226588047523633907 -->
<g id="edge15" class="edge">
<title>&#45;1686421403185681449&#45;&gt;&#45;3226588047523633907</title>
<path fill="none" stroke="#b2df8a" d="M3933.81,-1223.76C4157.52,-1199.96 4511.05,-1162.64 4573,-1157.76 4721.64,-1146.04 4760.43,-1161.08 4908,-1139.76 4928.87,-1136.74 4950.69,-1132.67 4972.09,-1128.13"/>
<polygon fill="#b2df8a" stroke="#b2df8a" points="4972.73,-1131.58 4981.76,-1126.04 4971.25,-1124.73 4972.73,-1131.58"/>
<text text-anchor="middle" x="4604.5" y="-1160.96" font-family="Times,serif" font-size="14.00" fill="#000000">RMPrepare</text>
</g>
<!-- &#45;476690147165211794 -->
<g id="node15" class="node">
<title>&#45;476690147165211794</title>
<ellipse fill="none" stroke="black" cx="2989" cy="-1087.43" rx="199.05" ry="52.33"/>
<text text-anchor="middle" x="2989" y="-1107.13" font-family="Times,serif" font-size="14.00">/\ msgs = {}</text>
<text text-anchor="middle" x="2989" y="-1090.63" font-family="Times,serif" font-size="14.00">/\ rmState = (r :&gt; &quot;aborted&quot; @@ s :&gt; &quot;aborted&quot;)</text>
<text text-anchor="middle" x="2989" y="-1074.13" font-family="Times,serif" font-size="14.00">/\ tmState = &quot;init&quot;</text>
<text text-anchor="middle" x="2989" y="-1057.63" font-family="Times,serif" font-size="14.00">/\ tmPrepared = {}</text>
</g>
<!-- &#45;1686421403185681449&#45;&gt;&#45;476690147165211794 -->
<g id="edge16" class="edge">
<title>&#45;1686421403185681449&#45;&gt;&#45;476690147165211794</title>
<path fill="none" stroke="#33a02c" d="M3588.99,-1211.91C3504.68,-1195.34 3399.31,-1174.97 3305,-1157.76 3258.42,-1149.25 3246.36,-1149.36 3200,-1139.76 3181.24,-1135.87 3161.62,-1131.51 3142.21,-1127.01"/>
<polygon fill="#33a02c" stroke="#33a02c" points="3143.15,-1123.63 3132.61,-1124.76 3141.55,-1130.45 3143.15,-1123.63"/>
<text text-anchor="middle" x="3444.28" y="-1160.96" font-family="Times,serif" font-size="14.00" fill="#000000">RMChooseToAbort</text>
</g>
<!-- &#45;1185406630426197321&#45;&gt;5184528711973156768 -->
<g id="edge17" class="edge">
<title>&#45;1185406630426197321&#45;&gt;5184528711973156768</title>
<path fill="none" stroke="#1f78b4" d="M4642,-1191.92C4642,-1178.9 4642,-1164.79 4642,-1151.29"/>
<polygon fill="#1f78b4" stroke="#1f78b4" points="4645.5,-1151.65 4642,-1141.65 4638.5,-1151.65 4645.5,-1151.65"/>
<text text-anchor="middle" x="4668.25" y="-1160.96" font-family="Times,serif" font-size="14.00" fill="#000000">TMAbort</text>
</g>
<!-- &#45;1185406630426197321&#45;&gt;&#45;4974900985114660661 -->
<g id="edge18" class="edge">
<title>&#45;1185406630426197321&#45;&gt;&#45;4974900985114660661</title>
<path fill="none" stroke="#b2df8a" d="M4494.82,-1207.38C4415.41,-1189.35 4315.4,-1169.04 4225,-1157.76 4049.73,-1135.88 4003.68,-1158.03 3828,-1139.76 3797.04,-1136.53 3764.49,-1132.24 3732.56,-1127.51"/>
<polygon fill="#b2df8a" stroke="#b2df8a" points="3733.2,-1124.07 3722.79,-1126.05 3732.16,-1130.99 3733.2,-1124.07"/>
<text text-anchor="middle" x="4360.34" y="-1160.96" font-family="Times,serif" font-size="14.00" fill="#000000">RMPrepare</text>
</g>
<!-- &#45;1185406630426197321&#45;&gt;&#45;3226588047523633907 -->
<g id="edge19" class="edge">
<title>&#45;1185406630426197321&#45;&gt;&#45;3226588047523633907</title>
<path fill="none" stroke="#33a02c" d="M4768.64,-1202.82C4835.89,-1181.17 4918.6,-1154.55 4987.3,-1132.43"/>
<polygon fill="#33a02c" stroke="#33a02c" points="4988.32,-1135.78 4996.77,-1129.39 4986.17,-1129.12 4988.32,-1135.78"/>
<text text-anchor="middle" x="4951.83" y="-1160.96" font-family="Times,serif" font-size="14.00" fill="#000000">RMChooseToAbort</text>
</g>
<!-- &#45;7225434331385223261 -->
<g id="node16" class="node">
<title>&#45;7225434331385223261</title>
<ellipse fill="none" stroke="black" cx="6026" cy="-1087.43" rx="207.01" ry="52.33"/>
<text text-anchor="middle" x="6026" y="-1107.13" font-family="Times,serif" font-size="14.00">/\ msgs = {[type |&#45;&gt; &quot;Prepared&quot;, rm |&#45;&gt; s]}</text>
<text text-anchor="middle" x="6026" y="-1090.63" font-family="Times,serif" font-size="14.00">/\ rmState = (r :&gt; &quot;working&quot; @@ s :&gt; &quot;prepared&quot;)</text>
<text text-anchor="middle" x="6026" y="-1074.13" font-family="Times,serif" font-size="14.00">/\ tmState = &quot;init&quot;</text>
<text text-anchor="middle" x="6026" y="-1057.63" font-family="Times,serif" font-size="14.00">/\ tmPrepared = {s}</text>
</g>
<!-- &#45;1185406630426197321&#45;&gt;&#45;7225434331385223261 -->
<g id="edge20" class="edge">
<title>&#45;1185406630426197321&#45;&gt;&#45;7225434331385223261</title>
<path fill="none" stroke="#e31a1c" d="M4830.09,-1222.5C5090.76,-1193.27 5559.76,-1140.7 5826.4,-1110.81"/>
<polygon fill="#e31a1c" stroke="#e31a1c" points="5826.71,-1114.29 5836.26,-1109.7 5825.93,-1107.34 5826.71,-1114.29"/>
<text text-anchor="middle" x="5420.87" y="-1160.96" font-family="Times,serif" font-size="14.00" fill="#000000">TMRcvPrepared</text>
</g>
<!-- &#45;8368542034928358435&#45;&gt;&#45;7914375883265526011 -->
<g id="edge21" class="edge">
<title>&#45;8368542034928358435&#45;&gt;&#45;7914375883265526011</title>
<path fill="none" stroke="#1f78b4" d="M2577.35,-1194.28C2557.63,-1178.51 2535.66,-1160.94 2515.37,-1144.71"/>
<polygon fill="#1f78b4" stroke="#1f78b4" points="2517.67,-1142.06 2507.67,-1138.55 2513.29,-1147.53 2517.67,-1142.06"/>
<text text-anchor="middle" x="2574.07" y="-1160.96" font-family="Times,serif" font-size="14.00" fill="#000000">TMAbort</text>
</g>
<!-- &#45;8368542034928358435&#45;&gt;6700361766525303124 -->
<g id="edge22" class="edge">
<title>&#45;8368542034928358435&#45;&gt;6700361766525303124</title>
<path fill="none" stroke="#b2df8a" d="M2468.79,-1215.94C2345.58,-1196.89 2174.89,-1172.44 2024,-1157.76 1880.01,-1143.75 1842.75,-1156.02 1699,-1139.76 1658.01,-1135.12 1614.12,-1128.51 1572.93,-1121.58"/>
<polygon fill="#b2df8a" stroke="#b2df8a" points="1573.61,-1118.15 1563.17,-1119.92 1572.44,-1125.05 1573.61,-1118.15"/>
<text text-anchor="middle" x="2190.73" y="-1160.96" font-family="Times,serif" font-size="14.00" fill="#000000">RMPrepare</text>
</g>
<!-- &#45;8368542034928358435&#45;&gt;&#45;476690147165211794 -->
<g id="edge23" class="edge">
<title>&#45;8368542034928358435&#45;&gt;&#45;476690147165211794</title>
<path fill="none" stroke="#33a02c" d="M2748.22,-1200.13C2768.51,-1191.75 2789.47,-1182.89 2809,-1174.26 2834.05,-1163.19 2860.8,-1150.77 2885.82,-1138.88"/>
<polygon fill="#33a02c" stroke="#33a02c" points="2887.16,-1142.12 2894.68,-1134.66 2884.15,-1135.8 2887.16,-1142.12"/>
<text text-anchor="middle" x="2898.15" y="-1160.96" font-family="Times,serif" font-size="14.00" fill="#000000">RMChooseToAbort</text>
</g>
<!-- &#45;633806864297459675 -->
<g id="node17" class="node">
<title>&#45;633806864297459675</title>
<ellipse fill="none" stroke="black" cx="1991" cy="-906.94" rx="253.14" ry="52.33"/>
<text text-anchor="middle" x="1991" y="-926.64" font-family="Times,serif" font-size="14.00">/\ msgs = {[type |&#45;&gt; &quot;Abort&quot;], [type |&#45;&gt; &quot;Prepared&quot;, rm |&#45;&gt; r]}</text>
<text text-anchor="middle" x="1991" y="-910.14" font-family="Times,serif" font-size="14.00">/\ rmState = (r :&gt; &quot;aborted&quot; @@ s :&gt; &quot;working&quot;)</text>
<text text-anchor="middle" x="1991" y="-893.64" font-family="Times,serif" font-size="14.00">/\ tmState = &quot;done&quot;</text>
<text text-anchor="middle" x="1991" y="-877.14" font-family="Times,serif" font-size="14.00">/\ tmPrepared = {}</text>
</g>
<!-- &#45;1911478502538603270&#45;&gt;&#45;633806864297459675 -->
<g id="edge24" class="edge">
<title>&#45;1911478502538603270&#45;&gt;&#45;633806864297459675</title>
<path fill="none" stroke="#fb9a99" d="M1972.52,-1034.8C1975.43,-1014.82 1978.79,-991.77 1981.84,-970.83"/>
<polygon fill="#fb9a99" stroke="#fb9a99" points="1985.3,-971.35 1983.28,-960.95 1978.37,-970.34 1985.3,-971.35"/>
<text text-anchor="middle" x="2027.1" y="-1003.8" font-family="Times,serif" font-size="14.00" fill="#000000">RMRcvAbortMsg</text>
</g>
<!-- 8301560317156807003 -->
<g id="node18" class="node">
<title>8301560317156807003</title>
<ellipse fill="none" stroke="black" cx="3872" cy="-906.94" rx="208.6" ry="75.66"/>
<text text-anchor="middle" x="3872" y="-943.14" font-family="Times,serif" font-size="14.00">/\ msgs = { [type |&#45;&gt; &quot;Abort&quot;],</text>
<text text-anchor="middle" x="3872" y="-926.64" font-family="Times,serif" font-size="14.00"> &#160;[type |&#45;&gt; &quot;Prepared&quot;, rm |&#45;&gt; r],</text>
<text text-anchor="middle" x="3872" y="-910.14" font-family="Times,serif" font-size="14.00"> &#160;[type |&#45;&gt; &quot;Prepared&quot;, rm |&#45;&gt; s] }</text>
<text text-anchor="middle" x="3872" y="-893.64" font-family="Times,serif" font-size="14.00">/\ rmState = (r :&gt; &quot;prepared&quot; @@ s :&gt; &quot;prepared&quot;)</text>
<text text-anchor="middle" x="3872" y="-877.14" font-family="Times,serif" font-size="14.00">/\ tmState = &quot;done&quot;</text>
<text text-anchor="middle" x="3872" y="-860.64" font-family="Times,serif" font-size="14.00">/\ tmPrepared = {}</text>
</g>
<!-- &#45;1911478502538603270&#45;&gt;8301560317156807003 -->
<g id="edge25" class="edge">
<title>&#45;1911478502538603270&#45;&gt;8301560317156807003</title>
<path fill="none" stroke="#b2df8a" d="M2136.83,-1048.63C2167.71,-1043.13 2199.7,-1038.27 2230,-1035.1 2468.29,-1010.23 3068.82,-1031.11 3308,-1017.1 3346.24,-1014.87 3613.56,-990.7 3651,-982.6 3672.6,-977.93 3695.03,-971.86 3716.96,-965.2"/>
<polygon fill="#b2df8a" stroke="#b2df8a" points="3717.72,-968.63 3726.24,-962.33 3715.65,-961.94 3717.72,-968.63"/>
<text text-anchor="middle" x="3520.45" y="-1003.8" font-family="Times,serif" font-size="14.00" fill="#000000">RMPrepare</text>
</g>
<!-- &#45;827602329687716797 -->
<g id="node19" class="node">
<title>&#45;827602329687716797</title>
<ellipse fill="none" stroke="black" cx="1342" cy="-906.94" rx="253.14" ry="52.33"/>
<text text-anchor="middle" x="1342" y="-926.64" font-family="Times,serif" font-size="14.00">/\ msgs = {[type |&#45;&gt; &quot;Abort&quot;], [type |&#45;&gt; &quot;Prepared&quot;, rm |&#45;&gt; r]}</text>
<text text-anchor="middle" x="1342" y="-910.14" font-family="Times,serif" font-size="14.00">/\ rmState = (r :&gt; &quot;prepared&quot; @@ s :&gt; &quot;aborted&quot;)</text>
<text text-anchor="middle" x="1342" y="-893.64" font-family="Times,serif" font-size="14.00">/\ tmState = &quot;done&quot;</text>
<text text-anchor="middle" x="1342" y="-877.14" font-family="Times,serif" font-size="14.00">/\ tmPrepared = {}</text>
</g>
<!-- &#45;1911478502538603270&#45;&gt;&#45;827602329687716797 -->
<g id="edge26" class="edge">
<title>&#45;1911478502538603270&#45;&gt;&#45;827602329687716797</title>
<path fill="none" stroke="#fb9a99" d="M1818.54,-1044.47C1722.68,-1017.01 1597.5,-981.14 1499.49,-953.06"/>
<polygon fill="#fb9a99" stroke="#fb9a99" points="1500.62,-949.75 1490.04,-950.36 1498.69,-956.48 1500.62,-949.75"/>
<text text-anchor="middle" x="1759.18" y="-1003.8" font-family="Times,serif" font-size="14.00" fill="#000000">RMRcvAbortMsg</text>
</g>
<!-- &#45;1049854520183359729&#45;&gt;&#45;1049854520183359729 -->
<g id="edge27" class="edge">
<title>&#45;1049854520183359729&#45;&gt;&#45;1049854520183359729</title>
<path fill="none" stroke="#fb9a99" d="M4240.51,-1099.19C4258.74,-1096.76 4270.23,-1092.84 4270.23,-1087.43 4270.23,-1083.25 4263.36,-1079.95 4251.81,-1077.55"/>
<polygon fill="#fb9a99" stroke="#fb9a99" points="4252.44,-1074.11 4242,-1075.92 4251.29,-1081.01 4252.44,-1074.11"/>
<text text-anchor="middle" x="4320.11" y="-1082.38" font-family="Times,serif" font-size="14.00" fill="#000000">RMRcvAbortMsg</text>
</g>
<!-- 8883184041786986522 -->
<g id="node20" class="node">
<title>8883184041786986522</title>
<ellipse fill="none" stroke="black" cx="5009" cy="-906.94" rx="253.67" ry="52.33"/>
<text text-anchor="middle" x="5009" y="-926.64" font-family="Times,serif" font-size="14.00">/\ msgs = {[type |&#45;&gt; &quot;Abort&quot;], [type |&#45;&gt; &quot;Prepared&quot;, rm |&#45;&gt; s]}</text>
<text text-anchor="middle" x="5009" y="-910.14" font-family="Times,serif" font-size="14.00">/\ rmState = (r :&gt; &quot;aborted&quot; @@ s :&gt; &quot;prepared&quot;)</text>
<text text-anchor="middle" x="5009" y="-893.64" font-family="Times,serif" font-size="14.00">/\ tmState = &quot;done&quot;</text>
<text text-anchor="middle" x="5009" y="-877.14" font-family="Times,serif" font-size="14.00">/\ tmPrepared = {}</text>
</g>
<!-- &#45;1049854520183359729&#45;&gt;8883184041786986522 -->
<g id="edge28" class="edge">
<title>&#45;1049854520183359729&#45;&gt;8883184041786986522</title>
<path fill="none" stroke="#b2df8a" d="M4210.76,-1057.8C4263.52,-1049.55 4322.08,-1041.14 4376,-1035.1 4489.35,-1022.41 4519.7,-1037.08 4632,-1017.1 4712.08,-1002.86 4799.45,-978.17 4869.9,-955.86"/>
<polygon fill="#b2df8a" stroke="#b2df8a" points="4870.71,-959.28 4879.17,-952.91 4868.58,-952.61 4870.71,-959.28"/>
<text text-anchor="middle" x="4736.95" y="-1003.8" font-family="Times,serif" font-size="14.00" fill="#000000">RMPrepare</text>
</g>
<!-- &#45;2263904760830070858 -->
<g id="node21" class="node">
<title>&#45;2263904760830070858</title>
<ellipse fill="none" stroke="black" cx="3322" cy="-906.94" rx="199.05" ry="52.33"/>
<text text-anchor="middle" x="3322" y="-926.64" font-family="Times,serif" font-size="14.00">/\ msgs = {[type |&#45;&gt; &quot;Abort&quot;]}</text>
<text text-anchor="middle" x="3322" y="-910.14" font-family="Times,serif" font-size="14.00">/\ rmState = (r :&gt; &quot;aborted&quot; @@ s :&gt; &quot;aborted&quot;)</text>
<text text-anchor="middle" x="3322" y="-893.64" font-family="Times,serif" font-size="14.00">/\ tmState = &quot;done&quot;</text>
<text text-anchor="middle" x="3322" y="-877.14" font-family="Times,serif" font-size="14.00">/\ tmPrepared = {}</text>
</g>
<!-- &#45;1049854520183359729&#45;&gt;&#45;2263904760830070858 -->
<g id="edge29" class="edge">
<title>&#45;1049854520183359729&#45;&gt;&#45;2263904760830070858</title>
<path fill="none" stroke="#fb9a99" d="M3897.96,-1050.53C3775.82,-1020.29 3601.54,-977.15 3476.74,-946.25"/>
<polygon fill="#fb9a99" stroke="#fb9a99" points="3477.59,-942.86 3467.04,-943.85 3475.91,-949.65 3477.59,-942.86"/>
<text text-anchor="middle" x="3796.95" y="-1003.8" font-family="Times,serif" font-size="14.00" fill="#000000">RMRcvAbortMsg</text>
</g>
<!-- 5184528711973156768&#45;&gt;8301560317156807003 -->
<g id="edge30" class="edge">
<title>5184528711973156768&#45;&gt;8301560317156807003</title>
<path fill="none" stroke="#b2df8a" d="M4466.58,-1049.33C4436.16,-1043.87 4404.74,-1038.83 4375,-1035.1 4241.14,-1018.34 4201.67,-1054.32 4072,-1017.1 4041.39,-1008.32 4010.25,-994.26 3981.95,-979.12"/>
<polygon fill="#b2df8a" stroke="#b2df8a" points="3983.84,-976.17 3973.39,-974.45 3980.49,-982.31 3983.84,-976.17"/>
<text text-anchor="middle" x="4103.5" y="-1003.8" font-family="Times,serif" font-size="14.00" fill="#000000">RMPrepare</text>
</g>
<!-- 5184528711973156768&#45;&gt;8883184041786986522 -->
<g id="edge31" class="edge">
<title>5184528711973156768&#45;&gt;8883184041786986522</title>
<path fill="none" stroke="#fb9a99" d="M4776.65,-1042.66C4796.84,-1034.86 4817.19,-1026.26 4836,-1017.1 4867.41,-1001.81 4900.23,-982.15 4928.74,-963.74"/>
<polygon fill="#fb9a99" stroke="#fb9a99" points="4930.5,-966.77 4936.96,-958.38 4926.67,-960.91 4930.5,-966.77"/>
<text text-anchor="middle" x="4915.54" y="-1003.8" font-family="Times,serif" font-size="14.00" fill="#000000">RMRcvAbortMsg</text>
</g>
<!-- 1202513148741259631 -->
<g id="node22" class="node">
<title>1202513148741259631</title>
<ellipse fill="none" stroke="black" cx="4359" cy="-906.94" rx="253.67" ry="52.33"/>
<text text-anchor="middle" x="4359" y="-926.64" font-family="Times,serif" font-size="14.00">/\ msgs = {[type |&#45;&gt; &quot;Abort&quot;], [type |&#45;&gt; &quot;Prepared&quot;, rm |&#45;&gt; s]}</text>
<text text-anchor="middle" x="4359" y="-910.14" font-family="Times,serif" font-size="14.00">/\ rmState = (r :&gt; &quot;working&quot; @@ s :&gt; &quot;aborted&quot;)</text>
<text text-anchor="middle" x="4359" y="-893.64" font-family="Times,serif" font-size="14.00">/\ tmState = &quot;done&quot;</text>
<text text-anchor="middle" x="4359" y="-877.14" font-family="Times,serif" font-size="14.00">/\ tmPrepared = {}</text>
</g>
<!-- 5184528711973156768&#45;&gt;1202513148741259631 -->
<g id="edge32" class="edge">
<title>5184528711973156768&#45;&gt;1202513148741259631</title>
<path fill="none" stroke="#fb9a99" d="M4563.92,-1037.19C4527.42,-1014.17 4483.82,-986.67 4446.24,-962.97"/>
<polygon fill="#fb9a99" stroke="#fb9a99" points="4448.43,-960.21 4438.11,-957.84 4444.7,-966.13 4448.43,-960.21"/>
<text text-anchor="middle" x="4575.72" y="-1003.8" font-family="Times,serif" font-size="14.00" fill="#000000">RMRcvAbortMsg</text>
</g>
<!-- &#45;7914375883265526011&#45;&gt;&#45;7914375883265526011 -->
<g id="edge35" class="edge">
<title>&#45;7914375883265526011&#45;&gt;&#45;7914375883265526011</title>
<path fill="none" stroke="#fb9a99" d="M2642.51,-1099.19C2660.74,-1096.76 2672.23,-1092.84 2672.23,-1087.43 2672.23,-1083.25 2665.36,-1079.95 2653.81,-1077.55"/>
<polygon fill="#fb9a99" stroke="#fb9a99" points="2654.44,-1074.11 2644,-1075.92 2653.29,-1081.01 2654.44,-1074.11"/>
<text text-anchor="middle" x="2722.11" y="-1082.38" font-family="Times,serif" font-size="14.00" fill="#000000">RMRcvAbortMsg</text>
</g>
<!-- &#45;7914375883265526011&#45;&gt;&#45;827602329687716797 -->
<g id="edge33" class="edge">
<title>&#45;7914375883265526011&#45;&gt;&#45;827602329687716797</title>
<path fill="none" stroke="#b2df8a" d="M2350.42,-1040.71C2313.42,-1025.01 2270.07,-1009.23 2229,-1000.6 2119.32,-977.58 1836.34,-995.37 1725,-982.6 1657.72,-974.89 1584.58,-961.82 1520.42,-948.75"/>
<polygon fill="#b2df8a" stroke="#b2df8a" points="1521.36,-945.37 1510.86,-946.78 1519.95,-952.22 1521.36,-945.37"/>
<text text-anchor="middle" x="2315.68" y="-1003.8" font-family="Times,serif" font-size="14.00" fill="#000000">RMPrepare</text>
</g>
<!-- &#45;7914375883265526011&#45;&gt;&#45;2263904760830070858 -->
<g id="edge34" class="edge">
<title>&#45;7914375883265526011&#45;&gt;&#45;2263904760830070858</title>
<path fill="none" stroke="#fb9a99" d="M2609.99,-1056.85C2710.71,-1039.31 2842.2,-1017.3 2959.25,-1000.6 3026.49,-991.01 3044.86,-998.03 3111,-982.6 3141.42,-975.51 3173.53,-965.51 3203.29,-955.13"/>
<polygon fill="#fb9a99" stroke="#fb9a99" points="3204.45,-958.43 3212.71,-951.8 3202.11,-951.83 3204.45,-958.43"/>
<text text-anchor="middle" x="3009.12" y="-1003.8" font-family="Times,serif" font-size="14.00" fill="#000000">RMRcvAbortMsg</text>
</g>
<!-- &#45;7232903358684417468&#45;&gt;&#45;7232903358684417468 -->
<g id="edge37" class="edge">
<title>&#45;7232903358684417468&#45;&gt;&#45;7232903358684417468</title>
<path fill="none" stroke="#e31a1c" d="M1037.06,-1099.14C1055.44,-1096.7 1067.01,-1092.8 1067.01,-1087.43 1067.01,-1083.23 1059.95,-1079.93 1048.09,-1077.53"/>
<polygon fill="#e31a1c" stroke="#e31a1c" points="1048.98,-1074.13 1038.55,-1075.97 1047.85,-1081.04 1048.98,-1074.13"/>
<text text-anchor="middle" x="1112.38" y="-1082.38" font-family="Times,serif" font-size="14.00" fill="#000000">TMRcvPrepared</text>
</g>
<!-- &#45;7496497296444535640 -->
<g id="node23" class="node">
<title>&#45;7496497296444535640</title>
<ellipse fill="none" stroke="black" cx="269" cy="-906.94" rx="253.14" ry="52.33"/>
<text text-anchor="middle" x="269" y="-926.64" font-family="Times,serif" font-size="14.00">/\ msgs = {[type |&#45;&gt; &quot;Abort&quot;], [type |&#45;&gt; &quot;Prepared&quot;, rm |&#45;&gt; r]}</text>
<text text-anchor="middle" x="269" y="-910.14" font-family="Times,serif" font-size="14.00">/\ rmState = (r :&gt; &quot;prepared&quot; @@ s :&gt; &quot;working&quot;)</text>
<text text-anchor="middle" x="269" y="-893.64" font-family="Times,serif" font-size="14.00">/\ tmState = &quot;done&quot;</text>
<text text-anchor="middle" x="269" y="-877.14" font-family="Times,serif" font-size="14.00">/\ tmPrepared = {r}</text>
</g>
<!-- &#45;7232903358684417468&#45;&gt;&#45;7496497296444535640 -->
<g id="edge36" class="edge">
<title>&#45;7232903358684417468&#45;&gt;&#45;7496497296444535640</title>
<path fill="none" stroke="#1f78b4" d="M706.92,-1046.04C620.9,-1018.91 507.28,-983.09 417.33,-954.72"/>
<polygon fill="#1f78b4" stroke="#1f78b4" points="418.52,-951.42 407.93,-951.75 416.41,-958.1 418.52,-951.42"/>
<text text-anchor="middle" x="628.95" y="-1003.8" font-family="Times,serif" font-size="14.00" fill="#000000">TMAbort</text>
</g>
<!-- &#45;4568132850329190210 -->
<g id="node24" class="node">
<title>&#45;4568132850329190210</title>
<ellipse fill="none" stroke="black" cx="2688" cy="-906.94" rx="301.4" ry="52.33"/>
<text text-anchor="middle" x="2688" y="-926.64" font-family="Times,serif" font-size="14.00">/\ msgs = {[type |&#45;&gt; &quot;Prepared&quot;, rm |&#45;&gt; r], [type |&#45;&gt; &quot;Prepared&quot;, rm |&#45;&gt; s]}</text>
<text text-anchor="middle" x="2688" y="-910.14" font-family="Times,serif" font-size="14.00">/\ rmState = (r :&gt; &quot;prepared&quot; @@ s :&gt; &quot;prepared&quot;)</text>
<text text-anchor="middle" x="2688" y="-893.64" font-family="Times,serif" font-size="14.00">/\ tmState = &quot;init&quot;</text>
<text text-anchor="middle" x="2688" y="-877.14" font-family="Times,serif" font-size="14.00">/\ tmPrepared = {r}</text>
</g>
<!-- &#45;7232903358684417468&#45;&gt;&#45;4568132850329190210 -->
<g id="edge38" class="edge">
<title>&#45;7232903358684417468&#45;&gt;&#45;4568132850329190210</title>
<path fill="none" stroke="#b2df8a" d="M1004.47,-1057.12C1061.35,-1048.46 1125.26,-1039.99 1184,-1035.1 1582.26,-1001.96 1686.03,-1063.18 2083,-1017.1 2117.77,-1013.07 2125.38,-1005.75 2160,-1000.6 2254.41,-986.58 2279.75,-997.69 2374,-982.6 2419.88,-975.26 2468.97,-964.85 2514.39,-954.11"/>
<polygon fill="#b2df8a" stroke="#b2df8a" points="2515.16,-957.53 2524.08,-951.81 2513.54,-950.72 2515.16,-957.53"/>
<text text-anchor="middle" x="2191.5" y="-1003.8" font-family="Times,serif" font-size="14.00" fill="#000000">RMPrepare</text>
</g>
<!-- 3521423533464532559 -->
<g id="node25" class="node">
<title>3521423533464532559</title>
<ellipse fill="none" stroke="black" cx="751" cy="-906.94" rx="203.82" ry="52.33"/>
<text text-anchor="middle" x="751" y="-926.64" font-family="Times,serif" font-size="14.00">/\ msgs = {[type |&#45;&gt; &quot;Prepared&quot;, rm |&#45;&gt; r]}</text>
<text text-anchor="middle" x="751" y="-910.14" font-family="Times,serif" font-size="14.00">/\ rmState = (r :&gt; &quot;prepared&quot; @@ s :&gt; &quot;aborted&quot;)</text>
<text text-anchor="middle" x="751" y="-893.64" font-family="Times,serif" font-size="14.00">/\ tmState = &quot;init&quot;</text>
<text text-anchor="middle" x="751" y="-877.14" font-family="Times,serif" font-size="14.00">/\ tmPrepared = {r}</text>
</g>
<!-- &#45;7232903358684417468&#45;&gt;3521423533464532559 -->
<g id="edge39" class="edge">
<title>&#45;7232903358684417468&#45;&gt;3521423533464532559</title>
<path fill="none" stroke="#33a02c" d="M810.93,-1035.28C801.26,-1014.75 790.04,-990.89 779.93,-969.42"/>
<polygon fill="#33a02c" stroke="#33a02c" points="783.14,-968.03 775.72,-960.47 776.81,-971.01 783.14,-968.03"/>
<text text-anchor="middle" x="854.9" y="-1003.8" font-family="Times,serif" font-size="14.00" fill="#000000">RMChooseToAbort</text>
</g>
<!-- &#45;4974900985114660661&#45;&gt;8301560317156807003 -->
<g id="edge40" class="edge">
<title>&#45;4974900985114660661&#45;&gt;8301560317156807003</title>
<path fill="none" stroke="#1f78b4" d="M3558.96,-1035.45C3572.03,-1022.78 3587,-1010.12 3602.5,-1000.6 3605.36,-998.85 3654.21,-981.93 3709.55,-963.03"/>
<polygon fill="#1f78b4" stroke="#1f78b4" points="3710.56,-966.38 3718.89,-959.84 3708.3,-959.76 3710.56,-966.38"/>
<text text-anchor="middle" x="3628.75" y="-1003.8" font-family="Times,serif" font-size="14.00" fill="#000000">TMAbort</text>
</g>
<!-- &#45;4974900985114660661&#45;&gt;&#45;4568132850329190210 -->
<g id="edge41" class="edge">
<title>&#45;4974900985114660661&#45;&gt;&#45;4568132850329190210</title>
<path fill="none" stroke="#e31a1c" d="M3335.2,-1044.96C3245.36,-1024.14 3153.3,-1002.84 3143,-1000.6 3062.4,-983.08 2973.55,-964.76 2895.92,-949.08"/>
<polygon fill="#e31a1c" stroke="#e31a1c" points="2897.02,-945.74 2886.53,-947.19 2895.64,-952.6 2897.02,-945.74"/>
<text text-anchor="middle" x="3259.4" y="-1003.8" font-family="Times,serif" font-size="14.00" fill="#000000">TMRcvPrepared</text>
</g>
<!-- &#45;4543075241127103799 -->
<g id="node26" class="node">
<title>&#45;4543075241127103799</title>
<ellipse fill="none" stroke="black" cx="5707" cy="-906.94" rx="301.4" ry="52.33"/>
<text text-anchor="middle" x="5707" y="-926.64" font-family="Times,serif" font-size="14.00">/\ msgs = {[type |&#45;&gt; &quot;Prepared&quot;, rm |&#45;&gt; r], [type |&#45;&gt; &quot;Prepared&quot;, rm |&#45;&gt; s]}</text>
<text text-anchor="middle" x="5707" y="-910.14" font-family="Times,serif" font-size="14.00">/\ rmState = (r :&gt; &quot;prepared&quot; @@ s :&gt; &quot;prepared&quot;)</text>
<text text-anchor="middle" x="5707" y="-893.64" font-family="Times,serif" font-size="14.00">/\ tmState = &quot;init&quot;</text>
<text text-anchor="middle" x="5707" y="-877.14" font-family="Times,serif" font-size="14.00">/\ tmPrepared = {s}</text>
</g>
<!-- &#45;4974900985114660661&#45;&gt;&#45;4543075241127103799 -->
<g id="edge42" class="edge">
<title>&#45;4974900985114660661&#45;&gt;&#45;4543075241127103799</title>
<path fill="none" stroke="#e31a1c" d="M3722.18,-1049.29C3757.41,-1043.9 3793.69,-1038.9 3828,-1035.1 3964.73,-1019.99 3999.67,-1025.22 4137,-1017.1 4259.34,-1009.87 4289.79,-1005.4 4412.25,-1000.6 4630.06,-992.08 5176.74,-1009.97 5393,-982.6 5441.22,-976.5 5492.81,-965.96 5539.96,-954.69"/>
<polygon fill="#e31a1c" stroke="#e31a1c" points="5540.52,-958.16 5549.42,-952.41 5538.88,-951.35 5540.52,-958.16"/>
<text text-anchor="middle" x="4457.62" y="-1003.8" font-family="Times,serif" font-size="14.00" fill="#000000">TMRcvPrepared</text>
</g>
<!-- 6700361766525303124&#45;&gt;&#45;827602329687716797 -->
<g id="edge43" class="edge">
<title>6700361766525303124&#45;&gt;&#45;827602329687716797</title>
<path fill="none" stroke="#1f78b4" d="M1383.22,-1034.8C1376.67,-1014.64 1369.1,-991.34 1362.25,-970.25"/>
<polygon fill="#1f78b4" stroke="#1f78b4" points="1365.63,-969.32 1359.21,-960.89 1358.97,-971.49 1365.63,-969.32"/>
<text text-anchor="middle" x="1402.44" y="-1003.8" font-family="Times,serif" font-size="14.00" fill="#000000">TMAbort</text>
</g>
<!-- 6700361766525303124&#45;&gt;3521423533464532559 -->
<g id="edge44" class="edge">
<title>6700361766525303124&#45;&gt;3521423533464532559</title>
<path fill="none" stroke="#e31a1c" d="M1262.36,-1048.58C1155.96,-1019.31 1008.88,-978.87 899.77,-948.86"/>
<polygon fill="#e31a1c" stroke="#e31a1c" points="901.03,-945.57 890.46,-946.3 899.17,-952.32 901.03,-945.57"/>
<text text-anchor="middle" x="1179" y="-1003.8" font-family="Times,serif" font-size="14.00" fill="#000000">TMRcvPrepared</text>
</g>
<!-- &#45;3226588047523633907&#45;&gt;8883184041786986522 -->
<g id="edge45" class="edge">
<title>&#45;3226588047523633907&#45;&gt;8883184041786986522</title>
<path fill="none" stroke="#1f78b4" d="M5103.94,-1034.87C5098.69,-1023.28 5092.61,-1011.27 5086,-1000.6 5079.02,-989.36 5070.79,-978.01 5062.35,-967.29"/>
<polygon fill="#1f78b4" stroke="#1f78b4" points="5065.18,-965.23 5056.18,-959.64 5059.73,-969.62 5065.18,-965.23"/>
<text text-anchor="middle" x="5121.11" y="-1003.8" font-family="Times,serif" font-size="14.00" fill="#000000">TMAbort</text>
</g>
<!-- &#45;3025273913122715381 -->
<g id="node27" class="node">
<title>&#45;3025273913122715381</title>
<ellipse fill="none" stroke="black" cx="6346" cy="-906.94" rx="203.82" ry="52.33"/>
<text text-anchor="middle" x="6346" y="-926.64" font-family="Times,serif" font-size="14.00">/\ msgs = {[type |&#45;&gt; &quot;Prepared&quot;, rm |&#45;&gt; s]}</text>
<text text-anchor="middle" x="6346" y="-910.14" font-family="Times,serif" font-size="14.00">/\ rmState = (r :&gt; &quot;aborted&quot; @@ s :&gt; &quot;prepared&quot;)</text>
<text text-anchor="middle" x="6346" y="-893.64" font-family="Times,serif" font-size="14.00">/\ tmState = &quot;init&quot;</text>
<text text-anchor="middle" x="6346" y="-877.14" font-family="Times,serif" font-size="14.00">/\ tmPrepared = {s}</text>
</g>
<!-- &#45;3226588047523633907&#45;&gt;&#45;3025273913122715381 -->
<g id="edge46" class="edge">
<title>&#45;3226588047523633907&#45;&gt;&#45;3025273913122715381</title>
<path fill="none" stroke="#e31a1c" d="M5298.1,-1059.82C5429.9,-1040.6 5615.58,-1015.5 5779.25,-1000.6 5934.7,-986.46 5976.78,-1012.4 6130,-982.6 6162.37,-976.31 6196.48,-966.24 6227.8,-955.5"/>
<polygon fill="#e31a1c" stroke="#e31a1c" points="6228.59,-958.93 6236.88,-952.33 6226.28,-952.32 6228.59,-958.93"/>
<text text-anchor="middle" x="5824.62" y="-1003.8" font-family="Times,serif" font-size="14.00" fill="#000000">TMRcvPrepared</text>
</g>
<!-- &#45;476690147165211794&#45;&gt;&#45;2263904760830070858 -->
<g id="edge47" class="edge">
<title>&#45;476690147165211794&#45;&gt;&#45;2263904760830070858</title>
<path fill="none" stroke="#1f78b4" d="M3040.16,-1036.6C3054.99,-1023.79 3071.72,-1010.77 3088.5,-1000.6 3119.18,-982.02 3154.24,-965.81 3187.71,-952.37"/>
<polygon fill="#1f78b4" stroke="#1f78b4" points="3188.62,-955.77 3196.63,-948.84 3186.04,-949.26 3188.62,-955.77"/>
<text text-anchor="middle" x="3114.75" y="-1003.8" font-family="Times,serif" font-size="14.00" fill="#000000">TMAbort</text>
</g>
<!-- &#45;7225434331385223261&#45;&gt;&#45;7225434331385223261 -->
<g id="edge51" class="edge">
<title>&#45;7225434331385223261&#45;&gt;&#45;7225434331385223261</title>
<path fill="none" stroke="#e31a1c" d="M6228.06,-1099.14C6246.44,-1096.7 6258.01,-1092.8 6258.01,-1087.43 6258.01,-1083.23 6250.95,-1079.93 6239.09,-1077.53"/>
<polygon fill="#e31a1c" stroke="#e31a1c" points="6239.98,-1074.13 6229.55,-1075.97 6238.85,-1081.04 6239.98,-1074.13"/>
<text text-anchor="middle" x="6303.38" y="-1082.38" font-family="Times,serif" font-size="14.00" fill="#000000">TMRcvPrepared</text>
</g>
<!-- &#45;7225434331385223261&#45;&gt;&#45;4543075241127103799 -->
<g id="edge49" class="edge">
<title>&#45;7225434331385223261&#45;&gt;&#45;4543075241127103799</title>
<path fill="none" stroke="#b2df8a" d="M5941.77,-1039.3C5899.81,-1015.82 5848.83,-987.3 5805.12,-962.84"/>
<polygon fill="#b2df8a" stroke="#b2df8a" points="5807.09,-959.93 5796.65,-958.11 5803.67,-966.04 5807.09,-959.93"/>
<text text-anchor="middle" x="5926.57" y="-1003.8" font-family="Times,serif" font-size="14.00" fill="#000000">RMPrepare</text>
</g>
<!-- &#45;7225434331385223261&#45;&gt;&#45;3025273913122715381 -->
<g id="edge50" class="edge">
<title>&#45;7225434331385223261&#45;&gt;&#45;3025273913122715381</title>
<path fill="none" stroke="#33a02c" d="M6110.49,-1039.3C6153.88,-1015.1 6206.87,-985.55 6251.59,-960.6"/>
<polygon fill="#33a02c" stroke="#33a02c" points="6253.24,-963.69 6260.27,-955.76 6249.83,-957.58 6253.24,-963.69"/>
<text text-anchor="middle" x="6230.78" y="-1003.8" font-family="Times,serif" font-size="14.00" fill="#000000">RMChooseToAbort</text>
</g>
<!-- &#45;7506763789492889265 -->
<g id="node28" class="node">
<title>&#45;7506763789492889265</title>
<ellipse fill="none" stroke="black" cx="6937" cy="-906.94" rx="253.67" ry="52.33"/>
<text text-anchor="middle" x="6937" y="-926.64" font-family="Times,serif" font-size="14.00">/\ msgs = {[type |&#45;&gt; &quot;Abort&quot;], [type |&#45;&gt; &quot;Prepared&quot;, rm |&#45;&gt; s]}</text>
<text text-anchor="middle" x="6937" y="-910.14" font-family="Times,serif" font-size="14.00">/\ rmState = (r :&gt; &quot;working&quot; @@ s :&gt; &quot;prepared&quot;)</text>
<text text-anchor="middle" x="6937" y="-893.64" font-family="Times,serif" font-size="14.00">/\ tmState = &quot;done&quot;</text>
<text text-anchor="middle" x="6937" y="-877.14" font-family="Times,serif" font-size="14.00">/\ tmPrepared = {s}</text>
</g>
<!-- &#45;7225434331385223261&#45;&gt;&#45;7506763789492889265 -->
<g id="edge48" class="edge">
<title>&#45;7225434331385223261&#45;&gt;&#45;7506763789492889265</title>
<path fill="none" stroke="#1f78b4" d="M6209.15,-1062.62C6338.83,-1044.39 6516.48,-1016.61 6671,-982.6 6708.2,-974.42 6747.92,-964.13 6785.01,-953.82"/>
<polygon fill="#1f78b4" stroke="#1f78b4" points="6785.77,-957.25 6794.45,-951.18 6783.88,-950.5 6785.77,-957.25"/>
<text text-anchor="middle" x="6610.28" y="-1003.8" font-family="Times,serif" font-size="14.00" fill="#000000">TMAbort</text>
</g>
<!-- &#45;633806864297459675&#45;&gt;&#45;633806864297459675 -->
<g id="edge52" class="edge">
<title>&#45;633806864297459675&#45;&gt;&#45;633806864297459675</title>
<path fill="none" stroke="#fb9a99" d="M2233.71,-922.06C2255.48,-918.9 2269.14,-913.86 2269.14,-906.94 2269.14,-901.27 2259.95,-896.86 2244.63,-893.71"/>
<polygon fill="#fb9a99" stroke="#fb9a99" points="2245.65,-890.34 2235.2,-892.08 2244.46,-897.24 2245.65,-890.34"/>
<text text-anchor="middle" x="2319.02" y="-901.89" font-family="Times,serif" font-size="14.00" fill="#000000">RMRcvAbortMsg</text>
</g>
<!-- &#45;2259172906635484354 -->
<g id="node29" class="node">
<title>&#45;2259172906635484354</title>
<ellipse fill="none" stroke="black" cx="3191" cy="-703.12" rx="203.82" ry="75.66"/>
<text text-anchor="middle" x="3191" y="-739.32" font-family="Times,serif" font-size="14.00">/\ msgs = { [type |&#45;&gt; &quot;Abort&quot;],</text>
<text text-anchor="middle" x="3191" y="-722.82" font-family="Times,serif" font-size="14.00"> &#160;[type |&#45;&gt; &quot;Prepared&quot;, rm |&#45;&gt; r],</text>
<text text-anchor="middle" x="3191" y="-706.32" font-family="Times,serif" font-size="14.00"> &#160;[type |&#45;&gt; &quot;Prepared&quot;, rm |&#45;&gt; s] }</text>
<text text-anchor="middle" x="3191" y="-689.82" font-family="Times,serif" font-size="14.00">/\ rmState = (r :&gt; &quot;aborted&quot; @@ s :&gt; &quot;prepared&quot;)</text>
<text text-anchor="middle" x="3191" y="-673.32" font-family="Times,serif" font-size="14.00">/\ tmState = &quot;done&quot;</text>
<text text-anchor="middle" x="3191" y="-656.82" font-family="Times,serif" font-size="14.00">/\ tmPrepared = {}</text>
</g>
<!-- &#45;633806864297459675&#45;&gt;&#45;2259172906635484354 -->
<g id="edge53" class="edge">
<title>&#45;633806864297459675&#45;&gt;&#45;2259172906635484354</title>
<path fill="none" stroke="#b2df8a" d="M2116.05,-861.01C2183.13,-838.54 2267.69,-812.78 2345,-796.78 2558.25,-752.64 2806.38,-728.62 2978.53,-716.17"/>
<polygon fill="#b2df8a" stroke="#b2df8a" points="2978.53,-719.68 2988.25,-715.48 2978.03,-712.7 2978.53,-719.68"/>
<text text-anchor="middle" x="2376.5" y="-799.98" font-family="Times,serif" font-size="14.00" fill="#000000">RMPrepare</text>
</g>
<!-- &#45;1815354725276510052 -->
<g id="node30" class="node">
<title>&#45;1815354725276510052</title>
<ellipse fill="none" stroke="black" cx="1567" cy="-703.12" rx="253.14" ry="52.33"/>
<text text-anchor="middle" x="1567" y="-722.82" font-family="Times,serif" font-size="14.00">/\ msgs = {[type |&#45;&gt; &quot;Abort&quot;], [type |&#45;&gt; &quot;Prepared&quot;, rm |&#45;&gt; r]}</text>
<text text-anchor="middle" x="1567" y="-706.32" font-family="Times,serif" font-size="14.00">/\ rmState = (r :&gt; &quot;aborted&quot; @@ s :&gt; &quot;aborted&quot;)</text>
<text text-anchor="middle" x="1567" y="-689.82" font-family="Times,serif" font-size="14.00">/\ tmState = &quot;done&quot;</text>
<text text-anchor="middle" x="1567" y="-673.32" font-family="Times,serif" font-size="14.00">/\ tmPrepared = {}</text>
</g>
<!-- &#45;633806864297459675&#45;&gt;&#45;1815354725276510052 -->
<g id="edge54" class="edge">
<title>&#45;633806864297459675&#45;&gt;&#45;1815354725276510052</title>
<path fill="none" stroke="#fb9a99" d="M1891.32,-858.5C1826.94,-827.85 1743.13,-787.96 1676.83,-756.4"/>
<polygon fill="#fb9a99" stroke="#fb9a99" points="1678.66,-753.4 1668.13,-752.26 1675.66,-759.72 1678.66,-753.4"/>
<text text-anchor="middle" x="1841.59" y="-799.98" font-family="Times,serif" font-size="14.00" fill="#000000">RMRcvAbortMsg</text>
</g>
<!-- 8301560317156807003&#45;&gt;&#45;2259172906635484354 -->
<g id="edge55" class="edge">
<title>8301560317156807003&#45;&gt;&#45;2259172906635484354</title>
<path fill="none" stroke="#fb9a99" d="M3721.98,-854C3698.3,-846.17 3674.04,-838.35 3651,-831.28 3557.95,-802.73 3453.43,-773.6 3367.56,-750.44"/>
<polygon fill="#fb9a99" stroke="#fb9a99" points="3368.68,-747.12 3358.11,-747.9 3366.86,-753.88 3368.68,-747.12"/>
<text text-anchor="middle" x="3638.72" y="-799.98" font-family="Times,serif" font-size="14.00" fill="#000000">RMRcvAbortMsg</text>
</g>
<!-- 4298755523306665942 -->
<g id="node31" class="node">
<title>4298755523306665942</title>
<ellipse fill="none" stroke="black" cx="3741" cy="-703.12" rx="203.82" ry="75.66"/>
<text text-anchor="middle" x="3741" y="-739.32" font-family="Times,serif" font-size="14.00">/\ msgs = { [type |&#45;&gt; &quot;Abort&quot;],</text>
<text text-anchor="middle" x="3741" y="-722.82" font-family="Times,serif" font-size="14.00"> &#160;[type |&#45;&gt; &quot;Prepared&quot;, rm |&#45;&gt; r],</text>
<text text-anchor="middle" x="3741" y="-706.32" font-family="Times,serif" font-size="14.00"> &#160;[type |&#45;&gt; &quot;Prepared&quot;, rm |&#45;&gt; s] }</text>
<text text-anchor="middle" x="3741" y="-689.82" font-family="Times,serif" font-size="14.00">/\ rmState = (r :&gt; &quot;prepared&quot; @@ s :&gt; &quot;aborted&quot;)</text>
<text text-anchor="middle" x="3741" y="-673.32" font-family="Times,serif" font-size="14.00">/\ tmState = &quot;done&quot;</text>
<text text-anchor="middle" x="3741" y="-656.82" font-family="Times,serif" font-size="14.00">/\ tmPrepared = {}</text>
</g>
<!-- 8301560317156807003&#45;&gt;4298755523306665942 -->
<g id="edge56" class="edge">
<title>8301560317156807003&#45;&gt;4298755523306665942</title>
<path fill="none" stroke="#fb9a99" d="M3824.52,-832.8C3814.76,-817.76 3804.42,-801.82 3794.46,-786.48"/>
<polygon fill="#fb9a99" stroke="#fb9a99" points="3797.52,-784.77 3789.14,-778.29 3791.65,-788.58 3797.52,-784.77"/>
<text text-anchor="middle" x="3860.3" y="-799.98" font-family="Times,serif" font-size="14.00" fill="#000000">RMRcvAbortMsg</text>
</g>
<!-- &#45;827602329687716797&#45;&gt;&#45;827602329687716797 -->
<g id="edge58" class="edge">
<title>&#45;827602329687716797&#45;&gt;&#45;827602329687716797</title>
<path fill="none" stroke="#fb9a99" d="M1584.71,-922.06C1606.48,-918.9 1620.14,-913.86 1620.14,-906.94 1620.14,-901.27 1610.95,-896.86 1595.63,-893.71"/>
<polygon fill="#fb9a99" stroke="#fb9a99" points="1596.65,-890.34 1586.2,-892.08 1595.46,-897.24 1596.65,-890.34"/>
<text text-anchor="middle" x="1670.02" y="-901.89" font-family="Times,serif" font-size="14.00" fill="#000000">RMRcvAbortMsg</text>
</g>
<!-- &#45;827602329687716797&#45;&gt;&#45;1815354725276510052 -->
<g id="edge57" class="edge">
<title>&#45;827602329687716797&#45;&gt;&#45;1815354725276510052</title>
<path fill="none" stroke="#fb9a99" d="M1398.2,-855.54C1429.88,-827.12 1469.58,-791.51 1502.52,-761.96"/>
<polygon fill="#fb9a99" stroke="#fb9a99" points="1504.51,-764.88 1509.61,-755.6 1499.83,-759.67 1504.51,-764.88"/>
<text text-anchor="middle" x="1511.12" y="-799.98" font-family="Times,serif" font-size="14.00" fill="#000000">RMRcvAbortMsg</text>
</g>
<!-- 8883184041786986522&#45;&gt;8883184041786986522 -->
<g id="edge59" class="edge">
<title>8883184041786986522&#45;&gt;8883184041786986522</title>
<path fill="none" stroke="#fb9a99" d="M5252.64,-921.99C5274.18,-918.83 5287.67,-913.81 5287.67,-906.94 5287.67,-901.36 5278.76,-897.01 5263.87,-893.87"/>
<polygon fill="#fb9a99" stroke="#fb9a99" points="5264.59,-890.44 5254.13,-892.16 5263.37,-897.34 5264.59,-890.44"/>
<text text-anchor="middle" x="5337.55" y="-901.89" font-family="Times,serif" font-size="14.00" fill="#000000">RMRcvAbortMsg</text>
</g>
<!-- 7065774925379258844 -->
<g id="node32" class="node">
<title>7065774925379258844</title>
<ellipse fill="none" stroke="black" cx="4341" cy="-703.12" rx="253.67" ry="52.33"/>
<text text-anchor="middle" x="4341" y="-722.82" font-family="Times,serif" font-size="14.00">/\ msgs = {[type |&#45;&gt; &quot;Abort&quot;], [type |&#45;&gt; &quot;Prepared&quot;, rm |&#45;&gt; s]}</text>
<text text-anchor="middle" x="4341" y="-706.32" font-family="Times,serif" font-size="14.00">/\ rmState = (r :&gt; &quot;aborted&quot; @@ s :&gt; &quot;aborted&quot;)</text>
<text text-anchor="middle" x="4341" y="-689.82" font-family="Times,serif" font-size="14.00">/\ tmState = &quot;done&quot;</text>
<text text-anchor="middle" x="4341" y="-673.32" font-family="Times,serif" font-size="14.00">/\ tmPrepared = {}</text>
</g>
<!-- 8883184041786986522&#45;&gt;7065774925379258844 -->
<g id="edge60" class="edge">
<title>8883184041786986522&#45;&gt;7065774925379258844</title>
<path fill="none" stroke="#fb9a99" d="M4867.33,-863.14C4757.61,-829.99 4605.87,-784.15 4493.5,-750.2"/>
<polygon fill="#fb9a99" stroke="#fb9a99" points="4494.78,-746.93 4484.2,-747.39 4492.76,-753.63 4494.78,-746.93"/>
<text text-anchor="middle" x="4744.9" y="-799.98" font-family="Times,serif" font-size="14.00" fill="#000000">RMRcvAbortMsg</text>
</g>
<!-- &#45;2263904760830070858&#45;&gt;&#45;2263904760830070858 -->
<g id="edge61" class="edge">
<title>&#45;2263904760830070858&#45;&gt;&#45;2263904760830070858</title>
<path fill="none" stroke="#fb9a99" d="M3512.01,-922.96C3532.71,-919.9 3546.05,-914.56 3546.05,-906.94 3546.05,-900.82 3537.41,-896.16 3523.26,-892.98"/>
<polygon fill="#fb9a99" stroke="#fb9a99" points="3523.97,-889.56 3513.5,-891.2 3522.71,-896.44 3523.97,-889.56"/>
<text text-anchor="middle" x="3595.93" y="-901.89" font-family="Times,serif" font-size="14.00" fill="#000000">RMRcvAbortMsg</text>
</g>
<!-- 1202513148741259631&#45;&gt;1202513148741259631 -->
<g id="edge64" class="edge">
<title>1202513148741259631&#45;&gt;1202513148741259631</title>
<path fill="none" stroke="#fb9a99" d="M4602.64,-921.99C4624.18,-918.83 4637.67,-913.81 4637.67,-906.94 4637.67,-901.36 4628.76,-897.01 4613.87,-893.87"/>
<polygon fill="#fb9a99" stroke="#fb9a99" points="4614.59,-890.44 4604.13,-892.16 4613.37,-897.34 4614.59,-890.44"/>
<text text-anchor="middle" x="4687.55" y="-901.89" font-family="Times,serif" font-size="14.00" fill="#000000">RMRcvAbortMsg</text>
</g>
<!-- 1202513148741259631&#45;&gt;4298755523306665942 -->
<g id="edge62" class="edge">
<title>1202513148741259631&#45;&gt;4298755523306665942</title>
<path fill="none" stroke="#b2df8a" d="M4269.78,-857.53C4228.7,-836.69 4178.78,-813.36 4132,-796.78 4093.53,-783.16 4008.56,-762.63 3927.62,-744.36"/>
<polygon fill="#b2df8a" stroke="#b2df8a" points="3928.75,-741.03 3918.23,-742.24 3927.21,-747.85 3928.75,-741.03"/>
<text text-anchor="middle" x="4201.94" y="-799.98" font-family="Times,serif" font-size="14.00" fill="#000000">RMPrepare</text>
</g>
<!-- 1202513148741259631&#45;&gt;7065774925379258844 -->
<g id="edge63" class="edge">
<title>1202513148741259631&#45;&gt;7065774925379258844</title>
<path fill="none" stroke="#fb9a99" d="M4354.39,-854.23C4352.02,-827.65 4349.11,-795.03 4346.61,-767"/>
<polygon fill="#fb9a99" stroke="#fb9a99" points="4350.11,-766.86 4345.73,-757.21 4343.14,-767.48 4350.11,-766.86"/>
<text text-anchor="middle" x="4400.41" y="-799.98" font-family="Times,serif" font-size="14.00" fill="#000000">RMRcvAbortMsg</text>
</g>
<!-- 879461406137672776 -->
<g id="node33" class="node">
<title>879461406137672776</title>
<ellipse fill="none" stroke="black" cx="269" cy="-703.12" rx="253.14" ry="52.33"/>
<text text-anchor="middle" x="269" y="-722.82" font-family="Times,serif" font-size="14.00">/\ msgs = {[type |&#45;&gt; &quot;Abort&quot;], [type |&#45;&gt; &quot;Prepared&quot;, rm |&#45;&gt; r]}</text>
<text text-anchor="middle" x="269" y="-706.32" font-family="Times,serif" font-size="14.00">/\ rmState = (r :&gt; &quot;aborted&quot; @@ s :&gt; &quot;working&quot;)</text>
<text text-anchor="middle" x="269" y="-689.82" font-family="Times,serif" font-size="14.00">/\ tmState = &quot;done&quot;</text>
<text text-anchor="middle" x="269" y="-673.32" font-family="Times,serif" font-size="14.00">/\ tmPrepared = {r}</text>
</g>
<!-- &#45;7496497296444535640&#45;&gt;879461406137672776 -->
<g id="edge65" class="edge">
<title>&#45;7496497296444535640&#45;&gt;879461406137672776</title>
<path fill="none" stroke="#fb9a99" d="M269,-854.23C269,-827.65 269,-795.03 269,-767"/>
<polygon fill="#fb9a99" stroke="#fb9a99" points="272.5,-767.21 269,-757.21 265.5,-767.21 272.5,-767.21"/>
<text text-anchor="middle" x="318.88" y="-799.98" font-family="Times,serif" font-size="14.00" fill="#000000">RMRcvAbortMsg</text>
</g>
<!-- &#45;6953470119458486193 -->
<g id="node34" class="node">
<title>&#45;6953470119458486193</title>
<ellipse fill="none" stroke="black" cx="2171" cy="-703.12" rx="208.6" ry="75.66"/>
<text text-anchor="middle" x="2171" y="-739.32" font-family="Times,serif" font-size="14.00">/\ msgs = { [type |&#45;&gt; &quot;Abort&quot;],</text>
<text text-anchor="middle" x="2171" y="-722.82" font-family="Times,serif" font-size="14.00"> &#160;[type |&#45;&gt; &quot;Prepared&quot;, rm |&#45;&gt; r],</text>
<text text-anchor="middle" x="2171" y="-706.32" font-family="Times,serif" font-size="14.00"> &#160;[type |&#45;&gt; &quot;Prepared&quot;, rm |&#45;&gt; s] }</text>
<text text-anchor="middle" x="2171" y="-689.82" font-family="Times,serif" font-size="14.00">/\ rmState = (r :&gt; &quot;prepared&quot; @@ s :&gt; &quot;prepared&quot;)</text>
<text text-anchor="middle" x="2171" y="-673.32" font-family="Times,serif" font-size="14.00">/\ tmState = &quot;done&quot;</text>
<text text-anchor="middle" x="2171" y="-656.82" font-family="Times,serif" font-size="14.00">/\ tmPrepared = {r}</text>
</g>
<!-- &#45;7496497296444535640&#45;&gt;&#45;6953470119458486193 -->
<g id="edge66" class="edge">
<title>&#45;7496497296444535640&#45;&gt;&#45;6953470119458486193</title>
<path fill="none" stroke="#b2df8a" d="M407.82,-862.73C448.5,-851.23 493.27,-839.68 535,-831.28 598.66,-818.47 615.93,-823.85 680,-813.28 715.82,-807.38 723.91,-800.74 760,-796.78 891.45,-782.36 1819.68,-801.22 1950,-778.78 1972.57,-774.9 1995.95,-769.09 2018.68,-762.39"/>
<polygon fill="#b2df8a" stroke="#b2df8a" points="2019.42,-765.82 2027.98,-759.58 2017.39,-759.12 2019.42,-765.82"/>
<text text-anchor="middle" x="791.5" y="-799.98" font-family="Times,serif" font-size="14.00" fill="#000000">RMPrepare</text>
</g>
<!-- 4374714672709322915 -->
<g id="node35" class="node">
<title>4374714672709322915</title>
<ellipse fill="none" stroke="black" cx="918" cy="-703.12" rx="253.14" ry="52.33"/>
<text text-anchor="middle" x="918" y="-722.82" font-family="Times,serif" font-size="14.00">/\ msgs = {[type |&#45;&gt; &quot;Abort&quot;], [type |&#45;&gt; &quot;Prepared&quot;, rm |&#45;&gt; r]}</text>
<text text-anchor="middle" x="918" y="-706.32" font-family="Times,serif" font-size="14.00">/\ rmState = (r :&gt; &quot;prepared&quot; @@ s :&gt; &quot;aborted&quot;)</text>
<text text-anchor="middle" x="918" y="-689.82" font-family="Times,serif" font-size="14.00">/\ tmState = &quot;done&quot;</text>
<text text-anchor="middle" x="918" y="-673.32" font-family="Times,serif" font-size="14.00">/\ tmPrepared = {r}</text>
</g>
<!-- &#45;7496497296444535640&#45;&gt;4374714672709322915 -->
<g id="edge67" class="edge">
<title>&#45;7496497296444535640&#45;&gt;4374714672709322915</title>
<path fill="none" stroke="#fb9a99" d="M388.88,-860.48C445.82,-839.7 515.09,-815.59 578.25,-796.78 610.59,-787.16 619.36,-787.34 652,-778.78 687.21,-769.55 724.93,-759.23 760.57,-749.27"/>
<polygon fill="#fb9a99" stroke="#fb9a99" points="761.41,-752.67 770.1,-746.61 759.52,-745.93 761.41,-752.67"/>
<text text-anchor="middle" x="628.12" y="-799.98" font-family="Times,serif" font-size="14.00" fill="#000000">RMRcvAbortMsg</text>
</g>
<!-- &#45;4568132850329190210&#45;&gt;&#45;4568132850329190210 -->
<g id="edge69" class="edge">
<title>&#45;4568132850329190210&#45;&gt;&#45;4568132850329190210</title>
<path fill="none" stroke="#e31a1c" d="M2978.44,-921.31C3000.7,-918.13 3014.4,-913.34 3014.4,-906.94 3014.4,-901.7 3005.18,-897.53 2989.58,-894.45"/>
<polygon fill="#e31a1c" stroke="#e31a1c" points="2990.38,-891.03 2979.94,-892.83 2989.22,-897.94 2990.38,-891.03"/>
<text text-anchor="middle" x="3059.78" y="-901.89" font-family="Times,serif" font-size="14.00" fill="#000000">TMRcvPrepared</text>
</g>
<!-- &#45;4568132850329190210&#45;&gt;&#45;6953470119458486193 -->
<g id="edge68" class="edge">
<title>&#45;4568132850329190210&#45;&gt;&#45;6953470119458486193</title>
<path fill="none" stroke="#1f78b4" d="M2566.79,-858.63C2493.81,-830.14 2400.26,-793.62 2322.44,-763.24"/>
<polygon fill="#1f78b4" stroke="#1f78b4" points="2324.06,-760.11 2313.47,-759.74 2321.51,-766.63 2324.06,-760.11"/>
<text text-anchor="middle" x="2471.25" y="-799.98" font-family="Times,serif" font-size="14.00" fill="#000000">TMAbort</text>
</g>
<!-- 2252202094466483187 -->
<g id="node36" class="node">
<title>2252202094466483187</title>
<ellipse fill="none" stroke="black" cx="5039" cy="-703.12" rx="301.4" ry="52.33"/>
<text text-anchor="middle" x="5039" y="-722.82" font-family="Times,serif" font-size="14.00">/\ msgs = {[type |&#45;&gt; &quot;Prepared&quot;, rm |&#45;&gt; r], [type |&#45;&gt; &quot;Prepared&quot;, rm |&#45;&gt; s]}</text>
<text text-anchor="middle" x="5039" y="-706.32" font-family="Times,serif" font-size="14.00">/\ rmState = (r :&gt; &quot;prepared&quot; @@ s :&gt; &quot;prepared&quot;)</text>
<text text-anchor="middle" x="5039" y="-689.82" font-family="Times,serif" font-size="14.00">/\ tmState = &quot;init&quot;</text>
<text text-anchor="middle" x="5039" y="-673.32" font-family="Times,serif" font-size="14.00">/\ tmPrepared = {r, s}</text>
</g>
<!-- &#45;4568132850329190210&#45;&gt;2252202094466483187 -->
<g id="edge70" class="edge">
<title>&#45;4568132850329190210&#45;&gt;2252202094466483187</title>
<path fill="none" stroke="#e31a1c" d="M2878.05,-865.96C2950.33,-852.43 3033.65,-838.85 3110,-831.28 3466.57,-795.97 3558.83,-841.89 3916,-813.28 3969.33,-809.01 3981.92,-801.15 4035.25,-796.78 4340.88,-771.73 4420.92,-818.47 4725,-778.78 4772.84,-772.54 4824.02,-762.05 4870.87,-750.88"/>
<polygon fill="#e31a1c" stroke="#e31a1c" points="4871.69,-754.28 4880.59,-748.54 4870.04,-747.48 4871.69,-754.28"/>
<text text-anchor="middle" x="4080.62" y="-799.98" font-family="Times,serif" font-size="14.00" fill="#000000">TMRcvPrepared</text>
</g>
<!-- 3521423533464532559&#45;&gt;3521423533464532559 -->
<g id="edge72" class="edge">
<title>3521423533464532559&#45;&gt;3521423533464532559</title>
<path fill="none" stroke="#e31a1c" d="M945.48,-922.9C966.38,-919.83 979.82,-914.51 979.82,-906.94 979.82,-900.8 970.95,-896.14 956.41,-892.95"/>
<polygon fill="#e31a1c" stroke="#e31a1c" points="957.43,-889.58 946.97,-891.26 956.19,-896.47 957.43,-889.58"/>
<text text-anchor="middle" x="1025.2" y="-901.89" font-family="Times,serif" font-size="14.00" fill="#000000">TMRcvPrepared</text>
</g>
<!-- 3521423533464532559&#45;&gt;4374714672709322915 -->
<g id="edge71" class="edge">
<title>3521423533464532559&#45;&gt;4374714672709322915</title>
<path fill="none" stroke="#1f78b4" d="M792.93,-855.28C815.87,-827.55 844.43,-793.03 868.46,-763.99"/>
<polygon fill="#1f78b4" stroke="#1f78b4" points="871.12,-766.26 874.8,-756.33 865.73,-761.8 871.12,-766.26"/>
<text text-anchor="middle" x="865.76" y="-799.98" font-family="Times,serif" font-size="14.00" fill="#000000">TMAbort</text>
</g>
<!-- &#45;4543075241127103799&#45;&gt;&#45;4543075241127103799 -->
<g id="edge75" class="edge">
<title>&#45;4543075241127103799&#45;&gt;&#45;4543075241127103799</title>
<path fill="none" stroke="#e31a1c" d="M5997.44,-921.31C6019.7,-918.13 6033.4,-913.34 6033.4,-906.94 6033.4,-901.7 6024.18,-897.53 6008.58,-894.45"/>
<polygon fill="#e31a1c" stroke="#e31a1c" points="6009.38,-891.03 5998.94,-892.83 6008.22,-897.94 6009.38,-891.03"/>
<text text-anchor="middle" x="6078.78" y="-901.89" font-family="Times,serif" font-size="14.00" fill="#000000">TMRcvPrepared</text>
</g>
<!-- &#45;4543075241127103799&#45;&gt;2252202094466483187 -->
<g id="edge74" class="edge">
<title>&#45;4543075241127103799&#45;&gt;2252202094466483187</title>
<path fill="none" stroke="#e31a1c" d="M5558.33,-861.03C5451.55,-828.77 5307.79,-785.33 5198.6,-752.34"/>
<polygon fill="#e31a1c" stroke="#e31a1c" points="5199.84,-749.06 5189.26,-749.52 5197.82,-755.76 5199.84,-749.06"/>
<text text-anchor="middle" x="5438.4" y="-799.98" font-family="Times,serif" font-size="14.00" fill="#000000">TMRcvPrepared</text>
</g>
<!-- &#45;6923944097421231560 -->
<g id="node37" class="node">
<title>&#45;6923944097421231560</title>
<ellipse fill="none" stroke="black" cx="5683" cy="-703.12" rx="208.6" ry="75.66"/>
<text text-anchor="middle" x="5683" y="-739.32" font-family="Times,serif" font-size="14.00">/\ msgs = { [type |&#45;&gt; &quot;Abort&quot;],</text>
<text text-anchor="middle" x="5683" y="-722.82" font-family="Times,serif" font-size="14.00"> &#160;[type |&#45;&gt; &quot;Prepared&quot;, rm |&#45;&gt; r],</text>
<text text-anchor="middle" x="5683" y="-706.32" font-family="Times,serif" font-size="14.00"> &#160;[type |&#45;&gt; &quot;Prepared&quot;, rm |&#45;&gt; s] }</text>
<text text-anchor="middle" x="5683" y="-689.82" font-family="Times,serif" font-size="14.00">/\ rmState = (r :&gt; &quot;prepared&quot; @@ s :&gt; &quot;prepared&quot;)</text>
<text text-anchor="middle" x="5683" y="-673.32" font-family="Times,serif" font-size="14.00">/\ tmState = &quot;done&quot;</text>
<text text-anchor="middle" x="5683" y="-656.82" font-family="Times,serif" font-size="14.00">/\ tmPrepared = {s}</text>
</g>
<!-- &#45;4543075241127103799&#45;&gt;&#45;6923944097421231560 -->
<g id="edge73" class="edge">
<title>&#45;4543075241127103799&#45;&gt;&#45;6923944097421231560</title>
<path fill="none" stroke="#1f78b4" d="M5700.85,-854.23C5698.53,-834.74 5695.83,-812 5693.24,-790.21"/>
<polygon fill="#1f78b4" stroke="#1f78b4" points="5696.73,-789.94 5692.07,-780.42 5689.78,-790.77 5696.73,-789.94"/>
<text text-anchor="middle" x="5721.97" y="-799.98" font-family="Times,serif" font-size="14.00" fill="#000000">TMAbort</text>
</g>
<!-- &#45;3025273913122715381&#45;&gt;&#45;3025273913122715381 -->
<g id="edge77" class="edge">
<title>&#45;3025273913122715381&#45;&gt;&#45;3025273913122715381</title>
<path fill="none" stroke="#e31a1c" d="M6540.48,-922.9C6561.38,-919.83 6574.82,-914.51 6574.82,-906.94 6574.82,-900.8 6565.95,-896.14 6551.41,-892.95"/>
<polygon fill="#e31a1c" stroke="#e31a1c" points="6552.43,-889.58 6541.97,-891.26 6551.19,-896.47 6552.43,-889.58"/>
<text text-anchor="middle" x="6620.2" y="-901.89" font-family="Times,serif" font-size="14.00" fill="#000000">TMRcvPrepared</text>
</g>
<!-- &#45;2707623536267266073 -->
<g id="node38" class="node">
<title>&#45;2707623536267266073</title>
<ellipse fill="none" stroke="black" cx="6170" cy="-703.12" rx="253.67" ry="52.33"/>
<text text-anchor="middle" x="6170" y="-722.82" font-family="Times,serif" font-size="14.00">/\ msgs = {[type |&#45;&gt; &quot;Abort&quot;], [type |&#45;&gt; &quot;Prepared&quot;, rm |&#45;&gt; s]}</text>
<text text-anchor="middle" x="6170" y="-706.32" font-family="Times,serif" font-size="14.00">/\ rmState = (r :&gt; &quot;aborted&quot; @@ s :&gt; &quot;prepared&quot;)</text>
<text text-anchor="middle" x="6170" y="-689.82" font-family="Times,serif" font-size="14.00">/\ tmState = &quot;done&quot;</text>
<text text-anchor="middle" x="6170" y="-673.32" font-family="Times,serif" font-size="14.00">/\ tmPrepared = {s}</text>
</g>
<!-- &#45;3025273913122715381&#45;&gt;&#45;2707623536267266073 -->
<g id="edge76" class="edge">
<title>&#45;3025273913122715381&#45;&gt;&#45;2707623536267266073</title>
<path fill="none" stroke="#1f78b4" d="M6302.04,-855.54C6277.67,-827.59 6247.23,-792.68 6221.71,-763.42"/>
<polygon fill="#1f78b4" stroke="#1f78b4" points="6224.52,-761.31 6215.31,-756.08 6219.24,-765.92 6224.52,-761.31"/>
<text text-anchor="middle" x="6289.53" y="-799.98" font-family="Times,serif" font-size="14.00" fill="#000000">TMAbort</text>
</g>
<!-- &#45;7506763789492889265&#45;&gt;&#45;6923944097421231560 -->
<g id="edge78" class="edge">
<title>&#45;7506763789492889265&#45;&gt;&#45;6923944097421231560</title>
<path fill="none" stroke="#b2df8a" d="M6800.03,-862.55C6758.89,-850.87 6713.42,-839.27 6671,-831.28 6661.43,-829.48 6331.72,-797.47 6322,-796.78 6136.52,-783.63 6086.8,-812.88 5904,-778.78 5881.85,-774.65 5858.88,-768.79 5836.51,-762.14"/>
<polygon fill="#b2df8a" stroke="#b2df8a" points="5837.61,-758.82 5827.02,-759.26 5835.57,-765.52 5837.61,-758.82"/>
<text text-anchor="middle" x="6517.88" y="-799.98" font-family="Times,serif" font-size="14.00" fill="#000000">RMPrepare</text>
</g>
<!-- &#45;7506763789492889265&#45;&gt;&#45;2707623536267266073 -->
<g id="edge79" class="edge">
<title>&#45;7506763789492889265&#45;&gt;&#45;2707623536267266073</title>
<path fill="none" stroke="#fb9a99" d="M6797.46,-862.87C6728.13,-841.98 6642.93,-817.08 6566,-796.78 6496.64,-778.48 6419.97,-760.11 6352.71,-744.61"/>
<polygon fill="#fb9a99" stroke="#fb9a99" points="6353.57,-741.22 6343.04,-742.39 6352,-748.04 6353.57,-741.22"/>
<text text-anchor="middle" x="6666.65" y="-799.98" font-family="Times,serif" font-size="14.00" fill="#000000">RMRcvAbortMsg</text>
</g>
<!-- 5640263757456471582 -->
<g id="node39" class="node">
<title>5640263757456471582</title>
<ellipse fill="none" stroke="black" cx="6820" cy="-703.12" rx="253.67" ry="52.33"/>
<text text-anchor="middle" x="6820" y="-722.82" font-family="Times,serif" font-size="14.00">/\ msgs = {[type |&#45;&gt; &quot;Abort&quot;], [type |&#45;&gt; &quot;Prepared&quot;, rm |&#45;&gt; s]}</text>
<text text-anchor="middle" x="6820" y="-706.32" font-family="Times,serif" font-size="14.00">/\ rmState = (r :&gt; &quot;working&quot; @@ s :&gt; &quot;aborted&quot;)</text>
<text text-anchor="middle" x="6820" y="-689.82" font-family="Times,serif" font-size="14.00">/\ tmState = &quot;done&quot;</text>
<text text-anchor="middle" x="6820" y="-673.32" font-family="Times,serif" font-size="14.00">/\ tmPrepared = {s}</text>
</g>
<!-- &#45;7506763789492889265&#45;&gt;5640263757456471582 -->
<g id="edge80" class="edge">
<title>&#45;7506763789492889265&#45;&gt;5640263757456471582</title>
<path fill="none" stroke="#fb9a99" d="M6907.17,-854.49C6891.43,-827.33 6872,-793.82 6855.48,-765.33"/>
<polygon fill="#fb9a99" stroke="#fb9a99" points="6858.57,-763.68 6850.53,-756.79 6852.52,-767.2 6858.57,-763.68"/>
<text text-anchor="middle" x="6931.88" y="-799.98" font-family="Times,serif" font-size="14.00" fill="#000000">RMRcvAbortMsg</text>
</g>
<!-- &#45;2259172906635484354&#45;&gt;&#45;2259172906635484354 -->
<g id="edge81" class="edge">
<title>&#45;2259172906635484354&#45;&gt;&#45;2259172906635484354</title>
<path fill="none" stroke="#fb9a99" d="M3391.06,-718.17C3408.74,-715.01 3419.82,-709.99 3419.82,-703.12 3419.82,-697.81 3413.19,-693.61 3402.01,-690.51"/>
<polygon fill="#fb9a99" stroke="#fb9a99" points="3403.06,-687.16 3392.53,-688.4 3401.54,-693.99 3403.06,-687.16"/>
<text text-anchor="middle" x="3469.7" y="-698.07" font-family="Times,serif" font-size="14.00" fill="#000000">RMRcvAbortMsg</text>
</g>
<!-- 1155799811345671651 -->
<g id="node40" class="node">
<title>1155799811345671651</title>
<ellipse fill="none" stroke="black" cx="3446" cy="-499.3" rx="199.05" ry="75.66"/>
<text text-anchor="middle" x="3446" y="-535.5" font-family="Times,serif" font-size="14.00">/\ msgs = { [type |&#45;&gt; &quot;Abort&quot;],</text>
<text text-anchor="middle" x="3446" y="-519" font-family="Times,serif" font-size="14.00"> &#160;[type |&#45;&gt; &quot;Prepared&quot;, rm |&#45;&gt; r],</text>
<text text-anchor="middle" x="3446" y="-502.5" font-family="Times,serif" font-size="14.00"> &#160;[type |&#45;&gt; &quot;Prepared&quot;, rm |&#45;&gt; s] }</text>
<text text-anchor="middle" x="3446" y="-486" font-family="Times,serif" font-size="14.00">/\ rmState = (r :&gt; &quot;aborted&quot; @@ s :&gt; &quot;aborted&quot;)</text>
<text text-anchor="middle" x="3446" y="-469.5" font-family="Times,serif" font-size="14.00">/\ tmState = &quot;done&quot;</text>
<text text-anchor="middle" x="3446" y="-453" font-family="Times,serif" font-size="14.00">/\ tmPrepared = {}</text>
</g>
<!-- &#45;2259172906635484354&#45;&gt;1155799811345671651 -->
<g id="edge82" class="edge">
<title>&#45;2259172906635484354&#45;&gt;1155799811345671651</title>
<path fill="none" stroke="#fb9a99" d="M3276.98,-634.08C3300.93,-615.12 3327.07,-594.43 3351.49,-575.1"/>
<polygon fill="#fb9a99" stroke="#fb9a99" points="3353.54,-577.94 3359.21,-568.99 3349.2,-572.45 3353.54,-577.94"/>
<text text-anchor="middle" x="3376.02" y="-596.16" font-family="Times,serif" font-size="14.00" fill="#000000">RMRcvAbortMsg</text>
</g>
<!-- &#45;1815354725276510052&#45;&gt;&#45;1815354725276510052 -->
<g id="edge83" class="edge">
<title>&#45;1815354725276510052&#45;&gt;&#45;1815354725276510052</title>
<path fill="none" stroke="#fb9a99" d="M1809.71,-718.24C1831.48,-715.08 1845.14,-710.04 1845.14,-703.12 1845.14,-697.45 1835.95,-693.04 1820.63,-689.89"/>
<polygon fill="#fb9a99" stroke="#fb9a99" points="1821.65,-686.52 1811.2,-688.26 1820.46,-693.41 1821.65,-686.52"/>
<text text-anchor="middle" x="1895.02" y="-698.07" font-family="Times,serif" font-size="14.00" fill="#000000">RMRcvAbortMsg</text>
</g>
<!-- 4298755523306665942&#45;&gt;4298755523306665942 -->
<g id="edge85" class="edge">
<title>4298755523306665942&#45;&gt;4298755523306665942</title>
<path fill="none" stroke="#fb9a99" d="M3941.06,-718.17C3958.74,-715.01 3969.82,-709.99 3969.82,-703.12 3969.82,-697.81 3963.19,-693.61 3952.01,-690.51"/>
<polygon fill="#fb9a99" stroke="#fb9a99" points="3953.06,-687.16 3942.53,-688.4 3951.54,-693.99 3953.06,-687.16"/>
<text text-anchor="middle" x="4019.7" y="-698.07" font-family="Times,serif" font-size="14.00" fill="#000000">RMRcvAbortMsg</text>
</g>
<!-- 4298755523306665942&#45;&gt;1155799811345671651 -->
<g id="edge84" class="edge">
<title>4298755523306665942&#45;&gt;1155799811345671651</title>
<path fill="none" stroke="#fb9a99" d="M3644.41,-636.04C3614.63,-615.67 3581.71,-593.15 3551.38,-572.4"/>
<polygon fill="#fb9a99" stroke="#fb9a99" points="3553.53,-569.63 3543.3,-566.87 3549.58,-575.41 3553.53,-569.63"/>
<text text-anchor="middle" x="3652.22" y="-596.16" font-family="Times,serif" font-size="14.00" fill="#000000">RMRcvAbortMsg</text>
</g>
<!-- 7065774925379258844&#45;&gt;7065774925379258844 -->
<g id="edge86" class="edge">
<title>7065774925379258844&#45;&gt;7065774925379258844</title>
<path fill="none" stroke="#fb9a99" d="M4584.64,-718.17C4606.18,-715.01 4619.67,-709.99 4619.67,-703.12 4619.67,-697.54 4610.76,-693.19 4595.87,-690.05"/>
<polygon fill="#fb9a99" stroke="#fb9a99" points="4596.59,-686.62 4586.13,-688.34 4595.37,-693.52 4596.59,-686.62"/>
<text text-anchor="middle" x="4669.55" y="-698.07" font-family="Times,serif" font-size="14.00" fill="#000000">RMRcvAbortMsg</text>
</g>
<!-- 879461406137672776&#45;&gt;879461406137672776 -->
<g id="edge87" class="edge">
<title>879461406137672776&#45;&gt;879461406137672776</title>
<path fill="none" stroke="#fb9a99" d="M511.71,-718.24C533.48,-715.08 547.14,-710.04 547.14,-703.12 547.14,-697.45 537.95,-693.04 522.63,-689.89"/>
<polygon fill="#fb9a99" stroke="#fb9a99" points="523.65,-686.52 513.2,-688.26 522.46,-693.41 523.65,-686.52"/>
<text text-anchor="middle" x="597.02" y="-698.07" font-family="Times,serif" font-size="14.00" fill="#000000">RMRcvAbortMsg</text>
</g>
<!-- &#45;2904203587503338029 -->
<g id="node41" class="node">
<title>&#45;2904203587503338029</title>
<ellipse fill="none" stroke="black" cx="1621" cy="-499.3" rx="203.82" ry="75.66"/>
<text text-anchor="middle" x="1621" y="-535.5" font-family="Times,serif" font-size="14.00">/\ msgs = { [type |&#45;&gt; &quot;Abort&quot;],</text>
<text text-anchor="middle" x="1621" y="-519" font-family="Times,serif" font-size="14.00"> &#160;[type |&#45;&gt; &quot;Prepared&quot;, rm |&#45;&gt; r],</text>
<text text-anchor="middle" x="1621" y="-502.5" font-family="Times,serif" font-size="14.00"> &#160;[type |&#45;&gt; &quot;Prepared&quot;, rm |&#45;&gt; s] }</text>
<text text-anchor="middle" x="1621" y="-486" font-family="Times,serif" font-size="14.00">/\ rmState = (r :&gt; &quot;aborted&quot; @@ s :&gt; &quot;prepared&quot;)</text>
<text text-anchor="middle" x="1621" y="-469.5" font-family="Times,serif" font-size="14.00">/\ tmState = &quot;done&quot;</text>
<text text-anchor="middle" x="1621" y="-453" font-family="Times,serif" font-size="14.00">/\ tmPrepared = {r}</text>
</g>
<!-- 879461406137672776&#45;&gt;&#45;2904203587503338029 -->
<g id="edge88" class="edge">
<title>879461406137672776&#45;&gt;&#45;2904203587503338029</title>
<path fill="none" stroke="#b2df8a" d="M403.68,-658.44C479.64,-635.47 576.74,-608.85 665,-592.96 755.45,-576.68 779.49,-583.51 871,-574.96 1054.51,-557.81 1263.12,-536.93 1413.66,-521.62"/>
<polygon fill="#b2df8a" stroke="#b2df8a" points="1413.76,-525.13 1423.35,-520.63 1413.05,-518.16 1413.76,-525.13"/>
<text text-anchor="middle" x="696.5" y="-596.16" font-family="Times,serif" font-size="14.00" fill="#000000">RMPrepare</text>
</g>
<!-- &#45;6380063824779124669 -->
<g id="node42" class="node">
<title>&#45;6380063824779124669</title>
<ellipse fill="none" stroke="black" cx="488" cy="-499.3" rx="253.14" ry="52.33"/>
<text text-anchor="middle" x="488" y="-519" font-family="Times,serif" font-size="14.00">/\ msgs = {[type |&#45;&gt; &quot;Abort&quot;], [type |&#45;&gt; &quot;Prepared&quot;, rm |&#45;&gt; r]}</text>
<text text-anchor="middle" x="488" y="-502.5" font-family="Times,serif" font-size="14.00">/\ rmState = (r :&gt; &quot;aborted&quot; @@ s :&gt; &quot;aborted&quot;)</text>
<text text-anchor="middle" x="488" y="-486" font-family="Times,serif" font-size="14.00">/\ tmState = &quot;done&quot;</text>
<text text-anchor="middle" x="488" y="-469.5" font-family="Times,serif" font-size="14.00">/\ tmPrepared = {r}</text>
</g>
<!-- 879461406137672776&#45;&gt;&#45;6380063824779124669 -->
<g id="edge89" class="edge">
<title>879461406137672776&#45;&gt;&#45;6380063824779124669</title>
<path fill="none" stroke="#fb9a99" d="M323.7,-651.72C354.4,-623.42 392.85,-587.99 424.83,-558.52"/>
<polygon fill="#fb9a99" stroke="#fb9a99" points="427.15,-561.14 432.13,-551.79 422.4,-556 427.15,-561.14"/>
<text text-anchor="middle" x="434.94" y="-596.16" font-family="Times,serif" font-size="14.00" fill="#000000">RMRcvAbortMsg</text>
</g>
<!-- &#45;6953470119458486193&#45;&gt;&#45;2904203587503338029 -->
<g id="edge90" class="edge">
<title>&#45;6953470119458486193&#45;&gt;&#45;2904203587503338029</title>
<path fill="none" stroke="#fb9a99" d="M2025.41,-648.7C1948.36,-620.42 1853.74,-585.7 1775.4,-556.96"/>
<polygon fill="#fb9a99" stroke="#fb9a99" points="1776.96,-553.8 1766.37,-553.65 1774.55,-560.38 1776.96,-553.8"/>
<text text-anchor="middle" x="1962.37" y="-596.16" font-family="Times,serif" font-size="14.00" fill="#000000">RMRcvAbortMsg</text>
</g>
<!-- 6799175484104903779 -->
<g id="node43" class="node">
<title>6799175484104903779</title>
<ellipse fill="none" stroke="black" cx="2171" cy="-499.3" rx="203.82" ry="75.66"/>
<text text-anchor="middle" x="2171" y="-535.5" font-family="Times,serif" font-size="14.00">/\ msgs = { [type |&#45;&gt; &quot;Abort&quot;],</text>
<text text-anchor="middle" x="2171" y="-519" font-family="Times,serif" font-size="14.00"> &#160;[type |&#45;&gt; &quot;Prepared&quot;, rm |&#45;&gt; r],</text>
<text text-anchor="middle" x="2171" y="-502.5" font-family="Times,serif" font-size="14.00"> &#160;[type |&#45;&gt; &quot;Prepared&quot;, rm |&#45;&gt; s] }</text>
<text text-anchor="middle" x="2171" y="-486" font-family="Times,serif" font-size="14.00">/\ rmState = (r :&gt; &quot;prepared&quot; @@ s :&gt; &quot;aborted&quot;)</text>
<text text-anchor="middle" x="2171" y="-469.5" font-family="Times,serif" font-size="14.00">/\ tmState = &quot;done&quot;</text>
<text text-anchor="middle" x="2171" y="-453" font-family="Times,serif" font-size="14.00">/\ tmPrepared = {r}</text>
</g>
<!-- &#45;6953470119458486193&#45;&gt;6799175484104903779 -->
<g id="edge91" class="edge">
<title>&#45;6953470119458486193&#45;&gt;6799175484104903779</title>
<path fill="none" stroke="#fb9a99" d="M2171,-626.97C2171,-613.75 2171,-599.9 2171,-586.41"/>
<polygon fill="#fb9a99" stroke="#fb9a99" points="2174.5,-586.69 2171,-576.69 2167.5,-586.69 2174.5,-586.69"/>
<text text-anchor="middle" x="2220.88" y="-596.16" font-family="Times,serif" font-size="14.00" fill="#000000">RMRcvAbortMsg</text>
</g>
<!-- 4374714672709322915&#45;&gt;4374714672709322915 -->
<g id="edge93" class="edge">
<title>4374714672709322915&#45;&gt;4374714672709322915</title>
<path fill="none" stroke="#fb9a99" d="M1160.71,-718.24C1182.48,-715.08 1196.14,-710.04 1196.14,-703.12 1196.14,-697.45 1186.95,-693.04 1171.63,-689.89"/>
<polygon fill="#fb9a99" stroke="#fb9a99" points="1172.65,-686.52 1162.2,-688.26 1171.46,-693.41 1172.65,-686.52"/>
<text text-anchor="middle" x="1246.02" y="-698.07" font-family="Times,serif" font-size="14.00" fill="#000000">RMRcvAbortMsg</text>
</g>
<!-- 4374714672709322915&#45;&gt;&#45;6380063824779124669 -->
<g id="edge92" class="edge">
<title>4374714672709322915&#45;&gt;&#45;6380063824779124669</title>
<path fill="none" stroke="#fb9a99" d="M841.76,-652.82C809.27,-632.89 770.49,-610.49 734,-592.96 700.73,-576.98 663.92,-561.84 629.14,-548.62"/>
<polygon fill="#fb9a99" stroke="#fb9a99" points="630.42,-545.36 619.83,-545.11 627.96,-551.91 630.42,-545.36"/>
<text text-anchor="middle" x="815.08" y="-596.16" font-family="Times,serif" font-size="14.00" fill="#000000">RMRcvAbortMsg</text>
</g>
<!-- 2252202094466483187&#45;&gt;2252202094466483187 -->
<g id="edge96" class="edge">
<title>2252202094466483187&#45;&gt;2252202094466483187</title>
<path fill="none" stroke="#e31a1c" d="M5329.44,-717.49C5351.7,-714.31 5365.4,-709.52 5365.4,-703.12 5365.4,-697.88 5356.18,-693.71 5340.58,-690.63"/>
<polygon fill="#e31a1c" stroke="#e31a1c" points="5341.38,-687.21 5330.94,-689.01 5340.22,-694.11 5341.38,-687.21"/>
<text text-anchor="middle" x="5410.78" y="-698.07" font-family="Times,serif" font-size="14.00" fill="#000000">TMRcvPrepared</text>
</g>
<!-- &#45;9061329653259454021 -->
<g id="node44" class="node">
<title>&#45;9061329653259454021</title>
<ellipse fill="none" stroke="black" cx="5048" cy="-499.3" rx="208.6" ry="75.66"/>
<text text-anchor="middle" x="5048" y="-535.5" font-family="Times,serif" font-size="14.00">/\ msgs = { [type |&#45;&gt; &quot;Commit&quot;],</text>
<text text-anchor="middle" x="5048" y="-519" font-family="Times,serif" font-size="14.00"> &#160;[type |&#45;&gt; &quot;Prepared&quot;, rm |&#45;&gt; r],</text>
<text text-anchor="middle" x="5048" y="-502.5" font-family="Times,serif" font-size="14.00"> &#160;[type |&#45;&gt; &quot;Prepared&quot;, rm |&#45;&gt; s] }</text>
<text text-anchor="middle" x="5048" y="-486" font-family="Times,serif" font-size="14.00">/\ rmState = (r :&gt; &quot;prepared&quot; @@ s :&gt; &quot;prepared&quot;)</text>
<text text-anchor="middle" x="5048" y="-469.5" font-family="Times,serif" font-size="14.00">/\ tmState = &quot;done&quot;</text>
<text text-anchor="middle" x="5048" y="-453" font-family="Times,serif" font-size="14.00">/\ tmPrepared = {r, s}</text>
</g>
<!-- 2252202094466483187&#45;&gt;&#45;9061329653259454021 -->
<g id="edge94" class="edge">
<title>2252202094466483187&#45;&gt;&#45;9061329653259454021</title>
<path fill="none" stroke="#fdbf6f" d="M5041.31,-650.41C5042.18,-630.92 5043.19,-608.18 5044.16,-586.39"/>
<polygon fill="#fdbf6f" stroke="#fdbf6f" points="5047.65,-586.76 5044.6,-576.61 5040.65,-586.45 5047.65,-586.76"/>
<text text-anchor="middle" x="5077.14" y="-596.16" font-family="Times,serif" font-size="14.00" fill="#000000">TMCommit</text>
</g>
<!-- &#45;2562013044076734382 -->
<g id="node45" class="node">
<title>&#45;2562013044076734382</title>
<ellipse fill="none" stroke="black" cx="4484" cy="-499.3" rx="208.6" ry="75.66"/>
<text text-anchor="middle" x="4484" y="-535.5" font-family="Times,serif" font-size="14.00">/\ msgs = { [type |&#45;&gt; &quot;Abort&quot;],</text>
<text text-anchor="middle" x="4484" y="-519" font-family="Times,serif" font-size="14.00"> &#160;[type |&#45;&gt; &quot;Prepared&quot;, rm |&#45;&gt; r],</text>
<text text-anchor="middle" x="4484" y="-502.5" font-family="Times,serif" font-size="14.00"> &#160;[type |&#45;&gt; &quot;Prepared&quot;, rm |&#45;&gt; s] }</text>
<text text-anchor="middle" x="4484" y="-486" font-family="Times,serif" font-size="14.00">/\ rmState = (r :&gt; &quot;prepared&quot; @@ s :&gt; &quot;prepared&quot;)</text>
<text text-anchor="middle" x="4484" y="-469.5" font-family="Times,serif" font-size="14.00">/\ tmState = &quot;done&quot;</text>
<text text-anchor="middle" x="4484" y="-453" font-family="Times,serif" font-size="14.00">/\ tmPrepared = {r, s}</text>
</g>
<!-- 2252202094466483187&#45;&gt;&#45;2562013044076734382 -->
<g id="edge95" class="edge">
<title>2252202094466483187&#45;&gt;&#45;2562013044076734382</title>
<path fill="none" stroke="#1f78b4" d="M4910.63,-655.44C4830.25,-626.21 4726.14,-588.35 4640.88,-557.35"/>
<polygon fill="#1f78b4" stroke="#1f78b4" points="4642.33,-554.15 4631.74,-554.03 4639.94,-560.73 4642.33,-554.15"/>
<text text-anchor="middle" x="4804.39" y="-596.16" font-family="Times,serif" font-size="14.00" fill="#000000">TMAbort</text>
</g>
<!-- &#45;2892638645983117404 -->
<g id="node46" class="node">
<title>&#45;2892638645983117404</title>
<ellipse fill="none" stroke="black" cx="5670" cy="-499.3" rx="203.82" ry="75.66"/>
<text text-anchor="middle" x="5670" y="-535.5" font-family="Times,serif" font-size="14.00">/\ msgs = { [type |&#45;&gt; &quot;Abort&quot;],</text>
<text text-anchor="middle" x="5670" y="-519" font-family="Times,serif" font-size="14.00"> &#160;[type |&#45;&gt; &quot;Prepared&quot;, rm |&#45;&gt; r],</text>
<text text-anchor="middle" x="5670" y="-502.5" font-family="Times,serif" font-size="14.00"> &#160;[type |&#45;&gt; &quot;Prepared&quot;, rm |&#45;&gt; s] }</text>
<text text-anchor="middle" x="5670" y="-486" font-family="Times,serif" font-size="14.00">/\ rmState = (r :&gt; &quot;aborted&quot; @@ s :&gt; &quot;prepared&quot;)</text>
<text text-anchor="middle" x="5670" y="-469.5" font-family="Times,serif" font-size="14.00">/\ tmState = &quot;done&quot;</text>
<text text-anchor="middle" x="5670" y="-453" font-family="Times,serif" font-size="14.00">/\ tmPrepared = {s}</text>
</g>
<!-- &#45;6923944097421231560&#45;&gt;&#45;2892638645983117404 -->
<g id="edge97" class="edge">
<title>&#45;6923944097421231560&#45;&gt;&#45;2892638645983117404</title>
<path fill="none" stroke="#fb9a99" d="M5678.18,-627.26C5677.33,-614.03 5676.43,-600.15 5675.56,-586.63"/>
<polygon fill="#fb9a99" stroke="#fb9a99" points="5679.07,-586.65 5674.93,-576.89 5672.08,-587.1 5679.07,-586.65"/>
<text text-anchor="middle" x="5726.76" y="-596.16" font-family="Times,serif" font-size="14.00" fill="#000000">RMRcvAbortMsg</text>
</g>
<!-- 6787765039504244244 -->
<g id="node47" class="node">
<title>6787765039504244244</title>
<ellipse fill="none" stroke="black" cx="6220" cy="-499.3" rx="203.82" ry="75.66"/>
<text text-anchor="middle" x="6220" y="-535.5" font-family="Times,serif" font-size="14.00">/\ msgs = { [type |&#45;&gt; &quot;Abort&quot;],</text>
<text text-anchor="middle" x="6220" y="-519" font-family="Times,serif" font-size="14.00"> &#160;[type |&#45;&gt; &quot;Prepared&quot;, rm |&#45;&gt; r],</text>
<text text-anchor="middle" x="6220" y="-502.5" font-family="Times,serif" font-size="14.00"> &#160;[type |&#45;&gt; &quot;Prepared&quot;, rm |&#45;&gt; s] }</text>
<text text-anchor="middle" x="6220" y="-486" font-family="Times,serif" font-size="14.00">/\ rmState = (r :&gt; &quot;prepared&quot; @@ s :&gt; &quot;aborted&quot;)</text>
<text text-anchor="middle" x="6220" y="-469.5" font-family="Times,serif" font-size="14.00">/\ tmState = &quot;done&quot;</text>
<text text-anchor="middle" x="6220" y="-453" font-family="Times,serif" font-size="14.00">/\ tmPrepared = {s}</text>
</g>
<!-- &#45;6923944097421231560&#45;&gt;6787765039504244244 -->
<g id="edge98" class="edge">
<title>&#45;6923944097421231560&#45;&gt;6787765039504244244</title>
<path fill="none" stroke="#fb9a99" d="M5826.91,-648.04C5901.09,-620.16 5991.57,-586.15 6067.02,-557.8"/>
<polygon fill="#fb9a99" stroke="#fb9a99" points="6068.01,-561.16 6076.14,-554.37 6065.55,-554.61 6068.01,-561.16"/>
<text text-anchor="middle" x="6017.48" y="-596.16" font-family="Times,serif" font-size="14.00" fill="#000000">RMRcvAbortMsg</text>
</g>
<!-- &#45;2707623536267266073&#45;&gt;&#45;2707623536267266073 -->
<g id="edge99" class="edge">
<title>&#45;2707623536267266073&#45;&gt;&#45;2707623536267266073</title>
<path fill="none" stroke="#fb9a99" d="M6413.64,-718.17C6435.18,-715.01 6448.67,-709.99 6448.67,-703.12 6448.67,-697.54 6439.76,-693.19 6424.87,-690.05"/>
<polygon fill="#fb9a99" stroke="#fb9a99" points="6425.59,-686.62 6415.13,-688.34 6424.37,-693.52 6425.59,-686.62"/>
<text text-anchor="middle" x="6498.55" y="-698.07" font-family="Times,serif" font-size="14.00" fill="#000000">RMRcvAbortMsg</text>
</g>
<!-- &#45;8033124516123851071 -->
<g id="node48" class="node">
<title>&#45;8033124516123851071</title>
<ellipse fill="none" stroke="black" cx="6820" cy="-499.3" rx="253.67" ry="52.33"/>
<text text-anchor="middle" x="6820" y="-519" font-family="Times,serif" font-size="14.00">/\ msgs = {[type |&#45;&gt; &quot;Abort&quot;], [type |&#45;&gt; &quot;Prepared&quot;, rm |&#45;&gt; s]}</text>
<text text-anchor="middle" x="6820" y="-502.5" font-family="Times,serif" font-size="14.00">/\ rmState = (r :&gt; &quot;aborted&quot; @@ s :&gt; &quot;aborted&quot;)</text>
<text text-anchor="middle" x="6820" y="-486" font-family="Times,serif" font-size="14.00">/\ tmState = &quot;done&quot;</text>
<text text-anchor="middle" x="6820" y="-469.5" font-family="Times,serif" font-size="14.00">/\ tmPrepared = {s}</text>
</g>
<!-- &#45;2707623536267266073&#45;&gt;&#45;8033124516123851071 -->
<g id="edge100" class="edge">
<title>&#45;2707623536267266073&#45;&gt;&#45;8033124516123851071</title>
<path fill="none" stroke="#fb9a99" d="M6253.79,-653.35C6295.32,-631.37 6347.02,-607.2 6396.25,-592.96 6464.04,-573.35 6484.75,-588.54 6554,-574.96 6592.4,-567.43 6633.34,-557.12 6671.3,-546.56"/>
<polygon fill="#fb9a99" stroke="#fb9a99" points="6671.78,-550.06 6680.46,-543.99 6669.89,-543.32 6671.78,-550.06"/>
<text text-anchor="middle" x="6446.12" y="-596.16" font-family="Times,serif" font-size="14.00" fill="#000000">RMRcvAbortMsg</text>
</g>
<!-- 5640263757456471582&#45;&gt;5640263757456471582 -->
<g id="edge103" class="edge">
<title>5640263757456471582&#45;&gt;5640263757456471582</title>
<path fill="none" stroke="#fb9a99" d="M7063.64,-718.17C7085.18,-715.01 7098.67,-709.99 7098.67,-703.12 7098.67,-697.54 7089.76,-693.19 7074.87,-690.05"/>
<polygon fill="#fb9a99" stroke="#fb9a99" points="7075.59,-686.62 7065.13,-688.34 7074.37,-693.52 7075.59,-686.62"/>
<text text-anchor="middle" x="7148.55" y="-698.07" font-family="Times,serif" font-size="14.00" fill="#000000">RMRcvAbortMsg</text>
</g>
<!-- 5640263757456471582&#45;&gt;6787765039504244244 -->
<g id="edge101" class="edge">
<title>5640263757456471582&#45;&gt;6787765039504244244</title>
<path fill="none" stroke="#b2df8a" d="M6688.7,-657.96C6598.2,-627.52 6477.34,-586.86 6381.03,-554.47"/>
<polygon fill="#b2df8a" stroke="#b2df8a" points="6382.33,-551.21 6371.74,-551.34 6380.1,-557.85 6382.33,-551.21"/>
<text text-anchor="middle" x="6569.49" y="-596.16" font-family="Times,serif" font-size="14.00" fill="#000000">RMPrepare</text>
</g>
<!-- 5640263757456471582&#45;&gt;&#45;8033124516123851071 -->
<g id="edge102" class="edge">
<title>5640263757456471582&#45;&gt;&#45;8033124516123851071</title>
<path fill="none" stroke="#fb9a99" d="M6820,-650.41C6820,-623.83 6820,-591.21 6820,-563.18"/>
<polygon fill="#fb9a99" stroke="#fb9a99" points="6823.5,-563.39 6820,-553.39 6816.5,-563.39 6823.5,-563.39"/>
<text text-anchor="middle" x="6869.88" y="-596.16" font-family="Times,serif" font-size="14.00" fill="#000000">RMRcvAbortMsg</text>
</g>
<!-- 1155799811345671651&#45;&gt;1155799811345671651 -->
<g id="edge104" class="edge">
<title>1155799811345671651&#45;&gt;1155799811345671651</title>
<path fill="none" stroke="#fb9a99" d="M3641.51,-514.42C3659.04,-511.26 3670.05,-506.22 3670.05,-499.3 3670.05,-494.01 3663.6,-489.81 3652.7,-486.72"/>
<polygon fill="#fb9a99" stroke="#fb9a99" points="3653.51,-483.31 3642.98,-484.52 3651.96,-490.14 3653.51,-483.31"/>
<text text-anchor="middle" x="3719.93" y="-494.25" font-family="Times,serif" font-size="14.00" fill="#000000">RMRcvAbortMsg</text>
</g>
<!-- &#45;2904203587503338029&#45;&gt;&#45;2904203587503338029 -->
<g id="edge105" class="edge">
<title>&#45;2904203587503338029&#45;&gt;&#45;2904203587503338029</title>
<path fill="none" stroke="#fb9a99" d="M1821.06,-514.35C1838.74,-511.19 1849.82,-506.17 1849.82,-499.3 1849.82,-493.99 1843.19,-489.79 1832.01,-486.69"/>
<polygon fill="#fb9a99" stroke="#fb9a99" points="1833.06,-483.34 1822.53,-484.58 1831.54,-490.17 1833.06,-483.34"/>
<text text-anchor="middle" x="1899.7" y="-494.25" font-family="Times,serif" font-size="14.00" fill="#000000">RMRcvAbortMsg</text>
</g>
<!-- 5203242854118256312 -->
<g id="node49" class="node">
<title>5203242854118256312</title>
<ellipse fill="none" stroke="black" cx="1876" cy="-295.48" rx="199.05" ry="75.66"/>
<text text-anchor="middle" x="1876" y="-331.68" font-family="Times,serif" font-size="14.00">/\ msgs = { [type |&#45;&gt; &quot;Abort&quot;],</text>
<text text-anchor="middle" x="1876" y="-315.18" font-family="Times,serif" font-size="14.00"> &#160;[type |&#45;&gt; &quot;Prepared&quot;, rm |&#45;&gt; r],</text>
<text text-anchor="middle" x="1876" y="-298.68" font-family="Times,serif" font-size="14.00"> &#160;[type |&#45;&gt; &quot;Prepared&quot;, rm |&#45;&gt; s] }</text>
<text text-anchor="middle" x="1876" y="-282.18" font-family="Times,serif" font-size="14.00">/\ rmState = (r :&gt; &quot;aborted&quot; @@ s :&gt; &quot;aborted&quot;)</text>
<text text-anchor="middle" x="1876" y="-265.68" font-family="Times,serif" font-size="14.00">/\ tmState = &quot;done&quot;</text>
<text text-anchor="middle" x="1876" y="-249.18" font-family="Times,serif" font-size="14.00">/\ tmPrepared = {r}</text>
</g>
<!-- &#45;2904203587503338029&#45;&gt;5203242854118256312 -->
<g id="edge106" class="edge">
<title>&#45;2904203587503338029&#45;&gt;5203242854118256312</title>
<path fill="none" stroke="#fb9a99" d="M1706.98,-430.26C1730.93,-411.3 1757.07,-390.61 1781.49,-371.28"/>
<polygon fill="#fb9a99" stroke="#fb9a99" points="1783.54,-374.12 1789.21,-365.17 1779.2,-368.63 1783.54,-374.12"/>
<text text-anchor="middle" x="1806.02" y="-392.34" font-family="Times,serif" font-size="14.00" fill="#000000">RMRcvAbortMsg</text>
</g>
<!-- &#45;6380063824779124669&#45;&gt;&#45;6380063824779124669 -->
<g id="edge107" class="edge">
<title>&#45;6380063824779124669&#45;&gt;&#45;6380063824779124669</title>
<path fill="none" stroke="#fb9a99" d="M730.71,-514.42C752.48,-511.26 766.14,-506.22 766.14,-499.3 766.14,-493.63 756.95,-489.22 741.63,-486.07"/>
<polygon fill="#fb9a99" stroke="#fb9a99" points="742.65,-482.7 732.2,-484.44 741.46,-489.59 742.65,-482.7"/>
<text text-anchor="middle" x="816.02" y="-494.25" font-family="Times,serif" font-size="14.00" fill="#000000">RMRcvAbortMsg</text>
</g>
<!-- 6799175484104903779&#45;&gt;6799175484104903779 -->
<g id="edge109" class="edge">
<title>6799175484104903779&#45;&gt;6799175484104903779</title>
<path fill="none" stroke="#fb9a99" d="M2371.06,-514.35C2388.74,-511.19 2399.82,-506.17 2399.82,-499.3 2399.82,-493.99 2393.19,-489.79 2382.01,-486.69"/>
<polygon fill="#fb9a99" stroke="#fb9a99" points="2383.06,-483.34 2372.53,-484.58 2381.54,-490.17 2383.06,-483.34"/>
<text text-anchor="middle" x="2449.7" y="-494.25" font-family="Times,serif" font-size="14.00" fill="#000000">RMRcvAbortMsg</text>
</g>
<!-- 6799175484104903779&#45;&gt;5203242854118256312 -->
<g id="edge108" class="edge">
<title>6799175484104903779&#45;&gt;5203242854118256312</title>
<path fill="none" stroke="#fb9a99" d="M2074.41,-432.22C2044.63,-411.85 2011.71,-389.33 1981.38,-368.57"/>
<polygon fill="#fb9a99" stroke="#fb9a99" points="1983.53,-365.81 1973.3,-363.05 1979.58,-371.59 1983.53,-365.81"/>
<text text-anchor="middle" x="2082.22" y="-392.34" font-family="Times,serif" font-size="14.00" fill="#000000">RMRcvAbortMsg</text>
</g>
<!-- &#45;8313463379096753413 -->
<g id="node50" class="node">
<title>&#45;8313463379096753413</title>
<ellipse fill="none" stroke="black" cx="5048" cy="-295.48" rx="217.08" ry="75.66"/>
<text text-anchor="middle" x="5048" y="-331.68" font-family="Times,serif" font-size="14.00">/\ msgs = { [type |&#45;&gt; &quot;Commit&quot;],</text>
<text text-anchor="middle" x="5048" y="-315.18" font-family="Times,serif" font-size="14.00"> &#160;[type |&#45;&gt; &quot;Prepared&quot;, rm |&#45;&gt; r],</text>
<text text-anchor="middle" x="5048" y="-298.68" font-family="Times,serif" font-size="14.00"> &#160;[type |&#45;&gt; &quot;Prepared&quot;, rm |&#45;&gt; s] }</text>
<text text-anchor="middle" x="5048" y="-282.18" font-family="Times,serif" font-size="14.00">/\ rmState = (r :&gt; &quot;committed&quot; @@ s :&gt; &quot;prepared&quot;)</text>
<text text-anchor="middle" x="5048" y="-265.68" font-family="Times,serif" font-size="14.00">/\ tmState = &quot;done&quot;</text>
<text text-anchor="middle" x="5048" y="-249.18" font-family="Times,serif" font-size="14.00">/\ tmPrepared = {r, s}</text>
</g>
<!-- &#45;9061329653259454021&#45;&gt;&#45;8313463379096753413 -->
<g id="edge110" class="edge">
<title>&#45;9061329653259454021&#45;&gt;&#45;8313463379096753413</title>
<path fill="none" stroke="#ff7f00" d="M5048,-423.15C5048,-409.93 5048,-396.08 5048,-382.59"/>
<polygon fill="#ff7f00" stroke="#ff7f00" points="5051.5,-382.87 5048,-372.87 5044.5,-382.87 5051.5,-382.87"/>
<text text-anchor="middle" x="5105" y="-392.34" font-family="Times,serif" font-size="14.00" fill="#000000">RMRcvCommitMsg</text>
</g>
<!-- &#45;7205743032094238923 -->
<g id="node51" class="node">
<title>&#45;7205743032094238923</title>
<ellipse fill="none" stroke="black" cx="5639" cy="-295.48" rx="217.08" ry="75.66"/>
<text text-anchor="middle" x="5639" y="-331.68" font-family="Times,serif" font-size="14.00">/\ msgs = { [type |&#45;&gt; &quot;Commit&quot;],</text>
<text text-anchor="middle" x="5639" y="-315.18" font-family="Times,serif" font-size="14.00"> &#160;[type |&#45;&gt; &quot;Prepared&quot;, rm |&#45;&gt; r],</text>
<text text-anchor="middle" x="5639" y="-298.68" font-family="Times,serif" font-size="14.00"> &#160;[type |&#45;&gt; &quot;Prepared&quot;, rm |&#45;&gt; s] }</text>
<text text-anchor="middle" x="5639" y="-282.18" font-family="Times,serif" font-size="14.00">/\ rmState = (r :&gt; &quot;prepared&quot; @@ s :&gt; &quot;committed&quot;)</text>
<text text-anchor="middle" x="5639" y="-265.68" font-family="Times,serif" font-size="14.00">/\ tmState = &quot;done&quot;</text>
<text text-anchor="middle" x="5639" y="-249.18" font-family="Times,serif" font-size="14.00">/\ tmPrepared = {r, s}</text>
</g>
<!-- &#45;9061329653259454021&#45;&gt;&#45;7205743032094238923 -->
<g id="edge111" class="edge">
<title>&#45;9061329653259454021&#45;&gt;&#45;7205743032094238923</title>
<path fill="none" stroke="#ff7f00" d="M5199.05,-446.72C5283.17,-417.99 5388.02,-382.19 5474.25,-352.74"/>
<polygon fill="#ff7f00" stroke="#ff7f00" points="5475.18,-356.12 5483.51,-349.58 5472.92,-349.5 5475.18,-356.12"/>
<text text-anchor="middle" x="5418.22" y="-392.34" font-family="Times,serif" font-size="14.00" fill="#000000">RMRcvCommitMsg</text>
</g>
<!-- &#45;8644419438773030967 -->
<g id="node52" class="node">
<title>&#45;8644419438773030967</title>
<ellipse fill="none" stroke="black" cx="3934" cy="-295.48" rx="203.82" ry="75.66"/>
<text text-anchor="middle" x="3934" y="-331.68" font-family="Times,serif" font-size="14.00">/\ msgs = { [type |&#45;&gt; &quot;Abort&quot;],</text>
<text text-anchor="middle" x="3934" y="-315.18" font-family="Times,serif" font-size="14.00"> &#160;[type |&#45;&gt; &quot;Prepared&quot;, rm |&#45;&gt; r],</text>
<text text-anchor="middle" x="3934" y="-298.68" font-family="Times,serif" font-size="14.00"> &#160;[type |&#45;&gt; &quot;Prepared&quot;, rm |&#45;&gt; s] }</text>
<text text-anchor="middle" x="3934" y="-282.18" font-family="Times,serif" font-size="14.00">/\ rmState = (r :&gt; &quot;aborted&quot; @@ s :&gt; &quot;prepared&quot;)</text>
<text text-anchor="middle" x="3934" y="-265.68" font-family="Times,serif" font-size="14.00">/\ tmState = &quot;done&quot;</text>
<text text-anchor="middle" x="3934" y="-249.18" font-family="Times,serif" font-size="14.00">/\ tmPrepared = {r, s}</text>
</g>
<!-- &#45;2562013044076734382&#45;&gt;&#45;8644419438773030967 -->
<g id="edge112" class="edge">
<title>&#45;2562013044076734382&#45;&gt;&#45;8644419438773030967</title>
<path fill="none" stroke="#fb9a99" d="M4338.41,-444.88C4261.36,-416.6 4166.74,-381.88 4088.4,-353.14"/>
<polygon fill="#fb9a99" stroke="#fb9a99" points="4089.96,-349.98 4079.37,-349.82 4087.55,-356.56 4089.96,-349.98"/>
<text text-anchor="middle" x="4275.37" y="-392.34" font-family="Times,serif" font-size="14.00" fill="#000000">RMRcvAbortMsg</text>
</g>
<!-- 4913074967764604375 -->
<g id="node53" class="node">
<title>4913074967764604375</title>
<ellipse fill="none" stroke="black" cx="4484" cy="-295.48" rx="203.82" ry="75.66"/>
<text text-anchor="middle" x="4484" y="-331.68" font-family="Times,serif" font-size="14.00">/\ msgs = { [type |&#45;&gt; &quot;Abort&quot;],</text>
<text text-anchor="middle" x="4484" y="-315.18" font-family="Times,serif" font-size="14.00"> &#160;[type |&#45;&gt; &quot;Prepared&quot;, rm |&#45;&gt; r],</text>
<text text-anchor="middle" x="4484" y="-298.68" font-family="Times,serif" font-size="14.00"> &#160;[type |&#45;&gt; &quot;Prepared&quot;, rm |&#45;&gt; s] }</text>
<text text-anchor="middle" x="4484" y="-282.18" font-family="Times,serif" font-size="14.00">/\ rmState = (r :&gt; &quot;prepared&quot; @@ s :&gt; &quot;aborted&quot;)</text>
<text text-anchor="middle" x="4484" y="-265.68" font-family="Times,serif" font-size="14.00">/\ tmState = &quot;done&quot;</text>
<text text-anchor="middle" x="4484" y="-249.18" font-family="Times,serif" font-size="14.00">/\ tmPrepared = {r, s}</text>
</g>
<!-- &#45;2562013044076734382&#45;&gt;4913074967764604375 -->
<g id="edge113" class="edge">
<title>&#45;2562013044076734382&#45;&gt;4913074967764604375</title>
<path fill="none" stroke="#fb9a99" d="M4484,-423.15C4484,-409.93 4484,-396.08 4484,-382.59"/>
<polygon fill="#fb9a99" stroke="#fb9a99" points="4487.5,-382.87 4484,-372.87 4480.5,-382.87 4487.5,-382.87"/>
<text text-anchor="middle" x="4533.88" y="-392.34" font-family="Times,serif" font-size="14.00" fill="#000000">RMRcvAbortMsg</text>
</g>
<!-- &#45;2892638645983117404&#45;&gt;&#45;2892638645983117404 -->
<g id="edge114" class="edge">
<title>&#45;2892638645983117404&#45;&gt;&#45;2892638645983117404</title>
<path fill="none" stroke="#fb9a99" d="M5870.06,-514.35C5887.74,-511.19 5898.82,-506.17 5898.82,-499.3 5898.82,-493.99 5892.19,-489.79 5881.01,-486.69"/>
<polygon fill="#fb9a99" stroke="#fb9a99" points="5882.06,-483.34 5871.53,-484.58 5880.54,-490.17 5882.06,-483.34"/>
<text text-anchor="middle" x="5948.7" y="-494.25" font-family="Times,serif" font-size="14.00" fill="#000000">RMRcvAbortMsg</text>
</g>
<!-- 5214283869744258255 -->
<g id="node54" class="node">
<title>5214283869744258255</title>
<ellipse fill="none" stroke="black" cx="6216" cy="-295.48" rx="199.05" ry="75.66"/>
<text text-anchor="middle" x="6216" y="-331.68" font-family="Times,serif" font-size="14.00">/\ msgs = { [type |&#45;&gt; &quot;Abort&quot;],</text>
<text text-anchor="middle" x="6216" y="-315.18" font-family="Times,serif" font-size="14.00"> &#160;[type |&#45;&gt; &quot;Prepared&quot;, rm |&#45;&gt; r],</text>
<text text-anchor="middle" x="6216" y="-298.68" font-family="Times,serif" font-size="14.00"> &#160;[type |&#45;&gt; &quot;Prepared&quot;, rm |&#45;&gt; s] }</text>
<text text-anchor="middle" x="6216" y="-282.18" font-family="Times,serif" font-size="14.00">/\ rmState = (r :&gt; &quot;aborted&quot; @@ s :&gt; &quot;aborted&quot;)</text>
<text text-anchor="middle" x="6216" y="-265.68" font-family="Times,serif" font-size="14.00">/\ tmState = &quot;done&quot;</text>
<text text-anchor="middle" x="6216" y="-249.18" font-family="Times,serif" font-size="14.00">/\ tmPrepared = {s}</text>
</g>
<!-- &#45;2892638645983117404&#45;&gt;5214283869744258255 -->
<g id="edge115" class="edge">
<title>&#45;2892638645983117404&#45;&gt;5214283869744258255</title>
<path fill="none" stroke="#fb9a99" d="M5813.46,-445.28C5890.41,-416.83 5985.25,-381.78 6063.53,-352.84"/>
<polygon fill="#fb9a99" stroke="#fb9a99" points="6064.39,-356.25 6072.56,-349.5 6061.96,-349.69 6064.39,-356.25"/>
<text text-anchor="middle" x="6009.25" y="-392.34" font-family="Times,serif" font-size="14.00" fill="#000000">RMRcvAbortMsg</text>
</g>
<!-- 6787765039504244244&#45;&gt;6787765039504244244 -->
<g id="edge117" class="edge">
<title>6787765039504244244&#45;&gt;6787765039504244244</title>
<path fill="none" stroke="#fb9a99" d="M6420.06,-514.35C6437.74,-511.19 6448.82,-506.17 6448.82,-499.3 6448.82,-493.99 6442.19,-489.79 6431.01,-486.69"/>
<polygon fill="#fb9a99" stroke="#fb9a99" points="6432.06,-483.34 6421.53,-484.58 6430.54,-490.17 6432.06,-483.34"/>
<text text-anchor="middle" x="6498.7" y="-494.25" font-family="Times,serif" font-size="14.00" fill="#000000">RMRcvAbortMsg</text>
</g>
<!-- 6787765039504244244&#45;&gt;5214283869744258255 -->
<g id="edge116" class="edge">
<title>6787765039504244244&#45;&gt;5214283869744258255</title>
<path fill="none" stroke="#fb9a99" d="M6218.51,-423.15C6218.25,-409.93 6217.97,-396.08 6217.71,-382.59"/>
<polygon fill="#fb9a99" stroke="#fb9a99" points="6221.21,-382.8 6217.51,-372.87 6214.21,-382.94 6221.21,-382.8"/>
<text text-anchor="middle" x="6267.99" y="-392.34" font-family="Times,serif" font-size="14.00" fill="#000000">RMRcvAbortMsg</text>
</g>
<!-- &#45;8033124516123851071&#45;&gt;&#45;8033124516123851071 -->
<g id="edge118" class="edge">
<title>&#45;8033124516123851071&#45;&gt;&#45;8033124516123851071</title>
<path fill="none" stroke="#fb9a99" d="M7063.64,-514.35C7085.18,-511.19 7098.67,-506.17 7098.67,-499.3 7098.67,-493.72 7089.76,-489.37 7074.87,-486.23"/>
<polygon fill="#fb9a99" stroke="#fb9a99" points="7075.59,-482.8 7065.13,-484.52 7074.37,-489.7 7075.59,-482.8"/>
<text text-anchor="middle" x="7148.55" y="-494.25" font-family="Times,serif" font-size="14.00" fill="#000000">RMRcvAbortMsg</text>
</g>
<!-- 5203242854118256312&#45;&gt;5203242854118256312 -->
<g id="edge119" class="edge">
<title>5203242854118256312&#45;&gt;5203242854118256312</title>
<path fill="none" stroke="#fb9a99" d="M2071.51,-310.6C2089.04,-307.44 2100.05,-302.4 2100.05,-295.48 2100.05,-290.19 2093.6,-285.99 2082.7,-282.9"/>
<polygon fill="#fb9a99" stroke="#fb9a99" points="2083.51,-279.49 2072.98,-280.7 2081.96,-286.32 2083.51,-279.49"/>
<text text-anchor="middle" x="2149.93" y="-290.43" font-family="Times,serif" font-size="14.00" fill="#000000">RMRcvAbortMsg</text>
</g>
<!-- &#45;8313463379096753413&#45;&gt;&#45;8313463379096753413 -->
<g id="edge120" class="edge">
<title>&#45;8313463379096753413&#45;&gt;&#45;8313463379096753413</title>
<path fill="none" stroke="#ff7f00" d="M5261.26,-310.25C5279.03,-307.07 5290.08,-302.15 5290.08,-295.48 5290.08,-290.32 5283.47,-286.21 5272.25,-283.14"/>
<polygon fill="#ff7f00" stroke="#ff7f00" points="5273.26,-279.78 5262.74,-281.04 5271.75,-286.61 5273.26,-279.78"/>
<text text-anchor="middle" x="5347.08" y="-290.43" font-family="Times,serif" font-size="14.00" fill="#000000">RMRcvCommitMsg</text>
</g>
<!-- &#45;4016352829786660666 -->
<g id="node55" class="node">
<title>&#45;4016352829786660666</title>
<ellipse fill="none" stroke="black" cx="5344" cy="-91.66" rx="225.57" ry="75.66"/>
<text text-anchor="middle" x="5344" y="-127.86" font-family="Times,serif" font-size="14.00">/\ msgs = { [type |&#45;&gt; &quot;Commit&quot;],</text>
<text text-anchor="middle" x="5344" y="-111.36" font-family="Times,serif" font-size="14.00"> &#160;[type |&#45;&gt; &quot;Prepared&quot;, rm |&#45;&gt; r],</text>
<text text-anchor="middle" x="5344" y="-94.86" font-family="Times,serif" font-size="14.00"> &#160;[type |&#45;&gt; &quot;Prepared&quot;, rm |&#45;&gt; s] }</text>
<text text-anchor="middle" x="5344" y="-78.36" font-family="Times,serif" font-size="14.00">/\ rmState = (r :&gt; &quot;committed&quot; @@ s :&gt; &quot;committed&quot;)</text>
<text text-anchor="middle" x="5344" y="-61.86" font-family="Times,serif" font-size="14.00">/\ tmState = &quot;done&quot;</text>
<text text-anchor="middle" x="5344" y="-45.36" font-family="Times,serif" font-size="14.00">/\ tmPrepared = {r, s}</text>
</g>
<!-- &#45;8313463379096753413&#45;&gt;&#45;4016352829786660666 -->
<g id="edge121" class="edge">
<title>&#45;8313463379096753413&#45;&gt;&#45;4016352829786660666</title>
<path fill="none" stroke="#ff7f00" d="M5146.15,-227.56C5174.85,-207.99 5206.38,-186.49 5235.68,-166.52"/>
<polygon fill="#ff7f00" stroke="#ff7f00" points="5237.56,-169.47 5243.85,-160.94 5233.62,-163.69 5237.56,-169.47"/>
<text text-anchor="middle" x="5261.88" y="-188.52" font-family="Times,serif" font-size="14.00" fill="#000000">RMRcvCommitMsg</text>
</g>
<!-- &#45;7205743032094238923&#45;&gt;&#45;7205743032094238923 -->
<g id="edge123" class="edge">
<title>&#45;7205743032094238923&#45;&gt;&#45;7205743032094238923</title>
<path fill="none" stroke="#ff7f00" d="M5852.26,-310.25C5870.03,-307.07 5881.08,-302.15 5881.08,-295.48 5881.08,-290.32 5874.47,-286.21 5863.25,-283.14"/>
<polygon fill="#ff7f00" stroke="#ff7f00" points="5864.26,-279.78 5853.74,-281.04 5862.75,-286.61 5864.26,-279.78"/>
<text text-anchor="middle" x="5938.08" y="-290.43" font-family="Times,serif" font-size="14.00" fill="#000000">RMRcvCommitMsg</text>
</g>
<!-- &#45;7205743032094238923&#45;&gt;&#45;4016352829786660666 -->
<g id="edge122" class="edge">
<title>&#45;7205743032094238923&#45;&gt;&#45;4016352829786660666</title>
<path fill="none" stroke="#ff7f00" d="M5541.18,-227.56C5512.58,-207.99 5481.15,-186.49 5451.96,-166.52"/>
<polygon fill="#ff7f00" stroke="#ff7f00" points="5454.04,-163.7 5443.81,-160.95 5450.09,-169.48 5454.04,-163.7"/>
<text text-anchor="middle" x="5557.35" y="-188.52" font-family="Times,serif" font-size="14.00" fill="#000000">RMRcvCommitMsg</text>
</g>
<!-- &#45;8644419438773030967&#45;&gt;&#45;8644419438773030967 -->
<g id="edge124" class="edge">
<title>&#45;8644419438773030967&#45;&gt;&#45;8644419438773030967</title>
<path fill="none" stroke="#fb9a99" d="M4134.06,-310.53C4151.74,-307.36 4162.82,-302.35 4162.82,-295.48 4162.82,-290.17 4156.19,-285.97 4145.01,-282.87"/>
<polygon fill="#fb9a99" stroke="#fb9a99" points="4146.06,-279.52 4135.53,-280.76 4144.54,-286.35 4146.06,-279.52"/>
<text text-anchor="middle" x="4212.7" y="-290.43" font-family="Times,serif" font-size="14.00" fill="#000000">RMRcvAbortMsg</text>
</g>
<!-- 8110929379837669015 -->
<g id="node56" class="node">
<title>8110929379837669015</title>
<ellipse fill="none" stroke="black" cx="4189" cy="-91.66" rx="199.05" ry="75.66"/>
<text text-anchor="middle" x="4189" y="-127.86" font-family="Times,serif" font-size="14.00">/\ msgs = { [type |&#45;&gt; &quot;Abort&quot;],</text>
<text text-anchor="middle" x="4189" y="-111.36" font-family="Times,serif" font-size="14.00"> &#160;[type |&#45;&gt; &quot;Prepared&quot;, rm |&#45;&gt; r],</text>
<text text-anchor="middle" x="4189" y="-94.86" font-family="Times,serif" font-size="14.00"> &#160;[type |&#45;&gt; &quot;Prepared&quot;, rm |&#45;&gt; s] }</text>
<text text-anchor="middle" x="4189" y="-78.36" font-family="Times,serif" font-size="14.00">/\ rmState = (r :&gt; &quot;aborted&quot; @@ s :&gt; &quot;aborted&quot;)</text>
<text text-anchor="middle" x="4189" y="-61.86" font-family="Times,serif" font-size="14.00">/\ tmState = &quot;done&quot;</text>
<text text-anchor="middle" x="4189" y="-45.36" font-family="Times,serif" font-size="14.00">/\ tmPrepared = {r, s}</text>
</g>
<!-- &#45;8644419438773030967&#45;&gt;8110929379837669015 -->
<g id="edge125" class="edge">
<title>&#45;8644419438773030967&#45;&gt;8110929379837669015</title>
<path fill="none" stroke="#fb9a99" d="M4019.98,-226.44C4043.93,-207.48 4070.07,-186.78 4094.49,-167.46"/>
<polygon fill="#fb9a99" stroke="#fb9a99" points="4096.54,-170.3 4102.21,-161.35 4092.2,-164.81 4096.54,-170.3"/>
<text text-anchor="middle" x="4119.02" y="-188.52" font-family="Times,serif" font-size="14.00" fill="#000000">RMRcvAbortMsg</text>
</g>
<!-- 4913074967764604375&#45;&gt;4913074967764604375 -->
<g id="edge127" class="edge">
<title>4913074967764604375&#45;&gt;4913074967764604375</title>
<path fill="none" stroke="#fb9a99" d="M4684.06,-310.53C4701.74,-307.36 4712.82,-302.35 4712.82,-295.48 4712.82,-290.17 4706.19,-285.97 4695.01,-282.87"/>
<polygon fill="#fb9a99" stroke="#fb9a99" points="4696.06,-279.52 4685.53,-280.76 4694.54,-286.35 4696.06,-279.52"/>
<text text-anchor="middle" x="4762.7" y="-290.43" font-family="Times,serif" font-size="14.00" fill="#000000">RMRcvAbortMsg</text>
</g>
<!-- 4913074967764604375&#45;&gt;8110929379837669015 -->
<g id="edge126" class="edge">
<title>4913074967764604375&#45;&gt;8110929379837669015</title>
<path fill="none" stroke="#fb9a99" d="M4387.41,-228.4C4357.63,-208.03 4324.71,-185.5 4294.38,-164.75"/>
<polygon fill="#fb9a99" stroke="#fb9a99" points="4296.53,-161.99 4286.3,-159.23 4292.58,-167.77 4296.53,-161.99"/>
<text text-anchor="middle" x="4395.22" y="-188.52" font-family="Times,serif" font-size="14.00" fill="#000000">RMRcvAbortMsg</text>
</g>
<!-- 5214283869744258255&#45;&gt;5214283869744258255 -->
<g id="edge128" class="edge">
<title>5214283869744258255&#45;&gt;5214283869744258255</title>
<path fill="none" stroke="#fb9a99" d="M6411.51,-310.6C6429.04,-307.44 6440.05,-302.4 6440.05,-295.48 6440.05,-290.19 6433.6,-285.99 6422.7,-282.9"/>
<polygon fill="#fb9a99" stroke="#fb9a99" points="6423.51,-279.49 6412.98,-280.7 6421.96,-286.32 6423.51,-279.49"/>
<text text-anchor="middle" x="6489.93" y="-290.43" font-family="Times,serif" font-size="14.00" fill="#000000">RMRcvAbortMsg</text>
</g>
<!-- &#45;4016352829786660666&#45;&gt;&#45;4016352829786660666 -->
<g id="edge129" class="edge">
<title>&#45;4016352829786660666&#45;&gt;&#45;4016352829786660666</title>
<path fill="none" stroke="#ff7f00" d="M5565.55,-106.29C5583.46,-103.1 5594.57,-98.23 5594.57,-91.66 5594.57,-86.58 5587.93,-82.51 5576.63,-79.46"/>
<polygon fill="#ff7f00" stroke="#ff7f00" points="5577.55,-76.08 5567.03,-77.36 5576.05,-82.92 5577.55,-76.08"/>
<text text-anchor="middle" x="5651.57" y="-86.61" font-family="Times,serif" font-size="14.00" fill="#000000">RMRcvCommitMsg</text>
</g>
<!-- 8110929379837669015&#45;&gt;8110929379837669015 -->
<g id="edge130" class="edge">
<title>8110929379837669015&#45;&gt;8110929379837669015</title>
<path fill="none" stroke="#fb9a99" d="M4384.51,-106.78C4402.04,-103.62 4413.05,-98.58 4413.05,-91.66 4413.05,-86.36 4406.6,-82.17 4395.7,-79.08"/>
<polygon fill="#fb9a99" stroke="#fb9a99" points="4396.51,-75.67 4385.98,-76.88 4394.96,-82.5 4396.51,-75.67"/>
<text text-anchor="middle" x="4462.93" y="-86.61" font-family="Times,serif" font-size="14.00" fill="#000000">RMRcvAbortMsg</text>
</g>
<!-- RMChooseToAbort -->
<g id="node57" class="node">
<title>RMChooseToAbort</title>
<polygon fill="#33a02c" stroke="black" points="7214.62,-1383.73 7214.62,-1419.73 7339.38,-1419.73 7339.38,-1383.73 7214.62,-1383.73"/>
<text text-anchor="middle" x="7277" y="-1396.68" font-family="Times,serif" font-size="14.00">RMChooseToAbort</text>
</g>
<!-- RMRcvAbortMsg -->
<g id="node58" class="node">
<title>RMRcvAbortMsg</title>
<polygon fill="#fb9a99" stroke="black" points="7364.12,-1383.73 7364.12,-1419.73 7479.88,-1419.73 7479.88,-1383.73 7364.12,-1383.73"/>
<text text-anchor="middle" x="7422" y="-1396.68" font-family="Times,serif" font-size="14.00">RMRcvAbortMsg</text>
</g>
<!-- TMAbort -->
<g id="node59" class="node">
<title>TMAbort</title>
<polygon fill="#1f78b4" stroke="black" points="7504.75,-1383.73 7504.75,-1419.73 7573.25,-1419.73 7573.25,-1383.73 7504.75,-1383.73"/>
<text text-anchor="middle" x="7539" y="-1396.68" font-family="Times,serif" font-size="14.00">TMAbort</text>
</g>
<!-- TMCommit -->
<g id="node60" class="node">
<title>TMCommit</title>
<polygon fill="#fdbf6f" stroke="black" points="7598.62,-1383.73 7598.62,-1419.73 7681.38,-1419.73 7681.38,-1383.73 7598.62,-1383.73"/>
<text text-anchor="middle" x="7640" y="-1396.68" font-family="Times,serif" font-size="14.00">TMCommit</text>
</g>
<!-- RMRcvCommitMsg -->
<g id="node61" class="node">
<title>RMRcvCommitMsg</title>
<polygon fill="#ff7f00" stroke="black" points="7706,-1383.73 7706,-1419.73 7836,-1419.73 7836,-1383.73 7706,-1383.73"/>
<text text-anchor="middle" x="7771" y="-1396.68" font-family="Times,serif" font-size="14.00">RMRcvCommitMsg</text>
</g>
<!-- RMPrepare -->
<g id="node62" class="node">
<title>RMPrepare</title>
<polygon fill="#b2df8a" stroke="black" points="7861.5,-1383.73 7861.5,-1419.73 7940.5,-1419.73 7940.5,-1383.73 7861.5,-1383.73"/>
<text text-anchor="middle" x="7901" y="-1396.68" font-family="Times,serif" font-size="14.00">RMPrepare</text>
</g>
<!-- TMRcvPrepared -->
<g id="node63" class="node">
<title>TMRcvPrepared</title>
<polygon fill="#e31a1c" stroke="black" points="7965.62,-1383.73 7965.62,-1419.73 8072.38,-1419.73 8072.38,-1383.73 7965.62,-1383.73"/>
<text text-anchor="middle" x="8019" y="-1396.68" font-family="Times,serif" font-size="14.00">TMRcvPrepared</text>
</g>
</g>
</svg>