learning_tla/glossary.md

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

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