2580 Tlaplus Syntax Cf31ead9

TLA+ Syntax Reference

Module Structure

---- MODULE ModuleName ----
EXTENDS StandardModules
CONSTANTS ConstantDeclarations
VARIABLES VariableDeclarations

Definitions

====

Standard Modules

Common modules to extend:

• Naturals: Natural numbers (0, 1, 2, ...), operators: +, -, *, /, %, ^, .., \div, \leq, \geq
• Integers: All integers, includes Naturals
• Reals: Real numbers
• Sequences: Sequence operations (Seq, Len, Append, Head, Tail, SubSeq)
• FiniteSets: Finite set operations (Cardinality, IsFiniteSet)
• TLC: TLC-specific operators (Print, Assert, JavaTime)

Variable Declarations

VARIABLES x, y, z

\* Group variables for convenience
vars == <<x, y, z>>

Constants

CONSTANTS MaxValue, NumProcesses, Data

Constants are parameters that remain fixed during execution.

Operators

Boolean Operators

• /\ - AND (conjunction)
• \/ - OR (disjunction)
• ~ - NOT (negation)
• => - Implies
• <=> - Equivalence (if and only if)

Comparison Operators

• = - Equality
• # or /= - Inequality
• <, >, \leq, \geq - Ordering

Set Operators

• \in - Element of
• \notin - Not element of
• \subseteq - Subset or equal
• \cup - Union
• \cap - Intersection
• \ - Set difference
• SUBSET S - Set of all subsets of S
• UNION S - Union of all sets in S

Set Construction

{1, 2, 3}                    \* Explicit set
{x \in S : P(x)}             \* Set filter
{e(x) : x \in S}             \* Set map

Sequence Operators

<<1, 2, 3>>                  \* Sequence literal
Len(seq)                     \* Length
seq[i]                       \* Index (1-based)
Append(seq, elem)            \* Append element
Head(seq)                    \* First element
Tail(seq)                    \* All but first
SubSeq(seq, m, n)            \* Subsequence from m to n
seq1 \o seq2                 \* Concatenation

Record Operators

[field1 |-> value1, field2 |-> value2]    \* Record literal
record.field                               \* Field access
[record EXCEPT !.field = newValue]         \* Update field

Function Operators

[x \in S |-> e(x)]                        \* Function definition
f[x]                                       \* Function application
DOMAIN f                                   \* Domain of function
[f EXCEPT ![x] = newValue]                 \* Update function

Temporal Operators

Action Operators

• [A]_v - A or variables v unchanged (stuttering)
• <<A>>_v - A and variables v changed (non-stuttering)
• ENABLED A - Action A is enabled
• UNCHANGED v - Variables v remain unchanged
• v' - Next-state value of v

Temporal Logic Operators

• []P - Always P (globally)
• <>P - Eventually P (finally)
• P ~> Q - P leads to Q (P implies eventually Q)
• [][A]_v - Always A or v unchanged
• WF_v(A) - Weak fairness of A with respect to v
• SF_v(A) - Strong fairness of A with respect to v

Common Patterns

Initial State Predicate

Init ==
    /\ x = 0
    /\ y = {}
    /\ z = <<>>

Action Definition

Action ==
    /\ Precondition          \* Guard/enabling condition
    /\ x' = x + 1            \* State update
    /\ UNCHANGED <<y, z>>    \* Other variables unchanged

Next State Relation

Next ==
    \/ Action1
    \/ Action2
    \/ Action3

Specification

Spec == Init /\ [][Next]_vars

With fairness:

Spec == Init /\ [][Next]_vars /\ WF_vars(Action1)

Type Invariant

TypeInvariant ==
    /\ x \in Nat
    /\ y \in SUBSET Data
    /\ z \in Seq(Data)

Safety Property

SafetyProperty ==
    /\ x \leq MaxValue
    /\ Cardinality(y) \leq 10

Liveness Property

LivenessProperty ==
    <>(x = MaxValue)         \* Eventually x reaches MaxValue

Quantifiers

\A x \in S : P(x)            \* For all x in S, P(x) holds
\E x \in S : P(x)            \* There exists x in S such that P(x)

Conditional Expressions

IF condition THEN expr1 ELSE expr2

CASE p1 -> e1
  [] p2 -> e2
  [] OTHER -> e3

LET Definitions

LET
    helper(x) == x + 1
    constant == 42
IN
    helper(constant)

CHOOSE Operator

CHOOSE x \in S : P(x)        \* Arbitrarily choose x from S satisfying P

Common Idioms

Nondeterministic Choice

\E x \in S :
    /\ Condition(x)
    /\ var' = x
    /\ UNCHANGED other_vars

Parameterized Action

Action(param) ==
    /\ param \in ValidParams
    /\ var' = f(param)
    /\ UNCHANGED other_vars

Next == \E p \in Params : Action(p)

Multiple Process Model

VARIABLES pc, data

Process(i) ==
    /\ pc[i] = "ready"
    /\ pc' = [pc EXCEPT ![i] = "running"]
    /\ data' = data \cup {i}

Next == \E i \in Processes : Process(i)

Message Passing

VARIABLES messages

Send(msg) ==
    messages' = messages \cup {msg}

Receive(msg) ==
    /\ msg \in messages
    /\ messages' = messages \ {msg}

Mutex Lock

VARIABLES lock, owner

Acquire(proc) ==
    /\ lock = FALSE
    /\ lock' = TRUE
    /\ owner' = proc

Release(proc) ==
    /\ lock = TRUE
    /\ owner = proc
    /\ lock' = FALSE
    /\ owner' = NULL

Comments

\* Single line comment

(* Multi-line
   comment *)

Operator Precedence (highest to lowest)

1. Function application: f[x], record access: r.field
2. Prefix operators: ~, DOMAIN, SUBSET, UNION, ENABLED, UNCHANGED
3. Postfix operators: ' (prime)
4. Infix operators (left to right within same level):
   • ^ (exponentiation)
   • *, /, \div, %
   • +, -, \o (concatenation)
   • .. (range)
   • Set operators: \cap, \cup, \
   • Comparison: =, #, /=, <, >, \leq, \geq, \in, \notin, \subseteq
   • /\ (AND)
   • \/ (OR)
   • => (implies)
   • <=> (equivalence)
5. Temporal operators: [], <>, ~>
6. Quantifiers: \A, \E

Use parentheses to clarify precedence when in doubt.