10. VIEW 为什么也会

VIEW 是另一个省时间的选项：你给 TLC 一个表达式，TLC 只用它的值来判断“两个状态是否相同”，其他变量都不看。常用来忽略计数器、日志这类不影响逻辑的变量。

例子：轮询 3 次后隐藏 spinner。x 是 spinner（1 显示，0 隐藏），tick 是计数。我们希望 spinner 最终一直隐藏。这个规格本身是对的。

---- MODULE Poll ----
\* 轮询 3 次后关掉加载指示。x 是 spinner（1 显示，0 隐藏），tick 是计数。
EXTENDS Naturals
VARIABLES x, tick
vars == <<x, tick>>
Init == x = 0 /\ tick = 0
Tick == tick < 3 /\ tick' = tick + 1 /\ x' = IF tick = 2 THEN 0 ELSE 1
Next == Tick
Spec == Init /\ [][Next]_vars /\ WF_vars(Next)
OnlyX == x
EndsHidden == <>[](x = 0)
====

# PollView.cfg（带 VIEW）
SPECIFICATION Spec
PROPERTY EndsHidden
VIEW OnlyX
CHECK_DEADLOCK FALSE

# Poll.cfg：同上，只是删掉 VIEW OnlyX 这一行

stateDiagram-v2
  [*] --> s0: x=0 tick=0
  s0 --> s1: Tick, x=1 tick=1
  s1 --> s2: Tick, x=1 tick=2
  s2 --> s3: Tick, x=0 tick=3

带 VIEW（只看 x）：

java -cp tla2tools.jar tlc2.TLC -config PollView.cfg Poll.tla

Error: Temporal properties were violated.

Error: The following behavior constitutes a counter-example:

State 1: <Initial predicate>
/\ x = 0
/\ tick = 0

State 2: <Tick line 7, col 9 to line 7, col 70 of module Poll>
/\ x = 1
/\ tick = 1

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

不带 VIEW：

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

Model checking completed. No error has been found.
4 states generated, 4 distinct states found, 0 states left on queue.

机制：只看 x 时，(x=1, tick=1) 和 (x=1, tick=2) 被当成同一个状态，所以 TLC 只看到 2 个状态。它以为系统可以一直停在 x=1，于是报了一个不存在的错误。和 SYMMETRY 相反，这里是“误报”而不是“漏报”，而且这次 TLC 没有打印任何警告。所以压缩状态的选项既可能让 TLC 漏报，也可能让它误报。教训一样：查活性时，去掉 VIEW。

说明：报告里显示 “State 3: Stuttering” 而不是循环，是我对 TLC 内部如何拼接反例的观察结果，具体原因我没有在源码层面核实。

练习

练习 10.1：带 VIEW 的那次，TLC 报的是漏报还是误报？

答案：误报。规格真实行为是 tick 到 3 后 x=0 并停住，规则成立；不带 VIEW 的运行给出了 “No error”。

练习 10.2：什么时候 VIEW 是安全的？

答案：被忽略的变量既不影响以后能做哪些动作，也不出现在你要检查的规则里。这里 tick 决定了 Tick 还能不能做，所以不能忽略。