# 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+

### 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).

### Tuples 📐

• Tuple constructor: << e_1, ..., e_n >>
• Cartesian product: S_1 \X ... \X S_n (also S_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,...

• 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 minus -a and Int

## 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)
• Leads-to: F ~> G
• Guarantee: F -+-> G
• Temporal hiding: \EE x: F
• Temporal universal quantification: \AA x: F