TLA+
See also TLA+ language summary and this summary. Here's another summary of operators.
| jargon | definition |
|---|---|
| Apalache | "symbolic model checker for TLA+." "Translates TLA+ into the logic supported by SMT solvers such as Microsoft Z3." Source: apalache github |
| behavior | aka execution |
| CONSTANT |
|
| CONSTANTS | See CONSTANT |
| execution | see behavior. Source: Lecture 1 video |
| deadlock | execution stopped when it wasn't supposed to |
| EXTENDS | Source: Lecture 2 video |
| FALSE | See also TRUE Source: Lecture 2 video |
| IF THEN | Source: Lecture 2 video |
| IF THEN ELSE | Source: Lecture 2 video |
| liveness property | "you have to look at the entire execution, which may be infinite, to determine that it is not satisfied." See also safety property |
| MODULE | Source: Lecture 2 video |
| PlusCal | User's manual |
| safety property | "if is not satisfied by an execution, then you can tell that it's not satisfied by looking at a finite portion of the execution—even if the execution is infinite." See also liveness property |
| state | assignment of values to variables Source: Lecture 1 video and Source: TLA+ chapter in "Software Specification Methods" |
| state machine, specification of |
|
| state predicate | "A formula that is true or false of a state. A state predicate is just an ordinary Boolean-valued formula that can contain variables but no primed variables and no temporal operators like <>." |
| step | change from one state to the next state. Source: Lecture 1 video |
| strong fairness | "A step of a process is strongly fair in a behavior iff there is no point in the behavior after which the step is enabled in infinitely many states but no such step occurs in the behavior." Source: session 9 See also weak fairness |
| strongly fair | see strong fairness |
| termination | execution stopped when it was supposed to |
| TLA | Temporal Logic of Actions |
| TLAPS | TLA+ proof system. Source: Lecture 1 video and Source: TLA+ Proof System (TLAPS) |
| TLA+ | language for high-level modeling digital systems. Here "high-level" refers to the design aspects, above the code. Examples of digital systems: algorithms, programs, and computer systems. "a formal specification language based on (untyped) ZF
set theory, first-order logic, and TLA (the Temporal Logic of Actions)" TLA+ version 2 user guide (2018) |
| TLA+ toolbox | IDE for TLA+.
Source: Lecture 1 video. Toolbox website |
| TLC | on-the-fly model checker for debugging TLA+ specifications Source: Specifying and Verifying Systems With TLA+ |
| TRUE | See also FALSE Source: Lecture 2 video |
| VARIABLE | Source: Lecture 2 video |
| VARIABLES | |
| weak fairness | the process must keep taking steps if it can See also strong fairness |
| weakly fair | see weak fairness |
| /\ | and |
| \/ | or Source: Lecture 2 video |
| <> | aka eventually |
| [] | aka always |
| ~> | aka leads to |
| ' | aka prime next value |
In module Sequences
See TLA+ summary page 8 of 9, and this summary.| jargon | definition |
|---|---|
| Append(seq,e) | the sequence obtained by appending the value e as the new last element of the sequence seq. For example, Append(<<1, 2>>, 42) equals <<1, 2, 42>>. Source: intermezzo 1 |
| Head(seq) | the first element of a non-empty sequence seq. For example, Head(<<"a", "c", "b">>) equals "a". Source: intermezzo 1 |
| \o | aka concatenation "seq1 \o seq2 is the sequence obtained by concatinating the sequences seq1 and seq2 in the obvious way. For example, seq \o <<e>> equals Append(seq,e) for any sequence seq and value e." Source: intermezzo 1 |
No comments:
Post a Comment