Evaluate your own named expressions at every state of a counterexample, as a table.

ExTLA.Trace.explore(trace,
  waiting: &length(&1.waiting),
  holder:  & &1.holder,
  quorum?: &(map_size(&1.votes) * 2 > 3)
)

format/1 prints every variable of every state, which is the right default and is what nineteen states of five variables makes unreadable. The question a reader actually has — when did the quorum first form, how many acceptors had promised by state 12 — is a function of the state, and this evaluates it at each one and prints a row.

TLA+ answers the same question with the Toolbox's Trace Explorer, which needs a generated spec, a TLC re-run and a GUI panel. Here a ExTLA.State.t() is a plain map and an arbitrary expression over one is an anonymous function, so the apparatus is Enum.map/2.

expressions is a keyword list, rendered in the order given: the caller's order is information, and sorting it would throw that away. Accepts a lasso/0 as readily as a t/0, marking the states that repeat.

Options

• :changed_only — hide rows whose value is the same at every state. A wide trace is mostly repetition and the interesting row is the one that moved. Defaults to false.
• :width — the column budget, defaulting to 68, the width format/1 rules its banners at. States are chunked into groups that fit it, each group repeating the name column. This is a promise about the number of states, not about a single value: a value wider than the budget is printed in full, because truncating it would make the table lie.

An expression that raises is reported, not swallowed

A counterexample is being explored because something is wrong, so an expression that assumes an invariant the trace violates is the normal case rather than an error. That cell is marked ⚠ and the exception's message is printed under the table, naming the state and the expression — the rest of the table still renders.

Pretty-print a trace or a lasso, marking the variables each step changed.

A trace beginning at a state already in hand, applying steps in order.

The trace a to_json/1 result came from.

Atom names are resolved against the atoms the system already has (ExTLA.State.Json), so a trace belonging to a different specification fails with the name that did not resolve rather than by quietly decoding into something else.

Generate the shortest trace from an initial state to the target.

A trace for an arbitrary path: the state init_index produces, then steps applied in order.

generate/3 is the shortest path to one state, which is what a safety violation needs. A liveness counterexample is not that shape — its prefix may be restricted to a subgraph and its cycle starts nowhere near an init — so the path is handed over rather than walked back from parent pointers.

A trace or a lasso as the behaviour it describes, with the index its cycle returns to.

nil for a plain trace and for a lasso with no cycle: those are prefixes of something longer, and ExTLA.Temporal's operators will say :inconclusive where the states do not reach far enough to settle a question.

A lasso's cycle ends where it began, so the repeated final state is dropped — the behaviour lists each state of the cycle once and lasso_start says where to loop back to. A cycle of one state is a terminal stuttering forever (02-dsl-semantics.md §5.3), and comes back as the prefix with lasso_start on its last state.

Export a trace as a sequence of state diffs, for programmatic consumption.

A misaligned trace — one whose actions, bindings and states cannot describe one behaviour — is refused with an ArgumentError rather than zipped. Enum.zip/1 stops at the shortest list, so a trace one action short would render three states of four and mark the wrong one [VIOLATION], never showing the state that actually violated.

The trace as data Jason.encode!/1 accepts, and from_json!/1 reads back.

Accepts a lasso too, which round-trips as %{prefix:, cycle:}. States and bindings go through ExTLA.State.Json, because inspect/1 produces something a person can read and a machine cannot parse — and the conformance pipeline runs mix extla.check --format json into mix extla.replay --trace, which needs the second.

Check that a counterexample is a behaviour the spec actually admits.

A pure function of the trace and the spec: no oracle, no second search, no implementation on the other end. A checker that hands back a trace is making a claim about the spec, and this is the claim checked against the spec rather than against a fixture recording what some other tool once said.

What it checks

1. The first state is one the spec's init blocks produce.
2. Every step names an action that is enabled with that binding in the state before it — ExTLA.ModelChecker.enabled_steps/3, the checker's own notion of what may happen next, so this cannot agree with a second enumeration instead of with the checker.
3. Every step's post-state is what that action's transition actually produces. This is the one a trace can fail while looking entirely plausible: real states, real actions, and a pairing between them that is a lie.
4. For a lasso, additionally: the cycle starts where the prefix ends, its steps are legal, and it closes — applying them returns to its own first state.
5. A stutter is final (02-dsl-semantics.md §5.3). A one-state cycle with no actions claims the behaviour stays there forever, which is only so where nothing is enabled; a deadlock trace likewise has to end at a successor-less state. A stutter at a live state is refused, because format/1 would render it as "has no successors" and so confirm a stutter placed in the wrong spot.

A safety trace must also refute the property it names

A legal path from an initial state is not yet a counterexample: a trace can describe a perfectly legal route to a state whose final step satisfies the property it is offered as a refutation of, and every check above would pass it. So a safety trace is additionally required to fail where it says it fails — a named invariant false in the final state, a named action property false over the final step. Neither needs a second implementation of anything: both predicates are already compiled on the spec.

What it deliberately does not check

For a temporal property, whether it is genuinely refuted along the behaviour, and whether the cycle satisfies the spec's fairness. Both are already checked, by ExTLA.TemporalCheck, which shares no code with ExTLA.ModelChecker.Liveness and is what makes that agreement evidence. A third implementation of the same semantics here would add a place for them to disagree and no new information — which is why the requirement above is scoped to safety.

Returns :ok, or {:error, message} naming the step and what was wrong with it.

validate/3, raising instead of returning an error. For a test that wants the message rather than a boolean.

The behaviour-trace invariant, stated once.

n states, n - 1 actions, one binding each, and `length` == n.

A trace is a behaviour: states with the steps between them. Everything downstream reads it by zipping the three lists, so a trace that breaks this describes no behaviour at all — and Enum.zip/2 does not say so, it silently stops at the shortest list.

Why it is asserted where a trace is built

Checking only where a trace is read (from_json!/1, to_diffs/1, validate/3) catches a malformed trace after it has left the code that broke it, often a few modules away and sometimes after it has already been rendered. So every producer in this library asserts it too, through well_formed!/2: a producer that breaks the invariant fails naming itself, which is where the fix goes.

length is checked too, and it is the field most easily left behind: it counts STATES, so an edit that changes the lists and not the count produces a trace that reads as one shape and reports another.

Returns :ok or {:error, message}.

well_formed/1, raising and naming the producer that broke it.

produced_by is the function that built the trace, because the message is read by whoever has to fix it and "a trace with 4 states and 4 actions" does not say whose.

Deliberately a raise rather than a returned error: a malformed trace is a bug in this library, not a condition a caller can handle, and the project's rule is to surface one at the earliest possible moment rather than to carry it to a consumer that will zip it away.