The fairness constraints a run actually has, expanded from what the spec declares.
02-dsl-semantics.md §5.2 gives two forms:
fairness :weak, [:done, :reset] # WF_vars(Done), WF_vars(Reset)
fairness :strong, acquire_lock: [:p] # \A p \in Procs : SF_vars(AcquireLock(p))The first is one constraint. The second is one constraint per element of the set p
ranges over, and the difference is the whole reason §5.2 exists: WF_vars(\E p : A(p))
says only that some process acts infinitely often, which is consistent with one
process starving while the others take turns, and is too weak to prove anything about a
particular one. distributed_lock's no_starvation is about a particular one.
So a declaration becomes a list of {fairness_def, binding}, and it is that list — the
graph's fairness_index — that the ENABLED bits are indexed by, one bit each, in this
order.
Why it needs a state
A param's generator is a function of (constants, state, bindings_so_far), so
enumerating what p ranges over means calling one. §5.2 restricts a quantified param to
a constant or a literal precisely so the answer cannot depend on the state, and §7
rejects a state-drawn one at compile time — so any state gives the same answer. The
checker passes the first initial state, for the same reason ExTLA.Coverage does when it
enumerates the param universe: it is a real state rather than a stand-in, and a
stand-in is how a generator that quietly does read the state would go unnoticed.
Summary
Types
One constraint: a declaration, and the binding of the leading params it is about.
%{} is the whole-action form.
Functions
The {action, enabled} predicates for one constraint, over a spec and its constants.
How a constraint reads, for a message: SF(acquire_lock, p: :p1) or WF(timeout).
Every fairness constraint of a spec under constants, in declaration order and, within
a per-binding declaration, in generator order.
SF_vars(A) over one behaviour: if A is repeatedly enabled — even intermittently —
it is eventually taken.
WF_vars(A) over one behaviour: if A is continuously enabled from some point on, it
is eventually taken.
Types
@type constraint() :: {ExTLA.Spec.Compiled.fairness_def(), binding :: map()}
One constraint: a declaration, and the binding of the leading params it is about.
%{} is the whole-action form.
Functions
The {action, enabled} predicates for one constraint, over a spec and its constants.
action is the constraint's action read as TLA+ reads one — a relation on a pair of
states, true when some binding the constraint permits carries the first to the
second. enabled is ENABLED for the same binding.
Both are what weak_fairness/5 and strong_fairness/5 need and cannot derive for
themselves, and building them here keeps the arithmetic of §5.2's per-binding form in
one place.
How a constraint reads, for a message: SF(acquire_lock, p: :p1) or WF(timeout).
Every fairness constraint of a spec under constants, in declaration order and, within
a per-binding declaration, in generator order.
The order is the bit order of ExTLA.StateGraph's enabled bitstrings, so it has to be
deterministic — the same reason the search itself is.
SF_vars(A) over one behaviour: if A is repeatedly enabled — even intermittently —
it is eventually taken.
SF_vars(A) == <>[]~(ENABLED <A>_vars) \/ []<><A>_varsThe only difference from weak_fairness/5 is the first disjunct: A must be disabled
from some point on, which over a lasso means disabled in every state of the cycle
rather than in one of them. That single quantifier is the whole distance between the
two, and it is why distributed_lock's no_starvation needs the strong form: a
competitor takes the lock and gives it back, so acquiring is disabled in some states of
the cycle and enabled in others, which satisfies WF and not SF.
WF_vars(A) over one behaviour: if A is continuously enabled from some point on, it
is eventually taken.
WF_vars(A) == []<>~(ENABLED <A>_vars) \/ []<><A>_varsEither A stops being enabled infinitely often, or it is taken infinitely often. Over a
lasso both reduce to the cycle, since nothing outside it recurs: the first is "A is
disabled somewhere in the cycle", the second is "an A-step occurs inside it". Those
are exactly the conditions ExTLA.ModelChecker.Liveness reads off a strongly connected
component, arrived at from the other direction — which is what makes checking one
against the other worth doing.
:inconclusive without a lasso: a prefix cannot establish that anything happens
infinitely often, nor that it stops.
enabled is passed separately rather than derived from action. ENABLED <A>_v
quantifies over every state
A could lead to, and a behaviour contains only the states that happened — so no
function of the observed steps can answer it. constraint_predicates/3 builds both from
a spec, which is where the answer actually lives.