learning:tla_summary

This page is read only. You can view the source, but not change it. Ask your administrator if you think this is wrong.
====== 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 |

----