documentation/vcg-example/trlc-Potato-Kitten.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 2.43.0 (0)
 -->
<!-- Title: %3 Pages: 1 -->
<svg width="1183pt" height="1749pt"
 viewBox="0.00 0.00 1182.99 1748.54" 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 1744.54)">
<title>%3</title>
<polygon fill="white" stroke="transparent" points="-4,4 -4,-1744.54 1178.99,-1744.54 1178.99,4 -4,4"/>
<!-- 0 -->
<g id="node1" class="node">
<title>0</title>
<ellipse fill="none" stroke="black" cx="632.73" cy="-1722.54" rx="36.29" ry="18"/>
<text text-anchor="start" x="612.73" y="-1719.84" font-family="Times,serif" font-weight="bold" font-size="14.00">Start</text>
</g>
<!-- 1 -->
<g id="node2" class="node">
<title>1</title>
<ellipse fill="none" stroke="black" cx="632.73" cy="-1553.99" rx="251.96" ry="114.6"/>
<text text-anchor="start" x="585.73" y="-1620.79" font-family="Times,serif" font-weight="bold" font-size="14.00">Assumption</text>
<text text-anchor="start" x="462.73" y="-1606.79" font-family="Times,serif" font-size="14.00">(declare&#45;fun |trlc.matches| (String String) Bool)</text>
<text text-anchor="start" x="493.73" y="-1592.79" font-family="Times,serif" font-size="14.00">;; value for a declared on potato.rsl:4:3</text>
<text text-anchor="start" x="485.23" y="-1578.79" font-family="Times,serif" font-size="14.00">(declare&#45;const |Potato.Kitten.a.value| Int)</text>
<text text-anchor="start" x="468.73" y="-1564.79" font-family="Times,serif" font-size="14.00">(define&#45;const |Potato.Kitten.a.valid| Bool true)</text>
<text text-anchor="start" x="493.23" y="-1550.79" font-family="Times,serif" font-size="14.00">;; value for b declared on potato.rsl:5:3</text>
<text text-anchor="start" x="485.23" y="-1536.79" font-family="Times,serif" font-size="14.00">(declare&#45;const |Potato.Kitten.b.value| Int)</text>
<text text-anchor="start" x="468.73" y="-1522.79" font-family="Times,serif" font-size="14.00">(define&#45;const |Potato.Kitten.b.valid| Bool true)</text>
<text text-anchor="start" x="494.23" y="-1508.79" font-family="Times,serif" font-size="14.00">;; value for c declared on potato.rsl:6:3</text>
<text text-anchor="start" x="485.73" y="-1494.79" font-family="Times,serif" font-size="14.00">(declare&#45;const |Potato.Kitten.c.value| Int)</text>
<text text-anchor="start" x="469.23" y="-1480.79" font-family="Times,serif" font-size="14.00">(define&#45;const |Potato.Kitten.c.valid| Bool true)</text>
</g>
<!-- 0&#45;&gt;1 -->
<g id="edge1" class="edge">
<title>0&#45;&gt;1</title>
<path fill="none" stroke="black" d="M632.73,-1704.35C632.73,-1697.3 632.73,-1688.5 632.73,-1678.71"/>
<polygon fill="black" stroke="black" points="636.23,-1678.62 632.73,-1668.62 629.23,-1678.62 636.23,-1678.62"/>
</g>
<!-- 2 -->
<g id="node3" class="node">
<title>2</title>
<ellipse fill="none" stroke="black" cx="632.73" cy="-1368.08" rx="149.4" ry="35.21"/>
<text text-anchor="start" x="608.23" y="-1378.88" font-family="Times,serif" font-weight="bold" font-size="14.00">Check</text>
<text text-anchor="start" x="557.73" y="-1364.88" font-family="Times,serif" font-size="14.00">;; validity check for a</text>
<text text-anchor="start" x="535.23" y="-1350.88" font-family="Times,serif" font-size="14.00">goal: |Potato.Kitten.a.valid|</text>
</g>
<!-- 1&#45;&gt;2 -->
<g id="edge2" class="edge">
<title>1&#45;&gt;2</title>
<path fill="none" stroke="black" d="M632.73,-1439.4C632.73,-1430.48 632.73,-1421.85 632.73,-1413.87"/>
<polygon fill="black" stroke="black" points="636.23,-1413.79 632.73,-1403.79 629.23,-1413.79 636.23,-1413.79"/>
</g>
<!-- 3 -->
<g id="node4" class="node">
<title>3</title>
<ellipse fill="none" stroke="black" cx="632.73" cy="-1261.37" rx="295.64" ry="35.21"/>
<text text-anchor="start" x="585.73" y="-1272.17" font-family="Times,serif" font-weight="bold" font-size="14.00">Assumption</text>
<text text-anchor="start" x="505.73" y="-1258.17" font-family="Times,serif" font-size="14.00">;; result of a &gt; 17 at potato.rsl:10:5</text>
<text text-anchor="start" x="431.73" y="-1244.17" font-family="Times,serif" font-size="14.00">(define&#45;const |tmp.1| Bool (&gt; |Potato.Kitten.a.value| 17))</text>
</g>
<!-- 2&#45;&gt;3 -->
<g id="edge3" class="edge">
<title>2&#45;&gt;3</title>
<path fill="none" stroke="black" d="M632.73,-1332.51C632.73,-1324.38 632.73,-1315.6 632.73,-1307.09"/>
<polygon fill="black" stroke="black" points="636.23,-1306.91 632.73,-1296.91 629.23,-1306.91 636.23,-1306.91"/>
</g>
<!-- 5 -->
<g id="node6" class="node">
<title>5</title>
<ellipse fill="none" stroke="black" cx="520.73" cy="-1164.56" rx="116.85" ry="25.41"/>
<text text-anchor="start" x="473.73" y="-1168.36" font-family="Times,serif" font-weight="bold" font-size="14.00">Assumption</text>
<text text-anchor="start" x="446.23" y="-1154.36" font-family="Times,serif" font-size="14.00">(assert (not |tmp.1|))</text>
</g>
<!-- 3&#45;&gt;5 -->
<g id="edge4" class="edge">
<title>3&#45;&gt;5</title>
<path fill="none" stroke="black" d="M592.3,-1226.14C580.59,-1216.23 567.89,-1205.49 556.49,-1195.83"/>
<polygon fill="black" stroke="black" points="558.73,-1193.14 548.83,-1189.35 554.2,-1198.48 558.73,-1193.14"/>
</g>
<!-- 7 -->
<g id="node8" class="node">
<title>7</title>
<ellipse fill="none" stroke="black" cx="777.73" cy="-1164.56" rx="89.61" ry="25.41"/>
<text text-anchor="start" x="730.73" y="-1168.36" font-family="Times,serif" font-weight="bold" font-size="14.00">Assumption</text>
<text text-anchor="start" x="722.23" y="-1154.36" font-family="Times,serif" font-size="14.00">(assert |tmp.1|)</text>
</g>
<!-- 3&#45;&gt;7 -->
<g id="edge5" class="edge">
<title>3&#45;&gt;7</title>
<path fill="none" stroke="black" d="M684.67,-1226.41C700.99,-1215.74 718.82,-1204.08 734.47,-1193.85"/>
<polygon fill="black" stroke="black" points="736.47,-1196.73 742.92,-1188.33 732.64,-1190.87 736.47,-1196.73"/>
</g>
<!-- 4 -->
<g id="node5" class="node">
<title>4</title>
<ellipse fill="none" stroke="black" cx="535.73" cy="-124.71" rx="37.09" ry="18"/>
<text text-anchor="start" x="515.23" y="-122.01" font-family="Times,serif" font-weight="bold" font-size="14.00">Node</text>
</g>
<!-- 17 -->
<g id="node18" class="node">
<title>17</title>
<ellipse fill="none" stroke="black" cx="339.73" cy="-35.36" rx="284.01" ry="35.21"/>
<text text-anchor="start" x="315.23" y="-46.16" font-family="Times,serif" font-weight="bold" font-size="14.00">Check</text>
<text text-anchor="start" x="146.73" y="-32.16" font-family="Times,serif" font-size="14.00">;; feasability check for a &gt; 17 and 100 / a + b * c &gt; 50</text>
<text text-anchor="start" x="294.23" y="-18.16" font-family="Times,serif" font-size="14.00">goal: |tmp.2|</text>
</g>
<!-- 4&#45;&gt;17 -->
<g id="edge6" class="edge">
<title>4&#45;&gt;17</title>
<path fill="none" stroke="black" d="M509.3,-111.93C487.24,-102.1 454.53,-87.52 423.71,-73.78"/>
<polygon fill="black" stroke="black" points="424.78,-70.43 414.22,-69.55 421.93,-76.82 424.78,-70.43"/>
</g>
<!-- 18 -->
<g id="node19" class="node">
<title>18</title>
<ellipse fill="none" stroke="black" cx="731.73" cy="-35.36" rx="89.61" ry="25.41"/>
<text text-anchor="start" x="684.73" y="-39.16" font-family="Times,serif" font-weight="bold" font-size="14.00">Assumption</text>
<text text-anchor="start" x="676.23" y="-25.16" font-family="Times,serif" font-size="14.00">(assert |tmp.2|)</text>
</g>
<!-- 4&#45;&gt;18 -->
<g id="edge7" class="edge">
<title>4&#45;&gt;18</title>
<path fill="none" stroke="black" d="M562.17,-111.93C591.16,-99.01 638.53,-77.89 675.85,-61.26"/>
<polygon fill="black" stroke="black" points="677.39,-64.41 685.1,-57.14 674.54,-58.01 677.39,-64.41"/>
</g>
<!-- 6 -->
<g id="node7" class="node">
<title>6</title>
<ellipse fill="none" stroke="black" cx="321.73" cy="-961.04" rx="321.97" ry="35.21"/>
<text text-anchor="start" x="274.73" y="-971.84" font-family="Times,serif" font-weight="bold" font-size="14.00">Assumption</text>
<text text-anchor="start" x="102.23" y="-957.84" font-family="Times,serif" font-size="14.00">;; result of a &gt; 17 and 100 / a + b * c &gt; 50 at potato.rsl:10:10</text>
<text text-anchor="start" x="208.23" y="-943.84" font-family="Times,serif" font-size="14.00">(define&#45;const |tmp.2| Bool false)</text>
</g>
<!-- 5&#45;&gt;6 -->
<g id="edge8" class="edge">
<title>5&#45;&gt;6</title>
<path fill="none" stroke="black" d="M496.73,-1139.25C463.57,-1105.68 403.28,-1044.62 362.87,-1003.7"/>
<polygon fill="black" stroke="black" points="365.33,-1001.21 355.81,-996.55 360.35,-1006.13 365.33,-1001.21"/>
</g>
<!-- 6&#45;&gt;4 -->
<g id="edge9" class="edge">
<title>6&#45;&gt;4</title>
<path fill="none" stroke="black" d="M332.08,-925.61C343.64,-884.06 360.73,-811.88 360.73,-748.62 360.73,-748.62 360.73,-748.62 360.73,-319.78 360.73,-254.73 356.14,-226.99 399.73,-178.71 423.05,-152.89 460.48,-139.52 490.18,-132.67"/>
<polygon fill="black" stroke="black" points="491.27,-136.02 500.32,-130.51 489.81,-129.17 491.27,-136.02"/>
</g>
<!-- 8 -->
<g id="node9" class="node">
<title>8</title>
<ellipse fill="none" stroke="black" cx="794.73" cy="-1067.75" rx="149.4" ry="35.21"/>
<text text-anchor="start" x="770.23" y="-1078.55" font-family="Times,serif" font-weight="bold" font-size="14.00">Check</text>
<text text-anchor="start" x="719.73" y="-1064.55" font-family="Times,serif" font-size="14.00">;; validity check for a</text>
<text text-anchor="start" x="697.23" y="-1050.55" font-family="Times,serif" font-size="14.00">goal: |Potato.Kitten.a.valid|</text>
</g>
<!-- 7&#45;&gt;8 -->
<g id="edge10" class="edge">
<title>7&#45;&gt;8</title>
<path fill="none" stroke="black" d="M782.2,-1138.65C783.6,-1130.84 785.19,-1121.98 786.76,-1113.24"/>
<polygon fill="black" stroke="black" points="790.25,-1113.58 788.57,-1103.12 783.36,-1112.34 790.25,-1113.58"/>
</g>
<!-- 9 -->
<g id="node10" class="node">
<title>9</title>
<ellipse fill="none" stroke="black" cx="811.73" cy="-961.04" rx="149.81" ry="35.21"/>
<text text-anchor="start" x="787.23" y="-971.84" font-family="Times,serif" font-weight="bold" font-size="14.00">Check</text>
<text text-anchor="start" x="736.23" y="-957.84" font-family="Times,serif" font-size="14.00">;; validity check for b</text>
<text text-anchor="start" x="713.73" y="-943.84" font-family="Times,serif" font-size="14.00">goal: |Potato.Kitten.b.valid|</text>
</g>
<!-- 8&#45;&gt;9 -->
<g id="edge11" class="edge">
<title>8&#45;&gt;9</title>
<path fill="none" stroke="black" d="M800.35,-1032.18C801.68,-1023.95 803.12,-1015.07 804.52,-1006.48"/>
<polygon fill="black" stroke="black" points="807.98,-1007.01 806.13,-996.58 801.07,-1005.89 807.98,-1007.01"/>
</g>
<!-- 10 -->
<g id="node11" class="node">
<title>10</title>
<ellipse fill="none" stroke="black" cx="801.73" cy="-854.33" rx="148.48" ry="35.21"/>
<text text-anchor="start" x="777.23" y="-865.13" font-family="Times,serif" font-weight="bold" font-size="14.00">Check</text>
<text text-anchor="start" x="727.23" y="-851.13" font-family="Times,serif" font-size="14.00">;; validity check for c</text>
<text text-anchor="start" x="704.73" y="-837.13" font-family="Times,serif" font-size="14.00">goal: |Potato.Kitten.c.valid|</text>
</g>
<!-- 9&#45;&gt;10 -->
<g id="edge12" class="edge">
<title>9&#45;&gt;10</title>
<path fill="none" stroke="black" d="M808.43,-925.46C807.65,-917.33 806.82,-908.55 806,-900.05"/>
<polygon fill="black" stroke="black" points="809.47,-899.49 805.03,-889.87 802.5,-900.16 809.47,-899.49"/>
</g>
<!-- 11 -->
<g id="node12" class="node">
<title>11</title>
<ellipse fill="none" stroke="black" cx="791.73" cy="-747.62" rx="383" ry="35.21"/>
<text text-anchor="start" x="744.73" y="-758.42" font-family="Times,serif" font-weight="bold" font-size="14.00">Assumption</text>
<text text-anchor="start" x="667.73" y="-744.42" font-family="Times,serif" font-size="14.00">;; result of b * c at potato.rsl:10:27</text>
<text text-anchor="start" x="528.73" y="-730.42" font-family="Times,serif" font-size="14.00">(define&#45;const |tmp.3| Int (* |Potato.Kitten.b.value| |Potato.Kitten.c.value|))</text>
</g>
<!-- 10&#45;&gt;11 -->
<g id="edge13" class="edge">
<title>10&#45;&gt;11</title>
<path fill="none" stroke="black" d="M798.43,-818.75C797.65,-810.62 796.82,-801.84 796,-793.34"/>
<polygon fill="black" stroke="black" points="799.47,-792.78 795.03,-783.16 792.5,-793.45 799.47,-792.78"/>
</g>
<!-- 12 -->
<g id="node13" class="node">
<title>12</title>
<ellipse fill="none" stroke="black" cx="788.73" cy="-640.91" rx="311.25" ry="35.21"/>
<text text-anchor="start" x="741.73" y="-651.71" font-family="Times,serif" font-weight="bold" font-size="14.00">Assumption</text>
<text text-anchor="start" x="650.23" y="-637.71" font-family="Times,serif" font-size="14.00">;; result of a + b * c at potato.rsl:10:23</text>
<text text-anchor="start" x="576.73" y="-623.71" font-family="Times,serif" font-size="14.00">(define&#45;const |tmp.4| Int (+ |Potato.Kitten.a.value| |tmp.3|))</text>
</g>
<!-- 11&#45;&gt;12 -->
<g id="edge14" class="edge">
<title>11&#45;&gt;12</title>
<path fill="none" stroke="black" d="M790.74,-712.04C790.51,-703.91 790.26,-695.13 790.01,-686.63"/>
<polygon fill="black" stroke="black" points="793.51,-686.34 789.72,-676.45 786.51,-686.54 793.51,-686.34"/>
</g>
<!-- 13 -->
<g id="node14" class="node">
<title>13</title>
<ellipse fill="none" stroke="black" cx="748.73" cy="-534.2" rx="225.63" ry="35.21"/>
<text text-anchor="start" x="724.23" y="-545" font-family="Times,serif" font-weight="bold" font-size="14.00">Check</text>
<text text-anchor="start" x="597.23" y="-531" font-family="Times,serif" font-size="14.00">;; division by zero check for 100 / a + b * c</text>
<text text-anchor="start" x="664.23" y="-517" font-family="Times,serif" font-size="14.00">goal: (not (= |tmp.4| 0))</text>
</g>
<!-- 12&#45;&gt;13 -->
<g id="edge15" class="edge">
<title>12&#45;&gt;13</title>
<path fill="none" stroke="black" d="M775.53,-605.33C772.35,-597.02 768.92,-588.03 765.6,-579.35"/>
<polygon fill="black" stroke="black" points="768.77,-577.83 761.93,-569.74 762.23,-580.33 768.77,-577.83"/>
</g>
<!-- 14 -->
<g id="node15" class="node">
<title>14</title>
<ellipse fill="none" stroke="black" cx="745.73" cy="-427.49" rx="251.96" ry="35.21"/>
<text text-anchor="start" x="698.73" y="-438.29" font-family="Times,serif" font-weight="bold" font-size="14.00">Assumption</text>
<text text-anchor="start" x="586.73" y="-424.29" font-family="Times,serif" font-size="14.00">;; result of 100 / a + b * c at potato.rsl:10:18</text>
<text text-anchor="start" x="575.73" y="-410.29" font-family="Times,serif" font-size="14.00">(define&#45;const |tmp.5| Int (floor_div 100 |tmp.4|))</text>
</g>
<!-- 13&#45;&gt;14 -->
<g id="edge16" class="edge">
<title>13&#45;&gt;14</title>
<path fill="none" stroke="black" d="M747.74,-498.62C747.51,-490.49 747.26,-481.71 747.01,-473.2"/>
<polygon fill="black" stroke="black" points="750.51,-472.92 746.72,-463.03 743.51,-473.12 750.51,-472.92"/>
</g>
<!-- 15 -->
<g id="node16" class="node">
<title>15</title>
<ellipse fill="none" stroke="black" cx="740.73" cy="-320.78" rx="263.5" ry="35.21"/>
<text text-anchor="start" x="693.73" y="-331.58" font-family="Times,serif" font-weight="bold" font-size="14.00">Assumption</text>
<text text-anchor="start" x="562.23" y="-317.58" font-family="Times,serif" font-size="14.00">;; result of 100 / a + b * c &gt; 50 at potato.rsl:10:32</text>
<text text-anchor="start" x="593.73" y="-303.58" font-family="Times,serif" font-size="14.00">(define&#45;const |tmp.6| Bool (&gt; |tmp.5| 50))</text>
</g>
<!-- 14&#45;&gt;15 -->
<g id="edge17" class="edge">
<title>14&#45;&gt;15</title>
<path fill="none" stroke="black" d="M744.08,-391.91C743.69,-383.78 743.27,-375 742.87,-366.49"/>
<polygon fill="black" stroke="black" points="746.36,-366.14 742.38,-356.32 739.36,-366.47 746.36,-366.14"/>
</g>
<!-- 16 -->
<g id="node17" class="node">
<title>16</title>
<ellipse fill="none" stroke="black" cx="730.73" cy="-214.07" rx="321.97" ry="35.21"/>
<text text-anchor="start" x="683.73" y="-224.87" font-family="Times,serif" font-weight="bold" font-size="14.00">Assumption</text>
<text text-anchor="start" x="511.23" y="-210.87" font-family="Times,serif" font-size="14.00">;; result of a &gt; 17 and 100 / a + b * c &gt; 50 at potato.rsl:10:10</text>
<text text-anchor="start" x="608.73" y="-196.87" font-family="Times,serif" font-size="14.00">(define&#45;const |tmp.2| Bool |tmp.6|)</text>
</g>
<!-- 15&#45;&gt;16 -->
<g id="edge18" class="edge">
<title>15&#45;&gt;16</title>
<path fill="none" stroke="black" d="M737.43,-285.2C736.65,-277.07 735.82,-268.29 735,-259.78"/>
<polygon fill="black" stroke="black" points="738.47,-259.23 734.03,-249.61 731.5,-259.89 738.47,-259.23"/>
</g>
<!-- 16&#45;&gt;4 -->
<g id="edge19" class="edge">
<title>16&#45;&gt;4</title>
<path fill="none" stroke="black" d="M656.18,-179.67C627.07,-166.63 595.07,-152.29 571.38,-141.68"/>
<polygon fill="black" stroke="black" points="572.64,-138.41 562.09,-137.52 569.78,-144.8 572.64,-138.41"/>
</g>
</g>
</svg>