Show pageOld revisionsBacklinksBack to top 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 | ---- learning/tla_summary.txt Last modified: 2025/08/20 10:20by fponzi