39 lines
No EOL
1.6 KiB
Markdown
39 lines
No EOL
1.6 KiB
Markdown
- Comments
|
||
- Line comments start with a `* comment`
|
||
- Multiline comments use `(* comment *)`
|
||
- In PlusCal algorithms: `(* --algorithm ... *)`
|
||
- Repeated dashes, at least four, are ignored, used just for readability, except to mark the start of a `--- MODULE <name> ----`
|
||
- Repeated equal signs, at least four, terminate a `MODULE` definition
|
||
- Every value in TLA+ is a set. So every element of a set is also a set, so every set is a set of sets.
|
||
- `1..3` is a set of three elements,
|
||
but we don't know what their elements are.
|
||
- `BOOLEAN = {TRUE, FALSE}`
|
||
- `∈` can be written `\in`
|
||
- Quantifiers
|
||
- `∀` can be written `\A` (any)
|
||
- `∃` can be written `\E` (exists)
|
||
- Combinations:
|
||
- `∀ x ∈ S, ∀ y ∈ S :` can be written `∀ x, y ∈ S`
|
||
- `∀ x ∈ S : ∀ y ∈ T :` can be written `∀ x ∈ S, y ∈ T`
|
||
- `∀ x ∈ S : ∀ y ∈ T : ∀ z ∈ T : ∀ p ∈ U : ∀ q ∈ V :`
|
||
can be written<br/> `∀ x ∈ S, y, z ∈ T, p ∈ U , q ∈ V :`
|
||
- Sets
|
||
- Simple: `{e : x ∈ S}`
|
||
- Union is the union of all given sets:<br>
|
||
|
||
UNION {1..3, {0, 5}, 2..7, {6, 7}}
|
||
* equals
|
||
1..3 ∪ {0,5} ∪ 2..7 ∪ {6,8}
|
||
* equals
|
||
0..8
|
||
- `UNION (SUBSET S) = S`
|
||
- `S ⊆ SUBSET (UNION S)`
|
||
- `SUBSET S` is the set of all subsets of `S`
|
||
- In math
|
||
- this is called the powerset of `S`
|
||
- this is written `𝒫(S)`
|
||
- `𝒫` is not recognized or rendered by TLA+
|
||
- `CONSTANT Op(_, _)` defines dyadic operator `Op`.
|
||
In TLC we will be able to tell Toolbox that it is an operator
|
||
such that e.g. `Op(a, b)` is `a+2*b`
|
||
|