# ExTLA v0.6.0 - Table of Contents

> Describe your system's states, find the invalid ones automatically, and check that your GenServers behave as described.

## Pages

- [ExTLA](readme.md)
- [Using ExTLA](usage-rules.md)
- [Changelog](changelog.md)

- Guides
  - [Getting started](getting-started.md)
  - [Reference](reference.md)

- Tutorial
  - [Introduction: what this is, and where it comes from](00-introduction.md)
  - [The mathematics of TLA, and what it is good for](01-mathematics.md)
  - [The DSL in practice](02-dsl.md)
  - [Invariants](03-invariants.md)
  - [Temporal properties, and the difference fairness makes](04-temporal.md)
  - [Symmetry, and who is responsible for it](05-symmetry.md)
  - [Layer 1 — invariants on a running GenServer](06-layer1.md)
  - [Layer 3 — does the implementation conform?](07-layer3.md)
  - [From a system you have to a specification you can check](08-modelling.md)
  - [When it explodes](09-when-it-explodes.md)
  - [Putting a specification in your project](10-in-your-project.md)

- Reference
  - [DSL reference](02-dsl-semantics.md)
  - [Examples](07-examples.md)

- Background
  - [TLA+ — Temporal Logic of Actions](tla-plus-primer.md)

- License
  - [License](license.md)

## Modules

- [ExTLA](ExTLA.md): Describe your system's states, find the invalid ones automatically, and check that your
GenServers behave as described.

- Specifications
  - [ExTLA.Function](ExTLA.Function.md): TLA+ function operations. In TLA+, a function maps every element
of its domain to a value. Elixir maps serve as the implementation.
  - [ExTLA.Set](ExTLA.Set.md): Set operations corresponding to TLA+ set theory operators.
Builds on Elixir's MapSet with additional TLA+ operations.

  - [ExTLA.Spec](ExTLA.Spec.md): `use ExTLA.Spec` turns a module into a specification.
  - [ExTLA.Spec.CompileError](ExTLA.Spec.CompileError.md): Raised when a spec module violates one of the rules in `02-dsl-semantics.md`.
  - [ExTLA.Spec.DSL](ExTLA.Spec.DSL.md): The macros that form the specification DSL.
  - [ExTLA.Spec.DomainError](ExTLA.Spec.DomainError.md): Raised by `f[x]` where `x` is outside the domain of `f`
(`02-dsl-semantics.md` §1.6).
  - [ExTLA.Spec.Helpers](ExTLA.Spec.Helpers.md): 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.
  - [ExTLA.Spec.PredicateError](ExTLA.Spec.PredicateError.md): Raised when a predicate — `invariant`, `terminal`, `action_property`, or a
state predicate inside a `temporal` — evaluates to something other than
`true` or `false`.
  - [ExTLA.Spec.Test](ExTLA.Spec.Test.md): ExUnit helpers for model checking in tests.

  - [ExTLA.Spec.Type](ExTLA.Spec.Type.md): The `type:` annotation grammar of `02-dsl-semantics.md` §1.5.
  - [ExTLA.Temporal](ExTLA.Temporal.md): `ENABLED`, as the liveness graph records it.

- Model checking
  - [ExTLA.Config](ExTLA.Config.md): Global configuration for ExTLA behavior.

  - [ExTLA.Coverage](ExTLA.Coverage.md): What a model-checking run exercised.
  - [ExTLA.ModelChecker](ExTLA.ModelChecker.md): Exhaustive state-space model checker for `ExTLA.Spec` modules. Analogous to TLC
for TLA+.
  - [ExTLA.Profile](ExTLA.Profile.md): What each of *your* declarations cost, measured in reductions.
  - [ExTLA.Spec.Compiled](ExTLA.Spec.Compiled.md): The compiled representation of a `ExTLA.Spec` module.
This is what the model checker operates on.
  - [ExTLA.State](ExTLA.State.md): 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.
  - [ExTLA.State.InvalidTermError](ExTLA.State.InvalidTermError.md): Raised when a spec variable holds a term that cannot be deterministically
serialized (`02-dsl-semantics.md` §6).

  - [ExTLA.StateGraph](ExTLA.StateGraph.md): The state graph built during model checking. Nodes are states, edges are
labeled transitions.
  - [ExTLA.Symmetry.UnsoundError](ExTLA.Symmetry.UnsoundError.md): Raised by `verify_symmetry: true` when the reduced and unreduced runs disagree.
  - [ExTLA.Trace](ExTLA.Trace.md): Counterexample traces.

- Layer 1: runtime invariants
  - [ExTLA.Invariant](ExTLA.Invariant.md): Layer 1: invariants and properties on a running OTP process, checked at every transition.
  - [ExTLA.Invariant.Agent](ExTLA.Invariant.Agent.md): Layer 1 for an `Agent`, whose transitions are functions its callers pass in.
  - [ExTLA.Invariant.Test](ExTLA.Invariant.Test.md): ExUnit helpers for testing Layer 1 declarations in isolation.
  - [ExTLA.Invariant.Violation](ExTLA.Invariant.Violation.md): A Layer 1 property that did not hold, and what to do about it.

