mix extla.simulate (ExTLA v0.6.0)

Run random traces of a ExTLA.GenServer module against the specification it refines.

Usage

mix extla.simulate MyApp.TransferServer
mix extla.simulate MyApp.TransferServer --traces 5000 --steps 100
mix extla.simulate MyApp.TransferServer --inject-failures --seed 42

Where mix extla.check explores every reachable state of the specification, this runs the implementation and checks each transition against the spec with the same refinement check the runtime wrapper uses.

Options

--traces             How many random traces (default 100).
--steps              Maximum steps per trace (default 25).
--seed               Reproduce a previous run. The seed is always reported.
--concurrency        Traces to run at once (default 1).
--inject-failures    Kill and restart the server mid-trace, and check that
                     recovery lands in a state the spec's invariants admit.
                     A crash is not a step of the specification — nothing in
                     the DSL models one — so the restart itself is not checked
                     as a transition.
--unrestricted       Also generate messages for actions the spec DISABLES in
                     the current state, which asks whether the implementation
                     refuses what the spec forbids. Off by default: most
                     servers are not written to, and the resulting
                     `:not_enabled` is a true finding about nearly all of
                     them.
--format             human (default) or json.
--against-graph      Also require every observed state to be a node of the
                     model checker's graph and every step an edge. Off by
                     default: it needs a completed graph, which not every
                     simulation target has.

                     The graph is built once and each behaviour is held
                     against it as that behaviour finishes, so this runs
                     the traces you asked for and no others, under the
                     options you asked for.

How the server starts

Each trace starts its own server with GenServer.start_link(module, []). There is no --init-arg: a server that needs a different argument is simulated from a test with ExTLA.Simulation.run/2, whose init_arg: option takes one. The spec's constants come from config :extla, Spec, constants: %{…} or the default: beside each declaration, the same place the server under Layer 3 reads them.

Exit codes

0  no finding in the traces that were run
1  a conformance violation — the counterexample is printed as a trace —
   or, under `--against-graph`, a behaviour that left the checker's graph
2  the server stopped or stopped answering, which is a finding of a different
   kind: nothing about conformance was decided after that point

The two findings behind 1 are named apart in the verdict line, and they are different answers: a conformance violation is about the implementation, while leaving the graph may be about the SEARCH — ExTLA.Conformance's :checker class is the one finding no other gate in the project can produce.

A green run has checked the traces it drew and nothing else. The coverage line says which actions those were, and a run over a generator that never produced an action says nothing about it.