144 lines
No EOL
4.6 KiB
Markdown
144 lines
No EOL
4.6 KiB
Markdown
# Glossary
|
|
|
|
## @
|
|
|
|
- @: in a temporal formula, the value being modified in a `EXCEPT` clause
|
|
- See: temporal formula
|
|
|
|
## A
|
|
|
|
- Action: In TLA+, any operator containing primed variables.
|
|
- This is what is meant by the "A" in TLA.
|
|
- The short name for an action formula
|
|
- See: action expression, formula
|
|
- Action expression: An expression that can contain anything a state expression can,
|
|
as well as `'` and `UNCHANGED`. It has value on a step.
|
|
- See: state expression, step
|
|
- Assumption: a constant formula introduced by `ASSUME`
|
|
- See: constant expression, formula
|
|
- Auxiliary variable: a variable that is not part of the state of the system,
|
|
called imaginary variables in the lectures
|
|
- Also called elsewhere a "helper variable" or "ghost variable"
|
|
- `await`: in PlusCal, a keyword that introduces a condition that must be true before
|
|
the rest of the label can be executed.
|
|
- See: `when`
|
|
|
|
## B
|
|
|
|
- Behavior: a given sequence of states
|
|
|
|
## C
|
|
|
|
- Conjunction: AND
|
|
- See: Disjunction
|
|
- Constant: a module-complete expression that has no declared variables,
|
|
and no non-constant operators.
|
|
It is also a state expression that has the same value on all states
|
|
- See: module-complete expression, state expression.
|
|
|
|
## D
|
|
|
|
- deadlock:
|
|
- a behavior property, where no action is enabled
|
|
- or worded differently: a reachable state from which no other state is reachable
|
|
- disjunction: OR
|
|
- See: conjunction
|
|
|
|
## E
|
|
|
|
- `EXTENDS`: a TLA+ operator that imports a module without frills
|
|
- See: `INSTANCE`
|
|
|
|
## F
|
|
|
|
- fairness: a behavior property, existing in two versions
|
|
- weak fairness: a behavior cannot stutter indefinitely
|
|
- declared by `fair process` instead of `process`
|
|
- strong fairness: TODO
|
|
- declared by `fair+ process`
|
|
- formula: a boolean-valued expression
|
|
|
|
## G
|
|
|
|
- general temporal substitution law:
|
|
- `THEOREM [](v1 = e1) /\ (v2 = e2) /\ ... => (f = (f WITH v1 <- e1, v2 <- e2, ...))`
|
|
- With the substitution of all v_i being simultaneous
|
|
- See: simple substitution law, temporal substitution law
|
|
- ghost variable: see auxiliary variable
|
|
|
|
## H
|
|
|
|
- helper variable: see auxiliary variable
|
|
|
|
## I
|
|
|
|
- iff : if and only if
|
|
- imaginary variable: see auxiliary variable
|
|
- `INSTANCE`: a TLA+ operator that imports a module, allowing the replacement of symbols with expressions
|
|
- See: `EXTENDS`, refinement mapping
|
|
|
|
## M
|
|
|
|
- _module-closed_:
|
|
- expression: an expression, after resolution, contains only:
|
|
- built-in TLA+ operators and constructs
|
|
- numbers and strings
|
|
- declared constants and variables
|
|
- identifiers declared locally within the expression
|
|
- formula: a formula which is a boolean-valued module-closed expression
|
|
|
|
## N
|
|
|
|
- Next State Relationship: the `Spec == Init /\ [][Next]_vars` temporal formula
|
|
|
|
## P
|
|
|
|
- `pc` : program counter
|
|
- In PlusCal, the next label
|
|
- In non-concurrent code, a single value
|
|
- In concurrent code, a function from process values to strings representing the next label for the process
|
|
|
|
## R
|
|
|
|
- refinement mapping: the process replacing symbols during an import with expressions
|
|
- See: `INSTANCE`, [lecture 10.2](lamport_video/docs/lecture10-2.md)
|
|
|
|
## S
|
|
|
|
- `self`: in a process, the value of the process
|
|
- sequence: a sequence of length N is a function with domain 1..N (not 0..N-1)
|
|
- may be infinite or finite. Finite ones are called tuples
|
|
- See: tuple
|
|
- simple substitution law:
|
|
- `THEOREM (v = e) => (f = (f WITH v <- e))`
|
|
- See general temporal substitution law, temporal substitution law
|
|
- state expression: an expression that can include everything in a constant expression, plus declared variables.
|
|
- It is an action expression whose value only depends on the first state of the step.
|
|
- See: constant expression, action expression
|
|
- step: a pair of states
|
|
- See: action expression
|
|
- stuttering:
|
|
- in a behavior, make a new state where nothing happens and all variables are unchanged
|
|
- a stuttering step is one in which all variables defined by the formule are unchanged
|
|
|
|
## T
|
|
|
|
- temporal formula: any formula including at least one temporal operator
|
|
- See: formula, temporal operator
|
|
- temporal operator: one of
|
|
- `[]` - box operator, meaning always
|
|
- `<>` - diamond operator, meaning eventually
|
|
- `~>` - leads-to operator
|
|
- See: https://www.learntla.com/core/temporal-logic.html
|
|
- See: temporal formula
|
|
- temporal substitution law:
|
|
- `THEOREM [](v = e) => (f = (f WITH v <- e))`
|
|
- See general temporal substitution law, simple substitution law
|
|
- TLA: a linear temporal logic, on which TLA+ is based
|
|
- tuple: a finite sequence
|
|
- See: sequence
|
|
|
|
## W
|
|
|
|
- `when`: in PlusCal, a synonym for `await`.
|
|
- See: `await` |