# TLA+ cheatsheet in Markdown

I realized that I needed $\tla{}$ syntax highlighting for my next blog post. Since highlightjs did not support $\tla{}$, I have introduced a syntax highlighlting file in tlaplus-highlightjs. The best way to test highlighting is by typing the TLA+ Summary by Leslie Lamport (originally, in pdf) on this page.

All the contents below is simply retyping of the TLA+ Summary in Markdown.
Hence, all the credit for the original content goes to Leslie Lamport, not to
me. I only added a few comments regarding typing $\tla{}$ in ASCII and adjusted
some typesetting to make it work in Markdown. These comments are shown in
*italic*, or in $\tla{}$ comments such as:

```
original text \* I: my single-line comment
(* or
in a multiline comment *)
```

In addition to that, since it is not easy to combine math and code highlighting, I am using the ASCII typesetting as well as the Unicode typesetting, as produced by tlauc. For the Unicode characters, no syntax highlighting is introduced: These characters are already distinct enough for my eye. Finally, Markdown is not nearly as good as LaTeX. I could not reproduce the last section of TLA+ Summary, which maps ASCII operators to their LaTeX presentation.

## Module-Level Constructs

```
---- MODULE M ----
```

Begins the module or submodule named $M$. *(At least four leading dashes ‘-‘
are required.)*

```
EXTENDS M_1, ..., 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, ..., C_n
CONSTANT C_1, ..., C_n
```

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 the $C$ is an operator with the indicated number of arguments.

```
VARIABLES x_1, ..., x_n
VARIABLE x_1, ..., x_n
```

Declares the $x_j$ to be variables (parameters that are flexible variables).

```
ASSUME P
```

Asserts $P$ as an assumption.

```
F(x_1, ..., x_n) == exp
F(x_1, ..., 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
f[x ∈ S] ≜ exp
```

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

**Note**: $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 <- e_1, ..., p_m <- e_m
INSTANCE M WITH p_1 ← e_1, …, p_m ← 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, ..., x_n) == INSTANCE M WITH p_1 <- e_1, ..., p_m <- e_m
N(x_1, ..., x_n) ≜ INSTANCE M WITH p_1 ← e_1, …, p_m ← 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. *(At least four equal signs = are
required.)*

## The Constant Operators

### Logic

```
p /\ q \* I: p and q
p ∧ q
p \/ q \* I: p or q
p ∨ q
~p \* I: not p
¬p
p => q \* I: p implies q
p ⇒ q
p <=> q \* I: p if and only if q
p ⇔ q
TRUE
FALSE
BOOLEAN \* the set { TRUE, FALSE }
\A x \in S: P \* I: forall x in S: P, see Note (1) below
∀ x ∈ S: P
\E x \in S: P \* I: exists x in S: P, see Note (1) below
∃ x ∈ S: P
CHOOSE x \in S: P \* An x in S satisfying P
```

