Modules
Describe your system's states, find the invalid ones automatically, and check that your GenServers behave as described.
Global configuration for ExTLA behavior.
Layer 2 and Layer 3, checked against each other. See "What conformance checks" in
guides/reference.md.
What a model-checking run exercised.
Canonical, collision-resistant state identity.
TLA+ function operations. In TLA+, a function maps every element of its domain to a value. Elixir maps serve as the implementation.
Layer 3: a GenServer checked against the specification it claims to refine.
Sending a message to an instrumented server and getting the outcome as a value.
The engine behind Layer 3's callback wrappers. Not called directly.
A Layer 3 conformance failure: the implementation took a step its specification does not permit, or reached an abstract state the specification forbids.
Layer 1: invariants and properties on a running OTP process, checked at every transition.
Layer 1 for an Agent, whose transitions are functions its callers pass in.
The engine behind Layer 1's callback wrappers. Not called directly.
ExUnit helpers for testing Layer 1 declarations in isolation.
A Layer 1 property that did not hold, and what to do about it.
Exhaustive state-space model checker for ExTLA.Spec modules. Analogous to TLC
for TLA+.
Temporal property checking over the liveness graph.
Parallel state exploration: one coordinator, N workers, one shared graph. Selected by
workers: n on ExTLA.ModelChecker.run/2; see "Parallel exploration" in
guides/reference.md.
Safety property checking: invariants and action properties, checked incrementally during state exploration.
What each of your declarations cost, measured in reductions.
StreamData generators derived from a specification, for a consumer's own property tests.
The formal relationship between an abstract specification and a concrete implementation.
A refinement mapping that does not hold up: at compile time from validate!/3, or at
runtime from abstract!/3 when a mapping produces something that is not a state of
the spec.
Run a spec-level behaviour against a real implementation.
Set operations corresponding to TLA+ set theory operators. Builds on Elixir's MapSet with additional TLA+ operations.
Random walks over the real implementation, checked against the spec at every step.
Random messages, derived from a spec's own action definitions.
use ExTLA.Spec turns a module into a specification.
Compiles an init or action body into the guard and transition functions of
ExTLA.Spec.Compiled.action_def/0.
Raised when a spec module violates one of the rules in 02-dsl-semantics.md.
The compiled representation of a ExTLA.Spec module.
This is what the model checker operates on.
The macros that form the specification DSL.
Which spec variables each block reads and writes, computed at compile time.
Raised by f[x] where x is outside the domain of f
(02-dsl-semantics.md §1.6).
Content versions for spec items and for a spec as a whole.
Functions available inside action, init, invariant, terminal and
action_property blocks. use ExTLA.Spec imports this module whole, so this list
is a spec body's vocabulary.
Compiles an action's params: — the DSL's only source of nondeterminism
(02-dsl-semantics.md §3).
Raised when a predicate — invariant, terminal, action_property, or a
state predicate inside a temporal — evaluates to something other than
true or false.
Resolves the three name classes of 02-dsl-semantics.md §1 inside a spec block.
Parses a temporal block into the bounded fragment of
02-dsl-semantics.md §5.1
ExUnit helpers for model checking in tests.
The type: annotation grammar of 02-dsl-semantics.md §1.5.
A state is an immutable snapshot of all specification variables. A step is a pair of consecutive states (pre-state and post-state). A behavior is a (possibly infinite) sequence of states.
Raised when a spec variable holds a term that cannot be deterministically
serialized (02-dsl-semantics.md §6).
The JSON form of a state term, and back again.
A term that is not §6-permitted, or JSON that does not decode to one.
The state graph built during model checking. Nodes are states, edges are labeled transitions.
DOT and JSON renderings of a state graph — the bodies of
ExTLA.StateGraph.to_dot/2 and ExTLA.StateGraph.to_json/1.
Symmetry reduction: states that differ only by a permutation of interchangeable constants are one state.
Raised by verify_symmetry: true when the reduced and unreduced runs disagree.
ENABLED, as the liveness graph records it.
The fairness constraints a run actually has, expanded from what the spec declares.
Counterexample traces.
The body of ExTLA.Trace.explore/3: named expressions evaluated at every state of a
counterexample, rendered as a table.
Mix Tasks
Run model checking on ExTLA.Spec modules.
Explore a counterexample mix extla.check --format json already wrote, without running the
checker again.
Drive a ExTLA.GenServer through a spec-level behaviour, or check a captured one.
Run random traces of a ExTLA.GenServer module against the specification it refines.
Report the state of every spec_version: stamp, and update the stale ones.
Render a ExTLA.Spec module's state graph as DOT, for Graphviz.