The standard operators of TLA+
In this document, we summarize the standard TLA+ operators in a form that is similar to manuals on programming languages. The purpose of this document is to provide you with a quick reference, whenever you are looking at the Summary of TLA. The TLA+ Video Course by Leslie Lamport is an excellent starting point, if you are new to TLA+. For a comprehensive description and philosophy of the language, check Specifying Systems and the TLA+ Home Page. You can find handy extensions of the standard library in Community Modules.
We explain the semantics of the operators under the lenses of the Apalache model checker. Traditionally, the emphasis was put on the temporal operators and action operators, as they build the foundation of TLA. We focus on the "+" aspect of the language, which provides you with a language for writing a single step by a state machine. This part of the language is absolutely necessary for writing and reading system specifications. Moreover, we treat equally the "core" operators of TLA+ and the "library" operators: This distinction is less important to the language users than to the tool developers.
In this document, we present the semantics of TLA+, as if it was executed on a computer that is equipped with an additional device that we call an oracle. Most of the TLA+ operators are understood as deterministic operators, so they can be executed on your computer. A few operators are nondeterministic, so they require the oracle to resolve nondeterminism, see Control Flow and Nondeterminism. This is one of the most important features that makes TLA+ distinct from programming languages. Wherever possible, we complement the English semantics with code in Python. Although our semantics are more restrictive than the denotational semantics in Chapter 16 of Specifying Systems, they are very close to the treatment of TLA+ by the model checkers: Apalache and TLC. Our relation between TLA+ operators and Python code bears some resemblance to SALT and PlusPy.
Here, we are using the ASCII notation of TLA+, as this is what you type. We give the nice LaTeX notation in the detailed description. The translation table between the LaTeX notation and ASCII can be found in Summary of TLA.
The "+" Operators in TLA+
Booleans π₯
Good old Booleans. Learn more...
 Boolean algebra:
 Boolean set:
BOOLEAN
Control flow and nondeterminism π
Hidden powers of TLA+. Learn more...
 Nondeterminism with
A_1 \/ ... \/ A_n
 Nondeterminism with
\E x \in S: P
 Nondeterminism with
IF p THEN e_1 ELSE e_2
 Nondeterminism with
CASE
andCASEOTHER
Deterministic conditionals π
You need them less often than you think. Learn more...
 Deterministic
IFTHENELSE
 Deterministic
CASE
andCASEOTHER
Integers π’
Unbounded integers like in Python. Learn more...
Strings π‘
String constants. You learned it!
 String literals, e.g.,
"hello"
and"TLA+ is awesome"
. In Apalache, the literals have the type
Str
.
 In Apalache, the literals have the type
 Set of all finite strings:
STRING
. In Apalache, the set
STRING
has the typeSet(Str)
.
 In Apalache, the set
Sets π£
Like frozen sets in Python, but cooler Learn more...
 Set constructors:
 Enumeration:
{ e_1, ..., e_n }
 Filter:
{ x \in S: p }
 Map:
{ e: x \in S }
 Powers:
SUBSET S
andUNION S
 Enumeration:
 Set algebra:
 Union:
S \union T
(alsoS \cup T
),  Intersection:
S \intersect T
(alsoS \cap T
),  Difference:
S \ T
 Union:
 Set predicates:
 Membership:
x \in S
andx \notin S
,  Subsets:
S \subseteq T
,  Finiteness:
IsFinite
 Membership:
 Cardinality of a finite set:
Cardinality
Logic π
How logicians write loops. Learn more...
 Equality:
=
and/=
(also#
)  Bounded quantifiers:
\A x \in S: p
and\E x \in S: p
 Unbounded quantifiers:
\A x: p
and\E x: p
 Choice:
CHOOSE x \in S: p
andCHOOSE x: p
Functions πΉ
Like frozen dictionaries in Python, but cooler. Learn more...
 Function constructor:
[ x \in S > e ]
 Set of functions:
[S > T]
 Function application:
f[e]
 Function replacement:
[ f EXCEPT ![e_1] = e_2 ]
 Function domain:
DOMAIN f
Records π
Records like everywhere else. Learn more...
 Record constructor:
[ h_1 > e_1, ..., h_n > e_n ]
 Set of records:
[ h_1: S_1, ..., h_n: S_n ]
 Access by field name:
e.h
 Records are functions. All operators of functions are supported.
Tuples π
Well, tuples, indexed with 1, 2, 3... Learn more...
 Tuple constructor:
<< e_1, ..., e_n >>
 Cartesian product:
S_1 \X ... \X S_n
(alsoS_1 \times ... \times S_n
)  Tuples are functions. All operators of functions are supported.
Sequences π
Functions that pretend to be lists, indexed with 1, 2, 3,...
 Add to end:
Append(s, e)
 First and rest:
Head(s)
andTail(s)
 Length:
Len(s)
 Concatenation:
s \o t
(alsos \circ t
)  Subsequence:
SubSeq(s, i, k)
 Sequence filter:
SelectSeq(s, Test)
 Set of finite sequences over
S
:Seq(S)
 Sequences are functions. All operators of functions and tuples are supported.
Bags π
 TBD
Reals π
Like "reals" in your math classes, not floating point

All operators of
Integers
but interpreted over reals 
a / b
,Real
,Infinity
Naturals πΎ
If you are Indiana Jones...
 All operators of
Integers
except: unary minusa
andInt
The "A" Operators in TLA+
Action operators π
Taking a step
 Prime:
e'
 Preservation:
UNCHANGED e
 Stuttering:
[A]_e
and<A>_e
 Action enablement:
ENABLED A
 Sequential composition:
A \cdot B
The "TL" Operators in TLA+
Temporal operators π
Talking about computations, finite and infinite
 Always:
[]F
 Eventually:
<>F
 Weak fairness:
WF_e(A)
 Strong fairness:
SF_e(A)
 Leadsto:
F ~> G
 Guarantee:
F +> G
 Temporal hiding:
\EE x: F
 Temporal universal quantification:
\AA x: F