# `ExTLA.ModelChecker`
[🔗](https://github.com/dcoai/extla/blob/v0.6.0/lib/ex_tla/model_checker.ex#L1)

Exhaustive state-space model checker for `ExTLA.Spec` modules. Analogous to TLC
for TLA+.

The search is breadth-first, and that is not an implementation detail: an invariant is
evaluated when a state is first discovered, so the first violation found is at minimal
distance from `init` and the trace is the shortest counterexample. A depth-first search
would report *a* counterexample, which is a much less useful thing to hand someone.

`check_liveness: true` adds temporal checking: the search also builds the liveness graph,
and `ExTLA.ModelChecker.Liveness` looks for the fair cycle that refutes a temporal
property. It is off by default, because the graph costs memory and time and a spec that
declares no `temporal` has nothing to gain from it. `mix extla.check` turns it on for a
spec that declares one.

`symmetry: [:processes]` collapses states that differ only by a permutation of an
interchangeable constant, and `verify_symmetry: true` checks the declaration was sound by
running the model both ways (`ExTLA.Symmetry`). `workers: n` explores each level across
`n` processes (`ExTLA.ModelChecker.Parallel`). Either one together with
`check_liveness: true` raises, because neither combination gives a sound liveness answer.

`run/2` lists every option.

# `config`

```elixir
@type config() :: %{
  optional(:constants) => map(),
  optional(:max_states) => pos_integer(),
  optional(:workers) => pos_integer(),
  optional(:check_deadlock) => boolean(),
  optional(:check_liveness) => boolean(),
  optional(:liveness_graph) => boolean(),
  optional(:symmetry) => [atom()] | nil,
  optional(:verify_symmetry) => boolean(),
  optional(:state_constraint) => (ExTLA.State.t() -> boolean()) | nil,
  optional(:fingerprint_bits) => 64 | 128,
  optional(:profile) => boolean(),
  optional(:invariants) => :all | [atom()],
  optional(:action_properties) => :all | [atom()],
  optional(:temporals) => :all | [atom()]
}
```

# `result`

```elixir
@type result() :: %{
  status: :ok | :violation | :max_states_reached | :constrained | :deadlock,
  states_found: non_neg_integer(),
  distinct_states: non_neg_integer(),
  transitions: non_neg_integer(),
  diameter: non_neg_integer(),
  deadlock: boolean(),
  duration_ms: non_neg_integer(),
  violation: ExTLA.Trace.t() | ExTLA.Trace.lasso() | nil,
  coverage: ExTLA.Coverage.t(),
  profile: ExTLA.Profile.t() | nil,
  warnings: [String.t()],
  fingerprint_bits: pos_integer(),
  collision_estimate: float()
}
```

# `bindings`

Every parameter binding of an action in a state, guard or no guard.

# `check_safety`

Run only safety checking: `run/2` with `check_liveness: false`, whatever the config says.

# `checked_invariants`

Every invariant a run will check: the spec's own, preceded by the implicit
`:type_ok` of `02-dsl-semantics.md` §1.5 when any variable is typed.

`type_ok` goes first deliberately. A state outside its declared type makes
every other invariant's verdict on that state uninteresting — the useful thing
to report is that a variable holds something the spec says it cannot.

# `enabled_bindings`

Every parameter binding of an action whose guard holds in a state.

Params bind left to right and each generator receives the bindings made before
it, so a later param can be constrained by an earlier one. A generator that
returns nothing disables the action here, exactly as a false guard would.

# `enabled_steps`

Every `{action, binding}` a state admits — the choices available from it, without
applying any of them.

`successors/3` answers the same question and applies the transitions, which is what the
search needs and what a caller choosing ONE of them does not: `ExTLA.Simulation.Generator`
picks a candidate and asks the refinement for a message, and
`ExTLA.PropertyTest.action_sequences/3` picks one and walks. Both use this, so a
simulation, a property test and the checker agree on what may happen next.

Actions are taken in declaration order and bindings in generator order, so the list is
the same on every run.

# `explore`

Run the model checker and return the full state graph, for inspection.

**The caller owns the returned graph.** It is backed by two ETS tables created in the
calling process, and they live until that process exits — which is the point: the graph
is the return value, and releasing it here would hand back a term whose contents are
gone. `run/2`, which discards the graph, is where the release belongs, and it does it by
searching in a process of its own.

A caller that keeps a graph beyond one short-lived process should say when it is done
with it: `ExTLA.StateGraph.delete/1`.

# `run`

Run the model checker on a spec module.

    ExTLA.ModelChecker.run(Specs.Counter, %{constants: %{max: 3}})

## Options

  * `constants:` — a map assigning the spec's constants. Default `%{}`. Each constant's
    `default:` fills in what this leaves out, and an explicit value wins. `run/2` reads no
    application config: `mix extla.check` adds `config :extla, Spec, constants: %{…}` with
    `ExTLA.Spec.Compiled.resolve_constants/1` and passes the result here.
  * `max_states:` — the state budget. Default `1_000_000`. The search stops once the graph
    has passed it, so the count reported with `:max_states_reached` exceeds the limit.
  * `workers:` — processes exploring each breadth-first level. Default `1`;
    `ExTLA.Config.workers/0` returns the machine's answer if you want it. Raises together
    with `check_liveness: true`.
  * `check_deadlock:` — report a reachable state with no enabled action and no `terminal`
    admitting it. Default `true`.
  * `check_liveness:` — check the spec's `temporal` properties. Default `false`. Raises
    together with `symmetry:` or `workers:` above one.
  * `liveness_graph:` — build the liveness graph without checking anything with it, for
    measuring it. Default `false`; `check_liveness: true` implies it.
  * `symmetry:` — constants whose elements are interchangeable. Default `nil`.
  * `verify_symmetry:` — run the model with and without `symmetry:` and raise
    `ExTLA.Symmetry.UnsoundError` if any verdict differs. Default `false`.
  * `state_constraint:` — a predicate on states; a state that fails it is not expanded,
    and the run's status is `:constrained`. Default `nil`.
  * `fingerprint_bits:` — `64` or `128`. Default `64`.
  * `profile:` — measure what each declaration costs, in reductions (`ExTLA.Profile`).
    Default `false`, and free when off.
  * `invariants:`, `action_properties:`, `temporals:` — `:all` (the default) or a list of
    declaration names to check. A name the spec does not declare is refused.

Returns the verdict and keeps nothing: the search runs in a process of its own, so the
graph's ETS tables are freed when it ends, and an exception is re-raised in the caller
with its original stack. `explore/2` returns the graph instead.

# `steps`

Every `{action, binding}` in a state, guard or no guard.

The counterpart of `bindings/3` to `enabled_steps/3`'s `enabled_bindings/3`. A simulation
that sends only enabled messages can never find an implementation that accepts one the
spec forbids, which is why the unfiltered form is offered rather than assumed away.

# `successors`

Every successor of a state: one per action, per binding of that action's
params, whose guard holds.

Nondeterminism comes from `params:` and only from `params:`
(`02-dsl-semantics.md` §3), so this is the whole of it. Actions are taken in
declaration order and bindings in generator order, which makes the search
deterministic — a checker whose state graph varied between runs could not be
compared to TLC.

---

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