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

Parses a `temporal` block into the bounded fragment of
`02-dsl-semantics.md` §5.1:

    formula  ::= temporal | Enum.all?(^constant, fn x -> formula end)
    temporal ::= pred | always(pred) | eventually(pred)
               | always(eventually(pred)) | eventually(always(pred))
               | pred ~> pred | always(pred ~> pred)

**The nesting is bounded, and the grammar says so.** `always`, `eventually`
and `~>` take a `pred`, not a `formula`, so `always(always(P))` is outside the
grammar and fails to compile with the module, declaration and line — the
checker evaluates these seven shapes and no others.

There is no negation, conjunction or disjunction **of formulas**. A `pred` may
of course contain `not`/`and`/`or`; the restriction is on combining formulas.

This is deliberate, not a gap: the fragment covers the properties people
actually write and is checkable by SCC analysis without constructing a Büchi
automaton. A formula outside it is a compile error naming the unsupported
operator — never a silently weaker check.

`P ~> Q` already means `always(P implies eventually(Q))`, so `always(P ~> Q)`
is accepted and collapsed rather than rejected: TLA+ users write it out of
habit and it means the same thing.

# `parse!`

Parse a temporal block into quoted code that builds a
`ExTLA.Spec.Compiled.temporal_formula()`.

---

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