跳转到内容
learning

11. 回到 pstack：statechart 技能和 PickWorker

pstack 的 statechart 技能，用白话说就是一个“自动跑 TLC 并画图”的流程：

  1. 跑 TLC。 用固定参数 -workers 1 -fp 0 -lncheck final，保证每次结果一样。
  2. 删掉坏规则再跑。 有规则被打破时，记下它的反例，把它从配置里拿掉再跑，看剩下的规则是否成立。第一次出错后，每次重跑最多走 100,000 个不同状态。
  3. 画 Mermaid 图。 状态不超过 500 个时画完整状态图，写进 chart.mmd；可以用一个“视图模块”把 TLA+ 状态换成读者看得懂的名字。
  4. 写报告。 report.md 写哪些规则成立、哪些被打破，原始输出留在 tlc.out。

PickWorker 是它测试集里的一个例子，结构和第 9 节的 Leader 完全一样：从两个 worker 里选一个，规则是“终究会选到 w1”。

---- MODULE PickWorker ----
EXTENDS TLC
CONSTANTS Workers, First
VARIABLE picked
Init == picked = {}
Pick(w) == picked = {} /\ picked' = {w}
Next == \E w \in Workers : Pick(w)
Spec == Init /\ [][Next]_picked /\ WF_picked(Next)
Perms == Permutations(Workers)
PicksFirst == <>(First \in picked)
====

带 SYMMETRY（测试集原样的 PickWorker.cfg）：

终端窗口
java -cp tla2tools.jar tlc2.TLC -config PickWorker.cfg PickWorker.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（NoSym.cfg，只删了那一行）：

终端窗口
java -cp tla2tools.jar tlc2.TLC -config NoSym.cfg PickWorker.tla
Error: Temporal properties were violated.
State 1: <Initial predicate>
picked = {}
State 2: <Pick ...>
picked = {w2}
State 3: Stuttering
3 states generated, 3 distinct states found, 0 states left on queue.

发现是什么：TLC 带着 SYMMETRY 说“没错误”，同时打了警告。statechart 的报告只保留结论，丢掉了这行警告，于是 report.md 把 PicksFirst 列在“成立的规则”里。去掉 SYMMETRY 就能看到真相：选到 w2 时，w1 永远不会被选上。我上次查看 GitHub main 分支时，那份报告仍写着 “Rules that hold PicksFirst”；之后是否修改，未知。

对你的意义：读 statechart 报告时，如果配置里有 SYMMETRY 或 VIEW，又有 PROPERTY（活性），把这两项去掉再跑一次，或直接看 tlc.out 里有没有那行 Warning。

练习

Section titled “练习”
练习 11.1：为什么带 SYMMETRY 时只有 2 个状态？

答案：{w1} 和 {w2} 被当成同一个状态，只剩“还没选”和“选了一个”。

练习 11.2：如果要修这个技能，最小的改动是什么？

答案：一种做法是在 report.md 里原样保留 TLC 的 Warning；更稳的是：检查活性规则时自动去掉 SYMMETRY 和 VIEW 再跑。这是我的建议，不是 pstack 已有的行为。

本课进度：