learning_tla/cheatsheet.md

# TLA+ symbols and identifiers

Note that PlusCal allows user-defined operators, so any operator shown as non-native
may be introduced by a module if it is part of the user-definable symbols, 
as defined by Table 4 in the P-syntax manual.

## Arrows
### Oriented
#### Single `->`

- `->`
  - In `[S -> D]`: the set of functions from domain S to destination set (codomain) D
- `<-` :  
  - used in TLA+ only as part of `INSTANCE` statements with `WITH` clauses
    - Example: `INSTANCE Foo WITH x <- e`
  - used in TLC Toolbox CFG files to assign values to constants (but doesn't work in TLC CLI)
  - used in lectures to represent substitution in expressions, like `f WITH v <- e`,
    which substitutes expression `e` for the symbol `v` in expression `f`.
- `|->`, used only as `[x |-> y]`, 
  - a function mapping a single element `x` to value `y`,
  - if `x` is a string, that function is called a _record_ or _struct_
  - if `x` is a natural, that function is called a _sequence_ or _tuple_ if the domain is finite.
- `>-` and `-<` : not native TLA+ symbols

#### Double `=>`

- `=>` : implies
  - `A => B = B \/ ~A`
- `<=>`: logical equivalence, same as `=` but only applicable to booleans
  - `A <=> B = (A => B) /\ (B => A)`
  - `A <=> B = (A /\ B) \/ (~A /\ ~B)`
- `>=` : greater than or equal operator
- `<=` : less than or equal operator
- `=<` : less than or equal operator
- `>=<`: not part of TLA+

#### Tilde `~>`

- `~>`: _leads to_
  - TODO
- `<~`: not a native TLA+ symbol

### Symmetric

- `<->` : logical equivalence
  - Unlike `=`, only applies to booleans

No other symmetric arrow is a native TLA+ symbol.

## Brackets etc
### `[]`: _always_ or functions

- Empty: _always_ temporal operator _box_
  - `[]P` means `P` is true in every state of the system, 
    i.e. it is an invariant
  - `~[]P`:  in EVERY behaviour, there exists at least one state where P is false
  - `[foo]_bar` 
    - is shorthand for `foo \/ UNCHANGED bar`, assuming `bar` is a sequence, e.g. `<<x, y>>`
    - which means for `foo \/ (x' = x /\ y` = y)`
  - The combination `[]<>` _always eventually_ can be called _repeatedly_
    - `[]<>P` means  that `P` will keep becoming true infinitely often. 
    - It's like saying "no matter when you look, `P` will eventually be true again."
    - Meaning at some point in the future, `P` will become true and remain true forever after. 
    - It's like saying "eventually, `P` will always hold."
- Non-empty: functions
  - In `[S -> D]`, a set of functions. See Arrows/`-->`
  - In `[x |-> y]` a specific function. See Arrows/`|->`
  - TODO check: "For any function `f = [x ∈ DOMAIN f: x ↦ f[x]]`"

### `{}`: sets

- `{}` : empty set 
- `{ x1, ... xN }` : enumerated set
- `{ x: y }` : a set comprehension. Two kinds have names:
  - `{ expr: x \in S }`: a _set map_, read as "values of expr where x is in S"
  - `( x \in S: expr }`: a _set filter_, read as "keys of S where expr holds true"

### `<>`: eventually, tuples 

- `<>`: _eventually_ temporal operator _diamond_
  - Meaning at some point in the future, `P` will become true and remain true forever after. It's like saying "eventually, `P` will always hold."
- `<>[]`: _eventually always_
  - At some point in the future, `P` will become true and remain true forever after. 
  - It's like saying "eventually, `P` will always hold."
- `<<A>>_v` means `A` is true AND `v` changes
  - Compare to `[A]_v` meaning `A` is true OR `v`doesn't change
- `<<a, b, c>>` defines a tuple/sequence. Some texts (incorrectly ?) use `(a, b, c)`. 

### `()`

- `(a, b, c)` : tuple construction is referenced somewhere, but should be `<<a, b, c>>`
- `f(x, y, z)` : non-niladic function application
  - niladic function `f` application is written `f`
  - that is because a niladic function and its application are actually the same
- Expressions grouping for arithmetic
- Logical and temporal precedence grouping

## Predefined functions and operators, by module

All are pure functions, no mutators.

### At least some direct engine support


#### Naturals

- `+`, `-`, `*`, `/`, `^`, `%`: arithmetic
- `<`, `<=`, `>`, `>=` and less-used `=<` for `<=`
- `Nat` : the set of natural integers
  - Cannot be enumerated by TLC (in a quantifier or CHOOSE)
  - Can be used for membership checking
- `..` to define "range" sets like `1..3 = {1, 2, 3}`
- `\div`: integer floor division: `10 \div 3 = 3`

#### Integers

- All of `Naturals`, plus...
- `Int` : the set of all integers
- unary `-`: negative numbers, like `-2`

#### Sequences

- `Append(S, e)`: appends element `e` at the end of sequence S and returns the result
- `Head(S)`: first element of S (cf. Lisp CAR)
- `Len(S)`: length of sequence
- `\o`: concatenation of two sequences (vs seq + element for `Append`)
- `SelectSeq(seq, Op(_))` : filter a sequence using `Op`
  - `IsEven(x) == x % 2 = 0` (`%` has precedence over `=`)
  - `SelectSeq(<<1, 2, 3>>, IsEven) = <<2>>`
- `Seq(set)`: the set of all sequences of `set` elements (so countable infinite, aleph-null)
  - Is actually efficient in TLC, counter-intuitively
  - Cannot be enumerated by TLC (in a quantifier or CHOOSE)
  - Can be used for membership checking
- `SubSeq(S, m, n)`: subsequence of s from m to n, both included
- `Tail(S)`: sequence S without first element (cf. Lisp CDR)

Required for PlusCal procedures.

#### TLC

- `:>` shorthand notation for functions with a singleton domain
  - `a :> b = [x \in {a} |-> b]`
- `@@`: dyadic function merge
  - if both operands share the same key use the LEFT one (cf. [LearnTLA+](https://learntla.com/reference/standard-library.html#tlc)
    (other sources say the right one)
- SortSeq(seq, Op(_, _))
    Sorts the sequence with comparator Op.
- `Any`
  - Used as `x \in Any` to get any value `x` of any type
  - Do not use in a spec
  - May be useful for modeling properties

- `Assert(e, t)`: checks that `e` is true and returns, or prints `t` if `e` if false
- `JavaTime`: The current epoch time.
- `Permutations(set)`: all functions acting as permutations of the set
  - `Permutations(S) == {f \in [S -> S] : \A w \in S : \E v \in S : f[v]=w}`
- `Print(t, e)`:
  - From one source: prints the value of `e` with tag `t`
  - From the Standard modules page on LearnTLA: `Print(val, out)`: Prints `ToString(val)`, and evaluates to `out` as an expression.
  - From experience: requires `e = TRUE` and prints `t` to output
- `PrintT(val)`: Equivalent to `Print(val, TRUE)`.
- `RandomElement(set)`: Randomly pulls an element from set. The value can be different on different runs!
- `SortSetq(seq)`: Sorts a sequence
- `TLCEval(v)`: Evaluates `v` and caches the result. Can be used to speed up recursive definitions.
- `TLCGet(val)`: val can be either an integer or a string.
  - If an integer, retrieves the value from the corresponding `TLCSet`.
  - If a string, retrieves statistics from the current model run. The following strings are valid:
    - “queue”
    - “generated”
    - “distinct”
    - "duration”: number of seconds elapsed since the beginning of model checking
    - “level”: the length of the current behavior
      - can be used to bound an unbound model.
    - “diameter”: the length of the longest global behavior
    - “stats”: all of the global stats (everything excluding “level”), as a struct.
- `TLCSet(i, val)`: Sets the value for `TLCGet(i)`.
  - `i` must be a positive integer.
  - `TLCSet` can be called multiple times in the same step.
- `ToString(val)`: String conversion.

<blockquote>
Each TLC worker thread carries a distinct “cache” for the values of TLCGet(i). 
As such, it’s generally inadvisable to use TLCSet to profile information that lasts beyond a single step. 

TLCSet statements evaluated during the initial state, however, will be propagated to all workers.
</blockquote>

#### TLCExt

- `AssertEq(a, b)`: Equivalent to a = b, except that if a # b, it also prints the values of a and b.
  - This does not terminate model checking!
- `AssertError(str, exp)`: True if exp doesn’t throw an error, or if exp throws an error that exactly matches str.
  - False otherwise
  - This does not terminate model checking!
- `Trace`: Returns the “history” of the current behavior, as a sequence of structs.
- `TLCModelValue(str)`: Creates a new model value with name str.
  - Can only be used in constant definitions, as part of an ordinary assignment.
```tla+ code fragment
CONSTANT Threads <- {
  TLCModelValue(ToString(i)): i \in 1..3
}
```
- assigns the constant `Threads` a set of model values corresponding to the strings `"1"`, `"2"`, and `"3"`.
- This is useful for scenarios where you want to represent distinct entities (like threads)
  in a model without tying them to specific numeric values.

### 100% TLA+ user space modules
#### Bags

Bags defines a special kind of functions,
from items to natural values, meant to represent their "count".

- `IsABag(f)`
  - `IsABag([a |-> 3, b |-> 7]) = TRUE` because both 3 and 7 are naturals
  - `IsABag([a |-> 3, b |-> "B"]) = FALSE` because "B" is not a natural
  - `IsABag([a |-> 3, b |-> -2]) = FALSE` because -2 is not a natural
  - Any function over the empty set passes `IsABag` because no elements fail to be naturals
- `BagToSet(bag)` : returns the domain of bag
  - equivalent to `DOMAIN bag`
- `SetToBag(set)` creates a bag with set elements as keys and counts all equal to 1
  - equivalent to `[x \in set |-> 1]`
- `BagIn(e, bag)` : `e \in DOMAIN bag`
- `EmptyBag` : `<<>>
  - Subtlety: any function over the empty set is the `EmptyBag`
