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∈set↦expression]

For example:

sqr = [i∈1..42↦i²]

Defines sqr to be an array with index set 1..42 such that sqr[i] = i² 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.

$r m S t a t e^{'} = [s \in R M \mapsto IF s = r THEN " prepared " ELSE r m S t a t e [s]]$