Using ExTLA

ExTLA's DSL is written in Elixir syntax and is not Elixir. Inside init, action, invariant and the other declarations, familiar constructs mean different things, and the difference is the point: these blocks describe a specification, which a model checker enumerates, not a program that runs.

Every rule below is enforced at compile time and names a diagnostic you will see if you break it. The full table, keyed by the diagnostic's kind, is §7 of the DSL reference, which is also the normative semantics.

The nine things that look like Elixir and are not

1. Assignment is a next-state relation, not a rebinding

action :transfer, params: [amount: 1..10] do
  require balance >= amount
  balance = balance - amount      # the NEXT state's balance
  log = append(log, amount)       # and the next state's log
end

A bare name on the right reads the pre-state; a name on the left names the post-state. So x = x + 1 is not a mutation, it is a relation between two states, and the order of the assignments in the block does not matter. Assigning the same variable twice is :variable_assigned_twice — not last-write-wins, because there is no "last" in a conjunction.

Outside init and action, assignment is :assignment_outside_init_or_action. Assigning a name that no variable declares is :assignment_to_undeclared_variable.

2. ^name is a constant, not a match pin

constant :accounts
variable :balances, type: [^accounts ~> 0..100]

action :pay, params: [to: ^accounts] do
  require balances[to] < ^max_balance
end

^ marks a constant reference. A bare name that happens to match a constant is :constant_without_pin — the compiler refuses it rather than guessing, because a bare name is how a variable is read.

3. require is an enabling condition, not Kernel.SpecialForms.require/2

action :withdraw, params: [n: 1..5] do
  require balance >= n     # this action is DISABLED where this is false
  balance = balance - n
end

A false require does not raise and does not fail the check: the action is simply not available in that state. An action that is never enabled anywhere is reported by the coverage report, not by an error — which is why mix extla.check prints one.

4. Guards and lets evaluate in source order

action :consume, params: [c: ^clients] do
  require Map.has_key?(inbox, c)   # guard FIRST
  let msg = inbox[c]               # then the lookup is safe
  inbox = delete(inbox, c)
end

Order decides between a disabled action and a raised ExTLA.Spec.DomainError. f[x] outside the domain of f raises rather than answering nil, so a let that reads before its guard has run turns a state the action should skip into a crash. Put the guard above the read.

5. Reserved names

:state, :old and :new are the DSL's own bindings — state inside a Layer 1 invariant, old and new inside an action_property. Declaring a variable or constant with one of those names is refused.

:type_ok is reserved: it is the implicit invariant compiled from your type: annotations, and declaring it yourself is :implicit_invariant_redeclared.

6. Liveness is skipped under symmetry and --workers, and refused by the API

mix extla.check checks every temporal the spec declares, and skips liveness, with a warning that names the reason, in three cases: --safety-only, a symmetry: in the spec's configuration, and --workers above one. The safety properties are still checked.

mix extla.check MySpec               # safety and liveness
mix extla.check MySpec --workers 8   # safety in parallel; warns that liveness was skipped

ExTLA.ModelChecker.run/2 infers nothing: check_liveness: defaults to false, and check_liveness: true together with symmetry: or workers: above one raises, because neither combination gives a sound answer. Symmetry reduction merges states a temporal property can tell apart, so the reduced graph can hold cycles the real one does not; and under workers each process holds only part of the graph, so a cycle spanning two of them cannot be found.

If you need both, run two checks: one with the reduction or the workers, one without. ExTLA.Spec.Test.assert_spec/2 passes its config straight to run/2, so a test that should check a temporal property says check_liveness: true.

7. mode and telemetry are compile-time

config :extla, mode: :disabled       # recompiles every module that uses ExTLA.Invariant
config :extla, telemetry: :verbose

Both are read with Application.compile_env/2, so changing either recompiles your modules, not just ExTLA's. mode: :disabled emits no wrapper at all — the module compiles as though the invariants were not there — which is what makes it free rather than cheap.

An invariant :x, enabled: false removes that one declaration at compile time. A module whose invariants are all removed cannot be asserted about: assert_invariants/2 raises rather than passing for every state.

8. Choosing a task

9. The set vocabulary is in scope, and two operators are renamed

