src/img/trpl17-07.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="300pt"
 viewBox="0.00 0.00 1131.00 1000.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 236)">
<polygon fill="white" stroke="none" points="-4,4 -4,-236 267.4,-236 267.4,4 -4,4"/>
<g id="clust1" class="cluster">
<title>cluster_not_fut</title>
</g>
<g id="clust2" class="cluster">
<title>cluster_boxes</title>
</g>
<g id="clust3" class="cluster">
<title>cluster_box_1</title>
</g>
<g id="clust4" class="cluster">
<title>cluster_box_2_internal</title>
<polygon fill="lightgrey" stroke="black" points="118.45,-156 118.45,-200 147.95,-200 147.95,-156 118.45,-156"/>
<text text-anchor="middle" x="133.2" y="-182.7" font-family="Times,serif" font-size="14.00">b1</text>
</g>
<g id="clust5" class="cluster">
<title>cluster_box_2</title>
</g>
<g id="clust6" class="cluster">
<title>cluster_box_2_internal</title>
<polygon fill="none" stroke="black" points="118.45,-88 118.45,-132 147.95,-132 147.95,-88 118.45,-88"/>
<text text-anchor="middle" x="133.2" y="-114.7" font-family="Times,serif" font-size="14.00">b2</text>
</g>
<g id="clust7" class="cluster">
<title>cluster_target</title>
<polygon fill="none" stroke="black" stroke-width="2" points="185.4,-8 185.4,-169 255.4,-169 255.4,-8 185.4,-8"/>
<text text-anchor="middle" x="220.4" y="-151.7" font-family="Times,serif" font-size="14.00">pinned</text>
</g>
<!-- pin -->
<g id="node1" class="node">
<title>pin</title>
<polyline fill="none" stroke="black" points="31,-137 55,-137"/>
<text text-anchor="start" x="34" y="-143.2" font-family="Times,serif" font-size="14.00">Pin</text>
<polygon fill="none" stroke="black" points="31,-114.5 31,-137 55,-137 55,-114.5 31,-114.5"/>
<text text-anchor="start" x="41.12" y="-120.7" font-family="Times,serif" font-size="14.00"> </text>
</g>
<!-- box1 -->
<!-- pin&#45;&gt;box1 -->
<!-- box2 -->
<g id="node3" class="node">
<title>box2</title>
<ellipse fill="black" stroke="black" cx="132.7" cy="-98" rx="1.8" ry="1.8"/>
</g>
<!-- pin&#45;&gt;box2 -->
<g id="edge3" class="edge">
<title>pin:c&#45;&gt;box2</title>
<path fill="none" stroke="black" d="M44,-125.75C44,-125.75 119.8,-101.77 130.46,-98.39"/>
</g>
<!-- box1&#45;&gt;box2 -->
<!-- fut -->
<g id="node4" class="node">
<title>fut</title>
<polyline fill="none" stroke="black" points="209.9,-109.75 230.9,-109.75"/>
<text text-anchor="start" x="212.9" y="-115.95" font-family="Times,serif" font-size="14.00">fut</text>
<polygon fill="none" stroke="black" points="209.9,-87.25 209.9,-109.75 230.9,-109.75 230.9,-87.25 209.9,-87.25"/>
<text text-anchor="start" x="217.03" y="-93.45" font-family="Times,serif" font-size="14.00">0</text>
<polygon fill="none" stroke="black" points="209.9,-64.75 209.9,-87.25 230.9,-87.25 230.9,-64.75 209.9,-64.75"/>
<text text-anchor="start" x="218.53" y="-70.95" font-family="Times,serif" font-size="14.00"> </text>
<polygon fill="none" stroke="black" stroke-dasharray="5,2" points="209.9,-42.25 209.9,-64.75 230.9,-64.75 230.9,-42.25 209.9,-42.25"/>
<text text-anchor="start" x="214.78" y="-48.45" font-family="Times,serif" font-size="14.00">...</text>
<polygon fill="none" stroke="black" points="209.9,-19.75 209.9,-42.25 230.9,-42.25 230.9,-19.75 209.9,-19.75"/>
<text text-anchor="start" x="217.03" y="-25.95" font-family="Times,serif" font-size="14.00">1</text>
</g>
<!-- box2&#45;&gt;fut -->
<g id="edge4" class="edge">
<title>box2&#45;&gt;fut:target</title>
<path fill="none" stroke="black" d="M133.7,-98C133.7,-98 166.84,-98.4 197.7,-98.48"/>
<polygon fill="black" stroke="black" points="197.38,-101.98 207.39,-98.5 197.39,-94.98 197.38,-101.98"/>
</g>
<!-- fut&#45;&gt;fut -->
<g id="edge5" class="edge">
<title>fut:c&#45;&gt;fut:internal</title>
<path fill="none" stroke="black" d="M220.4,-76C196.78,-85 149.55,-85 149.55,-53.5 149.55,-30.13 175.54,-24.1 198.61,-26.22"/>
<polygon fill="black" stroke="black" points="198,-29.66 208.41,-27.71 199.05,-22.74 198,-29.66"/>
</g>
</g>
</svg>