# `ExTLA.Temporal.Fairness`
[🔗](https://github.com/dcoai/extla/blob/v0.6.0/lib/ex_tla/temporal/fairness.ex#L1)

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.

# `constraint`

```elixir
@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.

# `constraint_predicates`

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.

# `describe`

How a constraint reads, for a message: `SF(acquire_lock, p: :p1)` or `WF(timeout)`.

# `expand`

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.

# `strong_fairness`

`SF_vars(A)` over one behaviour: if A is *repeatedly* enabled — even intermittently —
it is eventually taken.

    SF_vars(A)  ==  <>[]~(ENABLED <A>_vars)  \/  []<><A>_vars

The 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.

# `weak_fairness`

`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>_vars

Either 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.

---

*Consult [api-reference.md](api-reference.md) for complete listing*