The state graph built during model checking. Nodes are states, edges are labeled transitions.
Memory model: fingerprints and parent pointers, not states
The graph does NOT retain the states it has explored. Each visited state contributes one fixed-size record:
fingerprint => {state_id, parent_id, action_name, params}A state is materialized only while its successors are being computed, and then
discarded. When a trace is needed — once, on violation — the path is walked
back to an initial state through the parent pointers and the states are
regenerated by replaying the recorded actions forward from init.
Storing every state for the whole run would, at 10M states of roughly 1KB each, need about 10GB of RAM, which puts the checker out of reach of the machines people actually have. The record above is on the order of 64 bytes regardless of how large a state is, so memory becomes a function of the state count rather than of state size — and trace generation, which happens at most once per run, pays the replay cost instead. This is the same trade TLC makes.
The consequence to be aware of: a spec whose actions are expensive to apply pays that cost twice on the failing path. That is the right place for it to fall.
Why the graph carries the spec and the constants
Replay needs them. path_to/2 recovers a list of {action, params}, and
turning that back into states means running init and then each action —
which cannot be done from the identifiers alone. ExTLA.Trace.generate/3 takes
only the graph and a state id, so the graph is where they have to live.
Why an initial state records which init produced it
Several init blocks are disjuncted (02-dsl-semantics.md), so replay has to
know which one to run for the root of the path. node_record.init_index
carries it; it is nil for every non-initial state, where action and
params say what happened instead.
The liveness graph is a separate, opt-in structure
Parent pointers are a spanning tree: every node has one in-edge, the tree is
acyclic by construction, and no cycle of the real graph is visible in it.
Liveness checking is cycle detection, so this record cannot support it — which
is why successors/2 reads an edge table and raises when there is none, rather
than deriving something wrong from parent pointers.
So a run that asks for it records, additionally, per expanded state:
state_id => [{action, params, successor_id}] # every out-edge
state_id => enabled_bits # one bit per fairness constraintThe edge table is what an SCC search runs over. The bits are what fairness needs: WF
and SF are conditions on ENABLED A at each state of a cycle, which is a function of
the state — and the state is discarded as soon as it has been expanded, so the bit has
to be taken while it is still in hand. They are indexed by fairness_index, the
expansion (02-dsl-semantics.md §5.2) of the spec's fairness declarations (ExTLA.Temporal.Fairness).
Cost is a function of the branching factor and of how large a binding is — an action whose param is a message record carries that record in every edge — but not of how large a state is, which is the property the record above exists to keep. It is opt-in for that reason and paid for only when asked for, which is TLC's split too.
Only an expanded state has edges. A run that stopped early — max_states, a state
constraint holding states back, a safety violation halting the search — leaves a
partial edge table, and a liveness verdict read off a partial graph would be a claim
about behaviours that were never explored. Checking one is a completed run's privilege.
ETS
nodes and fingerprints are ETS tables, owned by the process that called
new/3 and deleted when it exits. The struct itself carries only the table
identifiers and the counters, so add_state/5 returning an updated struct is
about the counters; the tables are mutated in place. That is the shape the
parallel checker (workers:) needs, and it costs nothing in a single process.
Summary
Functions
Record a state's out-edges and its enabled bits. Called once per expanded state; a no-op on a safety-only graph, so the caller does not branch.
Register a state by fingerprint, returning its id and whether it is new. The state itself is not retained.
Count one transition, whether or not it discovered a new state.
Release the graph's two ETS tables.
The BFS level of a state: 1 for an initial state, one more than its parent otherwise. Equal to the number of states on the shortest path to it, which is the number TLC reports as a counterexample's length.
Whether the indexth fairness constraint was enabled in a state.
The ENABLED bits of a state, in fairness_index order.
The id this graph knows a state by, or nil if it never registered one.
How many distinct states are registered right now, read from the shared fingerprint
table rather than from this struct's state_count.
Whether this graph carries the liveness structure.
Mark an expanded state that has no successors and that no terminal predicate
admits.
Mark an expanded state that has no successors.
A new, empty graph for spec under constants.
The node record for a state id.
The action path from an initial state to the target, walked through parent
pointers. ExTLA.Trace replays this to regenerate the states themselves.
Every strongly connected component of the edge table, as sets of state ids.
The same, over a subset of the states — the edges to anything outside it are ignored.
The state an id names, regenerated by replaying the path to it.
Successors of a state, from the edge table.
Export as DOT for Graphviz.
Export as JSON for tooling and editor integration.
Turn on the liveness graph, with the fairness constraints its enabled bits are indexed
by — ExTLA.Temporal.Fairness.expand/3, which needs the constants and so cannot run
until a state exists.
Types
@type node_record() :: %{ parent: state_id() | nil, action: atom() | nil, params: map() | nil, init_index: non_neg_integer() | nil, depth: pos_integer() }
@type state_id() :: non_neg_integer()
@type t() :: %ExTLA.StateGraph{ constants: map(), deadlocked: MapSet.t(state_id()), diameter: non_neg_integer(), edges: %{required(state_id()) => [edge()]} | nil, enabled: %{required(state_id()) => bitstring()} | nil, fairness_index: [{ExTLA.Spec.Compiled.fairness_def(), map()}] | nil, fingerprint_bits: 64 | 128, fingerprints: :ets.table(), ids: :atomics.atomics_ref(), initial_states: MapSet.t(state_id()), nodes: :ets.table(), spec: ExTLA.Spec.Compiled.t(), state_count: non_neg_integer(), symmetry: [ExTLA.Symmetry.mapping()] | nil, terminal: MapSet.t(state_id()), transition_count: non_neg_integer() }
Functions
Record a state's out-edges and its enabled bits. Called once per expanded state; a no-op on a safety-only graph, so the caller does not branch.
Every out-edge, including the ones that led to a state already seen — those are exactly the edges that close a cycle, and a cycle is what liveness checking is looking for.
Register a state by fingerprint, returning its id and whether it is new. The state itself is not retained.
parent is nil for an initial state, in which case action is the index of
the init block that produced it.
A newly discovered state is validated here (ExTLA.State.validate!/1, the
02-dsl-semantics.md §6 restriction on pids, references, ports, funs and floats), and a state already seen is
not — it was validated when it was first found. This is the graph's job rather than the
caller's because §6 exists for fingerprinting: the terms it rejects are exactly those
whose encoding does not identify a state. Callers may assume that a state which has
entered the graph is one the checker has vetted.
Count one transition, whether or not it discovered a new state.
Release the graph's two ETS tables.
For a caller that holds a graph longer than the process that built it: an ETS table is
owned by a process, not reachable from a term, so dropping the last reference to a graph
frees nothing. ExTLA.ModelChecker.explore/2 hands the graph — and this obligation — to
its caller; run/2 discards the graph and searches in a process of its own so that the
process's exit does this.
Returns :ok, and is a no-op on a graph whose tables are already gone, so a caller that
releases twice, or that releases a graph its owner has already taken down with it, is
not punished for being careful.
The BFS level of a state: 1 for an initial state, one more than its parent otherwise. Equal to the number of states on the shortest path to it, which is the number TLC reports as a counterexample's length.
Whether the indexth fairness constraint was enabled in a state.
The ENABLED bits of a state, in fairness_index order.
The id this graph knows a state by, or nil if it never registered one.
Fingerprinted the same way add_state/5 fingerprints — under the run's symmetry
mapping, if it has one — so a state and its symmetric twin give the same id, which is
what makes the answer meaningful under a reduction rather than merely defined.
ExTLA.Trace carries states rather than ids, because a behaviour is meaningful without
the graph that found it. This is how a caller holding one asks the graph which node it
is looking at.
How many distinct states are registered right now, read from the shared fingerprint
table rather than from this struct's state_count.
The two agree on a single-threaded search. They do not agree inside a worker: under
workers: each process accumulates its own state_count so that the coordinator can
sum the contributions, and that field therefore holds a fragment while the level
is in flight. A worker asking whether the run has passed max_states is asking about
the whole graph, which is what this answers.
:ets.info/2 with :size is O(1) — it reads a counter the table maintains, not the
table — so this is affordable per expanded state, which is where the limit is checked.
Whether this graph carries the liveness structure.
Mark an expanded state that has no successors and that no terminal predicate
admits.
Mark an expanded state that has no successors.
A new, empty graph for spec under constants.
The node record for a state id.
The action path from an initial state to the target, walked through parent
pointers. ExTLA.Trace replays this to regenerate the states themselves.
The first element is the init block that produced the root.
Every strongly connected component of the edge table, as sets of state ids.
Tarjan's algorithm, in ids order so a run's components — and therefore any counterexample read off them — are the same every time.
A component is maximal: it is every state mutually reachable from every other. That
says nothing on its own about whether a behaviour can cycle in it, which is a question
about the spec's fairness and belongs to ExTLA.ModelChecker.Liveness. A state with no
out-edges comes back as a component of one, and whether stuttering there forever counts
as a cycle is the same kind of question (02-dsl-semantics.md §5.3).
The same, over a subset of the states — the edges to anything outside it are ignored.
Liveness checking asks this of the subgraph where a property is false, and again of
smaller subgraphs as strong fairness rules components out (ExTLA.ModelChecker.Liveness).
The state an id names, regenerated by replaying the path to it.
The graph retains no states, so this costs a walk back through the parent pointers
and one action application per step. That is the trade the memory model makes, paid here
rather than carried through the whole search — and it is why every caller of this is
either bounded (to_dot/2) or a test.
Successors of a state, from the edge table.
Raises when the graph was built without check_liveness: true: there is no
cheaper source, and guessing from parent pointers would be wrong — they form a
spanning tree, which has no cycles at all.
Export as DOT for Graphviz.
Node labels are regenerated by replay, since the graph retains no states, so this is
bounded: past :max_states (default 500) it
raises and names the true count rather than rendering a prefix that looks complete.
Requires a graph built with the edge table (liveness_graph: true, which
check_liveness: true implies) — parent pointers are a spanning tree, and drawing one
as though it were the transition relation is the failure this refuses.
Options
:max_states— refuse past this many states.:highlight— aExTLA.Trace.t()whose states and steps are drawn emphasised. This is how a counterexample is shown on the graph it was found in. Note that a run which halted at a violation left a partial graph — the state that refuted the invariant was registered, but the expansion of its predecessor stopped there — so the last highlighted state may have no drawn in-edge. That is the graph being honest about where the search stopped, not the export losing an edge.
Initial states carry a double border, declared terminals a doubled octagon, and deadlocked states a fill.
Export as JSON for tooling and editor integration.
Every state, with its depth, its flags and its variables; every edge, with the action and the parameter binding that produced it. The states are regenerated by replay, so this costs one action application per step per state — the trade the memory model makes, paid here rather than carried through the whole search.
Requires the edge table, for the reason to_dot/2 does.
Turn on the liveness graph, with the fairness constraints its enabled bits are indexed
by — ExTLA.Temporal.Fairness.expand/3, which needs the constants and so cannot run
until a state exists.
A spec with no fairness declarations still gets a liveness graph, with zero-width
bits: the edge table alone answers always, eventually and ~>; fairness is what
the bits are for.