# `ExTLA.ModelChecker.Liveness`
[🔗](https://github.com/dcoai/extla/blob/v0.6.0/lib/ex_tla/model_checker/liveness.ex#L1)

Temporal property checking over the liveness graph.

A liveness property is refuted by an infinite behaviour, and an infinite behaviour in a
finite graph is a **lasso**: a finite prefix, then a cycle repeated forever. The states
a behaviour visits infinitely often are a strongly connected set, so the search is for
a strongly connected component that (a) the property forbids being cycled in forever
and (b) the spec's fairness constraints permit cycling in.

## What "permits" means

A component `S` is unfair when a fairness constraint says it cannot be the tail of a
behaviour (`02-dsl-semantics.md` §5.2):

- **WF(A)** is broken by `S` when `A` is enabled in *every* state of `S` and no edge
  inside `S` takes it — continuously enabled and never taken.
- **SF(A)** is broken by `S` when `A` is enabled in *some* state of `S` and no edge
  inside `S` takes it — repeatedly enabled and never taken.

Both read the ENABLED bits `ExTLA.StateGraph` recorded while each state was materialized,
and the edges beside them. That is what the liveness graph is for.

A broken WF kills every strongly connected *subset* of `S` too: a subset has `A` enabled
everywhere as well, and no more edges to take it with. A broken SF does not — dropping
the states where `A` is enabled can leave a smaller component that is fair. So the
search does exactly that and recurses, which is the shape of the Emerson–Lei algorithm
and the reason this is not just "Tarjan, then filter".

## A terminal state stutters forever

`02-dsl-semantics.md` §5.3: a state with no successors is a legal end of a behaviour,
which stutters there. So a stuck state is a self-loop here, and it is always fair —
nothing is enabled in it, so no constraint can require anything to be taken. A
leads-to whose consequent has not held by then is violated there, which is the correct
verdict and the one that refutes the Raft election example's `eventually_elect_leader`
(`07-examples.md`).

## The supported fragment

`02-dsl-semantics.md` §5.1, as `ExTLA.Spec.Temporal` parses it. Each formula reduces to
one of six shapes, and each shape to a question about components:

| Formula | Refuted by |
|---|---|
| `pred` | an initial state where it is false |
| `always(pred)` | any reachable state where it is false |
| `eventually(pred)` | a fair component of the ¬pred subgraph, reached without leaving it |
| `always(eventually(pred))` | a fair component of the ¬pred subgraph, reached any way at all |
| `eventually(always(pred))` | a fair component holding a ¬pred state |
| `p ~> q` | a reachable `p ∧ ¬q` state that reaches a fair component of the ¬q subgraph |

`always(pred)` needs no component search: every reachable state has a fair continuation,
because a walk to a *bottom* component is always available and a bottom component is
always fair — every action enabled inside it has its edge inside it, since nothing
leaves.

A nesting outside this table raises rather than being approximated. §5.1's grammar is
recursive and admits shapes like `always(eventually(always(p)))`; evaluating one of
those as though it were something simpler would be a silently weaker check.

## What it costs

One pass materializing every state to evaluate the properties' predicates — the states
are not kept — the graph stores parent pointers rather than states, so that memory stays
a small fixed record per state — so they are regenerated, one transition each,
holding only the states that still have children to generate. Then Tarjan per property,
which is linear in the graph.

# `verdict`

```elixir
@type verdict() :: :ok | {:violation, atom(), ExTLA.Trace.lasso()}
```

# `answerable?`

Whether this graph can carry a liveness verdict at all.

The non-raising counterpart to the check below, so a caller can decline to ask rather than
crash after the search. A `state_constraint:` holds states back without expanding them,
so a constrained run reaches the end with a graph that has fewer edge entries than
states, and the check would raise `ArgumentError` there, taking the valid safety result
with it.

The pairing is only *conditionally* bad: a constraint that never actually holds a state
back leaves a complete graph and liveness works. That is why this is a predicate the
caller consults rather than an up-front refusal like symmetry's and workers' — those are
unconditionally incompatible and can be rejected before any work happens.

# `check`

Check a spec's temporal properties against a completed liveness graph.

`selected` is `:all` or a list of property names, the way `invariants:` selects
invariants. A run reports only the first violation, so asking one property at a time is
how to get a verdict for each.

Returns the first violation in declaration order, with the lasso that refutes it.

---

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