TLX.Expr (TLX v0.5.2)

Copy Markdown

Provides the e/1 macro for capturing Elixir expressions as TLA+ AST.

This module is automatically imported into DSL scope — you don't need to import it manually.

Usage

guard e(x < max)
next :x, e(x + 1)
invariant :bounded, expr: e(x >= 0 and x <= 5)

The name e is short for "expression". It avoids collision with the expr schema option on invariant and property entities.

case/do inside e()

Native Elixir case expressions are transformed at macro expansion into case_of/1 IR, producing a TLA+ CASE with OTHER:

e(case state do
  :queued    -> :queued
  :deployed  -> :deployed
  _          -> :deploying
end)

Only literal atom/integer patterns and _ (wildcard) are supported. Use case_of/1 directly for complex conditions.

Summary

Functions

e(body)

Capture an Elixir expression as a TLA+ expression.

next(keyword)

Set multiple variable transitions at once.

transitions(keyword)

Functions

e(body)

(macro)

Capture an Elixir expression as a TLA+ expression.

The expression is quoted (not evaluated) and wrapped for the emitters. Any case var do pattern -> expr end nodes are transformed into {:case_of, clauses} IR where _ becomes the :otherwise sentinel.

next(keyword)

(macro)

Set multiple variable transitions at once.

next flag1: true, turn: 2, pc1: :waiting

Expands to:

next :flag1, true
next :turn, 2
next :pc1, :waiting

Also available as transitions/1 (alias).

transitions(keyword)

(macro)