Render a ExTLA.Spec module's state graph as DOT, for Graphviz.
Usage
mix extla.visualize Specs.TransferProtocol
mix extla.visualize Specs.TransferProtocol --output graph.dot
mix extla.visualize Specs.TransferProtocol --max-states 2000
mix extla.visualize Specs.X --output g.dot && dot -Tsvg g.dot -o g.svgConstants come from the same two places mix extla.check takes them from, in the
same order of precedence, and a constant with neither is the same error.
What it draws
Every reachable state as a node labelled with its variables, and every transition as an
edge labelled with its action and that action's parameter binding. Initial states carry a
double border, declared terminal states a doubled octagon, and deadlocked states a
fill.
A spec whose invariant is refuted is drawn with its counterexample emphasised, and the run says so. That graph is partial — the search stopped at the violation — which is the honest picture of what was explored rather than of the whole state space.
Options
--output Write here instead of to stdout.
--max-states How many states to explore, and therefore at most how many
to draw (default 500).
--format dot, and only dot. See below.Why DOT only
DOT is enough: Graphviz renders it to SVG, PNG or PDF, and a bespoke viewer would be one
more thing to maintain. A --format html or --format mermaid is refused with a message
saying so rather than silently ignored.
Why it refuses a large graph, and why the search stops there too
Node labels are regenerated by replay, because the state graph keeps fingerprints rather
than states, and a layout engine given tens of thousands of nodes returns a hairball
rather than a picture.
Past --max-states the task refuses: rendering the first 500 of 58,359 would hand back
something that looks complete.
--max-states bounds the search as well, and means the same thing here as in
mix extla.check — how many states to explore. Exploring past a limit the task will refuse
to draw is work thrown away.
The cost is stated rather than hidden: a bounded search cannot name the real size of the state space, so the refusal says more than N instead of a number it does not have. The action is the same either way: raise the flag, or shrink the model.
Exit codes
0 the graph was written
1 the spec has a violation; the graph was still written, with the
counterexample emphasised, and it covers only what the search reached
2 more states than `--max-states`, so nothing was drawnExit code 1 is not a failure of the task. It is the same distinction mix extla.check
draws: the picture is real, and it is a picture of an interrupted search.
Exit code 2 is not a failure of the spec. It is mix extla.check's code for a run that did
not see the whole state space, and it is separate from 1 because "too big to draw" and
"the design is wrong" are different answers.