# `mix extla.check`
[🔗](https://github.com/dcoai/extla/blob/v0.6.0/lib/mix/tasks/extla.check.ex#L1)

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.

---

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