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 the declarations, definitions, assumptions, and theorems from the modules named M1, ..., Mn into the current module. |
| constants C1, ..., Cn | Declares the Cj to be constant parameters (rigid variables). Each Cj is either an identifier or has the form C(-,...,-), the latter form indicating that C is an operator with the indicated number of arguments. |
| variables x1, ..., xn | Declares the xj to be variables (parameters that are flexible variables). |
| assume P | Asserts P as an assumption. |
| F(x1, ..., xn) == exp | Defines F to be the operator such that F(e1,...,en) equals exp with each identifier xk replaced by ek. (For n = 0, it is written F == 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.) |
| instance M with p1 <- e1, ..., pm <- em | 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 pj of M with ej. (If m = 0, the 'with' is omitted.) |
| N(x1, ..., xn) == instance M with p1 <- e1, ..., pm <- em | For each defined operator F of module M, this defines N(d1,...,dn)!F to be the operator whose definition is obtained from the definition of F by replacing each declared constant or variable pj of M with ej, and then replacing each identifier xk with dk. (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
| 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: e1 if p is true, else e2. |
| CASE p1 -> e1 [] ... [] pn -> en | Some ei such that pi is true. |
| CASE ... [] OTHER -> e | Some ei such that pi is true, or e if all pi are false. |
| LET d1 == e1 ... dn == en IN e | e in the context of the definitions. |
| / p1 ... pn | Conjunction p1 / ... / pn. |
| \\/ p1 ... pn | Disjunction p1 \\/ ... \\/ pn. |
Action Operators
| Operator | Description |
|---|---|
| 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 · B | Composition of actions. |
Temporal Operators
| Operator | Meaning |
|---|---|
| []F | F is always true. |
| <>F | F is eventually true. |
| WF_e(A) | Weak fairness for action A. |
| SF_e(A) | Strong fairness for action A. |
| 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