7. 活性：终究要发生的事

“活性”（liveness）是“好事终究要发生”：比如“请求最终会完成”。它和不变式不一样，不能在单个状态上判断，要看一整条无限长的路。TLA+ 里用 <>P 表示“P 终究会成立”，[]P 表示“P 一直成立”，<>[]P 表示“从某一刻起 P 一直成立”。这种关于“时间先后”的公式叫“时序性质”（temporal property），在 cfg 里写成 PROPERTY，不是 INVARIANT。

例子：没有失败的按钮，我们希望它最终变成 done。

---- MODULE Eventually ----
\* 和 Button 一样，但没有失败。我们希望“最终一定成功”。
VARIABLE status

Init == status = "idle"
Click   == status = "idle"    /\ status' = "loading"
Succeed == status = "loading" /\ status' = "done"

Next == Click \/ Succeed
Spec == Init /\ [][Next]_status

EventuallyDone == <>(status = "done")
====

SPECIFICATION Spec
PROPERTY EventuallyDone
CHECK_DEADLOCK FALSE

stateDiagram-v2
  [*] --> idle
  idle --> loading: Click
  loading --> done: Succeed
  loading --> loading: 什么都不做(停住)

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

真实输出（确实失败了）：

Error: Temporal properties were violated.

Error: The following behavior constitutes a counter-example:

State 1: <Initial predicate>
status = "idle"

State 2: <Click line 6, col 12 to line 6, col 52 of module Eventually>
status = "loading"

State 3: Stuttering

“Stuttering” 直译是“结巴”，在这里指“原地踏步”：系统停在 loading，什么也不做，一直到永远。还记得 [][Next]_status 允许“什么都不变”的那一步吗？规格里没说 Succeed 一定会被执行，所以 TLC 认为“请求永远挂着”也是合法的行为，于是“最终成功”不成立。活性的反例是一个“套索”（lasso）：一段路，加上一个无限重复的结尾（这里是原地踏步）。

练习

练习 7.1：怎样让它通过？

答案：告诉 TLC“能做的事不能一直不做”，也就是下一节的公平。把 Spec 改成 Init /\ [][Next]_status /\ WF_status(Next)（配套文件 EventuallyFair.tla），真实输出：

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

练习 7.2：为什么不变式检查从来不会报 “Stuttering”？

答案：不变式只看每个状态本身，原地踏步不会产生新状态，所以不会让它出错。只有“终究要发生”的规则才会被“一直不动”打破。