9. SYMMETRY 为什么会骗过活性检查

SYMMETRY 是一个省时间的选项：你告诉 TLC“这几个值可以互换”，比如 t1 和 t2 两个标签页地位一样。TLC 就把“只是交换了名字”的状态当成同一个状态，只存一个代表。Permutations(Tabs) 表示 Tabs 里所有交换方式，它来自 EXTENDS TLC。

例子：两个标签页抢主标签页（leader），我们希望 t1 终究当上。这显然不对：t2 可能先抢到。

---- MODULE Leader ----
\* 两个标签页抢“主标签页”。我们希望 t1 最终当上主标签页。
EXTENDS TLC
CONSTANTS Tabs, First
VARIABLE leader

Init == leader = "none"
Pick(t) == leader = "none" /\ leader' = t
Next == \E t \in Tabs : Pick(t)
Spec == Init /\ [][Next]_leader /\ WF_leader(Next)

Perms == Permutations(Tabs)
FirstLeads == <>(leader = First)
====

# LeaderSym.cfg（带 SYMMETRY）
CONSTANTS Tabs = {t1, t2}
CONSTANTS First = t1
SPECIFICATION Spec
PROPERTY FirstLeads
SYMMETRY Perms
CHECK_DEADLOCK FALSE

# Leader.cfg：同上，只是删掉 SYMMETRY Perms 这一行

stateDiagram-v2
  [*] --> none
  none --> t1: Pick(t1)
  none --> t2: Pick(t2) 这条路 t1 永远当不上

带 SYMMETRY：

java -cp tla2tools.jar tlc2.TLC -config LeaderSym.cfg Leader.tla

Warning: Declaring symmetry during liveness checking is dangerous. It might cause TLC to miss violations of the stated liveness properties. Please check liveness without symmetry defined.
Model checking completed. No error has been found.
3 states generated, 2 distinct states found, 0 states left on queue.

不带 SYMMETRY：

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

Error: Temporal properties were violated.

Error: The following behavior constitutes a counter-example:

State 1: <Initial predicate>
leader = "none"

State 2: <Pick line 8, col 12 to line 8, col 41 of module Leader>
leader = t2

State 3: Stuttering
3 states generated, 3 distinct states found, 0 states left on queue.

真实的机制：带 SYMMETRY 时，TLC 认为 leader = t1 和 leader = t2 只是名字不同，于是只存了一个（2 个状态，而不带时是 3 个）。但我们的规则里点名了 t1（First = t1），t1 和 t2 对这条规则来说根本不一样。被合并掉的那条“t2 赢了”的路，正是反例。TLC 自己也知道风险，所以先打出那行 Warning：“在活性检查中声明对称很危险，可能漏掉违反，请不带对称再查一次。” 官方配置文档也写了“使用对称时不能检查活性性质”（见第 13 节的 docs.tlapl.us 链接）。

打个比方（只是帮助记忆，机制以上一段为准）：质检员只看“一张代表照片”来代表两个长得一样的盒子，可你要问的偏偏是“贴了 t1 标签的那个盒子”。

练习

练习 9.1：规则改成 <>(leader # "none")（终究有人当上），带 SYMMETRY 还危险吗？

答案：这条规则不点名任何一个标签页，交换 t1 和 t2 不改变它的真假，所以这里合并是安全的。但 TLC 仍会打印同样的警告，因为它不替你判断。稳妥的做法始终是：查活性时去掉 SYMMETRY。（推理结论，未单独运行。）

练习 9.2：只查不变式时能用 SYMMETRY 吗？

答案：可以，这正是它的主要用途，前提是不变式同样不点名某个具体的值。

本课进度：