mix extla.replay (ExTLA v0.6.0)

Copy Markdown View Source

Drive a ExTLA.GenServer through a spec-level behaviour, or check a captured one.

Usage

# Replay a model-checker counterexample (from `mix extla.check --format json`)
mix extla.replay MyApp.TransferServer --trace counterexample.json

# Check a captured trace from a running system
mix extla.replay MyApp.TransferServer --captured incident.json

Driving options (--trace only)

--init-arg TERM   the argument the server is started with (default []): a literal
                  term such as `[start: 0]`; an expression is refused, never run
--server NAME     drive a running, registered process (`MyApp.Server` or `:name`)
                  instead of starting one; it is not stopped afterwards
--timeout MS      milliseconds to wait for each reply (default 5000)

They are ExTLA.Replay.counterexample/3's :init_arg, :server and :timeout. --init-arg with --server is refused, since a running server is not started. All three are refused with --captured, which drives nothing.

--trace needs concrete_message/2 on the refinement module: it starts from abstract actions and has to produce the message that causes each. --captured needs only abstract/1 and abstract_action/1, and starts nothing — it is a pure check over recorded data, which is what makes it usable in a test suite against a fixture or offline against an incident.

The file formats

--trace takes what mix extla.check --format json writes: either the whole document — {"schema_version": …, "specs": [...]}, from which the entry for the server's spec is used — or a single trace object lifted out of it. A document written by a different schema version is refused, naming both versions; re-run mix extla.check --format json.

--captured takes an array of {"message": …, "state": …} objects, oldest first, where state is the CONCRETE state the implementation was in after that message. Both encodings are ExTLA.State.Json's, so a state is written the way the checker writes one and no second format has to be learned.

Steps a trace names and this cannot drive

A trace's actions are not all actions of the spec. ExTLA.Simulation writes :unmapped for a message the refinement mapping does not model — its normal answer, not an error — and :restart for a crash injected by --inject-failures. concrete_message/2 has no clause for either.

:unmapped is skipped, and listed in the report and in skipped under --format json. The claim :unmapped makes is that the message does not move the abstract state, so the behaviour is unchanged by it; the trace's post-state is still checked.

:restart is reproduced: the server is killed with :kill, not stopped politely, because a crash runs no terminate/2. It is then started again, and the replay checks that recovery lands in the state the trace records. This is possible only for a server this task started; against --server a restart exits 3.

Output

--format human|json   the report as text (default) or as a JSON document

Exit codes

0  the behaviour was reproduced, or the capture conforms
1  a conformance violation — the step and its finding are printed
2  the implementation could not follow the trace. Not a conformance failure:
   the spec permits a behaviour the code does not take, and which of the two
   is wrong is not something this can decide
3  the trace names a step this cannot reproduce — a `:restart` against a
   server it was handed and does not own. A limit of the replay rather than
   a claim about the implementation, which is why it is not 2