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

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

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.

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.

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.

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 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.

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.

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.