1234567891011121314151617181920212223242526272829303132333435363738394041424344454647484950515253545556575859606162636465 |
- <?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.40.1 (20161225.0304)
- -->
- <!-- Title: state transitions Pages: 1 -->
- <svg width="98pt" height="231pt"
- viewBox="0.00 0.00 98.00 231.00" 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 227)">
- <title>state transitions</title>
- <polygon fill="#ffffff" stroke="transparent" points="-4,4 -4,-227 94,-227 94,4 -4,4"/>
- <!-- __initial -->
- <g id="node1" class="node">
- <title>__initial</title>
- <ellipse fill="#000000" stroke="#000000" stroke-width="2" cx="45" cy="-217.5" rx="5.5" ry="5.5"/>
- </g>
- <!-- _a -->
- <g id="node4" class="node">
- <title>_a</title>
- <polygon fill="transparent" stroke="transparent" stroke-width="2" points="73,-184 17,-184 17,-148 73,-148 73,-184"/>
- <text text-anchor="start" x="41.6646" y="-162.2" font-family="Helvetica,sans-Serif" font-size="12.00" fill="#000000">a</text>
- <path fill="none" stroke="#000000" stroke-width="2" d="M29.3333,-149C29.3333,-149 60.6667,-149 60.6667,-149 66.3333,-149 72,-154.6667 72,-160.3333 72,-160.3333 72,-171.6667 72,-171.6667 72,-177.3333 66.3333,-183 60.6667,-183 60.6667,-183 29.3333,-183 29.3333,-183 23.6667,-183 18,-177.3333 18,-171.6667 18,-171.6667 18,-160.3333 18,-160.3333 18,-154.6667 23.6667,-149 29.3333,-149"/>
- </g>
- <!-- __initial->_a -->
- <g id="edge1" class="edge">
- <title>__initial->_a</title>
- <path fill="none" stroke="#000000" d="M45,-211.9886C45,-207.6293 45,-201.1793 45,-194.4801"/>
- <polygon fill="#000000" stroke="#000000" points="48.5001,-194.0122 45,-184.0122 41.5001,-194.0122 48.5001,-194.0122"/>
- <text text-anchor="middle" x="46.3895" y="-195" font-family="Helvetica,sans-Serif" font-size="10.00" fill="#000000"> </text>
- </g>
- <!-- _c -->
- <g id="node2" class="node">
- <title>_c</title>
- <polygon fill="transparent" stroke="transparent" stroke-width="2" points="90,-46 0,-46 0,0 90,0 90,-46"/>
- <text text-anchor="start" x="42" y="-29.2" font-family="Helvetica,sans-Serif" font-size="12.00" fill="#000000">c</text>
- <text text-anchor="start" x="5.8404" y="-9.2" font-family="Helvetica,sans-Serif" font-size="12.00" fill="#000000">enter ^out.in_c</text>
- <polygon fill="#000000" stroke="#000000" points="0,-23 0,-23 90,-23 90,-23 0,-23"/>
- <path fill="none" stroke="#000000" stroke-width="2" d="M13,-1C13,-1 77,-1 77,-1 83,-1 89,-7 89,-13 89,-13 89,-33 89,-33 89,-39 83,-45 77,-45 77,-45 13,-45 13,-45 7,-45 1,-39 1,-33 1,-33 1,-13 1,-13 1,-7 7,-1 13,-1"/>
- </g>
- <!-- _b -->
- <g id="node3" class="node">
- <title>_b</title>
- <polygon fill="transparent" stroke="transparent" stroke-width="2" points="90,-120 0,-120 0,-74 90,-74 90,-120"/>
- <text text-anchor="start" x="41.6646" y="-103.2" font-family="Helvetica,sans-Serif" font-size="12.00" fill="#000000">b</text>
- <text text-anchor="start" x="5.505" y="-83.2" font-family="Helvetica,sans-Serif" font-size="12.00" fill="#000000">enter ^out.in_b</text>
- <polygon fill="#000000" stroke="#000000" points="0,-97 0,-97 90,-97 90,-97 0,-97"/>
- <path fill="none" stroke="#000000" stroke-width="2" d="M13,-75C13,-75 77,-75 77,-75 83,-75 89,-81 89,-87 89,-87 89,-107 89,-107 89,-113 83,-119 77,-119 77,-119 13,-119 13,-119 7,-119 1,-113 1,-107 1,-107 1,-87 1,-87 1,-81 7,-75 13,-75"/>
- </g>
- <!-- _b->_c -->
- <g id="edge2" class="edge">
- <title>_b->_c</title>
- <path fill="none" stroke="#000000" d="M45,-73.9916C45,-68.476 45,-62.474 45,-56.5881"/>
- <polygon fill="#000000" stroke="#000000" points="48.5001,-56.249 45,-46.2491 41.5001,-56.2491 48.5001,-56.249"/>
- <text text-anchor="middle" x="46.3895" y="-57" font-family="Helvetica,sans-Serif" font-size="10.00" fill="#000000"> </text>
- </g>
- <!-- _a->_b -->
- <g id="edge3" class="edge">
- <title>_a->_b</title>
- <path fill="none" stroke="#000000" d="M45,-147.8711C45,-142.4482 45,-136.3229 45,-130.2494"/>
- <polygon fill="#000000" stroke="#000000" points="48.5001,-130.21 45,-120.21 41.5001,-130.21 48.5001,-130.21"/>
- <text text-anchor="middle" x="46.3895" y="-131" font-family="Helvetica,sans-Serif" font-size="10.00" fill="#000000"> </text>
- </g>
- </g>
- </svg>
|