- `(+)`: dyadic bag addition merges two bags, adding counts on merged keys
- `(-)`: dyadic bag subtraction, subtracting counts on all keys present in the right argument,
  and dropping all keys with resulting negative **or zero** counts
- `BagUnion(set)` : bag addition of all members of the set
- `\sqsubseteq` : dyadic operator: true IFF all elements in the right operand have
  at least as high a count as those in the left operand
`SubBag(bag)` : the set of all subbags of `bag` as defined by `\sqsubseteq`
  - `SubBag(EmptyBag) = {<<>>}`
  - `SubBag([a |-> 2]) = {<<>>, [a -> 1], [a -> 2]}`
- `BagOfAll(Op(_), bag)` : mapping of `Op` over the bag KEYS (not values)
  - `BagOfAll(LAMBDA x: x^2, <<1, 3, 5>>) = (1 :> 1 @@ 4 :> 3 @@ 9 :> 5)`
- `BagCardinality(bag)` : the sum of all counts in the bag
- `CopiesIn(e, bag)` : the count for key `e` in the bag, 0 if it is absent

#### FiniteSets

- `Cardinality(S)`: number of elements in S
- `IsFiniteSet(S)`: is S finite ?

#### Json

- `ToJson(val)` : convert to a JSON string
  - sets and sequences -> JSON arrays
  - functions: objects with string keys; converting any non-string source elements to their string representation
