ExTLA.Replay (ExTLA v0.6.0)

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

ExTLA.Refinement.concrete_message/2 — the inverse of 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.

Summary

Types

result()

violation()

Functions

counterexample(module, trace, opts \\ [])

Replay a model-checker counterexample against the implementation.

trace(module, captured, opts \\ [])

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

Types

result()

@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()

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

Functions

counterexample(module, trace, opts \\ [])

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(module, captured, opts \\ [])

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.