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

Counterexample traces.

When the model checker finds a violation it produces a trace: the shortest
sequence of states from an initial state to the violating one. The search is
breadth-first and an invariant is evaluated when a state is first discovered,
so "the first violation found" and "the shortest counterexample" are the same
thing.

The states are not stored during the run (`ExTLA.StateGraph`), so a trace is
*regenerated*: the path of `{action, params}` is walked back through parent
pointers and replayed forward from the `init` block that produced the root.

# `lasso`

```elixir
@type lasso() :: %{prefix: t(), cycle: t() | nil}
```

A liveness counterexample: a finite prefix, then a cycle repeated forever.

`cycle` is `nil` where a single state refutes the property — `pred` and `always(pred)`
are settled by one state, and printing an invented cycle after it would suggest the
reason lay somewhere it does not. A `cycle` whose `actions` are empty is a state that
stutters forever: a `terminal` (`02-dsl-semantics.md` §5.3), which is a legal end of a
behaviour and refutes anything that was still waiting for something to happen.

# `t`

```elixir
@type t() :: %ExTLA.Trace{
  actions: [atom()],
  bindings: [map()],
  length: non_neg_integer(),
  message: String.t(),
  property: atom() | nil,
  states: [ExTLA.State.t()],
  type: :safety | :liveness | :deadlock
}
```

# `explore`

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.

# `format`

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

# `from`

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

# `from_json!`

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`

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

# `replay`

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.

# `to_behavior`

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.

# `to_diffs`

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.

# `to_json`

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.

# `validate`

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

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

# `well_formed`

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

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

---

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