- Layer 3: conformance
  - [ExTLA.Conformance](ExTLA.Conformance.md): Layer 2 and Layer 3, checked against each other. See "What conformance checks" in
`guides/reference.md`.
  - [ExTLA.GenServer](ExTLA.GenServer.md): Layer 3: a GenServer checked against the specification it claims to refine.
  - [ExTLA.GenServer.Violation](ExTLA.GenServer.Violation.md): A Layer 3 conformance failure: the implementation took a step its specification does not
permit, or reached an abstract state the specification forbids.
  - [ExTLA.PropertyTest](ExTLA.PropertyTest.md): StreamData generators derived from a specification, for a consumer's own property tests.
  - [ExTLA.Refinement](ExTLA.Refinement.md): The formal relationship between an abstract specification and a concrete implementation.
  - [ExTLA.Refinement.Error](ExTLA.Refinement.Error.md): 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.

  - [ExTLA.Replay](ExTLA.Replay.md): Run a spec-level behaviour against a real implementation.
  - [ExTLA.Simulation](ExTLA.Simulation.md): Random walks over the real implementation, checked against the spec at every step.
  - [ExTLA.State.Json](ExTLA.State.Json.md): The JSON form of a state term, and back again.
  - [ExTLA.State.Json.Error](ExTLA.State.Json.Error.md): A term that is not §6-permitted, or JSON that does not decode to one.

- Internals
  - [ExTLA.Fingerprint](ExTLA.Fingerprint.md): Canonical, collision-resistant state identity.
  - [ExTLA.GenServer.Driver](ExTLA.GenServer.Driver.md): Sending a message to an instrumented server and getting the outcome as a value.
  - [ExTLA.GenServer.Runtime](ExTLA.GenServer.Runtime.md): The engine behind Layer 3's callback wrappers. Not called directly.
  - [ExTLA.Invariant.Runtime](ExTLA.Invariant.Runtime.md): The engine behind Layer 1's callback wrappers. Not called directly.
  - [ExTLA.ModelChecker.Liveness](ExTLA.ModelChecker.Liveness.md): Temporal property checking over the liveness graph.
  - [ExTLA.ModelChecker.Parallel](ExTLA.ModelChecker.Parallel.md): 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`.
  - [ExTLA.ModelChecker.Safety](ExTLA.ModelChecker.Safety.md): Safety property checking: invariants and action properties, checked
incrementally during state exploration.
  - [ExTLA.Simulation.Generator](ExTLA.Simulation.Generator.md): Random messages, derived from a spec's own action definitions.
  - [ExTLA.Spec.Block](ExTLA.Spec.Block.md): Compiles an `init` or `action` body into the guard and transition functions of
`t:ExTLA.Spec.Compiled.action_def/0`.
  - [ExTLA.Spec.Deps](ExTLA.Spec.Deps.md): Which spec variables each block reads and writes, computed at compile time.
  - [ExTLA.Spec.Hash](ExTLA.Spec.Hash.md): Content versions for spec items and for a spec as a whole.
  - [ExTLA.Spec.Params](ExTLA.Spec.Params.md): Compiles an action's `params:` — the DSL's **only** source of nondeterminism
(`02-dsl-semantics.md` §3).
  - [ExTLA.Spec.Rewriter](ExTLA.Spec.Rewriter.md): Resolves the three name classes of `02-dsl-semantics.md` §1 inside a spec block.
  - [ExTLA.Spec.Temporal](ExTLA.Spec.Temporal.md): Parses a `temporal` block into the bounded fragment of
`02-dsl-semantics.md` §5.1
  - [ExTLA.StateGraph.Export](ExTLA.StateGraph.Export.md): DOT and JSON renderings of a state graph — the bodies of
`ExTLA.StateGraph.to_dot/2` and `ExTLA.StateGraph.to_json/1`.
  - [ExTLA.Symmetry](ExTLA.Symmetry.md): Symmetry reduction: states that differ only by a permutation of interchangeable
constants are one state.
  - [ExTLA.Temporal.Fairness](ExTLA.Temporal.Fairness.md): The fairness constraints a run actually has, expanded from what the spec declares.
  - [ExTLA.Trace.Explore](ExTLA.Trace.Explore.md): The body of `ExTLA.Trace.explore/3`: named expressions evaluated at every state of a
counterexample, rendered as a table.

## Mix Tasks

- [mix extla.check](Mix.Tasks.Extla.Check.md): Run model checking on `ExTLA.Spec` modules.
- [mix extla.explore](Mix.Tasks.Extla.Explore.md): Explore a counterexample `mix extla.check --format json` already wrote, without running the
checker again.
- [mix extla.replay](Mix.Tasks.Extla.Replay.md): Drive a `ExTLA.GenServer` through a spec-level behaviour, or check a captured one.
- [mix extla.simulate](Mix.Tasks.Extla.Simulate.md): Run random traces of a `ExTLA.GenServer` module against the specification it refines.
- [mix extla.stamp](Mix.Tasks.Extla.Stamp.md): Report the state of every `spec_version:` stamp, and update the stale ones.
- [mix extla.visualize](Mix.Tasks.Extla.Visualize.md): Render a `ExTLA.Spec` module's state graph as DOT, for Graphviz.