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 non-deterministic, so they require the oracle to resolve non-determinism, see Control Flow and Non-determinism. 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:
- FALSE and TRUE,
- A /\ B (also A \land B),
- A \/ B (also A \lor B),
- ~A (also \lnot A and \neg A),
- A => B,
- A <=> B (also A \equiv B)
Boolean set: BOOLEAN

Control flow and non-determinism 🔀

Hidden powers of TLA+. Learn more...

Non-determinism with A_1 \/ ... \/ A_n
Non-determinism with \E x \in S: P
Non-determinism with IF p THEN e_1 ELSE e_2
Non-determinism with CASE and CASE-OTHER

Deterministic conditionals 🚕

You need them less often than you think. Learn more...

Deterministic IF-THEN-ELSE
Deterministic CASE and CASE-OTHER

Integers 🔢

Unbounded integers like in Python. Learn more...

Integer algebra:
- -i, i + k, i - k,
- i * k, i \div k, i % k, i^k
Integer predicates:
- i < k, i > k,
- i <= k (also i =< k and i \leq k), i >= k (also i \geq k)
Integer sets: i..k, Int, Nat

Strings 🔡

String constants. You learned it!

String literals, e.g., "hello" and "TLA+ is awesome".
- In Apalache, the literals have the type Str.
Set of all finite strings: STRING.
- In Apalache, the set STRING has the type Set(Str).

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 and UNION S
Set algebra:
- Union: S \union T (also S \cup T),
- Intersection: S \intersect T (also S \cap T),
- Difference: S \ T
Set predicates:
- Membership: x \in S and x \notin S,
- Subsets: S \subseteq T,
- Finiteness: IsFinite
Cardinality of a finite set: Cardinality