# `ExTLA.StateGraph`
[🔗](https://github.com/dcoai/extla/blob/v0.6.0/lib/ex_tla/state_graph.ex#L1)

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 constraint

The 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.

# `edge`

```elixir
@type edge() :: {action :: atom(), params :: map(), successor :: state_id()}
```

# `node_record`

```elixir
@type node_record() :: %{
  parent: state_id() | nil,
  action: atom() | nil,
  params: map() | nil,
  init_index: non_neg_integer() | nil,
  depth: pos_integer()
}
```

# `state_id`

```elixir
@type state_id() :: non_neg_integer()
```

# `t`

```elixir
@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()
}
```

# `add_edges`

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.

# `add_state`

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_transition`

Count one transition, whether or not it discovered a new state.

# `delete`

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.

# `depth`

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.

# `enabled?`

Whether the `index`th fairness constraint was enabled in a state.

# `enabled_bits`

The ENABLED bits of a state, in `fairness_index` order.

# `id_of`

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.

# `live_state_count`

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.

# `liveness?`

Whether this graph carries the liveness structure.

# `mark_deadlocked`

Mark an expanded state that has no successors and that no `terminal` predicate
admits.

# `mark_terminal`

Mark an expanded state that has no successors.

# `new`

A new, empty graph for `spec` under `constants`.

# `node_record`

The node record for a state id.

# `path_to`

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.

# `sccs`

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).

# `sccs`

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`).

# `state_at`

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`

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.

# `to_dot`

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` — a `ExTLA.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.

# `to_json`

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.

# `with_liveness`

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.

---

*Consult [api-reference.md](api-reference.md) for complete listing*