5. 模型检查：TLC 把每一种顺序都走一遍

“模型检查”就是：从起点出发，把每个状态下所有能做的动作都试一遍，得到新状态，再从新状态继续试，直到没有新状态为止。TLC 默认按“广度优先”的顺序做，也就是先走完所有 1 步能到的状态，再走 2 步能到的，以此类推。所以它找到的错误路径通常是最短的。

例子：两个标签页各点一次按钮，谁先谁后不知道。

---- MODULE TwoTabs ----
\* 两个标签页各自点一次按钮，先后顺序不定
VARIABLES a, b
vars == <<a, b>>

Init == a = "idle" /\ b = "idle"

ClickA == a = "idle" /\ a' = "clicked" /\ b' = b
ClickB == b = "idle" /\ b' = "clicked" /\ a' = a

Next == ClickA \/ ClickB
Spec == Init /\ [][Next]_vars
====

SPECIFICATION Spec
CHECK_DEADLOCK FALSE

stateDiagram-v2
  [*] --> 都没点
  都没点 --> 只有A点了: ClickA
  都没点 --> 只有B点了: ClickB
  只有A点了 --> 都点了: ClickB
  只有B点了 --> 都点了: ClickA

java -cp tla2tools.jar tlc2.TLC -config TwoTabs.cfg TwoTabs.tla

Model checking completed. No error has been found.
5 states generated, 4 distinct states found, 0 states left on queue.
The depth of the complete state graph search is 3.

TLC 找到 4 个状态，正好是图里的 4 个格子。“depth 3” 指最长要走 3 层（起点算第 1 层）。注意 ClickA 里写了 b' = b：TLA+ 里没写到的变量下一刻可以是任何值，所以每个动作都要说清楚其他变量不变。UNCHANGED b 是同样的意思。

练习

练习 5.1：换成 3 个标签页，每个点一次，会有几个状态？

答案：每个页面“点了/没点”两种，2 × 2 × 2 = 8 个。N 个页面就是 2 的 N 次方，这就是“状态爆炸”：变量一多，状态数长得非常快。（这道是算出来的，没有跑。）

练习 5.2：如果 ClickA 里忘了写 b' = b，会怎样？

答案：b 的下一刻值就没有约束，TLC 会直接报错，不会乱猜。我实际跑过，真实输出：Error: Successor state is not completely specified by action ClickA of the next-state relation. The following variable is not assigned: b.