- Record field (period).
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 $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.)
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}
$$
(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}$.
$e | {\prime}$ | $[$ The value of $e$ in the final state of a step] |
---|---|---|
$[A]_{e}$ | $\left[A \vee\left(e | {\prime}=e\right)\right]$ |
$\langle A\rangle_{e}$ | $\left[A \wedge\left(e | {\prime} \neq e\right)\right]$ |
ENABLED $A$ | $[$ An step is possible $]$ | |
UNCHANGED $e$ | $\left[e | {\prime}=e\right]$ |
$A \cdot B$ | $[$ Composition of actions $]$ |
$$
\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}
$$
$+ | {(1)}$ | $-{ } | {(1)}$ | $*$ | $(1)$ | $/{ } | {(2)}$ | $\circ{ } | {(3)}$ | ++ |
---|---|---|---|---|---|---|---|---|---|---|
$\div | {(1)}$ | $\% | {(1)}$ | - | $(1,4)$ | $\ldots$ | ||||
$\oplus | {(5)}$ | $\ominus{ } | {(5)}$ | $\otimes$ | $\oslash$ | $\odot$ | – | |||
(1) $ | {(1)}$ | $>{ } | {(1)}$ | $\leq$ | ${ } | {(1)}$ | $\geq{ } | {(1)}$ | $\sqcap$ | $* *$ |
$\prec$ | $\succ$ | $\preceq$ | $\succeq$ | $\sqcup$ | $\sim-$ | |||||
$\ll$ | $\gg$ | $<:$ | $:> | {(6)}$ | $\&$ | $\& \&$ | ||||
$\sqsubset$ | $\sqsupset$ | $\sqsubseteq{ } | {(5)}$ | $\sqsupseteq$ | $\mid$ | $\% \%$ | ||||
$\subset$ | $\supset$ | $\supseteq$ | $\star$ | $@ @(6)$ | ||||||
$\vdash$ | $\dashv$ | $\models$ | $=$ | $\bullet$ | $\# \#$ | |||||
$\sim$ | $\simeq$ | $\approx$ | $\cong$ | $\$$ | $\$ \$$ | |||||
$\bigcirc$ | $::=$ | $\asymp$ | $\doteq$ | $? ?$ | $!!$ | |||||
$\propto$ | $\checkmark$ | $\uplus$ |
Postfix Operators (7)
$\sim \quad$ - $#$
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}
$$
Module Sequences
$\circ$ | Head | SelectSeq | SubSeq |
---|---|---|---|
Append | Len | Seq | Tail |
Module Bags
$\oplus$ | BagIn | CopiesIn | SubBag |
---|---|---|---|
$\ominus$ | BagOfAll | EmptyBag | |
$\sqsubseteq$ | BagToSet | IsABag | |
BagCardinality | BagUnion | SetToBag |
Module RealTime
RTBound RTnow now (declared to be a variable)
Module $T L C$
$:>$ Print Assert JavaTime Permutations SortSeq
$/$ or $\backslash]$ | land | V | $\backslash /$ or $\backslash$ lor | $\Rightarrow$ | ||||
---|---|---|---|---|---|---|---|---|
$\sim$ or $\backslash \operatorname{lr}$ | not or | $\equiv$ | $\Leftrightarrow$ or | $\triangleq$ | $==$ | |||
$\notin$ | $\neq$ | $\#$ or $/=$ | ||||||
$«$ | $>$ | $\square$ | [] | |||||
$<$ | $>$ | $>$ | $\diamond$ | $<>$ | ||||
or | $=<$ or $⇐$ | $\geq$ | or >= | $\sim$ | $\sim$ | |||
$\gg$ | $\backslash g g$ | $\xrightarrow{\square}$ | $-+→$ | |||||
$\succ$ | $\mapsto$ | $\ | -\rangle$ | |||||
$\succeq$ | $\div$ | |||||||
$\supseteq$ | . | |||||||
$\supset$ | 0 | or | ||||||
$\sqsupset$ | $\bullet$ | |||||||
eteq | $\sqsupseteq$ | $\star$ | ||||||
$1-$ | $\dashv$ | -1 | O | |||||
$\mid=$ | $=$ | $=1$ | $\sim$ | |||||
$\rightarrow$ | $\leftarrow$ | $←$ | $\simeq$ | |||||
or | $\cup$ | or | $\asymp$ | |||||
$\sqcup$ | $\approx$ | |||||||
$(+)$ or 1 | $\uplus$ | $\cong$ | ||||||
$(-)$ or 1 | $\times$ | $\backslash X$ or | $\doteq$ | |||||
(.) or 1 | 2 | $\backslash w r$ | $x | {y}$ | $x | {\wedge} y | {(2)}$ | |
$(\backslash X)$ or | $\propto$ | $x | {+}$ | $\mathrm{x} | {\wedge}+(2)$ | |||
(/) or 1 | “s” | “s” (1) | $x | {*}$ | $\mathrm{x} | {\wedge} *{ } | {(2)}$ | |
$\backslash E$ | $\forall$ | $\backslash \mathrm{A}$ | $x | {\#}$ | $x | {\wedge} \# | {(2)}$ | |
$\backslash \mathrm{EE}$ | $\forall$ | $\backslash \mathrm{AA}$ | $\prime$ | , | ||||
]_v | $_{v}$ | $»\_v$ | ||||||
$W F_{-} v$ | $\mathrm{SF}_{2}$ | SF_v |