用状态机组合 TLA+ 规约
原文由 Hillel Wayne 于 发布，订阅该博客
去年一位客户找我解决一个问题：他们希望把两个大型的 TLA+ 规约组合起来，作为更大系统的一部分。通常并不推荐这样做，而是应该把两个系统硬编码到同一个大型规约里，但这两个规约都异常庞大，各自又有大量内部不变式。他们需要一种能够独立开发两个规约，再以最小代价集成起来的办法。
这就是我想出的方案。提醒一下：这是一套面向进阶 TLA+ 用户的复杂方案。如果你想要更（非常）平易近人的入门介绍，可以看看我的网站 learntla。
示例
先来看一个用于说明问题的系统：Worker 向 Server 发送认证请求。如果密码与 Server 内部的密码一致，Server 就返回“valid”，否则返回“invalid”。如果 Worker 收到“invalid”，就会进入错误状态。处于该状态时，Worker 可以重试并提交新的认证请求。
Worker 和 Server 通过请求/响应共享状态。为了增加一点复杂性，我们还会给 Server 加上内部状态——一个对 Worker 不可见的请求日志。
我们可以用这个例子来展示组合时会遇到的问题以及我的解法（不过我得说，这个例子其实有点过于简单，还不足以体现这种做法的真正价值）。
组合的问题
我们理想中的组合应该尽可能简单、无痛。如果已有规约是 WorkerSpec 和 ServerSpec，最简单的组合方式无非就是
CombinedSpec == WorkerSpec /\ ServerSpec我在这里深入讨论过其中的问题，核心在于：如果 ServerSpec 和 WorkerSpec 都是“常规”规约，它们会对共享变量施加相互矛盾的约束。
例如，WorkerSpec 很可能会读取 Server 的响应，但不会去修改它。因此，为了让 WorkerSpec 能独立于组合单独运行，我们不得不声明响应永远不会改变——这就等同于说我们不能修改它，从而导致 ServerSpec 根本无法发送响应！
常规的变通方法是把 WorkerSpec 和 ServerSpec 都拆成一组组动作，再以互不矛盾的方式小心地缝合在一起。听起来有多复杂，做起来就有多复杂：组合两个规约的工作量，可能跟从头编写它们相当。
这正是我想要寻找更好办法的原因。
核心思路
我们需要做的是：先编写只描述“世界一部分”的规约，再把它们纳入代表“完整世界”的主规约中。为此，我们要利用 TLA+ 最强大的特性之一：我们可以用 x' 来同时为 x 赋下一个状态的值并约束下一个状态的值可以是什么。比如我们有
VARIABLE x, y
Foo ==
/\ x' \in {0, 1}
/\ y' \in {0, 1}
Bar == x' < y'
Next == Foo /\ Bar当 TLC 求值 Next 时，它会把 Foo 中的 x' 和 y' 当作赋值来处理。共有四种可能的赋值，模型检查器会全部尝试。
接着，由于 x' 和 y' 已经选定，TLC 就会把 Bar 中的语句当作约束来解读。四种可能中有三种违背了该约束，于是被 TLC 排除，最终只剩下一个合法的后继状态。
这意味着，规约 Q 可以把 X 和 Y 两个规约拿来，让它们相互制约。X 可以有一个将 x_log 加一的动作 Inc，然后 Q 规定只有当 y_flag 为真时 Inc 才能发生。同样，Q 还可以让一次赋值触发另一次赋值：
Inc ==
/\ x_log' = x_log + 1
Sync ==
IF ~y_flag /\ y_flag'
THEN Inc
ELSE TRUE
Next == (X!Next \/ Y!Next) /\ Sync现在，把 y_flag 置为真就会强制触发 x_log 的递增。Q 正在利用一个规约去驱动系统中另一个规约的副作用。
这本质上就是一个状态机！转移上的约束就是守卫条件，转移上的赋值就是效果。这些都可以施加到状态机本身并不知晓的其他规约之上。
在实践中让这一想法落地的做法如下：
- 为核心组件的所有高层状态转移编写一个抽象状态机
- 将其他组件写成“开放式”规约，不完全描述它们的后继状态。
- 精化核心组件到主规约中，并通过
Sync动作给状态转移加上守卫和副作用。
解决方案
我们会用三个独立的规约来建模：workerSM.tla、server.tla 和 system.tla。
状态机
由于整个系统都围绕 Worker 的状态机展开，我们先从 workerSM.tla 开始。它并不描述 Worker 状态转移时发生了什么，只描述有哪些转移。
------------------- MODULE workerSM -------------------
EXTENDS Integers
VARIABLES state
Transitions == {
[from |-> "init", to |-> "ready"]
, [from |-> "ready", to |-> "requesting"]
, [from |-> "requesting", to |-> "done"]
, [from |-> "requesting", to |-> "error"]
, [from |-> "error", to |-> "ready"]
}
Init == state = "init"
Valid(t) == state = t.from
ValidTransitions == {t \in Transitions: Valid(t)}
ValidOutcomes == {t.to : t \in ValidTransitions}
Done ==
state = "done"
Next ==
\E t \in ValidOutcomes:
state' = t
Fairness ==
/\ WF_state(Next)
/\ SF_state(state' = "done")
Spec == Init /\ [][Next]_state /\ Fairness
Liveness == <>Done
=========================================================Transitions 表示合法转移的集合。三个 Valid- 开头的算子只是辅助定义。加上它们是好习惯；大多数 TLA+ 规约的辅助定义都还不够多。
Fairness 约束看起来有点复杂，但它的意思其实很简单：我们不能总是从 requesting 转移到 error。如果进入该状态足够多次，最终一定会转到 done。
除此之外，这个规约没有对转移施加任何条件：转移到 done 并不需要“做任何事”。这部分工作要留给 system.tla 来完成。
显示 cfg
我用它来直接测试 Worker。
SPECIFICATION Spec
PROPERTY Liveness
CHECK_DEADLOCK FALSE检查通过，说明该规约保证了 <>Done。
接下来，是要与 Worker 集成的外部组件。
服务器
------------------- MODULE server -------------------
CONSTANTS Password, NULL
VARIABLE req, resp, log
internal == <<log>> \* (a)
external == <<req, resp>> \* (a)
vars == <<external, internal>> \* (a)
Init ==
/\ req = NULL
/\ resp = NULL
/\ log = {}
CheckRequest ==
/\ req # NULL
/\ log' = log \union {req}
/\ IF req = Password THEN
resp' = "valid"
ELSE
resp' = "invalid"
/\ req' = NULL
Next == \* (b)
CheckRequest
Spec == Init /\ [][Next]_internal \* (c)
====在这个规约里我们做了三件不寻常的事。第一，我们把变量分成了 internal 和 external 两组 (a)。external 变量代表与其他组合部分共享的状态，而 internal 只与 server 自身的属性相关。这里我们用 req 表示发往 Server 的请求，用 resp 表示响应。
第二，该规约会平凡地死锁 (b)。Next 中只有 CheckRequest 一个动作，而 CheckRequest 仅在 req 非空时才可执行，但规约本身没有任何地方会让 req 变为非空。这个规约不是“自包含”的，必须被另一个规约使用才有意义。
第三，Spec 仅对 internal 变量保持口吃不变性。这是通过写成 [][Next]_internal 而非 [][Next]_vars 来实现的 (c)。这是最容易被忽略的一点，但它会让后续的规约组合与规约精化都变得更简单。
现在我们把 Server 和 Worker 放在一起。
系统
这是目前为止最复杂的部分。我们先给出完整规约，再分段讲解最重要的部分。
系统规约
---- MODULE system ----
EXTENDS TLC, Integers, Sequences
CONSTANT NULL
VARIABLES ws \* worker state
, server_req \* requests to server
, server_resp \* server response
, server_log \* log (internal to server)
Strings == {"a", "b", "c"}
comm_vars == <<server_req, server_resp>>
vars == <<ws, server_log, comm_vars>>
Worker == INSTANCE workerSM WITH state <- ws
Server == INSTANCE server WITH
req <- server_req,
resp <- server_resp,
log <- server_log,
Password <- "a"
Sync ==
LET i == <<ws, ws'>> IN
/\ CASE
i = <<"ready", "requesting">> ->
/\ \E x \in Strings:
/\ server_req' = x
/\ server_resp' = NULL
[] i = <<"requesting", "error">> ->
/\ server_resp = "invalid"
/\ UNCHANGED comm_vars
[] i = <<"requesting", "done">> ->
/\ server_resp = "valid"
/\ UNCHANGED comm_vars
[] OTHER -> UNCHANGED comm_vars
Init ==
/\ Worker!Init
/\ Server!Init
Done == \* No deadlock on finish
/\ Worker!Done
/\ UNCHANGED vars
ServerNext ==
/\ Server!Next
/\ UNCHANGED ws
WorkerNext ==
/\ Worker!Next
/\ Sync
/\ UNCHANGED server_log
Next ==
\/ WorkerNext
\/ ServerNext
\/ Done
Fairness ==
/\ WF_vars(Next)
Spec == Init /\ [][Next]_vars /\ Fairness
RefinesServer == Server!Spec
RefinesWorker == Worker!Spec
====VARIABLES ws \* worker state
, server_req \* requests to server
, server_resp \* server response
, server_log \* log (internal to server)
Strings == {"a", "b", "c"}
comm_vars == <<server_req, server_resp>>
vars == <<ws, server_log, comm_vars>>我喜欢按用途和所属规约来分组 vars。由于 Server 和 Worker 都会用到 server_req 和 _resp，我把它们单独放进 comm_vars 一组。
Worker == INSTANCE workerSM WITH state <- ws
Server == INSTANCE server WITH
req <- server_req,
resp <- server_resp,
log <- server_log,
Password <- "a"出于教学方便，我把 Server 的 Password 常量硬编码了。我们不需要实例化 NULL 常量，因为它在 system.tla 和 server.tla 中同名，会自动传递。
Sync ==
\* See next section
Init ==
/\ Worker!Init
/\ Server!Init
ServerNext ==
/\ Server!Next
/\ UNCHANGED ws
WorkerNext ==
/\ Worker!Next
/\ Sync
/\ UNCHANGED server_log
Done == \* No deadlock on finish
/\ Worker!Done
/\ UNCHANGED vars
Next ==
\/ WorkerNext
\/ ServerNext
\/ DoneInit只是分别调用Worker!Init和Server!Init来初始化各自的变量。这里很简单，因为它们没有共享变量。如果存在两者共用的部分，或者system需要额外的簿记变量，我会在这里单独处理。ServerNext的意思就是“Server 可以自行处理状态更新”，同时考虑ws的口吃（因为每一步都必须给所有变量赋值）。Server 在系统中是独立活跃的，其行为并不同步依赖于 Worker。组合时并不总是能让各组件保持分离，但在可行时这样做会更方便。WorkerNext也是同理：它的行为独立于ServerNext。但“system”的作用正是在这里开始体现——体现在Sync中。
Sync
Sync 才是真正有意思的地方。
Sync ==
LET i == <<ws, ws'>> IN
CASE
i = <<"ready", "requesting">> ->
/\ \E x \in Strings:
server_req' = x
/\ server_resp' = NULL
[] i = <<"requesting", "error">> ->
/\ server_resp = "invalid"
/\ UNCHANGED comm_vars
[] i = <<"requesting", "done">> ->
/\ server_resp = "valid"
/\ UNCHANGED comm_vars
[] OTHER -> UNCHANGED comm_vars回顾前面的解释，带撇变量一旦被赋值，就可以在后面的表达式中作为约束使用。这意味着我们可以在一个动作中尝试一次转移，再在后面的动作里检验该转移是否合法。这正是让整套方案奏效的关键。如果没有这一点，我们就只能把守卫和副作用跟转移写在同一个动作里。例如，下面这行：
[] i = <<"requesting", "error">> ->
/\ server_resp = "invalid"
/\ UNCHANGED comm_vars我们把 requesting -> error 的转移约束为仅当 Server 响应为“invalid”时才可能发生。而这只有在 Server!Next 拒绝了密码时才会出现。但我们的 Worker 完全不需要知道这一点。我们可以独立开发两者，再依靠 Sync 来正确组合它们的行为。
我们也可以利用这一点来驱动系统中的副作用：
[] i = <<"ready", "requesting">> ->
/\ \E x \in Strings:
server_req' = x
/\ server_resp' = NULL这会让 ready -> requesting 的转移同时触发一个请求（并清空任何未处理的响应）。这随后会使 Server!CheckRequest 变为可执行，进而使 ServerNext 可执行，从而让 Server 能够对系统做出反应。
精化
别忘了，我们一开始引入整套机制，就是为了把两个复杂的规约组合在一起。我们必须确保组合方式不会违背其中任何一个规约自身的属性。这由下面几行来保证：
RefinesServer == Server!Spec
RefinesWorker == Worker!Spec这些是精化属性。粗略地说，它们检查 system.tla 不会让 Server 或 Worker 做出超出其原本能力范围的行为。例如，如果我们从 log 中删除了某些内容，该属性就会失败，因为这在 Server!Spec 中是不可能发生的。1
在 TLA+ 中，精化是可传递的。workerSM.tla 具有活性属性 <>Done。既然我已经在 workerSM.cfg 中验证过它，就不需要在 system.tla 中再测一次。如果 RefinesWorker 通过，那么 Worker!Liveness 也必然通过！
为何精化具有传递性
当我们测试 RefinesWorker 时，实际验证的是
Spec => Worker!Spec
(S) (WS)而通过对 workerSM.tla 的模型检查，我们已经知道
Worker!Spec => Worker!Liveness (2)
(WS) (WL)蕴涵具有传递性：如果 S => WS 且 WS => WL，那么 S => WL。
而目前它是失败的：
显示 cfg
SPECIFICATION Spec
CONSTANTS
NULL = NULL
PROPERTY
RefinesServer
RefinesWorker
问题在于 Worker 可能一直选错密码，导致 Server 不断拒绝，Worker 永远无法完成。一种修复方法是规定系统永不重试相同的密码：
Sync ==
\* ...
/\ \E x \in Strings:
/\ x \notin server_log
/\ server_req' = x这样规约就能通过了。如果你担心这会把 Server 的内部 log 泄露给 system，也可以给 Worker 同样加一个 log，无论是放在 system.tla 里，还是作为一个独立组件纳入 Sync 都可以。2 另一种修复方法是使用强公平约束：
Sync ==
\* ...
/\ \E x \in Strings:
/\ server_req' = x
Fairness ==
/\ WF_vars(Next)
/\ SF_vars(WorkerNext /\ server_req' = "a")它的意思是：如果“以发送正确密码的方式执行 WorkerNext”这件事始终最终是可行的，那么规约最终一定会这样执行。这能在不改变系统核心逻辑的前提下让规约通过。
封闭开放世界
最后一件事：让 server.tla 变得可模型检查。我们无法直接测试它，因为它不是一个“封闭”规约：它依赖其他规约来发送请求。对于更复杂的规约，我们希望能够独立于组合来测试其属性。
好在，这在 TLA+ 社区里已经是一个“已解决的问题”：把开放规约精化为封闭规约。我们通过一个新文件 MCserver.tla 来实现：
---- MODULE MCserver ----
EXTENDS TLC, server
Strings == {"a", "b", "c"}
ASSUME Password \in Strings
MCInit == Init
WorldNext ==
/\ \E x \in Strings:
req' = x
/\ UNCHANGED <<log, resp>>
MCNext ==
\/ Next
\/ WorldNext
MCSpec == MCInit /\ [][MCNext]_vars
====它为 Server 增加了一个可以发送请求的外部 World。现在我们就可以通过模型检查 MCserver.tla 来测试 server.tla 的行为。
显示 cfg
SPECIFICATION MCSpec
CONSTANT
NULL = NULL
Password = "b"如果你使用的是 VSCode TLA+ 插件的 nightly 版本，在 server.tla 上运行 “Check model with TLC” 命令会自动使用 MCserver.tla 来运行模型检查器。它还自带 TLA+ 调试器。VSCode 插件非常好用。
优点与缺点
这要做的工作可不少！那为什么不直接写一个大规约算了？
之所以要组合规约，就是为了能够独立地开发它们。当每个规约只有约 30 行时，这不算什么；但当它们各自都有 200 多行时，你就没法轻易把它们重写成一个规约了。
因此我们来把它和更常规的组合方式对比一下。我以 MongoDB Raft 组合为例，Murat Demirbas 在这里对其做了分析。独立的规约是 MongoStaticRaft 和 MongoLoglessDynamicRaft，它们在 MongoRaftReconfig 中被组合在一起。MongoStaticRaft 的 Next 如下所示：
\* MongoStaticRaft
Next ==
\* (a)
\/ \E s \in Server : ClientRequest(s)
\* etc
\* (b)
\/ \E s \in Server : \E Q \in Quorums(config[s]) : BecomeLeader(s, Q)
\* etc而组合后的 Next 则如下所示：
\* MongoRaftReconfig
Next ==
\/ OSMNext /\ UNCHANGED csmVars
\/ CSMNext /\ UNCHANGED osmVars
\/ JointNext
OSMNext ==
\* (a)
\/ \E s \in Server : OSM!ClientRequest(s)
\* etc
JointNext ==
\* (b)
\/ \E i \in Server : \E Q \in Quorums(config[i]) :
/\ OSM!BecomeLeader(i, Q)
/\ CSM!BecomeLeader(i, Q)
\* etc位于 (a) 下的动作必须在 OSMNext 中手动重复，而位于 (b) 下的动作则必须与另一个规约在 JointNext 中小心地交织在一起。这是组合两个规约的标准做法，需要集成的规约越多，难度就越大。在这种范式下也很难检验精化。
我试图通过基于 Sync 的方法同时避免这两个问题。每个组件都已有自己的 Next，可以不加修改地直接使用。任何影响共享变量的操作，都由额外的 Sync 算子来处理。
这个规约是否会从我的方法中受益？我也不确定。我设计这套方法是针对一个主“机器”与外部组件交互的场景，而在这里两个规约是平等的。我有一个转换后大致样子的草图，但不确定它是否一定更好。
改动草图
这是在不额外添加状态机的情况下的方案。挑选一个“主”规约，比如 CSM。那么 Spec 就变成
Next ==
\/ OSMNext
\/ CSMNext
OSMNext ==
/\ OSM!Next
/\ UNCHANGED <<csmVars>>
/\ UNCHANGED <<sharedVars>> \* new op
CSMNext ==
/\ CSM!Next
/\ Sync
/\ UNCHANGED <<osmVars>>我们需要在 OSMNext 中加入 sharedVars，这样它就不会自行调用 OSM!BecomeLeader——这必须通过 Sync 来发生。sharedVars 会与 csmVars 和 osmVars 共享部分变量。
Sync 会看起来和 JointNext 类似：
Sync ==
\/ \E i \in Server : \E Q \in Quorums(config[i]) :
/\ OSM!BecomeLeader(i, Q)
/\ CSM!BecomeLeader(i, Q)
\/ \* ...
\/ UNCHANGED <<sharedVars>>让我有点不爽的是，我们在 CSMNext 和 Sync 中都重复了 CSM!BecomeLeader，但这是确保 OSM 和 CSM 对 i 和 Q 使用相同取值最直接的方法。我也想过一些去重的方法，但都依赖于对 TLA+ 语义的创造性滥用。
我的判断是，常规组合适用于更广泛的场景，但在 Sync 适用的场景中，它更易于维护、可扩展性也更好。
两种方法都难以很好地处理“一对多”的情况。也就是你有一个针对单个 Worker 的规约，却想用它来扩展出 N 个 Worker，其中 N 是一个模型参数。我在文章 Using Abstract Data Types in TLA+ 中讨论过为什么这会如此困难。
结论
这是一项强大的技术，但也需要经验并会增加复杂度。如果你需要编写非常大型的规约，或是需要一套可复用的组件库，它就很合适。对于较小的规约，我还是推荐使用把所有组件放在同一个规约里的标准做法。
这套方法是为一位咨询客户开发的，效果非常好。我很兴奋能与大家分享！如果你喜欢这篇内容，可以在这里阅读其他进阶 TLA+ 技巧，比如如何让模型检查更快。
感谢 Murat Demirbas 和 Andrew Helwer 提供的反馈。如果你喜欢这篇文章，欢迎订阅我的 Newsletter！我每周都会在上面发布新文章。
我为企业提供形式化方法培训，让软件开发更快、更便宜、更安全。了解更多请点击这里。
附录：Sync 不使用带撇变量
一些公司的风格指南禁止在后续动作中将带撇变量用作表达式。在这种情况下，你可以用下面的方式达到同样的效果：
-Sync ==
- LET i == <<ws, ws'>> IN
+Sync(t) ==
+ LET i == <<t.from, t.to>> IN
+Do(t) ==
+ /\ ws = t.from
+ /\ ws' = t.to
WorkerNext ==
- /\ Worker!Next
- /\ Sync
+ /\ \E t \in Worker!ValidTransitions:
+ /\ Do(t)
+ /\ Sync(t)
/\ UNCHANGED server_logDo(t) 实际上只是在模拟 Worker!Next 的行为，区别在于它让我们能够“保存”所使用的转移并将其传入 Sync。
这对于保留传入动作的参数也很有用，而这在组合中有时是必需的。
评论
登录后参与讨论