Differences

This shows you the differences between two versions of the page.

--- learning:tla_summary [2025/08/20 10:04] – fponzi
+++ learning:tla_summary [2025/08/20 10:20] (current) – fponzi
@@ Line 7: / Line 7: @@
 ----
-====== Summary of TLA+ ======
+====== Module-Level Constructs ======
-===== 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. |
-  * ''module M'' :: Begins the module or submodule named ''M''.
+----
-  * ''extends M1, ..., Mn'' :: Incorporates declarations, definitions, assumptions, and theorems from modules ''M1, ..., Mn''.
-  * ''constants C1, ..., Cn'' :: Declares constant parameters (rigid variables).
-  * ''variables x1, ..., xn'' :: Declares flexible variables.
-  * ''assume P'' :: Asserts ''P'' as an assumption.
-  * ''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 p1 <- e1, ..., pm <- em'' :: Parameterized instantiation.
-  * ''theorem P'' :: Asserts that ''P'' can be proved.
-  * ''local def'' :: Makes definitions local.
-  * ''===='' :: Ends the current module or submodule.
-\===== The Constant Operators =====
+====== The Constant Operators ======
-**Logic**
+^ 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 |
-* ''/'', ''/'', ''\~'', ''=>'', ''<=>'', ''TRUE'', ''FALSE'', ''BOOLEAN''
+----
-* ''\A x ∈ S : p''
-* ''\E x ∈ S : p''
-* ''CHOOSE x ∈ S : p''
-**Sets**
+====== Miscellaneous Constructs ======
-* ''='', ''#'', ''∈'', ''/∈'', ''\cup'', ''\cap'', ''⊆'', ''''
+^ Construct ^ Description ^
-* ''{e1, ..., en}'', ''{x ∈ S : p}'', ''{e : x ∈ S}'', ''SUBSET S'', ''UNION S''
+| **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. |
-**Functions**
+----
-* ''f\[e]'', ''DOMAIN f'', ''\[x ∈ S |-> e]'', ''\[S -> T]'', ''\[f EXCEPT !\[e1] = e2]''
+====== Action Operators ======
-**Records**
+^ 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. |
-* ''e.h'', ''\[h1 |-> e1, ..., hn |-> en]'', ''\[h1: S1, ..., hn: Sn]'', ''\[r EXCEPT !.h = e]''
+----
-**Tuples**
+====== Temporal Operators ======
-* ''e\[i]'', ''<\<e1, ..., en>>'', ''S1 \X ... \X Sn''
+^ 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. |
-\===== Miscellaneous Constructs =====
+----
-* ''IF p THEN e1 ELSE e2''
+====== Standard Modules ======
-* ''CASE p1 -> e1 \[] ... \[] pn -> en''
-* ''CASE ... \[] OTHER -> e''
-* ''LET d1 == e1 ... dn == en IN e''
-* Conjunctions: ''/\ p1 ... /\ pn''
-* Disjunctions: ''/ p1 ... / pn''
-\===== Action Operators =====
+^ 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 |
-* ''e' '' :: Value of ''e'' in next state
+----
-* ''\[A]\_e'' :: ''A / (e' = e)''
-* ''<A>\_e'' :: ''A /\ (e' # e)''
-* ''ENABLED A'' :: Step ''A'' is possible
-* ''UNCHANGED e'' :: ''e' = e''
-* ''A \cdot B'' :: Composition of actions
-\===== Temporal Operators =====
+====== ASCII Equivalents ======
-* ''\[]F'' :: Always ''F''
+^ Symbol ^ ASCII ^
-* ''<>F'' :: Eventually ''F''
+| ∧ | /\\ or \\land |
-* ''WF\_e(A)'', ''SF\_e(A)'' :: Weak/Strong fairness
+| ∨ | \\/ or \\lor |
-* ''F \~> G'' :: ''F'' leads to ''G''
+| ¬ | ~ or \\lnot |
+| = | = |
+| ≠ | # or /= |
+| ∈ | \\in |
+| /∈ | \\notin |
+| ⊆ | \\subseteq |
+| ⊂ | \\subset |
+| ⊇ | \\supseteq |
+| ⊃ | \\supset |
+| -> | -> |
+| <- | <- |
+| [] | [] |
+| <> | <> |
+| |-> | |-> |
+| × | \\X or × |
+| · | \\cdot |
+| ○ | \\circ |
+| • | \\bullet |
-\===== User-Definable Operator Symbols =====
+----
-Common infix operators: ''+'', ''-'', ''\*'', ''/'', ''^'', ''..'', ''/'', ''/'', ''<='', ''>='', ''<'' , ''>'', ''#'', ''=|='', ''|='', ''⊆'', ''⊂'', ''@@'', '':>'', ''%''.
-Postfix operators: ''^+'', ''^\*'', ''^#''
-\===== Precedence Ranges of Operators =====
-Operators have precedence ranges; overlapping ranges mean precedence unspecified. Examples:
-* Prefix: ''\~'' (4–4), ''ENABLED'' (4–15), ''UNCHANGED'' (4–15), ''\[]'' (4–15), ''<>'' (4–15)
-* Infix: ''=>'' (1–1), ''/'' (3–3), ''/'' (3–3), ''='' (5–5), ''#'' (5–5), ''<'' (5–5), ''>'' (5–5), ''\cup'' (8–8), ''\cap'' (8–8)
-* Postfix: ''^+'', ''^\*'', ''^#'', ''' (15–15)
-\===== Operators Defined in Standard Modules =====
-**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 Representation of Typeset Symbols =====
-* ''/'' or ''\land''
-* ''/'' or ''\lor''
-* ''\~'' or ''\lnot''
-* ''#'' or ''/='' :: not equal
-* ''∈'' :: ''\in''
-* ''/∈'' :: ''\notin''
-* ''<<'' :: ''\langle''
-* ''>>'' :: ''\rangle''
-* ''<='', ''>='' :: ''<= or =<'', ''>= or =>''
-* ''⊆'' :: ''\subseteq'', ''⊂'' :: ''\subset''
-* ''⊇'' :: ''\supseteq'', ''⊃'' :: ''\supset''
-* ''->'' :: implication arrow
-* ''<-'' :: reverse arrow
-* ''\[]'' :: always
-* ''<>'' :: eventually
-* ''|->'' :: maps-to
-* ''\div'', ''\cdot'', ''\circ'', ''\bullet''
-* ''x^y'', ''x^\*'', ''x^+'', ''x^#''
----
-This is the TLA+ Summary rewritten in DokuWiki-friendly notation.