You can access to a quick pdf summary about the tla+ language here: https://lamport.azurewebsites.net/tla/summary-standalone.pdf.

This is a web accessible version.

• Module-Level Constructs
• The Constant Operators
• Miscellaneous Constructs
• Action Operators
• Temporal Operators
• User-Definable Operator Symbols
• Precedence Ranges of Operators
• Operators Defined in Standard Modules.
• ASCII Representation of Typeset Symbols 1

MODULE $M$Begins the module or submodule named $M$.

EXTENDS $M_{1}, \ldots, M_{n}$

Incorporates the declarations, definitions, assumptions, and theorems from the modules named $M_{1}, \ldots, M_{n}$ into the current module.

CONSTANTS $C_{1}, \ldots, C_{n}^{(1)}$

Declares the $C_{j}$ to be constant parameters (rigid variables). Each $C_{j}$ is either an identifier or has the form $C\left(\_, \ldots, \_\right)$, the latter form indicating that $C$ is an operator with the indicated number of arguments.

$$ \text { VARIABLES } x_{1}, \ldots, x_{n}^{(1)} $$

Declares the $x_{j}$ to be variables (parameters that are flexible variables).

Asserts $P$ as an assumption.

$F\left(x_{1}, \ldots, x_{n}\right) \triangleq \exp$

Defines $F$ to be the operator such that $F\left(e_{1}, \ldots, e_{n}\right)$ equals exp with each identifier $x_{k}$ replaced by $e_{k}$. (For $n=0$, it is written $F \triangleq \exp$.)

$f[x \in S] \triangleq \exp ^{(2)}$

Defines $f$ to be the function with domain $S$ such that $f[x]=\exp$ for all $x$ in $S$. (The symbol $f$ may occur in exp, allowing a recursive definition.)

1. The terminal S in the keyword is optional.
2. $x \in S$ may be replaced by a comma-separated list of items $v \in S$, where $v$ is either a comma-separated list or a tuple of identifiers.

INSTANCE $M$ WITH $p_{1} \leftarrow e_{1}, \ldots, p_{m} \leftarrow e_{m}$

For each defined operator $F$ of module $M$, this defines $F$ to be the operator whose definition is obtained from the definition of $F$ in $M$ by replacing each declared constant or variable $p_{j}$ of $M$ with $e_{j}$. (If $m=0$, the WITH is omitted.) $N\left(x_{1}, \ldots, x_{n}\right) \triangleq$ INSTANCE $M$ WITH $p_{1} \leftarrow e_{1}, \ldots, p_{m} \leftarrow e_{m}$

For each defined operator $F$ of module $M$, this defines $N\left(d_{1}, \ldots, d_{n}\right)!F$ to be the operator whose definition is obtained from the definition of $F$ by replacing each declared constant or variable $p_{j}$ of $M$ with $e_{j}$, and then replacing each identifier $x_{k}$ with $d_{k}$. (If $m=0$, the WITH is omitted.)

THEOREM $P$

Asserts that $P$ can be proved from the definitions and assumptions of the current module.

LOCAL def

Makes the definition(s) of def (which may be a definition or an INSTANCE statement) local to the current module, thereby not obtained when extending or instantiating the module.

Ends the current module or submodule.

$=\neq \in \cup$.

$\left\{e_{1}, \ldots, e_{n}\right\} \quad$ [Set consisting of elements $\left.e_{i}\right]$

$\{x \in S: p\}$ (2) [Set of elements $x$ in $S$ satisfying $p$ ]

$\{e: x \in S\}^{(1)} \quad$ [Set of elements $e$ such that $x$ in $\left.S\right]$

SUBSET $S \quad$ [Set of subsets of $S$ ]

UNION $S \quad[$ Union of all elements of $S]$

