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

Run a spec-level behaviour against a real implementation.

Where `ExTLA.GenServer`'s wrapper checks whatever the system happens to do, this starts
from a sequence of *abstract* actions and makes the implementation follow it. Two
sources of such a sequence, and both matter:

- `counterexample/3` replays a trace the model checker produced. This closes the loop
  that makes the three layers one tool rather than three: Layer 2 finds a design bug
  before any code exists, and this runs that exact trace against the code.
- `trace/3` checks a **captured** behaviour — from staging, from production, from a
  recorded test run — with the same `ExTLA.GenServer.Runtime.check_step!/5` the runtime
  wrapper uses. Nothing needs to be running: it is a pure function over recorded data, so
  it runs in a test suite against a fixture or offline against an incident.

## A counterexample the implementation cannot follow is itself a finding

It means the spec permits a behaviour the code does not, so one of the two is wrong.
That is reported as a result, not as an error — which is why every check in
`ExTLA.GenServer.Runtime` has a form that returns its finding. A report saying *which step*
failed cannot be assembled by catching the exception the wrapper raises.

## What drives the server

`c:ExTLA.Refinement.concrete_message/2` — the inverse of
`c:ExTLA.Refinement.abstract_action/1`, and the callback `ExTLA.Refinement.validate!/3`
round-trips at compile time. A refinement that does not define it can be *checked* as it
runs and cannot be *driven*, which is most of what this module is
for; `counterexample/3` says so by name rather than failing with an undefined function.

# `result`

```elixir
@type result() :: %{
  status: :ok | :violation | :not_followed | :not_replayable,
  steps_checked: non_neg_integer(),
  violation: violation() | nil,
  detail: String.t() | nil,
  skipped: [{pos_integer(), atom()}]
}
```

# `violation`

```elixir
@type violation() :: %{
  step: non_neg_integer(),
  kind:
    :not_enabled
    | :diverged
    | :unmapped_but_moved
    | :invariant
    | :action_property,
  action: atom() | nil,
  message: term(),
  detail: String.t()
}
```

# `counterexample`

Replay a model-checker counterexample against the implementation.

Accepts a `ExTLA.Trace` or a lasso (`%{prefix:, cycle:}`), whose cycle is replayed once —
a lasso describes a behaviour repeating forever, and one pass is what can be executed.

Options:

- `:server` — a pid or registered name to drive. Without it the module is started with
  `GenServer.start_link(module, init_arg)`.
- `:init_arg` — the argument for that start (default `[]`).
- `:timeout` — per message (default 5000).

Returns `:not_followed` when the implementation refuses a message the trace calls for —
the server stopping, or timing out. That is the informative case above: the spec permits
a step the code does not take.

# `trace`

Check a captured trace — `[{message, concrete_state}]`, oldest first — against the spec.

The state in each pair is the state the implementation was in **after** that message.
Every consecutive pair is a transition, mapped through `abstract/1` and checked with the
same step check the wrapper uses; the spec's invariants and action properties are checked
beside it.

A capture of one entry is checked for the spec's invariants and nothing else: one state
is not a step.

---

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