learning:tla_summary

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
Next revision		 Previous revision
learning:tla_summary [2024/10/07 16:51] – fponzilearning: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.+====== The Constant Operators ======
  
-**extends M1, ..., Mn**+^ 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 |
  
-Incorporates the declarations, definitions, assumptions, and theorems from the modules named M1, ..., Mn into the current module.+----
  
-**constants C1, ..., Cn**+====== Miscellaneous Constructs ======
  
-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.+^ 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. |
  
-**variables x1, ..., xn**+----
  
-Declares the xj to be variables (parameters that are flexible variables).+====== Action Operators ======
  
-**assume P**+^ 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. |
  
-Asserts P as an assumption.+----
  
-**F(x1, ..., xn) Δ = exp**+====== Temporal Operators ======
  
-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.)+^ 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. |
  
-**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.)+====== Standard Modules ======
  
-**instance M with p1 ← e1, ..., pm ← em**+^ 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 |
  
-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.)+----
  
-**theorem P**+====== ASCII Equivalents ======
  
-Asserts that P can be proved from the definitions and assumptions of the current module.+^ Symbol ^ ASCII ^ 
 +| ∧ | /\\ or \\land | 
 +| ∨ | \\/ or \\lor | 
 +| ¬ | ~ or \\lnot | 
 +| = | = | 
 +| ≠ | # or /= | 
 +| ∈ | \\in | 
 +| /∈ | \\notin | 
 +| ⊆ | \\subseteq | 
 +| ⊂ | \\subset | 
 +| ⊇ | \\supseteq | 
 +| ⊃ | \\supset | 
 +| -> | -> | 
 +| <- | <- | 
 +| [] | [] | 
 +| <> | <> | 
 +| |-> | |-> | 
 +| × | \\X or × | 
 +| · | \\cdot | 
 +| ○ | \\circ | 
 +| • | \\bullet |
  
-**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. +
- +
-===== The Constant Operators ===== +
- +
-=== Logic === +
-<m> ∧ ∨ ¬ ⇒ ≡ \text{true} \text{false} \text{boolean} \</m> +
- +
-<m>∀ x ∈ S : p</m> +
- +
-<m>∃ x ∈ S : p</m> +
- +
-<m>\text{choose } x ∈ S : p</m> +
- +
-=== Sets === +
-<m>= \neq ∈ \notin ∪ ∩ ⊆ \setminus </m> +
- +
-<m>\{e1, ..., en\} [\text{Set consisting of elements } e_i]</m> +
- +
-<m>\{x ∈ S : p\} [\text{Set of elements } x \text{ in } S \text{ satisfying } p]</m> +
- +
-<m>\subset S [\text{Set of subsets of } S]</m> +
- +
-<m>\text{union} S [\text{Union of all elements of } S]</m> +
- +
-=== Functions === +
-<m>f[e] [\text{Function application}]</m> +
- +
-<m>\text{domain} f [\text{Domain of function } f]</m> +
- +
-<m>[x ∈ S \mapsto e] [\text{Function } f \text{ such that } f[x] = e \text{ for } x ∈ S]</m> +
- +
-<m>[S \to T] [\text{Set of functions } f \text{ with } f[x] \in T \text{ for } x \in S]</m> +
- +
-=== Records === +
-<m>e.h [\text{The h-field of record } e]</m> +
- +
-<m>[h1 \mapsto e1, ..., hn \mapsto en] [\text{The record whose } h_i \text{ field is } e_i]</m> +
- +
-=== Tuples === +
-<m>e[i] [\text{The i-th component of tuple } e]</m> +
- +
-<m>\langle e1, ..., en \rangle [\text{The n-tuple whose i-th component is } e_i]</m> +
- +
-<m>S1 \times ... \times Sn [\text{The set of all n-tuples with i-th component in } S_i]</m> +
- +
-===== Miscellaneous Constructs ===== +
- +
-**if p then e1 else e2** [e1 if p is true, else e2] +
- +
-**case p1 → e1 ... pn → en** +
- +
-**case p1 → e1 ... pn → en 2 other → e** +
- +
-**let d1 Δ = e1 ... dn Δ = en in e** +
- +
-===== Action Operators ===== +
- +
-<m>e′ [\text{The value of } e \text{ in the final state of a step}]</m> +
- +
-<m>[A]e [A \lor (e′ = e)]</m> +
- +
-<m>\langle A \rangle e [A \land (e′ \neq e)]</m> +
- +
-<m>\text{enabled} A [\text{An } A \text{ step is possible}]</m> +
- +
-<m>\text{unchanged } e [e′ = e]</m> +
- +
-<m>A \cdot B [\text{Composition of actions}]</m> +
- +
-===== Temporal Operators ===== +
- +
-<m>\square F [F \text{ is always true}]</m> +
- +
-<m>\Diamond F [F \text{ is eventually true}]</m> +
- +
-<m>\text{WF}_e(A) [\text{Weak fairness for action } A]</m> +
- +
-<m>\text{SF}_e(A) [\text{Strong fairness for action } A]</m> +
- +
-===== User-Definable Operator Symbols ===== +
- +
-=== Infix Operators === +
- +
-<m> + - * / \circ ++</m> +
- +
-<m>< > <= >= \equiv</m> +
- +
-<m>& \land \lor</m> +
- +
-**Postfix Operators:** <m>\^+ \^* \^#</m> +
- +
-===== Precedence Ranges of Operators ===== +
- +
-The relative precedence of two operators is unspecified if their ranges overlap. +
-**Prefix Operators:** +
-<m> ¬ 4–4</m> +
- +
-**Infix Operators:** +
-<m>\Rightarrow 1-1</m> +
-<m> +− . 2−2</m> +
- +
-===== Operators Defined in Standard Modules ===== +
- +
-Modules Naturals, Integers, Reals: +
- +
-**+** **-** <m> \cdot ^ \text{Int, Real} </m> +
- +
-Modules Sequences: +
- +
-**\circ Head SelectSeq SubSeq Append** +
- +
-Modules FiniteSets: +
- +
-**IsFiniteSet Cardinality** +
- +
-Modules Bags: +
- +
-<m>\oplus \BagIn \text{CopiesIn} \text{SubBag} BagOfAll EmptyBag</m> +
- +
-Modules RealTime: +
- +
-**RTBound RTnow now** +
- +
-Modules TLC: +
- +
-**:> @@ Print Assert JavaTime SortSeq** +
- +
-===== ASCII Representation of Typeset Symbols ===== +
- +
-<m> \land \lnot \in \leq \gg \prec \preceq \subseteq \infty </m> +
- +
-<m> \forall \exists \subset \circ \bullet \sim \approx \cong \times \cup \cap </m> +
- +
-<m> \star \bigcirc \sim= \odot \oplus \ominus </m> +
- +
-<m>\simeq \doteq \asymp</m>+
  
  • learning/tla_summary.1728319916.txt.gz
  • Last modified: 2024/10/07 16:51
  • by fponzi