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

Control flow and non-determinism πŸ”€

Hidden powers of TLA+. Learn more...

Deterministic conditionals πŸš•

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

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.
  • 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...

Logic πŸ™

How logicians write loops. Learn more...

Functions πŸ’Ή

Like frozen dictionaries in Python, but cooler. Learn more...

Records πŸ“š

Records like everywhere else. Learn more...

Tuples πŸ“

Well, tuples, indexed with 1, 2, 3... Learn more...

Sequences 🐍

Functions that pretend to be lists, indexed with 1, 2, 3,...

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