Summary

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.

Summary of TLA $^{+}$

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}, \dots, M_{n}$

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

CONSTANTS $C_{1}, \dots, 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 (, \dots,)$ , 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).

ASSUME $P$

Asserts $P$ as an assumption.

$F (x_{1}, \dots, x_{n}) ≜ exp$

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

$f [x \in S] ≜ 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}, \dots, 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 (x_{1}, \dots, x_{n}) ≜$ INSTANCE $M$ WITH $p_{1} \leftarrow e_{1}, \dots, p_{m} \leftarrow e_{m}$

For each defined operator $F$ of module $M$ , this defines $N (d_{1}, \dots, d_{n})! 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.

The Constant Operators

Sets

$= \neq = \in \cup$ .

${e_{1}, \dots, e_{n}}$ [Set consisting of elements $e_{i}]$

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

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

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

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

Functions

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

Records

$e . h [h_{1} \mapsto e_{1}, \dots, h_{n} \mapsto e_{n}] [h_{1} : S_{1}, \dots, h_{n} : S_{n}] [r EXCEPT! . h = e] [Record r equal to r except r . h = e] [The h -field of record e] [The record whose h_{i} field is e_{i}] [Set of all records with h_{i} field in S_{i}] [3)$

Tuples

\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)! $[e_{1}]$ or !.h may be replaced by a comma separated list of items $! a_{1} \dots a_{n}$ , where each $a_{i}$ is $[e_{i}]$ or. $h_{i}$ .

Miscellaneous Constructs

Action Operators

$e^{'}$	$[$ The value of $e$ in the final state of a step]
$[A]_{e}$	$[A \lor (e^{'} = e)]$
$⟨ A ⟩_{e}$	$[A \land (e^{'} \neq = e)]$
ENABLED $A$	$[$ An step is possible $]$
UNCHANGED $e$	$[e^{'} = e]$
$A \cdot B$	$[$ Composition of actions $]$

Temporal Operators

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

User-Definable Operator Symbols

Infix Operators

$+^{(1)}$	$-^{(1)}$	$*$	$(1)$	$/^{(2)}$	$\circ^{(3)}$	++
$\div^{(1)}$	$%^{(1)}$	-	$(1, 4)$	$\dots$
$\oplus^{(5)}$	$⊖^{(5)}$	$\otimes$	$⊘$	$⊙$	--
(1) $^{(1)}$	$>^{(1)}$	$\leq$	$^{(1)}$	$\geq^{(1)}$	$⊓$	$* *$
$≺$	$≻$	$⪯$	$⪰$	$⊔$	$\sim -$
$≪$	$≫$	$<:$	$: >^{(6)}$	$&$	$&&$
$⊏$	$⊐$	$⊑^{(5)}$	$⊒$	$∣$	$%%$
$\subset$	$\supset$		$\supseteq$	$⋆$	$@@ (6)$
$⊢$	$⊣$	$⊨$	$=$	$∙$	$##$
$\sim$	$≃$	$\approx$	$≅$	$$$	$$$$
$◯$	$::=$	$≍$	$≐$	$??$	$!!$
$\propto$	$✓$	$⊎$

Postfix Operators (7)

$\sim$ - $＃$

(1) Defined by the Naturals, Integers, and Reals modules.

(2) Defined by the Reals module.

(3) Defined by the Sequences module.

(4) $x^{\land} y$ is printed as $x^{y}$ .

(5) Defined by the Bags module.

(6) Defined by the $T L C$ module.

(7) $e^{\land} +$ is printed as $e^{+}$ , and similarly for $^{\land} *$ and $\land #$ .

Precedence Ranges of Operators

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

Operators Defined in Standard Modules.

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

$\circ$	Head	SelectSeq	SubSeq
Append	Len	Seq	Tail

Module FiniteSets
IsFiniteSet Cardinality

Module Bags

$\oplus$	BagIn	CopiesIn
$⊖$	BagOfAll	EmptyBag
$⊑$	BagToSet	IsABag
BagCardinality	BagUnion	SetToBag

Module RealTime

RTBound RTnow now (declared to be a variable)

Module $T L C$

$:>$ Print Assert JavaTime Permutations SortSeq

ASCII Representation of Typeset Symbols

$/$ or $</span>]$	land	V	$/$ or $</span> lor$	$\Rightarrow$
$\sim$ or $</span> lr$	not or \neg	$\equiv$	$\Leftrightarrow$ or \equiv	$≜$	$==$
\in		$\in /$	\notin	$\neq =$	$#$ or $/ =$
$<<$		\rangle	$>$	$□$	[]
$<$		$>$	$>$	$⋄$	$<>$
\leq or	$=<$ or $<=$	$\geq$	\geq or >=	$\sim$	$\sim$
\ll		$≫$	$</span> gg$	$□$	$- + - >$
\prec		$≻$	\succ	$\mapsto$	$∥ - ⟩$
\preceq		$⪰$	\succeq	$\div$	\div
\subsete		$\supseteq$	\supseteq	.	\cdot
\subset		$\supset$	\supset	0	\o or \circ
\sqsubse		$⊐$	\sqsupset	$∙$	\bullet
\sqsubse	eteq	$⊒$	\sqsupseteq	$⋆$	\star
$1 -$		$⊣$	-1	O	\bigcirc
$∣=$		$=$	$= 1$	$\sim$	\sim
$\to$		$\leftarrow$	$< -$	$≃$	\simeq
\cap or	\intersect	$\cup$	\cup or \union	$≍$	\asymp
\sqcap		$⊔$	\sqcup	$\approx$	\approx
$(+)$ or 1	\oplus	$⊎$	\uplus	$≅$	\cong
$(-)$ or 1	\ominus	$\times$	$or \times$	$≐$	\doteq
(.) or 1	\odot	2	$</span> w r$	$x^{y}$	$x^{\land} y^{(2)}$
$(</span> X) or$	\otimes	$\propto$	\propto	$x^{+}$	$x^{\land} + (2)$
(/) or 1	\oslash	"s"	"s" (1)	$x^{*}$	$x^{\land} *^{(2)}$
$</span> E$		$\forall$	$</span> A$	$x^{#}$	$x^{\land} #^{(2)}$
$</span> EE$		$\forall$	$</span> AA$	$'$	,
]_v		\rangle $_{v}$	$>>_v$
$W F_{-} v$		$SF_{2}$	SF_v

(1) $s$ is a sequence of characters.

(2) $x$ and $y$ are any expressions.

(3) a sequence of four or more - or $=$ characters.

(1) Action composition (\cdot).

(2) Record field (period).

TLA+ Wiki