我们能在 TLA⁺ 中表达可达性属性吗？

# TLA+ 中能否表达可达性属性？ 来源：https://ahelwer.ca/post/2026-09-26-reachability/ 我阅读了 Hillel Wayne 的新文章《*TLA+ 无法解决一切*》（https://www.linkedin.com/pulse/tla-wont-solve-everything-hillel-wayne-3edyc/），并对他提到的 TLA+ 无法表达的某些内容产生了执念： > 可能性与可达性属性：即即使你实际上未决定执行，也总有可能让 P 成真。例如“我总可以关闭计算机”或“用户总能更改他们的密码”。这些无法用 <\>P 来表达，因为那意味着“对于所有行为，P 至少发生一次”，而我们实际需要的是“对于所有行为前缀，都存在至少一个行为，其中 P 至少发生一次”。 这引发了我思考。前阵子我在阅读 Lamport 的新书《*并发程序科学*》（https://lamport.azurewebsites.net/tla/science-book.html），进展顺利直到被第 5.1 节《*可能性与准确性*》彻底难倒。该节正是讨论这个话题：如何在 TLA+ 中表达可能性/可达性属性。我当时完全无法理解，甚至认为文中存在重大错误。Hillel 的文章激励我重新研究（https://ahelwer.ca/post/2026-09-26-reachability/#fn:1），我很高兴现在基本理解了，并将尝试用自认为合理的方式进行解释。如果你更想让 Lamport 本人讲解，请阅读上述教材的第 5.1 节或 Lamport 1998 年 10 月的论文《*证明可能性属性*》（https://lamport.azurewebsites.net/pubs/lamport-possibility.pdf）。 我们将探讨两个问题： 1. 能否在 TLA+ 中使用有穷状态模型检查器 TLC 来检验可达性属性？（可以，绝对可以，但需要对 TLC 进行修改） 2. 可达性属性在 TLA+ 语义中是否真的合理，还是某种侵入线性时态逻辑的丑陋分支时态逻辑？（令人惊讶的是，它是合理的！） ## TLA+ 已具备可达性属性——某种程度上！ TLA+ 中一个更突出（且奇怪²）的运算符是 `ENABLED`。在给定状态下，若操作 `A` 可在该状态下执行，则 `ENABLED A` 的求值为真。最常见的应用是检查 `[]ENABLED Next`。这表示你的系统始终有可能采取下一个非停机步骤。若此属性曾为假，则说明你的系统发生了死锁！这是一个非常有用的属性，以至于 TLC 默认会进行检查。³ `ENABLED` 也能让你编写最基本的可达性属性，即询问是否有可能在*单一步骤*内达到某个状态。属性 `[](ENABLED Next /\ P')` 检查你是否总能在一步内达到状态 `P`。TLC 目前会检查此属性。然而，它并不十分有用。我们通常想知道 `P` 是否能在*多个步骤*内达到。Lamport 定义了另一个运算符，他用上标加号 `+` 来书写。⁴ 其含义对任何熟悉正则表达式的人来说都很熟悉：它表示一个或多个操作可以串联。因此 Lamport 将完整的可达性属性表达为 `[](ENABLED [Next]_v^+ /\ P')`，意味着一个或多个 `Next` 步骤（或停机步骤）可被执行以达到 `P`，而不仅仅是一步。这个公式用 ASCII 表示相当难看，这里美化一下： $$ \\Box\\text{E}\(\[Next\]\_v^+ \\land P' \) $$ TLC *目前无法*检查此属性；它仅存在于 Lamport 的构想中。它看起来也颇像分支时态逻辑。异端！稍后详述。 ## TLC 当前及未来可检查的属性 除了 `ENABLED`，TLC 最近还添加了对基本可达性属性的支持（https://github.com/tlaplus/tlaplus/pull/1377）。这些仍处于测试阶段，因此你必须在模型文件中将其声明为 `_POSSIBLE P`。这并非检查从每个系统状态出发的可达性；而是检查 `P` 是否*可能*在任何时候满足，即是否存在从某个初始状态开始的行为满足它。你可以在此阅读其动机（https://github.com/tlaplus/tlaplus/issues/860#issue-2075413374），这主要是作为规范的“单元测试”⁵。在 TLC 常规的广度优先搜索中检查 `_POSSIBLE` 很简单：如果状态探索结束时从未遇到 `P`，则报告失败。最近还发现（https://github.com/tlaplus/tlaplus/issues/860#issuecomment-5655381578），`_POSSIBLE` 提供了一种更符合人体工程学的轨迹验证方式，因此它很可能会继续保留在语言中。 那么完全的可能/可达性属性呢？我们能否检查 `P` 是否从*每个*系统状态都可达？TLC *肯定能够*检查这些，但需要更多工作。值得庆幸的是，这项工作是为模型检查增加一个额外的独立过程，而不是与现有机制纠缠在一起，因此实现起来可能风险较小，不会破坏现有功能。要使用的算法称为*反向可达性*。在完整状态图被探索后，进行一次在状态图上*反向*的广度优先搜索，从每个满足 `P` 的状态开始，追溯所有*转换到*这些状态的状态。如果最后还有未探索的状态，那么你就知道 `P` 从那些状态不可达，因此报告违反。这些剩余状态甚至能提供一个很好的反例用于开始调试！ 这是否会在 TLC 中实现尚不可知，但似乎是个不错的主意。 ## 悄然引入分支时态推理 在这里，我将尽力解释 Lamport 设计的技巧，以将看似分支时态推理的东西引入线性时态逻辑。预先说明，本节的技术性将远高于其他部分。TLA+ 的语义从根本上将规范定义为无限线性行为的集合。这个行为集合本身通常也是无限的⁶。那么，在这个无限线性行为的无限集合中，当我们说 `REACHABLE P` 时，可能意味着什么？按照惯例，TLA+ 公式必须适用于此集合中的*每个*行为。但我们关心的并非每个行为是否实际到达 `P`；我们想知道的是每个行为*是否可能*到达 `P`！这种对未来可能情况的推测性推理在分支时态逻辑中非常常见，但对线性时态逻辑而言则很陌生。 根本技巧在于滥用公平性假设。公平性假设是一个谓词，你可以用它来过滤行为集合。以常见用法为例，一个只是静止不动（无限停机）的系统是传统 TLA+ 规范的一个完全有效行为，但并不有趣。因此，许多规范若想检查“系统最终达到目标状态”这样的活性属性，会使用诸如“如果某个操作持续可用，则最终必须被采取”的公平性假设来禁止那些无趣的行为。非正式地，我喜欢将公平性假设视为在规范中添加了洋流，广泛地将系统推向期望状态。你的系统仍可在整个状态空间中运行，但它无法永远停滞在某处，因为洋流会推动它走向更高效的行为。公平性假设通常用于编码系统的“理想路径”，例如发送网络消息最终成功之类的事情。 如果一个公平性假设*机器封闭*，那么它不会阻止系统拒绝有限行为，只会拒绝无限行为——例如拒绝那个静止不动、无限停机的行为⁷。更正式地说，如果公平性假设是机器封闭的，那么每个有限系统行为前缀*必须*能够以满足你公平性假设的方式扩展。用非术语来说，这意味着在行为的任何给定时刻，它都可以醒悟并说：“哦，糟糕，我忘了我需要满足公平性假设！”然后它可以执行一系列操作去满足它。行为永远不会在一个有限步骤序列之后达到无法挽回的境地。你可能已经注意到“有限前缀必须能以某种方式扩展以满足某事”的表述听起来有点像讨论推测性的未来执行！而这正是关键所在。 假设你想检查状态 \(P\) 是否从每个可能的系统状态都可达。如果这是真的，那么系统行为的一个子集将包含状态 \(P\)。实际上，一个子集将包含 \(P\) 无限多次。用 TLA+ 的术语来说，它们满足公式 \(\Box \Diamond P\)⁸。如果你能写一个机器封闭的公平性假设 \(F\)，它只接受非常有限的系统轨迹集合，且所有这些轨迹都满足 \(\Box \Diamond P\)，那么会怎样？那么，根据机器封闭的定义，规范的每个有限前缀都可以扩展为满足 \(\Box \Diamond P\)⁹。因此，规范接受的每个有限前缀都能到达 \(P\)！这就是 TLA+ 中语义有效的可达性属性！表示为： $$ \(Spec \space \land \space F\) \Rarr \Box \Diamond P $$ 这样，我们就把陈述“\(P\) 是否可由所有状态可达”的问题简化为寻找一个合适的公平性假设。持怀疑态度的读者可能有理由认为我在这个细节中塞进了不少东西。比如，确实，如果一个神奇的公平性假设从天而降，它既是机器封闭的，又 somehow 唯一地选出了满足 \(\Box \Diamond P\) 的轨迹，那么我想这是可行的。但我们有什么理由相信这样的公平性假设存在呢？对于任意规范，我们实际上又该如何推导它？ ## 构造公平性假设 首先我们应该给人们一个退出点。如果你只关心对有限状态系统进行可达性模型检查，我们已经证明可达性属性在 TLA+ 中是可行的！谈论可达性并不是 TLA+ 语义中某种无法弥补的断裂。去 TLA+ 邮件列表上吵着要为 TLC 添加可达性检查吧。本节的其余部分将只吸引那些想要形式化证明无限状态系统属性的怪胎。 重申一下，如果你想证明一个规范满足可达性属性 \(P\)，只需推导出一个机器封闭的公平性假设 \(F\)，使得： $$ \(Spec \space \land \space F\) \Rarr \Box \Diamond P $$ Lamport 在《*证明可能性属性*》（https://lamport.azurewebsites.net/pubs/lamport-possibility.pdf）中给出了 \(F\) 的一般化存在性构造，因此如果 \(P\) 确实*是*可达的，那么一个合适的公平性假设必须存在，但没有一种机械的方法来推导 \(F\)，使其易于在证明中推理；这需要创造力！ 让我们看一个例子。考虑一个单变量 \(x\) 的规范，它作为一个计数器，可以递增或递减： $$ Up ≜ x' = x + 1 $$ $$ Down ≜ \(x > 0\) \land x' = x - 1 $$ $$ Next ≜ Up \lor Down $$ $$ Spec ≜ \(x = 1\) \land \Box[Next]_x $$ 假设我们想证明 \(x = 0\) 总是可达的，这当然是可行的。我们能想出什么样的公平性假设 \(F\)，既能保证机器封闭又能确保 \(\Box \Diamond (x = 0)\)？ 我们的第一次尝试可能是保守而熟悉地采用 \(F = SF_x(Down)\)。任何由子操作的弱公平性或强公平性合取组成的公平性假设总是机器封闭的。然而，这是不够的。一个行为每执行两个 `Up` 步骤就执行一个 `Down` 步骤，这个行为满足此 \(F\)，却从未达到 \(x = 0\)： $$ 1 \rightarrow 2 \rightarrow 3 \rightarrow 2 \rightarrow 3 \rightarrow 4 \rightarrow 3 \rightarrow 4 \rightarrow 5 \rightarrow \ldots $$ 必须承认，我们不得不放弃通常构建机器封闭公平性假设的安全方法，并信任我们自己证明潜在公式是机器封闭的能力。沿着这个新方向的第二个好尝试是 \(F = \Diamond \Box [Down]_x\)：在某个时刻，行为说“不管了，我只递减”。这很有希望！如果它只递减，那么它将单调地朝向 \(x = 0\)！它也是机器封闭的，因为任何行为都可以在任何时候停下来并开始递减。不幸的是，它失败了，因为它允许永久停机： $$ 1 \rightarrow 1 \rightarrow 1 \rightarrow 1 \rightarrow 1 \rightarrow \ldots $$ 修复方法简单而熟悉：将其与 `Down` 的弱公平性合取： $$ F = \Diamond \Box [Down]_x \land WF_x(Down) $$ 这也是机器封闭的，并且它确实确保 \(\Box \Diamond (x = 0)\)。所以我们做到了！我们可以使用传统的活性证明技术¹⁰来证明从每个状态出发 \(x = 0\) 的可达性。 实际上，我们的例子暗示了一个更广泛的模式。为任意规范定义 \(F\)，一个不错的起点形式如下： $$ F = \Diamond \Box [A]_v \land SF_v(A) $$ 其中 \(A\) 是一个操作（不一定是 \(Next\) 的精确子操作），它会使系统中的每个状态都更接近 \(P\)。这样，任何行为都可以在任何时候抛下一切，直接朝向 \(P\) 前进。具体细节当然取决于你的规范。 ## 在最终一致性中的应用 在之前的一篇文章中（https://ahelwer.ca/post/2023-11-01-tla-finite-monotonic/），我写了一个最终一致性系统（一种无冲突复制数据类型）的模型。最终一致性系统有一个特性：每个副本总是会与其他副本稍有不同，但如果事务停止流动，所有副本保证最终会收敛到相同的系统视图。我当时没有意识到，这实际上是一个可达性属性！我们希望系统*能够*收敛，而不是它一定会收敛！我最终以一种笨拙的方式表达了这一点，通过一个人为的布尔标志，该标志可在任何时候触发以停止新事务，然后检查当标志为真时系统最终收敛。现在，利用上述关于在 TLA+ 中表达可达性属性的知识，这个标志本可以成为一个公平性假设！当时实际上有人建议过类似的做法（https://github.com/tlaplus/Examples/pull/97#discussion_r1802130732），尽管我当时并不理解。 所以实际上，TLC *确实*现在支持检查可达性属性，只要用户以 \((Spec \space \land \space F) \Rarr \Box \Diamond P\) 的形式表达它们！要求相当高，因为像我这样拥有十多年 TLA+ 经验的人，直到写这篇博客文章才理解这种方法。在 TLC 中将可达性检查作为独立功能实现，并采用反向可达性传递，将极大地提高易用性。 ## 讨论 - lobste.rs (https://lobste.rs/s/8pjbtj/can_we_have_reachability_properties_tla) - Mastodon (https://discuss.systems/@ahelwer/117338159798722923) - LinkedIn (https: