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.