Differences

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

--- learning:tla_summary [2024/10/07 16:51] – fponzi
+++ learning:tla_summary [2024/10/07 16:52] (current) – old revision restored (2024/09/28 17:58) fponzi
@@ Line 7: / Line 7: @@
 ----
-====== Summary of TLA+ ======
-===== Module-Level Constructs =====
+====== Summary of TLA { }^{+} ======
-**module M**
+  * Module-Level Constructs
+  * The Constant Operators
+  * Miscellaneous Constructs
+  * Action Operators
+  * Temporal Operators
+  * User-Definable Operator Symbols
+  * Precedence Ranges of Operators
+  * Operators Defined in Standard Modules.
+  * ASCII Representation of Typeset Symbols 1
-Begins the module or submodule named M.
+===== Module-Level Constructs =====
-**extends M1, ..., Mn**
+===== \Gamma =====
-Incorporates the declarations, definitions, assumptions, and theorems from the modules named M1, ..., Mn into the current module.
+MODULE $M$Begins the module or submodule named $M$.
-**constants C1, ..., Cn**
+EXTENDS $M_{1}, \ldots, M_{n}$
-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.
+Incorporates the declarations, definitions, assumptions, and theorems from the modules named $M_{1}, \ldots, M_{n}$ into the current module.
-**variables x1, ..., xn**
+CONSTANTS $C_{1}, \ldots, C_{n}^{(1)}$
-Declares the xj to be variables (parameters that are flexible variables).
+Declares the $C_{j}$ to be constant parameters (rigid variables). Each $C_{j}$ is either an identifier or has the form $C\left(\_, \ldots, \_\right)$, the latter form indicating that $C$ is an operator with the indicated number of arguments.
-**assume P**
+$$
+\text { VARIABLES } x_{1}, \ldots, x_{n}^{(1)}
+$$
-Asserts P as an assumption.
+Declares the $x_{j}$ to be variables (parameters that are flexible variables).
-**F(x1, ..., xn) Δ = exp**
+===== ASSUME P =====
-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.)
+Asserts $P$ as an assumption.
-**f[x ∈ S] Δ = exp**
+$F\left(x_{1}, \ldots, x_{n}\right) \triangleq \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.)
+Defines $F$ to be the operator such that $F\left(e_{1}, \ldots, e_{n}\right)$ equals exp with each identifier $x_{k}$ replaced by $e_{k}$. (For $n=0$, it is written $F \triangleq \exp$.)
-**instance M with p1 ← e1, ..., pm ← em**
+$f[x \in S] \triangleq \exp ^{(2)}$
-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.)
+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.)
-**theorem P**
+  - The terminal S in the keyword is optional.
+  - $x \in S$ may be replaced by a comma-separated list of items $v \in S$, where $v$ is either a comma-separated list or a tuple of identifiers.
-Asserts that P can be proved from the definitions and assumptions of the current module.
+INSTANCE $M$ WITH $p_{1} \leftarrow e_{1}, \ldots, p_{m} \leftarrow e_{m}$
-**local def**
+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 $p_{j}$ of $M$ with $e_{j}$. (If $m=0$, the WITH is omitted.) $N\left(x_{1}, \ldots, x_{n}\right) \triangleq$ INSTANCE $M$ WITH $p_{1} \leftarrow e_{1}, \ldots, p_{m} \leftarrow e_{m}$
-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.
+For each defined operator $F$ of module $M$, this defines $N\left(d_{1}, \ldots, d_{n}\right)!F$ to be the operator whose definition is obtained from the definition of $F$ by replacing each declared constant or variable $p_{j}$ of $M$ with $e_{j}$, and then replacing each identifier $x_{k}$ with $d_{k}$. (If $m=0$, the WITH is omitted.)
-===== The Constant Operators =====
+THEOREM $P$
-=== Logic ===
+Asserts that $P$ can be proved from the definitions and assumptions of the current module.
-<m> ∧ ∨ ¬ ⇒ ≡ \text{true} \text{false} \text{boolean} \</m>
-<m>∀ x ∈ S : p</m>
+LOCAL def
-<m>∃ x ∈ S : p</m>
+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.
-<m>\text{choose } x ∈ S : p</m>
+Ends the current module or submodule.
-=== Sets ===
+===== The Constant Operators =====
-<m>= \neq ∈ \notin ∪ ∩ ⊆ \setminus </m>
-<m>\{e1, ..., en\} [\text{Set consisting of elements } e_i]</m>
+{{https://cdn.mathpix.com/cropped/2024_06_23_576f0b4b8da858775992g-4.jpg?height=224&width=813&top_left_y=124&top_left_x=157}}
-<m>\{x ∈ S : p\} [\text{Set of elements } x \text{ in } S \text{ satisfying } p]</m>
+===== Sets =====
-<m>\subset S [\text{Set of subsets of } S]</m>
+$=\neq \in \cup$.
-<m>\text{union} S [\text{Union of all elements of } S]</m>
+$\left\{e_{1}, \ldots, e_{n}\right\} \quad$ [Set consisting of elements $\left.e_{i}\right]$
-=== Functions ===
+$\{x \in S: p\}$ (2) [Set of elements $x$ in $S$ satisfying $p$ ]
-<m>f[e] [\text{Function application}]</m>
-<m>\text{domain} f [\text{Domain of function } f]</m>
+$\{e: x \in S\}^{(1)} \quad$ [Set of elements $e$ such that $x$ in $\left.S\right]$
-<m>[x ∈ S \mapsto e] [\text{Function } f \text{ such that } f[x] = e \text{ for } x ∈ S]</m>
+SUBSET $S \quad$ [Set of subsets of $S$ ]
-<m>[S \to T] [\text{Set of functions } f \text{ with } f[x] \in T \text{ for } x \in S]</m>
+UNION $S \quad[$ Union of all elements of $S]$
-=== Records ===
+===== Functions =====
-<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>
+$$
+\begin{array}{ll}
+f[e] & {[\text { Function application] }} \\
+\text { DOMAIN } f & {[\text { Domain of function } f]} \\
+{[x \in S \mapsto e]{ }^{(1)}} & {[\text { Function } f \text { such that } f[x]=e \text { for } x \in S]} \\
+{[S \rightarrow T]} & {[\text { Set of functions } f \text { with } f[x] \in T \text { for } x \in} \\
+{\left[f \text { EXCEPT }!\left[e_{1}\right]=e_{2}\right]^{(3)}} & {\left[\text { Function } \widehat{f} \text { equal to } f \text { except } \widehat{f}\left[e_{1}\right]=e_{2}\right]}
+\end{array}
+$$
-=== Tuples ===
+===== Records =====
-<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>
+$\begin{array}{ll}e . h & \text { [The } h \text {-field of record } e] \\ {\left[h_{1} \mapsto e_{1}, \ldots, h_{n} \mapsto e_{n}\right]} & \left.\text { [The record whose } h_{i} \text { field is } e_{i}\right] \\ {\left[h_{1}: S_{1}, \ldots, h_{n}: S_{n}\right]} & \left.\text { [Set of all records with } h_{i} \text { field in } S_{i}\right] \\ {[r \text { EXCEPT }!. h=e]} & \text { [3) } \\ \text { [Record } \widehat{r} \text { equal to } r \text { except } \widehat{r} . h=e]\end{array}$
-<m>S1 \times ... \times Sn [\text{The set of all n-tuples with i-th component in } S_i]</m>
+===== Tuples =====
-===== Miscellaneous Constructs =====
+$$
+\begin{array}{ll}
+e[i] & {\left[\text { The } i^{\text {th }} \text { component of tuple } e\right]} \\
+\left\langle e_{1}, \ldots, e_{n}\right\rangle & {\left[\text { The } n \text {-tuple whose } i^{\text {th }} \text { component is } e_{i}\right]} \\
+S_{1} \times \ldots \times S_{n} & \text { [The set of all } \left.n \text {-tuples with } i^{\text {th }} \text { component in } S_{i}\right]
+\end{array}
+$$
-**if p then e1 else e2** [e1 if p is true, else e2]
+  - $x \in S$ may be replaced by a comma-separated list of items $v \in S$, where $v$ is either a comma-separated list or a tuple of identifiers
+  - $x$ may be an identifier or tuple of identifiers.
-**case p1 → e1 ... pn → en**
+(3)! $\left[e_{1}\right]$ or !.h may be replaced by a comma separated list of items $!a_{1} \cdots a_{n}$, where each $a_{i}$ is $\left[e_{i}\right]$ or.$h_{i}$.
-**case p1 → e1 ... pn → en 2 other → e**
+===== Miscellaneous Constructs =====
-**let d1 Δ = e1 ... dn Δ = en in e**
+{{https://cdn.mathpix.com/cropped/2024_06_23_576f0b4b8da858775992g-5.jpg?height=416&width=1145&top_left_y=122&top_left_x=162}}
 ===== Action Operators =====
-<m>e′ [\text{The value of } e \text{ in the final state of a step}]</m>
+^$e^{\prime}$            ^$[$ The value of $e$ in the final state of a step]     ^
+|$[A]_{e}$               |$\left[A \vee\left(e^{\prime}=e\right)\right]$         |
-<m>[A]e [A \lor (e′ = e)]</m>
+|$\langle A\rangle_{e}$  |$\left[A \wedge\left(e^{\prime} \neq e\right)\right]$  |
+|ENABLED $A$             |$[$ An step is possible $]$                            |
-<m>\langle A \rangle e [A \land (e′ \neq e)]</m>
+|UNCHANGED $e$           |$\left[e^{\prime}=e\right]$                            |
+|$A \cdot B$             |$[$ Composition of actions $]$                         |
-<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>
+$$
+\begin{array}{ll}
-<m>\Diamond F [F \text{ is eventually true}]</m>
+\square F & {[F \text { is always true }]} \\
+\diamond F & {[F \text { is eventually true }]} \\
-<m>\text{WF}_e(A) [\text{Weak fairness for action } A]</m>
+\mathrm{WF}_{e}(A) & {[\text { Weak fairness for action } A]} \\
+\mathrm{SF}_{e}(A) & {[\text { Strong fairness for action } A]} \\
-<m>\text{SF}_e(A) [\text{Strong fairness for action } A]</m>
+F \sim G & {[F \text { leads to } G]}
+\end{array}
+$$
 ===== User-Definable Operator Symbols =====
-=== Infix Operators ===
+===== Infix Operators =====
-<m> + - * / \circ ++</m>
+^$+^{(1)}$       ^$-{ }^{(1)}$        ^$*$                     ^$(1)$          ^$/{ }^{(2)}$     ^$\circ{ }^{(3)}$  ^++     ^
+|$\div^{(1)}$    |$\%^{(1)}$          |-                       |$(1,4)$        |$\ldots$         |                  |       |
+|$\oplus^{(5)}$  |$\ominus{ }^{(5)}$  |$\otimes$               |$\oslash$      |$\odot$          |–                 |       |
+|(1) $^{(1)}$    |$>{ }^{(1)}$        |$\leq$                  |${ }^{(1)}$    |$\geq{ }^{(1)}$  |$\sqcap$          |$* *$  |
+|$\prec$         |$\succ$             |$\preceq$               |$\succeq$      |$\sqcup$         |$\sim-$           |       |
+|$\ll$           |$\gg$               |$<:$                    |$:>^{(6)}$     |$\&$             |$\& \&$           |       |
+|$\sqsubset$     |$\sqsupset$         |$\sqsubseteq{ }^{(5)}$  |$\sqsupseteq$  |$\mid$           |$\% \%$           |       |
+|$\subset$       |$\supset$           |                        |$\supseteq$    |$\star$          |$@ @(6)$          |       |
+|$\vdash$        |$\dashv$            |$\models$               |$=$            |$\bullet$        |$\# \#$           |       |
+|$\sim$          |$\simeq$            |$\approx$               |$\cong$        |$\$$             |$\$ \$$           |       |
+|$\bigcirc$      |$::=$               |$\asymp$                |$\doteq$       |$? ?$            |$!!$              |       |
+|$\propto$       |$\checkmark$        |$\uplus$                |               |                 |                  |       |
-<m>< > <= >= \equiv</m>
+Postfix Operators (7)
-<m>& \land \lor</m>
+$\sim \quad$ - $＃$
-**Postfix Operators:** <m>\^+ \^* \^#</m>
+  - Defined by the Naturals, Integers, and Reals modules.
+  - Defined by the Reals module.
+  - Defined by the Sequences module.
+  - $x^{\wedge} y$ is printed as $x^{y}$.
+  - Defined by the Bags module.
+  - Defined by the $T L C$ module.
+  - $e^{\wedge}+$ is printed as $e^{+}$, and similarly for ${ }^{\wedge} *$ and $\wedge \#$.
 ===== Precedence Ranges of Operators =====
-The relative precedence of two operators is unspecified if their ranges overlap.
+The relative precedence of two operators is unspecified if their ranges overlap. Left-associative operators are indicated by (a).
-**Prefix Operators:**
-<m> ¬ 4–4</m>
-**Infix Operators:**
+{{https://cdn.mathpix.com/cropped/2024_06_23_576f0b4b8da858775992g-7.jpg?height=1394&width=1163&top_left_y=291&top_left_x=176}}((  - Action composition ().
-<m>\Rightarrow 1-1</m>
+  - Record field (period).
-<m> +− . 2−2</m>
+))
-===== Operators Defined in Standard Modules =====
+===== Operators Defined in Standard Modules. =====
-Modules Naturals, Integers, Reals:
+Modules Naturals, Integers, Reals
-**+** **-** <m> \cdot ^ \text{Int, Real} </m>
+$$
+\begin{aligned}
+& +\quad-{ }^{(1)} \quad * \quad /^{(2)} \quad \sim^{-(3)} \quad \text {.. } \quad \text { Nat } \quad \text { Real }^{(2)} \\
+& \div \quad \% \quad \geq \quad>\quad \text { Int }^{(4)} \quad \text { Infinity }{ }^{(2}
+\end{aligned}
+$$
-Modules Sequences:
+  - Only infix - is defined in Naturals.
+  - Defined only in Reals module.
+  - Exponentiation.
+  - Not defined in Naturals module.
-**\circ Head SelectSeq SubSeq Append**
+Module Sequences
-Modules FiniteSets:
+^$\circ$  ^Head  ^SelectSeq  ^SubSeq  ^
+|Append   |Len   |Seq        |Tail    |
-**IsFiniteSet Cardinality**
+===== Module FiniteSets  IsFiniteSet Cardinality =====
-Modules Bags:
+Module Bags
-<m>\oplus \BagIn \text{CopiesIn} \text{SubBag} BagOfAll EmptyBag</m>
+^$\oplus$        ^BagIn     ^CopiesIn  ^SubBag  ^
+|$\ominus$       |BagOfAll  |EmptyBag  |        |
+|$\sqsubseteq$   |BagToSet  |IsABag    |        |
+|BagCardinality  |BagUnion  |SetToBag  |        |
-Modules RealTime:
+Module RealTime
-**RTBound RTnow now**
+RTBound RTnow now (declared to be a variable)
-Modules TLC:
+Module $T L C$
-**:> @@ Print Assert JavaTime SortSeq**
+$:>$ Print Assert JavaTime Permutations SortSeq
 ===== ASCII Representation of Typeset Symbols =====
-<m> \land \lnot \in \leq \gg \prec \preceq \subseteq \infty </m>
+^            $/$ or $\backslash]$            ^      land      ^          V          ^  $\backslash /$ or $\backslash$ lor  ^       $\Rightarrow$       ^                                    ^
+|  $\sim$ or $\backslash \operatorname{lr}$  |    not or      |      $\equiv$       |        $\Leftrightarrow$ or          |       $\triangleq$        |                $==$                |
-<m> \forall \exists \subset \circ \bullet \sim \approx \cong \times \cup \cap </m>
+|                                            |                |      $\notin$       |                                      |          $\neq$           |            $\#$ or $/=$            |
+|                    $<<$                    |                |                     |                 $>$                  |         $\square$         |                 []                 |
-<m> \star \bigcirc \sim= \odot \oplus \ominus </m>
+|                    $<$                     |                |         $>$         |                 $>$                  |        $\diamond$         |                $<>$                |
+|                     or                     |  $=<$ or $<=$  |       $\geq$        |                or >=                 |          $\sim$           |               $\sim$               |
+|                                            |                |        $\gg$        |           $\backslash g g$           |  $\xrightarrow{\square}$  |               $-+->$               |
+|                                            |                |       $\succ$       |                                      |         $\mapsto$         |            $\|-\rangle$            |
+|                                            |                |      $\succeq$      |                                      |          $\div$           |                                    |
+|                                            |                |     $\supseteq$     |                                      |             .             |                                    |
+|                                            |                |      $\supset$      |                                      |             0             |                or                  |
+|                                            |                |     $\sqsupset$     |                                      |         $\bullet$         |                                    |
+|                                            |      eteq      |    $\sqsupseteq$    |                                      |          $\star$          |                                    |
+|                    $1-$                    |                |      $\dashv$       |                  -1                  |             O             |                                    |
+|                  $\mid=$                   |                |         $=$         |                 $=1$                 |          $\sim$           |                                    |
+|               $\rightarrow$                |                |    $\leftarrow$     |                 $<-$                 |         $\simeq$          |                                    |
+|                     or                     |                |       $\cup$        |                 or                   |         $\asymp$          |                                    |
+|                                            |                |      $\sqcup$       |                                      |         $\approx$         |                                    |
+|                 $(+)$ or 1                 |                |      $\uplus$       |                                      |          $\cong$          |                                    |
+|                 $(-)$ or 1                 |                |      $\times$       |          $\backslash X$ or           |         $\doteq$          |                                    |
+|                  (.) or 1                  |                |          2          |           $\backslash w r$           |          $x^{y}$          |        $x^{\wedge} y^{(2)}$        |
+|            $(\backslash X)$ or             |                |      $\propto$      |                                      |          $x^{+}$          |     $\mathrm{x}^{\wedge}+(2)$      |
+|                  (/) or 1                  |                |         “s”         |               “s” (1)                |          $x^{*}$          |  $\mathrm{x}^{\wedge} *{ }^{(2)}$  |
+|               $\backslash E$               |                |      $\forall$      |       $\backslash \mathrm{A}$        |         $x^{\#}$          |       $x^{\wedge} \#^{(2)}$        |
+|          $\backslash \mathrm{EE}$          |                |      $\forall$      |       $\backslash \mathrm{AA}$       |         $\prime$          |                 ,                  |
+|                    ]_v                     |                |       $_{v}$        |               $>>\_v$                |                           |                                    |
+|                $W F_{-} v$                 |                |  $\mathrm{SF}_{2}$  |                 SF_v                 |                           |                                    |
-<m>\simeq \doteq \asymp</m>
+  - $s$ is a sequence of characters.
+  - $x$ and $y$ are any expressions.
+  - a sequence of four or more - or $=$ characters.