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
SwhenAis enabled in every state ofSand no edge insideStakes it — continuously enabled and never taken. - SF(A) is broken by
SwhenAis enabled in some state ofSand no edge insideStakes 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.
Summary
Functions
Whether this graph can carry a liveness verdict at all.
Check a spec's temporal properties against a completed liveness graph.
Types
@type verdict() :: :ok | {:violation, atom(), ExTLA.Trace.lasso()}
Functions
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 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.