TLA+ | EagleBear2002 的博客

Terminology

TLA：时序逻辑行为（Temporal Logic of Actions）

TLC：遍历 TLA+ 抽象出来的系统的每一个可能路径，并在每条可能的路径上对一些条件（称为“不变式”）进行检验。

对以下 C 语言代码进行验证：

int i;
int main() {
    // someNumber() return an int between 0 and 1000
    i = someNumber();
    i = i + 1;
}

两阶段提交

The TLA+ syntax for an array expression:

\[ [variable \in set \mapsto expression] \]

For example:

\[ sqr = [i \in 1..42 \mapsto i^2] \]

Defines \(sqr\) to be an array with index set \(1..42\) such that \(sqr[i] = i^2\) for all \(i\) in \(1..42\).

Math and TLA+ allows a function to have any set as its domain — for exxample, the set of all integers.

\[ rmState' = [s \in RM \mapsto \textup{IF} \; s = r \; \textup{THEN} \; \mathrm{"prepared"}\; \textup{ELSE} \; rmState[s]] \]