TLX.Temporal (TLX v0.5.2)

Temporal operators, quantifiers, and expression helpers for use in property, invariant, and action expressions.

These functions build tagged tuples that the emitters translate to TLA+ syntax.

Temporal operators

always(expr)              # []P
eventually(expr)          # <>P
always(eventually(expr))  # []<>P
leads_to(p, q)            # P ~> Q (equivalent to [](P => <>Q))
until(p, q)               # P U Q (strong — Q must eventually hold)
weak_until(p, q)          # P W Q (weak — P may hold forever)

Quantifiers

forall(:x, :set, expr)    # \A x \in set : expr
exists(:x, :set, expr)    # \E x \in set : expr

Expression helpers

ite(cond, then, else)     # IF cond THEN then ELSE else
let_in(:var, binding, body) # LET var == binding IN body

Summary

Functions

always(expr)

at(f, x)

Function application. f[x] in TLA+.

case_of(clauses)

CASE expression. CASE p1 -> e1 [] p2 -> e2 in TLA+.

choose(var, set, expr)

Deterministic choice. CHOOSE var \in set : expr in TLA+.

domain(f)

Domain of a function. DOMAIN f in TLA+.

equiv(p, q)

Equivalence. p <=> q in TLA+.

eventually(expr)

except(f, x, v)

Functional update. [f EXCEPT ![x] = v] in TLA+.

except_many(f, pairs)

Multi-key functional update. [f EXCEPT ![k1] = v1, ![k2] = v2] in TLA+.

exists(var, set, expr)

forall(var, set, expr)

implies(p, q)

Implication. p => q in TLA+.

ite(condition, then_expr, else_expr)

IF/THEN/ELSE conditional expression.

leads_to(p, q)

let_in(var, binding, body)

LET/IN local definition. LET var == binding IN body.

range(a, b)

Integer range set. a..b in TLA+.

record(pairs)

Record construction. [a |-> 1, b |-> 2] in TLA+.

until(p, q)

Strong until. P \U Q in TLA+. P holds until Q becomes true; Q must eventually hold.

weak_until(p, q)

Weak until. P \W Q in TLA+. P holds until Q becomes true, or P holds forever.