$$ \begin{array}{ll} f[e] & {[\text { Function application] }} \\ \text { DOMAIN } f & {[\text { Domain of function } f]} \\ {[x \in S \mapsto e]{ }^{(1)}} & {[\text { Function } f \text { such that } f[x]=e \text { for } x \in S]} \\ {[S \rightarrow T]} & {[\text { Set of functions } f \text { with } f[x] \in T \text { for } x \in} \\ {\left[f \text { EXCEPT }!\left[e_{1}\right]=e_{2}\right]^{(3)}} & {\left[\text { Function } \widehat{f} \text { equal to } f \text { except } \widehat{f}\left[e_{1}\right]=e_{2}\right]} \end{array} $$

$\begin{array}{ll}e . h & \text { [The } h \text {-field of record } e] \\ {\left[h_{1} \mapsto e_{1}, \ldots, h_{n} \mapsto e_{n}\right]} & \left.\text { [The record whose } h_{i} \text { field is } e_{i}\right] \\ {\left[h_{1}: S_{1}, \ldots, h_{n}: S_{n}\right]} & \left.\text { [Set of all records with } h_{i} \text { field in } S_{i}\right] \\ {[r \text { EXCEPT }!. h=e]} & \text { [3) } \\ \text { [Record } \widehat{r} \text { equal to } r \text { except } \widehat{r} . h=e]\end{array}$

$$ \begin{array}{ll} e[i] & {\left[\text { The } i^{\text {th }} \text { component of tuple } e\right]} \\ \left\langle e_{1}, \ldots, e_{n}\right\rangle & {\left[\text { The } n \text {-tuple whose } i^{\text {th }} \text { component is } e_{i}\right]} \\ S_{1} \times \ldots \times S_{n} & \text { [The set of all } \left.n \text {-tuples with } i^{\text {th }} \text { component in } S_{i}\right] \end{array} $$

1. $x \in S$ may be replaced by a comma-separated list of items $v \in S$, where $v$ is either a comma-separated list or a tuple of identifiers
2. $x$ may be an identifier or tuple of identifiers.

(3)! $\left[e_{1}\right]$ or !.h may be replaced by a comma separated list of items $!a_{1} \cdots a_{n}$, where each $a_{i}$ is $\left[e_{i}\right]$ or.$h_{i}$.

$$ \begin{array}{ll} \square F & {[F \text { is always true }]} \\ \diamond F & {[F \text { is eventually true }]} \\ \mathrm{WF}_{e}(A) & {[\text { Weak fairness for action } A]} \\ \mathrm{SF}_{e}(A) & {[\text { Strong fairness for action } A]} \\ F \sim G & {[F \text { leads to } G]} \end{array} $$

Postfix Operators (7)

$\sim \quad$ - $＃$

1. Defined by the Naturals, Integers, and Reals modules.
2. Defined by the Reals module.
3. Defined by the Sequences module.
4. $x^{\wedge} y$ is printed as $x^{y}$.
5. Defined by the Bags module.
6. Defined by the $T L C$ module.
7. $e^{\wedge}+$ is printed as $e^{+}$, and similarly for ${ }^{\wedge} *$ and $\wedge \#$.

The relative precedence of two operators is unspecified if their ranges overlap. Left-associative operators are indicated by (a).

¹⁾

Modules Naturals, Integers, Reals

$$ \begin{aligned} & +\quad-{ }^{(1)} \quad * \quad /^{(2)} \quad \sim^{-(3)} \quad \text {.. } \quad \text { Nat } \quad \text { Real }^{(2)} \\ & \div \quad \% \quad \geq \quad>\quad \text { Int }^{(4)} \quad \text { Infinity }{ }^{(2} \end{aligned} $$

1. Only infix - is defined in Naturals.
2. Defined only in Reals module.
3. Exponentiation.
4. Not defined in Naturals module.

Module Sequences

Module Bags

Module RealTime

RTBound RTnow now (declared to be a variable)

Module $T L C$

$:>$ Print Assert JavaTime Permutations SortSeq

1. $s$ is a sequence of characters.
2. $x$ and $y$ are any expressions.
3. a sequence of four or more - or $=$ characters.