**Note (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.

### Sets

```
S = T
S /= T
S ≠ T
x \in S
x ∈ S
x \notin S
x ∉ S
S \union T
S ∪ T
S \intersect T
S ∩ T
S \subseteq T
S ⊆ T
S \ T \* set difference
{ e_1, ..., e_n } \* Set consisting of elements e_i
{ x \in S: p } \* Set of elements x in S satisfying p, see Note (2) below
{ x ∈ S: p }
{ e: x \in S } \* Set of elements e such that x in S, see Note (1) above
{ e: x ∈ S }
SUBSET S \* Set of subsets of S
UNION S \* Union of all elements of S
```

**Note (2):** `x`

may be an identifier or a tuple of identifiers.

### Functions

```
f[e] \* Function application
DOMAIN f \* Domain of function f
[x \in S |-> e] \* Function f such that f[x] = e for x ∈ S, see Note (1) above
[x ∈ S ↦ e]
[S -> T] \* Set of functions f with f[x] ∈ T for x ∈ S
[S → T]
[f EXCEPT ![e_1] = e_2] \* Function g equal to f except g[e_1] = e_2, see Note (3) below
```

**Note (3):** `![e_1]`

or `!.h`

may be replaced by a comma-separated list of
items `!a_1...a_n`

, where each `a_i`

is `[e_i]`

or `.h_i`

.

### Records

```
e.h \* The h-field of record e
[h_1 |-> e_1, ..., h_n |-> e_n] \* The record whose h_i field is e_i
[h_1 ↦ e_1, ..., h_n ↦ e_n]
[h_1: S_1, ..., h_n: S_n] \* Set of all records with h_i field in S_i
[r EXCEPT !.h = e] \* Record s equal to r except s.h = e, see Note (3) above
```

### Tuples

```
e[i] \* The i-th component of tuple e
<<e_1, ..., e_n>> \* The n-tuple whose i-th component is e_i
⟨e_1, …, e_n⟩
S_1 \X ... \X S_n \* The set of all n-tuples with i-th component in S_i
S_1 × … × S_n
```

## Miscellaneous Constructs

```
IF p THEN e_1 ELSE e_2
\* e_1 if p is true else e_2
CASE p_1 -> e_1 [] ... [] p_n -> e_n
CASE p_1 → e_1 □ … □ p_n → e_n
\* Some e_i such that p_i is true
CASE p_1 -> e_1 [] … [] p_n -> e_n [] OTHER -> e
CASE p_1 → e_1 □ … □ p_n → e_n □ OTHER → e
\* Some e_i such that p_i is true, or e if all p_i are false
LET d_1 == e_1 ... d_n == e_n IN e
LET d_1 ≜ e_1 ... d_n ≜ e_n IN e
\* e in the context of the definitions d_1, ..., d_n
/\ p_1 \* the conjunction p_1 ∧ ... ∧ p_n
...
/\ p_n
\/ p_1 \* the disjunction p_1 ∨ ... ∨ p_n
...
\/ p_n
\* the same in Unicode
∧ p_1
...
∧ p_n
∨ p_1
...
∨ p_1
```

## Action Operators

```
e' \* The value of e in the final state of a step
[A]_e \* A ∨ (e' = e)
<A>_e \* A ∧ (e' ≠ e)
ENABLED A \* An A step is possible
UNCHANGED e \* e' = e
A \cdot B \* Composition of actions
```

## Temporal operators

```
[]F \* F is always true
□F
<>F \* F is eventually true
◇F
WF_e(A) \* Weak fairness for action A
SF_e(A) \* Strong fairness for action A
F ~> G \* F leads to G
F ↝ G
```

## User-Definable Operator Symbols

*We are using the ASCII notation. To see a nice typesetting of these operators,
check the PDF version in the TLA+ Summary*.

### Infix Operators

```
+ - * / \o ++
\div % ^ .. ... --
(+) (-) (\X) (/) (.) **
< > <= >= \sqcap //
\prec \succ \preceq \succeq \sqcup ^^
\ll \gg <: :> & &&
| %%
\sqsubset \sqsupset \sqsubseteq \sqsupseteq
\subset \supset \supseteq
\star @@
|- -| |= =| \bullet ##
~ \simeq \approx \cong $ $$
\bigcirc ::= \asymp \doteq ?? !!
\propto \wr \uplus
```

*Some of these operators are defined in the standard modules:*

`Naturals`

,`Integers`

,`Reals`

define:`+`

,`-`

,`*`

,`\div`

,`%`

,`^`

,`..`

,`<`

,`>`

,`<=`

,`>=`

`Reals`

defines:`/`

`Sequences`

defines:`\o`

`Bags`

defines:`(+)`

,`(-)`

,`\sqsubseteq`

`TLC`

defines:`:>`

,`@@`

### Postfix Operators

```
^+ ^* ^#
```

## Operators Defined in Standard Modules

**Module** $Naturals$

```
+ - * ^ .. Nat
\div % <= => < >
```

Note that $Naturals$ defines only infix `-`

.

**Module** $Integers$

```
+ - * ^ .. Nat
\div % <= => < > Int
```

**Module** $Reals$

```
+ - * / ^ .. Nat Real
\div % <= => < > Int Infinity
```

**Module** $Sequences$

```
\o Head SelectSeq SubSeq
Append Len Seq Tail
```

**Module** $FiniteSets$

```
IsFiniteSet Cardinality
```

**Module** $Bags$

```
(+) BagIn CopiesIn SubBag
(-) BagOfAll EmptyBag
\sqsubseteq BagToSet IsABag
BagCardinality BagUnion SetToBag
```

**Module** $RealTime$

```
RTBound RTNow \* declared to be a variable
```

**Module TLC**

```
:> @@ Print Assert JavaTime Permutations
SortSeq
```

## Precedence Ranges of Operators

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

**Prefix Operators**

```
~ 4-4 [] 4-15 UNION 8-8
ENABLED 4-15 <> 4-15 DOMAIN 9-9
UNCHANGED 4-15 SUBSET 8-8 - 12-12
```

**Infix Operators**

```
=> 1-1 <= 5-5 <: 7-7 (-) 11-11 (L)
-+-> 2-2 \ll 5-5 \ 8-8 - 11-11 (L)
<=> 2-2 \prec 5-5 \union 8-8 (L) -- 11-11 (L)
~> 2-2 \preceq 5-5 \intersect 8-8 (L) & 13-13 (L)
/\ 3-3 (L) \propto 5-5 .. 9-9 && 13-13 (L)
\/ 3-3 (L) \sim 5-5 ... 9-9 (.) 13-13 (L)
/= 5-5 \simeq 5-5 !! 9-13 (/) 13-13
-| 5-5 \sqsubset 5-5 ## 9-13 (L) (\X) 13-13 (L)
::= 5-5 \sqsubseteq 5-5 $ 9-13 (L) * 13-13 (L)
:= 5-5 \sqsupset 5-5 $$ 9-13 (L) ** 13-13 (L)
< 5-5 \sqsupseteq 5-5 ?? 9-13 (L) / 13-13
= 5-5 \subset 5-5 \sqcap 9-13 (L) // 13-13
=| 5-5 \subseteq 5-5 \sqcup 9-13 (L) \bigcirc 13-13 (L)
> 5-5 \succ 5-5 \uplus 9-13 (L) \bullet 13-13 (L)
\approx 5-5 \succeq 5-5 \wr 9-14 \div 13-13
\asymp 5-5 \supset 5-5 (+) 10-10 (L) \o 13-13 (L)
\cong 5-5 \supseteq 5-5 + 10-10 (L) \star 13-13 (L)
\doteq 5-5 |- 5-5 ++ 10-10 (L) ^ 14-14
>= 5-5 |= 5-5 % 10-11 ^^ 14-14
\gg 5-5 \cdot 5-14 (L) %% 10-11 (L) . 17-17 (L)
\in 5-5 @@ 6-6 (L) | 10-11 (L)
\notin 5-5 :> 7-7 || 10-11 (L)
```

**Postfix Operators**

```
^+ 15-15 ^* 15-15 ^# 15-15 ' 15-15
```

## ASCII Representation of Typeset Symbols

*Please check the TLA+ Summary. This is too much for Markdown.*