- `JsonSerialize(absoluteFilename, value)`: convert value to a JSON file
- `JsonDeserialize(absolutefilename)`: imports a JSON object from a file

#### Randomization

Provides pseudo-random subsets, which will prevent TLC from checking all possible states.

This is useful for optimization, but may introduce oversights.

- `RandomSubset(k, S)`:  random size-k subset of S.
- `RandomSetOfSubsets(k, n, S)`: k random subsets of S, where each random subset has on average n elements
  - May generate duplicates, so return fewer than `k` elements,
  - May return the empty set
- `TestRandomSetOfSubsets(k, n, S)`
  - Calls `RandomSetOfSubsets(k, n, S)` five times (hardcoded) and returns the number of unique sets each time,
    as a sequence


#### Reals

Nothing usable in TLC

#### Realtime

Nothing usable in TLC

## PlusCal
### Structure

- Defined within a TLA+ spec, by a block comment starting by:
  `(*--algorithm <name>` or `(*--fair algorithm <name>` where `<name>` is irrelevant,
  and finished by `end algorithm; *)`
  - Although the opening and closing comments do not have to be adjacent to
    `algorithm` and `end algorithm` some plugins may fail in that case,
    like the VSCode plugin as of 2025-02
- Order of sections
  1. Opening: `(*--[fair] algorithm foo`
  2. Declarations, semicolon-terminated, e.g.: 
    - `variable seq \in S \x S;` - only one `variable` clause
    - `index = 1;`
    - `seen = {};`
    - notice: no `:=`, no `==`
  3. Operator definitions: TLA+ code, wrapped in `define` / `end define`
  4. Macros (see [02-writing-specs](learn_tla/core/02-writing-specs.md))
  5. Procedures (see [07-concurrency](learn_tla/core/07-concurrency.md))
  6. Code, either indented off a `begin` for the algorithm body, or `[fair] process <name>` for a process
    - labels, as the unit of atomicity
      - always containing statements
      - adding a + to the label name makes it a "fair" label
      - adding a - to the label name makes it an "unfair" label 
    - statements, semicolon-terminated
    - assignments use `:=` and are limited to one par variable per label
  5. Closing: `end algorithm; *)` 

### Predefined

- Variables:
  - `pc` for Program Counter: the label of the NEXT statement to be executed
  - `self`: from the P-syntax spec:
    - "_Within the body of a process set, self equals the current process’s identifier_"
  - `stack` if the algorithm contains one or more procedures
- Labels
  - `Done` label: from the P-syntax spec: "There is an implicit label Done at
    the end of every process, and at the end of a uniprocess algorithm""
  - `Error` label: from the P-syntax spec: "There is an implicit label Error immediately after the body. 
    If control ever reaches that point, then execution of either the process (multiprocess algorithm)
    or the complete algorithm (uniprocess algorithm) halts"

## Tips and ideas

- Represent a directed graph: 
  - create a function `graph` on pairs of points,
    TRUE iff there is a directed edge between them,
  - `GraphType = [Node \X Node -> BOOLEAN]`
    This implies `graph \in GraphType` = TRUE.
- When using `tlc -dump dot <out> <spec.tla>`,
  the `<out>_liveness.dot` file represents the inner representation of TLC, and is generally considered useless except to debug TLC itself. 
  [Do not waste time on it](https://groups.google.com/g/tlaplus/c/olBAjD-9btA).