# `ExTLA.Temporal`
[๐](https://github.com/dcoai/extla/blob/v0.6.0/lib/ex_tla/temporal.ex#L1)
`ENABLED`, as the liveness graph records it.
## Two ways to evaluate a temporal formula
`ExTLA.ModelChecker.Liveness` evaluates the ยง5.1 fragment over the *state graph*, by
looking for a strongly connected component a fair behaviour could cycle in forever.
That answers a question about every behaviour of the spec at once, which is what model
checking is for.
The operators here answer the other question: does **this one behaviour** satisfy the
formula? That is what Layer 3 needs โ an implementation produces a trace, and the trace
is checked against the properties the spec claims. It is also a cross-check on the
first: a lasso the model checker hands back as a counterexample must come back
`:violated` when evaluated here, and its cycle must satisfy every fairness constraint
the spec declares. Two independent implementations of the same semantics that disagree
mean one of them is wrong.
## Three verdicts, because a finite trace is not a behaviour
A behaviour is infinite; a trace is a prefix of one. A prefix can *refute* `always(P)`
โ one state where P is false settles it โ and can *satisfy* `eventually(P)`, but it can
do neither the other way round: P might fail after the trace ends, or hold after it.
So every operator here returns `:holds`, `:violated` or **`:inconclusive`**, and never
collapses the third into the first. That is the same rule as `:max_states_reached` in
Layer 2, applied one level down.
A **lasso** removes the doubt. When the trace is a prefix followed by a cycle that
repeats forever โ which is what a model-checker counterexample is, and what a
simulation that reaches a `terminal` state produces โ the behaviour is fully described
by finitely many states, and every operator gives a definite answer. Pass the index the
cycle returns to as `lasso_start`; `ExTLA.Trace.to_behavior/1` computes it.
## Why this calls into the checker
Enabledness is a function of an action's params and guard alone (`02-dsl-semantics.md`
ยง2.1, ยง3). It does not consult the state graph โ an earlier draft took a `state_graph`
argument, but the graph records reachable successors, not enabledness, and a
parent-pointer graph records no successors at all.
It is computed here by the same `ExTLA.ModelChecker.enabled_bindings/3` that generates
the edges, and deliberately so. The bit and the edges sit next to each other in the
liveness graph and are read together by the fairness rules โ "enabled in every state of
this component, and taken in none of them" is a comparison between them. Two
implementations of "which bindings are enabled here" would eventually disagree, and a
fairness constraint reading a bit that disagrees with the edge beside it is unsound in
the direction that reports a violated property as holding.
# `action_predicate`
```elixir
@type action_predicate() :: (ExTLA.State.t(), ExTLA.State.t() -> boolean())
```
An action, as TLA+ means it: a relation on a pair of consecutive states.
# `behavior`
```elixir
@type behavior() :: ExTLA.State.behavior()
```
# `lasso_start`
```elixir
@type lasso_start() :: non_neg_integer() | nil
```
The index the cycle returns to, or `nil` when the trace is a prefix of something longer
and the operators cannot settle a question the states do not answer.
# `predicate`
```elixir
@type predicate() :: (ExTLA.State.t() -> boolean())
```
A state predicate, as a `temporal` block compiles to.
# `verdict`
```elixir
@type verdict() :: :holds | :violated | :inconclusive
```
What a finite trace establishes about a formula. `:inconclusive` is not a failure โ it
is the trace saying it does not reach far enough to know.
# `always`
`[]P` โ P holds in every state.
Refutable by any trace: one state where P is false settles it. Establishable only when
the trace is a lasso, because otherwise P may fail after it ends.
# `always_eventually`
`[]<>P` โ P is true infinitely often.
With a lasso, exactly "P occurs somewhere in the cycle": the cycle's states are the
ones that recur, and nothing else does.
# `box_action`
`[][A]_v` โ every step either satisfies A or leaves every variable in `vars` alone.
The stuttering allowance is what makes a TLA formula about a system rather than about a
transcript: a step that changes nothing the spec models is always permitted.
# `cycle`
The states that recur forever: the cycle of a lasso, or `nil` without one.
# `diamond_action`
`<>_v` โ some step satisfies A and changes at least one variable in `vars`.
The `_v` form excludes stuttering deliberately: "A happened" has to mean something
moved, or every behaviour satisfies it by standing still.
# `enabled?`
`ENABLED A`: whether the action has a legal successor from this state โ some binding of
its params for which every generator is non-empty and the guard holds.
`binding` restricts the question to one binding of the leading params, which is what
per-binding fairness asks (`02-dsl-semantics.md` ยง5.2): `ENABLED AcquireLock(p1)` is
`enabled?(state, acquire_lock, constants, %{p: :p1})`. The default `%{}` restricts
nothing and asks `ENABLED \E p : AcquireLock(p)`, which is the whole-action form and a
strictly weaker question โ the distinction ยง5.2 exists for.
# `enabled_among?`
The same question against bindings already computed.
The checker has the enabled bindings of every action in hand while it expands a state โ
they are what it turns into edges โ so the bits cost no guard evaluations of their own.
# `eventually`
`<>P` โ P holds in at least one state.
The mirror of `always/3`: satisfiable by any trace, refutable only by a lasso.
# `eventually_always`
`<>[]P` โ P becomes true and stays true forever.
Neither satisfiable nor refutable without a lasso: any prefix extends to a behaviour
where P holds forever after it, and to one where it does not. With a lasso it is
decided by the cycle alone โ the states outside it occur finitely often and cannot
settle what happens "forever after".
# `extends?`
Whether a full binding agrees with a partial one everywhere the partial one speaks.
Per-binding fairness, the ENABLED bits and `ExTLA.ModelChecker.Liveness`'s "was this
action taken inside the component" all ask it, so it has one definition rather than
three.
# `leads_to`
`P ~> Q` โ whenever P holds, Q holds then or later.
`:inconclusive` for any trace without a lasso, and that is not a weakness of the
implementation: a P with no Q after it may still get its Q in the next state, and a
trace where every P was answered may fail at the first state past the end. Neither
direction is settled by a prefix.
# `steps`
The steps of a behaviour, as `{pre, post}` pairs.
Under a lasso the last step is the one that closes it โ from the final state back to
`lasso_start`. Leaving it out would lose the step a fairness constraint is most often
satisfied by, and would let a cycle of one state have no steps at all.
---
*Consult [api-reference.md](api-reference.md) for complete listing*