This is an old revision of the document!
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.
Module-Level Constructs
| Construct | Description |
|---|---|
| module M | Begins the module or submodule named M. |
| extends M1, ..., Mn | Incorporates declarations, definitions, assumptions, and theorems from modules M1, ..., Mn into the current module. |
| constants C1, ..., Cn | Declares constants (rigid variables). Each Cj may be an identifier or an operator with arguments. |
| variables x1, ..., xn | Declares flexible variables. |
| assume P | States assumption P. |
| F(x1, ..., xn) == exp | Defines operator F. |
| f[x ∈ S] == exp | Defines function f with domain S. |
| instance M with p1 <- e1, ..., pm <- em | Instantiates module M with substitutions. |
| N(x1, ..., xn) == instance M with ... | Parameterized instantiation of M. |
| theorem P | Asserts that P can be proved. |
| local def | Makes definitions local. |
| ==== | Ends the current module or submodule. |
The Constant Operators
| Category | Operators | |
|---|---|---|
| Logic | / , \\/ , ~ , => , <=> , TRUE, FALSE, BOOLEAN, ∀, ∃, CHOOSE | |
| Sets | = , # , ∈ , /∈ , ∪ , ∩ , ⊆ , , {..}, SUBSET, UNION | |
| Functions | f[e], DOMAIN f, [x ∈ S | -> e], [S -> T], [f EXCEPT ![e1] = e2] |
| Records | e.h, [h1 | -> e1, ...], [h1: S1, ...], [r EXCEPT !.h = e] |
| Tuples | e[i], <<e1,...,en>>, S1 × ... × Sn |
Miscellaneous Constructs
| Construct | Description |
|---|---|
| IF p THEN e1 ELSE e2 | Conditional expression. |
| CASE p1 -> e1 [] ... [] pn -> en | Pattern-based conditional. |
| CASE ... [] OTHER -> e | Default case. |
| LET ... IN e | Local definitions. |
| / p1 ... pn | Conjunction. |
| \\/ p1 ... pn | Disjunction. |
Action Operators
| Operator | Description |
|---|---|
| e' | Value of e in next state. |
| [A]_e | A or (e' = e). |
| <A>_e | A and (e' ≠ e). |
| ENABLED A | Action A is possible. |
| UNCHANGED e | e' = e. |
| A · B | Composition of actions. |
Temporal Operators
| Operator | Meaning |
|---|---|
| []F | Always F. |
| <>F | Eventually F. |
| WF_e(A) | Weak fairness. |
| SF_e(A) | Strong fairness. |
| F ~> G | F leads to G. |
Standard Modules
| Module | Operators | |
|---|---|---|
| Naturals, Integers, Reals | + , - , * , / , | , .. , div , % , ≤ , ≥ , < , > , Infinity |
| Sequences | o , Head , Tail , Append , Len , Seq , SelectSeq , SubSeq | |
| FiniteSets | IsFiniteSet , Cardinality | |
| Bags | ⊕ , BagIn , CopiesIn , SubBag , BagOfAll , EmptyBag , BagToSet , IsABag , BagCardinality , BagUnion , SetToBag | |
| RealTime | RTBound , RTnow , now | |
| TLC | :> , @@ , Print , Assert , JavaTime , Permutations , SortSeq |
ASCII Equivalents
| Symbol | ASCII | ||
|---|---|---|---|
| ∧ | / or \\land | ||
| ∨ | \\/ or \\lor | ||
| ¬ | ~ or \\lnot | ||
| = | = | ||
| ≠ | # or /= | ||
| ∈ | \\in | ||
| /∈ | \\notin | ||
| ⊆ | \\subseteq | ||
| ⊂ | \\subset | ||
| ⊇ | \\supseteq | ||
| ⊃ | \\supset | ||
| -> | -> | ||
| <- | <- | ||
| [] | [] | ||
| <> | <> | ||
| -> | -> | ||
| × | \\X or × | ||
| · | \\cdot | ||
| ○ | \\circ | ||
| • | \\bullet |
fponzi