russell@unturf.com
db29a08762
B&W print-friendly diagrams + tinkerpop-0001 + wave-3 proof sections. Squash of 94 local commits onto remote master.
70 lines
3.3 KiB
Text
70 lines
3.3 KiB
Text
// Diagram 1: Inference Variable Dependency Graph
|
|
// Represents the graph passed to GraphUtils.tarjan() in Infer.java:1908
|
|
// Nodes = unresolved inference variables (UndetVar)
|
|
// Edges = bound dependencies (T_i appears in bounds of T_j)
|
|
//
|
|
// Render: dot -Tsvg 0001-inference-graph.dot -o 0001-inference-graph.svg
|
|
|
|
digraph inference_graph {
|
|
graph [
|
|
label="Inference Variable Dependency Graph\n(input to GraphUtils.tarjan() — Infer.java:1908)"
|
|
labelloc=t
|
|
fontsize=14
|
|
fontname="monospace"
|
|
bgcolor="#f8f8f8"
|
|
pad=0.5
|
|
]
|
|
node [fontname="monospace" fontsize=11]
|
|
edge [fontname="monospace" fontsize=10]
|
|
|
|
// ── Unresolved inference variables ──────────────────────────────────────
|
|
T1 [label="T1\n(UndetVar)" shape=ellipse style=filled fillcolor="#fff8a0" penwidth=2]
|
|
T2 [label="T2\n(UndetVar)" shape=ellipse style=filled fillcolor="#fff8a0" penwidth=2]
|
|
T3 [label="T3\n(UndetVar)" shape=ellipse style=filled fillcolor="#fff8a0" penwidth=2]
|
|
T4 [label="T4\n(UndetVar)" shape=ellipse style=filled fillcolor="#fff8a0" penwidth=2]
|
|
T5 [label="T5\n(UndetVar)" shape=ellipse style=filled fillcolor="#fff8a0" penwidth=2]
|
|
|
|
// ── Resolved variable (leaf, no deps) ───────────────────────────────────
|
|
T6 [label="T6\n(resolved)" shape=ellipse style=filled fillcolor="#b8f0b8"]
|
|
|
|
// ── Bound dependencies ──────────────────────────────────────────────────
|
|
T1 -> T2 [label="bound" style=dashed color="#555555"]
|
|
T2 -> T3 [label="bound" style=dashed color="#555555"]
|
|
T3 -> T1 [label="bound" style=dashed color="#cc0000" penwidth=2 label="back edge\n(creates cycle)"]
|
|
T4 -> T2 [label="bound" style=dashed color="#555555"]
|
|
T4 -> T5 [label="bound" style=dashed color="#555555"]
|
|
T5 -> T6 [label="bound" style=dashed color="#555555"]
|
|
|
|
// ── SCC: T1+T2+T3 form a strongly connected component ──────────────────
|
|
subgraph cluster_scc {
|
|
label="SCC → merged into super-node {T1,T2,T3}"
|
|
style=dashed
|
|
color="#cc0000"
|
|
penwidth=2
|
|
fontcolor="#cc0000"
|
|
T1; T2; T3;
|
|
}
|
|
|
|
// ── After Tarjan: acyclic graph ─────────────────────────────────────────
|
|
supernode [
|
|
label="{T1,T2,T3}\nsuper-node"
|
|
shape=rectangle
|
|
style="filled,rounded"
|
|
fillcolor="#ffcccc"
|
|
penwidth=2
|
|
]
|
|
|
|
T4_copy [label="T4" shape=ellipse style=filled fillcolor="#fff8a0"]
|
|
T5_copy [label="T5" shape=ellipse style=filled fillcolor="#fff8a0"]
|
|
T6_copy [label="T6\n(resolved)" shape=ellipse style=filled fillcolor="#b8f0b8"]
|
|
|
|
subgraph cluster_acyclic {
|
|
label="Acyclic graph after Tarjan (Infer.java:1907-1918)"
|
|
style=solid
|
|
color="#0055aa"
|
|
fontcolor="#0055aa"
|
|
T4_copy -> supernode [label="bound" style=dashed color="#555555"]
|
|
T4_copy -> T5_copy [label="bound" style=dashed color="#555555"]
|
|
T5_copy -> T6_copy [label="bound" style=dashed color="#555555"]
|
|
}
|
|
}
|