ExTLA tutorial. Previous: The DSL in practice.
An invariant is a boolean over the variables that must hold in every reachable state. The
checker evaluates each one in each state it discovers, and stops at the first state where one is
false — that is the counterexample Getting started ends with.
This page is about the rest of it: how to decide what to assert, how to read the report when every invariant holds (which is where a spec that verifies for the wrong reason gives itself away), how to state a property of a step rather than a state, and the failure you are most likely to meet first — a specification that finishes its work and is refuted for it.
Choosing what to assert
A specification with no invariants verifies instantly and proves nothing. The question is what to write, and there is a usable order.
Start with the types, which you have already written. Every variable's type: is checked in
every state as an invariant named type_ok, so the shape of your state is asserted before you
write a line. That is not a formality: a spec whose action drives a variable out of range is
refuted by it, and it is the invariant that most often catches a spec that is simply wrong about
its own state.
Then ask what the system promises its callers, and write each promise as a predicate that must never be false. Not "the code does X" — a specification is not a paraphrase of an implementation — but the things you would be embarrassed to be wrong about. For a lock: at most one holder. For a queue: nothing is delivered twice, nothing is lost. For an allocator: no two clients hold the same resource. These are usually few, short, and about relationships between variables rather than about any one of them.
Say what an invariant is for when the name will not carry it. desc: is where that goes. The
checker's counterexample names the invariant (invariant :mutual_exclusion does not hold in this state) and does not print its desc:, so the sentence is for whoever opens the spec to find out
what that name was protecting. (A temporal property's desc: is printed with its refutation,
and so is a Layer 1 invariant's with its violation — see Layer 1.)
invariant :mutual_exclusion,
desc: "at most one client holds the lock — THE property this design exists to keep" do
Enum.count(^clients, fn c -> pc[c] == :holding end) <= 1
endThen use the coverage report to check your own work, which the next two sections are about. The report is the only place that will tell you an invariant you were proud of was never once at risk.
type_ok is an invariant you did not write
The type: on each variable is checked as an invariant named type_ok, in every state, which is
why the table lists one the spec never declared. A state outside its type is reported as a
violation of it. The type is not used to prune the search: a spec whose action drives a variable
out of range does not get a smaller state space, it gets a counterexample.
The near-miss column
holding_means_taken reads nobody is holding, or the lock is not free — an implication, in the
p or q shape. Such an invariant can hold two ways: trivially, because p was true and q did not
matter, or because p was false and q carried it. The second is a near miss: a state in which
the invariant was actually pressed against. Of twenty states, twelve had a holder, and in each of
them free == false is what kept the invariant true.
mutual_exclusion shows -: it has no top-level or, so there is no non-trivial branch to
count, and the column says not measured rather than pretending. An invariant that IS measured
and reports 0 is flagged <-- never at risk: it held in every state without ever being pressed,
which is indistinguishable from true, and is the first thing to be suspicious of when a spec
verifies too easily.
An action that was never enabled
The other way a spec verifies for the wrong reason. Add a cancel action to the lock — a waiting
client may give up — and make the mistake that is easiest to make:
defmodule Tutorial.CancelLock do
use ExTLA.Spec
constant :clients, default: set([:alice, :bob, :carol])
variable :free, type: [true, false]
variable :pc, type: [^clients ~> [:idle, :waiting, :holding]]
init do
free = true
pc = for_each(^clients, fn _ -> :idle end)
end
action :request, params: [c: ^clients] do
require pc[c] == :idle
pc = update(pc, c, fn _ -> :waiting end)
end
action :acquire, params: [c: ^clients] do
require pc[c] == :waiting
require free
free = false
pc = update(pc, c, fn _ -> :holding end)
end
action :release, params: [c: ^clients] do
require pc[c] == :holding
free = true
pc = update(pc, c, fn _ -> :idle end)
end
action :cancel, params: [c: ^clients] do
require pc[c] == :wating
pc = update(pc, c, fn _ -> :idle end)
end
invariant :mutual_exclusion do
Enum.count(^clients, fn c -> pc[c] == :holding end) <= 1
end
invariant :holding_means_taken do
Enum.all?(^clients, fn c -> pc[c] != :holding end) or free == false
end
endmix extla.check Tutorial.CancelLock
Tutorial.CancelLock — verified
20 distinct states, 48 transitions, depth 5, 1ms
--- COVERAGE: Tutorial.CancelLock ----------------------------------
Actions enabled in states distinct
acquire 7 12 12
cancel 0 0 0 <-- NEVER ENABLED
release 12 12 0
request 16 24 7
Invariants evaluated near-miss
holding_means_taken 20 12
mutual_exclusion 20 -
type_ok 20 -
1 warning. Re-run with --strict-coverage to fail on these.
--------------------------------------------------------------------
warning: action :cancel was never enabled:wating is not :waiting, and pc[c] is never equal to it, so cancel is never enabled — and
the spec verifies, with the same twenty states as before. Every invariant holds in a system that
has no cancellation in it. Nothing about the verdict is wrong; what is wrong is what it is a
verdict about. The coverage table is the only place that shows, and --strict-coverage is how you
make a never-enabled action exit 3 rather than print a warning.
action_property — a property of a step
An invariant is a claim about each state on its own. Some properties are not of that kind: money is never created, the audit log only ever grows, the lock is never stolen from its holder. Each compares a state with the one before it, and no predicate over a single state can express any of them — every state involved is perfectly legal, and it is the transition between two of them that is wrong.
action_property is that claim. old and new are bound to the pre- and post-state, and the
property is evaluated on every step the checker takes:
defmodule Tutorial.AuditedLock do
use ExTLA.Spec
constant :clients, default: set([:alice, :bob])
variable :holder, type: ^clients | :none
variable :log, type: seq(^clients)
init do
holder = :none
log = seq()
end
action :acquire, params: [c: ^clients] do
require holder == :none
holder = c
log = append(log, c)
end
action :release do
require holder != :none
holder = :none
end
# Housekeeping, and the bug: it throws away everything but the first entry.
action :compact do
require len(log) > 1
log = seq([head(log)])
end
invariant :holder_is_logged do
holder == :none or len(log) > 0
end
action_property :log_only_grows do
len(new.log) >= len(old.log)
end
endNote what an invariant could not have caught. Every state this spec reaches is fine: a holder or
none, a log of some length, and holder_is_logged holds throughout. There is no bad state to find
— only a bad step, from a log of two entries to a log of one.
Tutorial.AuditedLock — VIOLATION: log_only_grows
10 distinct states, 10 transitions, depth 5, 1ms
═══ VIOLATION: log_only_grows ══════════════════════════════════════
action property :log_only_grows does not hold over the last step
State 1 (Init):
holder = :none
log = []
── acquire(c: :alice) ────────────────────
State 2:
holder = :alice ← changed
log = [:alice] ← changed
── release ────────────────────
State 3:
holder = :none ← changed
log = [:alice]
── acquire(c: :alice) ────────────────────
State 4:
holder = :alice ← changed
log = [:alice, :alice] ← changed
── compact ────────────────────
State 5 [VIOLATION]:
holder = :alice
log = [:alice] ← changed
════════════════════════════════════════════════════════════════════
--- COVERAGE: Tutorial.AuditedLock ---------------------------------
Actions enabled in states distinct
acquire 3 6 6
compact 1 0 0
release 3 3 3
Invariants evaluated near-miss
holder_is_logged 10 6
type_ok 10 -
This run stopped at a counterexample, mid-expansion: the numbers are a lower bound, not a census.
--------------------------------------------------------------------Read the last step, because that is where the whole finding is: the log holds two entries, and
compact replaces it with one. len(new.log) >= len(old.log) is 1 >= 2, and false.
Every state in that trace is legal. State 4 is a perfectly good state — a client holding the lock, two entries logged — and so is State 5. The counterexample is the arrow between them, which is why the trace for an action property is read differently from the trace for an invariant: for an invariant you look at where it ended, and for an action property you look at the last thing that happened.
Delete the compact action and the spec verifies.
02-dsl-semantics.md §4 is
normative on old and new — in particular that a bare variable name inside an
action_property is a compile error, because there it would be ambiguous which of the two you
meant.
When the trace is too big to read
That trace was five states of two variables and you read it by eye. Real ones are not like that. A Raft election counterexample is nineteen states of five variables, several of them maps over three servers, and the question you actually have — when did the quorum first form, how many acceptors had promised by state 12 — is a function of the state. Answering it from the dumps means reading nineteen blocks and doing arithmetic by hand.
So ask the function instead. ExTLA.Trace.explore/3 takes your own expressions, one row each,
and evaluates them at every state:
result = ExTLA.ModelChecker.run(Tutorial.AuditedLock, %{constants: %{clients: MapSet.new([:alice, :bob])}})
trace = result.violation
ExTLA.Trace.explore(trace,
holder: & &1.holder,
logged: &length(&1.log),
held?: &(&1.holder != :none)
)═══ EXPLORE: log_only_grows ════════════════════════════════════════
1 2 3 4 5
init acquire release acquire compact
─────────────────────────────────────────────────
holder :none :alice :none :alice :alice
logged 0 1 1 2 1
held? false true false true true
Bindings:
2 acquire(c: :alice)
4 acquire(c: :alice)
════════════════════════════════════════════════════════════════════logged going 2 → 1 at the last step is the whole finding, on one line.
TLA+ has the same tool — the Toolbox's Trace Explorer — and there it needs a generated
specification, a second TLC run and a GUI panel, because a TLA+ state is not a value your
program can hold. Here a state is a plain map and an expression over one is an anonymous
function, so the whole apparatus is Enum.map/2.
Three things worth knowing:
changed_only: truehides the rows that never move. On a wide trace most rows never move, and the one that does is the one you are looking for.- A lasso works too. The repeating states are marked
↺, so a liveness counterexample does not read as though it ended. - An expression that raises is reported at the state it raised in, and the rest of the table still renders. You are exploring this trace because something in it is wrong, so an expression that assumes an invariant this trace violates is the normal case, not an error.
Without re-running the checker
A counterexample from a CI run or an incident months ago can be explored from the file:
mix extla.check Tutorial.AuditedLock --format json > ce.json
mix extla.explore Tutorial.AuditedLock --trace ce.json \
--expr "logged: length(log)" \
--expr "held?: holder != :none"
--expr is repeatable, and inside one the state is in scope as each variable by its own name
and as state, the whole map. It compiles and evaluates what you typed, which is what the
Toolbox does with the expressions typed into its panel — there is no way to put an anonymous
function on a command line.
Nothing is searched: the states are read off disk. The module argument is there because the trace's atoms are resolved against the ones the system already has, so the spec must be loaded before its counterexample can be decoded.
Deadlock, and the terminal you will need
This is the first thing that will go wrong for you, so it is worth meeting deliberately.
A reachable state with no enabled action is a deadlock, and the checker reports it as a violation. That is the right default — for a lock, a queue, a protocol, a state nothing can leave is a bug. But it means that any specification which finishes its work is refuted, because finishing looks exactly like being stuck.
Here is the same lock, made one-shot: each client may take it once and is then :done.
defmodule Tutorial.OneShotLock do
use ExTLA.Spec
constant :clients, default: set([:alice, :bob])
variable :free, type: [true, false]
variable :pc, type: [^clients ~> [:idle, :waiting, :holding, :done]]
init do
free = true
pc = for_each(^clients, fn _ -> :idle end)
end
action :request, params: [c: ^clients] do
require pc[c] == :idle
pc = update(pc, c, fn _ -> :waiting end)
end
action :acquire, params: [c: ^clients] do
require pc[c] == :waiting
require free
free = false
pc = update(pc, c, fn _ -> :holding end)
end
action :finish, params: [c: ^clients] do
require pc[c] == :holding
free = true
pc = update(pc, c, fn _ -> :done end)
end
invariant :mutual_exclusion do
Enum.count(^clients, fn c -> pc[c] == :holding end) <= 1
end
endNothing about it is wrong. Every client gets the lock, uses it, and is done. And:
mix extla.check Tutorial.OneShotLock
Tutorial.OneShotLock — DEADLOCK
15 distinct states, 20 transitions, depth 7, 0ms
═══ DEADLOCK ═══════════════════════════════════════════════════════
this state has no successors and no `terminal` predicate admits it. If it is a legitimate end state, declare it: `terminal :name do … end` (02-dsl-semantics.md §5.3).
State 1 (Init):
free = true
pc = %{alice: :idle, bob: :idle}
── request(c: :alice) ────────────────────
State 2:
free = true
pc = %{alice: :waiting, bob: :idle} ← changed
── request(c: :bob) ────────────────────
State 3:
free = true
pc = %{alice: :waiting, bob: :waiting} ← changed
── acquire(c: :alice) ────────────────────
State 4:
free = false ← changed
pc = %{alice: :holding, bob: :waiting} ← changed
── finish(c: :alice) ────────────────────
State 5:
free = true ← changed
pc = %{alice: :done, bob: :waiting} ← changed
── acquire(c: :bob) ────────────────────
State 6:
free = false ← changed
pc = %{alice: :done, bob: :holding} ← changed
── finish(c: :bob) ────────────────────
State 7 [VIOLATION]:
free = true ← changed
pc = %{alice: :done, bob: :done} ← changed
════════════════════════════════════════════════════════════════════
--- COVERAGE: Tutorial.OneShotLock ---------------------------------
Actions enabled in states distinct
acquire 5 6 6
finish 6 6 5
request 7 8 3
Invariants evaluated near-miss
mutual_exclusion 15 -
type_ok 15 -
--------------------------------------------------------------------Read the last state: both clients are done, the lock is free, and no action is enabled
— request needs :idle, acquire needs :waiting, finish needs :holding. The system has
finished, and the checker cannot tell that from being wedged. Exit code 1.
The counterexample is still worth reading even here, because the state it ends in is the answer: if that state is what success looks like, you have found a missing declaration rather than a bug.
Declaring the end state
terminal names the states that are final on purpose:
defmodule Tutorial.OneShotLockDone do
use ExTLA.Spec
constant :clients, default: set([:alice, :bob])
variable :free, type: [true, false]
variable :pc, type: [^clients ~> [:idle, :waiting, :holding, :done]]
init do
free = true
pc = for_each(^clients, fn _ -> :idle end)
end
action :request, params: [c: ^clients] do
require pc[c] == :idle
pc = update(pc, c, fn _ -> :waiting end)
end
action :acquire, params: [c: ^clients] do
require pc[c] == :waiting
require free
free = false
pc = update(pc, c, fn _ -> :holding end)
end
action :finish, params: [c: ^clients] do
require pc[c] == :holding
free = true
pc = update(pc, c, fn _ -> :done end)
end
invariant :mutual_exclusion do
Enum.count(^clients, fn c -> pc[c] == :holding end) <= 1
end
terminal :all_done do
Enum.all?(^clients, fn c -> pc[c] == :done end)
end
endTutorial.OneShotLockDone — verified
15 distinct states, 20 transitions, depth 7, 0msThe same fifteen states, the same twenty transitions — the search did not change at all. What changed is that one of those states is now declared to be an ending. That is the whole mechanism, and it is worth being clear about what it does not do (§5.3):
- Invariants are still checked in a terminal state. Declaring an ending does not exempt it.
- No action is disabled by it. A
terminalis a claim about a state, not a stop instruction. - For liveness it stutters forever, so a
p ~> qwhoseqhas not happened by then is violated there — which is the correct verdict, because it never will happen.
There is also check_deadlock: false, which turns the whole check off. It is a key in the
config you pass to ExTLA.ModelChecker.run/2 or assert_spec/2, not a mix extla.check
flag: from the command line, the way to accept an end state is to declare it. Prefer the
declaration anyway: it says which states are meant to be final and leaves deadlock detection on
for every other state, which is where you want it.
A terminal that is too generous
The declaration is a claim, and like any claim it can be wider than you meant. Suppose
someone_done instead of all_done — one client finishing admits the state:
defmodule Tutorial.OneShotLockLoose do
use ExTLA.Spec
constant :clients, default: set([:alice, :bob])
variable :free, type: [true, false]
variable :pc, type: [^clients ~> [:idle, :waiting, :holding, :done]]
init do
free = true
pc = for_each(^clients, fn _ -> :idle end)
end
action :request, params: [c: ^clients] do
require pc[c] == :idle
pc = update(pc, c, fn _ -> :waiting end)
end
action :acquire, params: [c: ^clients] do
require pc[c] == :waiting
require free
free = false
pc = update(pc, c, fn _ -> :holding end)
end
action :finish, params: [c: ^clients] do
require pc[c] == :holding
free = true
pc = update(pc, c, fn _ -> :done end)
end
invariant :mutual_exclusion do
Enum.count(^clients, fn c -> pc[c] == :holding end) <= 1
end
# `any?`, not `all?` — one client finishing admits the state.
terminal :someone_done do
Enum.any?(^clients, fn c -> pc[c] == :done end)
end
endIt still verifies, and the coverage report is where it shows up — not in the tables, which are the same fifteen states as before, but in the warning under them:
Tutorial.OneShotLockLoose — verified
15 distinct states, 20 transitions, depth 7, 0ms
--- COVERAGE: Tutorial.OneShotLockLoose ----------------------------
Actions enabled in states distinct
acquire 5 6 6
finish 6 6 5
request 7 8 3
Invariants evaluated near-miss
mutual_exclusion 15 -
type_ok 15 -
--------------------------------------------------------------------
warning: terminal :someone_done admitted a live stateterminal_but_live: a state the predicate called final still had an enabled action. It is not
an error — a system may legitimately be allowed to stop early — but it almost always means the
predicate is broader than the end state it was written for, and a broad terminal is how a real
deadlock gets admitted as an ending. It stays a warning even under --strict-coverage, which fails
the build only on a never-enabled action or a vacuous property: an early stop can be legitimate,
so the checker reports it and leaves the judgement to you.
Next: Temporal properties, and the difference fairness makes.