ExTLA (ExTLA v0.6.0)

Copy Markdown View Source

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

A specification is Elixir code. The model checker explores every state it reaches, and the conformance layer checks a running GenServer against it. Start with Getting started; the tutorial that follows it builds one system across eleven pages.

Three layers, each useful on its own

  • Layer 1 — invariants on a running process. ExTLA.Invariant checks properties after every transition of a live GenServer, :gen_statem or Agent. Needs no specification and no model checker. Under MIX_ENV=prod it emits no code at all.

  • Layer 2 — the model checker. ExTLA.Spec compiles a specification module; ExTLA.ModelChecker explores its state space breadth-first, checks invariants and temporal properties, and reports the shortest counterexample — or the lasso — when it finds one. mix extla.check is the command-line form.

  • Layer 3 — conformance. ExTLA.GenServer and ExTLA.Refinement map an implementation's state onto a specification's, so mix extla.simulate can ask whether the code does what the specification says, and mix extla.replay can drive a counterexample through the real process.

A specification is ordinary Elixir that looks like this:

defmodule Specs.Counter do
  use ExTLA.Spec

  constant :max_val
  variable :count, type: 0..^max_val

  init do
    count = 0
  end

  action :increment do
    require count < ^max_val
    count = count + 1
  end

  invariant :in_bounds do
    count >= 0 and count <= ^max_val
  end
end

It looks like Elixir and is not: = inside init or action is a next-state equation rather than a rebinding, ^name is a constant rather than a match pin, and require is an enabling condition rather than Kernel.SpecialForms.require/2. 02-dsl-semantics.md is the normative account.

Where things are written down

The reference holds what a user looks up: the checker's options and their costs, the coverage report, the JSON result, conformance, and what ExTLA is not. The full design is the specification.

What is built is in the changelog and nowhere else, this moduledoc included.