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]]
$$