tools-only TLA+ Syntax Reference
Quick reference for TLA+ specification language.
Module Structure
---- MODULE ModuleName ----
EXTENDS Naturals, Sequences
CONSTANTS N
VARIABLES x, y, z
Init == x = 0 /\ y = 0 /\ z = 0
Next == ...
Spec == Init /\ [][Next]_<<x,y,z>>
====
Basic Syntax
Comments
\* Single-line comment
(* Multi-line
comment *)
Logical Operators
/\- AND (conjunction)\/- OR (disjunction)~- NOT (negation)=>- Implies<=>- Equivalence (if and only if)
Comparison Operators
=- Equality/=or#- Inequality<,<=,>,>=- Ordering
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)
Data Types
Booleans
BOOLEAN \* Set {TRUE, FALSE}
TRUE
FALSE
Numbers
Nat \* Natural numbers {0, 1, 2, ...}
0..10 \* Range from 0 to 10
x + y \* Addition
x - y \* Subtraction
x * y \* Multiplication
x \div y \* Integer division
x % y \* Modulo
Sets
{} \* Empty set
{1, 2, 3} \* Explicit set
{x \in S : P(x)} \* Set comprehension
x \in S \* Set membership
S \subseteq T \* Subset
S \cup T \* Union
S \cap T \* Intersection
S \ T \* Set difference
SUBSET S \* Power set (all subsets of S)
UNION S \* Union of all sets in S
Cardinality(S) \* Size of set S
Sequences
<<>> \* Empty sequence
<<1, 2, 3>> \* Explicit sequence
Seq(S) \* All sequences with elements from S
Head(seq) \* First element
Tail(seq) \* All but first element
Append(seq, x) \* Add x to end
Len(seq) \* Length of sequence
seq[i] \* i-th element (1-indexed)
SubSeq(seq, m, n) \* Subsequence from m to n
Records
[field1 |-> value1, field2 |-> value2] \* Record literal
r.field \* Field access
[r EXCEPT !.field = newValue] \* Update field
Functions
[x \in S |-> expr] \* Function definition
f[x] \* Function application
DOMAIN f \* Domain of function
[f EXCEPT ![x] = newValue] \* Update function
State and Actions
Variables
VARIABLES x, y, z
vars == <<x, y, z>> \* Tuple of all variables
Primed Variables
x' \* Value of x in next state
x' = x + 1 \* x increases by 1
UNCHANGED
UNCHANGED x \* x' = x
UNCHANGED <<x, y>> \* x' = x /\ y' = y
Initial State
Init ==
/\ x = 0
/\ y = 0
/\ z = <<>>
Actions
Action ==
/\ x > 0 \* Precondition (enabling condition)
/\ x' = x - 1 \* Effect on x
/\ y' = y + 1 \* Effect on y
/\ UNCHANGED z \* z doesn't change
Next-State Relation
Next ==
\/ Action1
\/ Action2
\/ Action3
Specification
Spec == Init /\ [][Next]_vars
\* With fairness
Spec == Init /\ [][Next]_vars /\ WF_vars(Action1)
Temporal Operators
Always and Eventually
[]P \* Always P (P holds in all states)
<>P \* Eventually P (P holds in some future state)
Leads-to
P ~> Q \* P leads to Q (if P holds, eventually Q holds)
\* Equivalent to: [](P => <>Q)
Weak and Strong Fairness
WF_vars(Action) \* Weak fairness: if Action is continuously enabled, it eventually happens
SF_vars(Action) \* Strong fairness: if Action is infinitely often enabled, it eventually happens
Common Patterns
State Machine
VARIABLES state
States == {"Init", "Working", "Done"}
TypeOK == state \in States
Init == state = "Init"
StartWork ==
/\ state = "Init"
/\ state' = "Working"
FinishWork ==
/\ state = "Working"
/\ state' = "Done"
Next ==
\/ StartWork
\/ FinishWork
Spec == Init /\ [][Next]_state
Counter
VARIABLES count
TypeOK == count \in Nat
Init == count = 0
Increment ==
/\ count < 10
/\ count' = count + 1
Decrement ==
/\ count > 0
/\ count' = count - 1
Next ==
\/ Increment
\/ Decrement
Message Queue
VARIABLES queue
TypeOK == queue \in Seq(Messages)
Init == queue = <<>>
Send(msg) ==
/\ queue' = Append(queue, msg)
Receive ==
/\ queue /= <<>>
/\ queue' = Tail(queue)
Next ==
\/ \E msg \in Messages : Send(msg)
\/ Receive
Distributed System with Processes
CONSTANTS N \* Number of processes
VARIABLES state \* state[p] is state of process p
Procs == 1..N
TypeOK == state \in [Procs -> States]
Init == state = [p \in Procs |-> "Init"]
ProcessAction(p) ==
/\ state[p] = "Init"
/\ state' = [state EXCEPT ![p] = "Working"]
Next == \E p \in Procs : ProcessAction(p)
Invariants and Properties
Type Invariant
TypeOK ==
/\ x \in Nat
/\ y \in BOOLEAN
/\ z \in Seq(Messages)
Safety Property
Safety ==
/\ x <= 100
/\ y => (z /= <<>>)
Liveness Property
\* Eventually reach done state
THEOREM Spec => <>[]( state = "Done" )
\* Every request is eventually granted
THEOREM Spec => [](request => <>grant)
TLC Model Checker Directives
Symmetry
SYMMETRY Permutations(Procs)
State Constraints
StateConstraint == count <= 5
Action Constraints
ActionConstraint == count' <= count + 1
Tips
- Use meaningful names -
state,queue,countare clearer thanx,y,z - Factor out type invariants - Define
TypeOKseparately - Use UNCHANGED - More concise than listing unchanged variables
- Quantify carefully -
\Ecan cause state explosion - Start simple - Add complexity incrementally
- Check TypeOK first - Ensures basic correctness before checking properties