src/img/trpl17-06.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.1.1 (20240910.0053)
 -->
<!-- Pages: 1 -->
<svg height="200pt"
 viewBox="0.00 0.00 906 771.00" xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink">
<g id="graph0" class="graph" transform="scale(4.16667 4.16667) rotate(0) translate(4 181)">
<polygon fill="white" stroke="none" points="-4,4 -4,-181 213.5,-181 213.5,4 -4,4"/>
<g id="clust1" class="cluster">
<title>cluster_box</title>
</g>
<g id="clust2" class="cluster">
<title>cluster_box_internal</title>
<polygon fill="none" stroke="black" points="82,-88 82,-132 111.5,-132 111.5,-88 82,-88"/>
<text text-anchor="middle" x="96.75" y="-114.7" font-family="Times,serif" font-size="14.00">b1</text>
</g>
<g id="clust3" class="cluster">
<title>cluster_deref</title>
<polygon fill="none" stroke="black" stroke-width="2" points="131.5,-8 131.5,-169 201.5,-169 201.5,-8 131.5,-8"/>
<text text-anchor="middle" x="166.5" y="-151.7" font-family="Times,serif" font-size="14.00">pinned</text>
</g>
<!-- pinned_box -->
<g id="node1" class="node">
<title>pinned_box</title>
<polyline fill="none" stroke="black" points="15,-109 39,-109"/>
<text text-anchor="start" x="18" y="-115.2" font-family="Times,serif" font-size="14.00">Pin</text>
<polygon fill="none" stroke="black" points="15,-86.5 15,-109 39,-109 39,-86.5 15,-86.5"/>
<text text-anchor="start" x="25.12" y="-92.7" font-family="Times,serif" font-size="14.00"> </text>
</g>
<!-- pin -->
<g id="node2" class="node">
<title>pin</title>
<ellipse fill="black" stroke="black" cx="96.25" cy="-98" rx="1.8" ry="1.8"/>
</g>
<!-- pinned_box&#45;&gt;pin -->
<g id="edge1" class="edge">
<title>pinned_box:c&#45;&gt;pin</title>
<path fill="none" stroke="black" d="M28,-97.75C28,-97.75 85.15,-97.96 94.08,-98"/>
</g>
<!-- box -->
<g id="node3" class="node">
<title>box</title>
<polyline fill="none" stroke="black" points="156,-109.75 177,-109.75"/>
<text text-anchor="start" x="159" y="-115.95" font-family="Times,serif" font-size="14.00">fut</text>
<polygon fill="none" stroke="black" points="156,-87.25 156,-109.75 177,-109.75 177,-87.25 156,-87.25"/>
<text text-anchor="start" x="163.12" y="-93.45" font-family="Times,serif" font-size="14.00">0</text>
<polygon fill="none" stroke="black" points="156,-64.75 156,-87.25 177,-87.25 177,-64.75 156,-64.75"/>
<text text-anchor="start" x="164.62" y="-70.95" font-family="Times,serif" font-size="14.00"> </text>
<polygon fill="none" stroke="black" stroke-dasharray="5,2" points="156,-42.25 156,-64.75 177,-64.75 177,-42.25 156,-42.25"/>
<text text-anchor="start" x="160.88" y="-48.45" font-family="Times,serif" font-size="14.00">...</text>
<polygon fill="none" stroke="black" points="156,-19.75 156,-42.25 177,-42.25 177,-19.75 156,-19.75"/>
<text text-anchor="start" x="163.12" y="-25.95" font-family="Times,serif" font-size="14.00">1</text>
</g>
<!-- pin&#45;&gt;box -->
<g id="edge2" class="edge">
<title>pin&#45;&gt;box:target</title>
<path fill="none" stroke="black" d="M97.25,-98C97.25,-98 120.73,-98.37 143.58,-98.47"/>
<polygon fill="black" stroke="black" points="143.48,-101.97 153.49,-98.5 143.5,-94.97 143.48,-101.97"/>
</g>
<!-- box&#45;&gt;box -->
<g id="edge3" class="edge">
<title>box:c&#45;&gt;box:internal</title>
<path fill="none" stroke="black" d="M166.5,-76C145.79,-85 104.38,-85 104.38,-53.5 104.38,-31.08 125.36,-24.62 144.93,-26"/>
<polygon fill="black" stroke="black" points="144.21,-29.43 154.62,-27.44 145.24,-22.51 144.21,-29.43"/>
</g>
</g>
</svg>