mix extla.check (ExTLA v0.6.0)

Copy Markdown View Source

Run model checking on ExTLA.Spec modules.

Usage

mix extla.check                                 # every spec in the project
mix extla.check Specs.TransferProtocol
mix extla.check Specs.TransferProtocol --max-states 100000
mix extla.check Specs.TransferProtocol --format json

Where the constants come from

A spec cannot be checked without an assignment for each of its constants, and the task takes them, in order of precedence, from:

  1. application config — config :extla, Specs.X, constants: %{accounts: …}
  2. constant :accounts, default: MapSet.new([…]) beside the declaration

A constant with neither is an error naming both places it could be supplied.

Symmetry is configured per spec

config :extla, Specs.X, symmetry: [:procs]

names constants whose elements are interchangeable, and the run checks under that reduction. Liveness is then skipped, with a warning saying so, because symmetry reduction and liveness are not sound together; check the temporal properties in a run without symmetry:. --verify-symmetry checks the declaration.

Options affecting the VERDICT

--strict-coverage    Treat a never-enabled action or a vacuous property as a
                     failure rather than a warning.
--allow-incomplete   Exit 0 even if the run was bounded. Off by default: see
                     the exit codes.
--fingerprint-bits   64 (default) or 128.

Other options

--max-states         State limit for the run.
--workers            Explore on N processes (default 1). Refused together
                     with liveness, so a spec that declares a `temporal`
                     has its safety checked in parallel and says so.
--safety-only        Skip liveness. Liveness is checked whenever the spec
                     declares a `temporal`; this turns it off, and with it the
                     liveness graph the check needs.
--verify-symmetry    Run the model with and without the `symmetry:` reduction
                     and fail if any verdict differs. Nothing can establish a
                     symmetry declaration's soundness statically, so this is
                     the check that catches a wrong one.
--profile            Report what each of YOUR declarations cost, in reductions
                     (`ExTLA.Profile`). Off by default and free when off. In
                     reductions rather than milliseconds because a reduction is
                     a function of the code and the data and not of the machine
                     or its load — so two profiles are comparable, and a wall
                     time taken on a busy box is not.
--format             human (default) or json.

Exit codes

0  verified
1  violation (a counterexample was printed — a trace, or a lasso where a
   temporal property was refuted)
2  incomplete — the state limit or a state constraint bounded the run, so
   the spec was NOT verified
3  coverage failure (with --strict-coverage)

Exit code 2 exists because "we ran out of budget" is not "it holds", and a tool that returns them as the same number teaches its users to believe something false.