All of TLA+'s set theory is callable unqualified inside a spec block — powerset, cross, cross_many, distributed_union, for_all?, exists?, range, choose, for_each, update, except, domain, function_set, record_set, plus union, intersection, difference, subset?, member?, size and the sequence operators. There is nothing to import and nothing to qualify: ExTLA.Set and ExTLA.Function hold the one implementation of each, and ExTLA.Spec.Helpers, which every spec imports, delegates to them.

Two are renamed, and only two. {f(x) : x \in S} is set_map/2 and {x \in S : P(x)} is set_filter/2, not map/2 and filter/2 — an unqualified map(xs, f) in a spec block reads as Enum.map/2 to every Elixir programmer, and these return a set, possibly a smaller one, since a non-injective function collapses elements exactly as in TLA+.

for_each/2 takes a set, not a sequence. [x \in S |-> e] ranges over a set. A list is a sequence — a function on 1..Len(s) already — and building a function over one would silently deduplicate it, so it raises ArgumentError by name instead of answering. Pass a MapSet or a range. For the same reason domain/1 of a sequence is its indices, MapSet.new(1..Len(s)), not its elements; domain/1 of a set is refused, because a set is neither a function nor a sequence.

Writing a refinement mapping: a bare term is a call

concrete_message/2 returns the message that causes an action, and a message does not carry how it arrives. So the mapping says:

A bare term is a call. That is what it has always meant, so no existing mapping changes — but it is the trap: map an action to :process_next when the server takes it in handle_cast/2, and the message arrives at handle_call/3, which has no clause for it. The server dies, and mix extla.replay reports :not_followed — "the spec permits a behaviour the implementation does not take" — about a server that is correct. Write {:cast, :process_next}.

The one ambiguity has a total escape: to send the literal two-tuple {:cast, 5} as a call, write {:call, {:cast, 5}}.

A cast completes when a :sys.get_state/2 behind it replies, which both drivers already make, so this costs no extra round-trip. A cast that never completes is a named finding, not a silent pass.

Wiring it into a project

• use ExTLA.Invariant goes directly after use GenServer, before the callbacks. The order is load-bearing: only callbacks defined after it are wrapped, which is what keeps the defaults use GenServer injects unwrapped.
• use ExTLA.GenServer, spec: Specs.Counter, refinement: __MODULE__.Refinement puts a server under Layer 3: spec: is the specification it claims to refine, refinement: the module that maps its state and messages onto the spec's.

• Configuration. config :extla, mode: :enabled | :log_only | :disabled and telemetry: :quiet | :verbose are compile-time (§7 above). config :extla, workers: n is what ExTLA.Config.workers/0 answers, and trace_buffer: n bounds the trace a Layer 3 server records. Per spec, config :extla, Specs.Counter, constants: %{max: 3} assigns constants for mix extla.check, mix extla.simulate and Layer 3, and symmetry: [:procs] there turns on the reduction for mix extla.check.

• jason is optional. Add {:jason, "~> 1.4"} for --format json and for the saved counterexamples mix extla.explore and mix extla.replay --trace read.

What a verdict does and does not say

mix extla.check exits 2 when the run was bounded — max_states was hit, or a state_constraint held states back. That is not a pass. A bounded run has verified nothing about the states it did not reach, and the exit code says so. --allow-incomplete (allow_incomplete: true for assert_spec/2) turns it into a pass when you have decided a partial answer is worth having.

Checking a recorded trace is different from model checking. Over a finite trace, a temporal property can be :inconclusive rather than :holds or :violated: a prefix can refute always P but cannot prove it. ExTLA.Temporal returns three verdicts for that reason, and a lasso (a prefix plus a repeating cycle) is what lets every operator answer definitely.

Writing specifications with an agent

The rules above are the ones an agent gets wrong, because each looks like ordinary Elixir and compiles to something else. Two more that are worth stating outright:

• Do not add @spec annotations to a spec module. They are not checked and they drift; the DSL's type: annotations are the checked ones.
• A specification that verifies is not a specification that is right. The coverage report is where a spec that checks nothing announces itself — a never-enabled action, a vacuous ~>, an invariant never at risk. Read it.