4. 动作

“动作”是一步变化：在什么条件下，变量从什么变成什么。还是上面的 Button，Click、Succeed、Fail、Reset 就是 4 个动作。

写法	含义
status = "idle"	条件（守卫）：只有现在是 idle 才能点
status' = "loading"	带撇号 ’ 的是“下一刻”的值
/\	“并且”，像 JS 的 &&
\/	“或者”，像 JS 的 ||
Next	所有动作的“或”：每一步从中挑一个能做的
[][Next]_status	每一步要么是 Next 里的某个动作，要么什么都不变（原地踏步）

把它想成一个 reducer：Next 是所有 case，守卫就是 if (state.status === "idle")。区别是 TLA+ 不需要有人 dispatch，只要条件成立，这个动作就“可以发生”，TLC 会把每种可以发生的情况都试。

“死锁”（deadlock）指走到一个状态后，没有任何动作能做。在按钮里，done 之后没有动作。如果把 cfg 里的 CHECK_DEADLOCK FALSE 删掉，就会看到下面的真实输出（配置文件是 ButtonDeadlock.cfg）：

java -cp tla2tools.jar tlc2.TLC -config ButtonDeadlock.cfg Button.tla

Error: Deadlock reached.
State 1: <Initial predicate>
status = "idle"
State 2: <Click line 7, col 12 to line 7, col 52 of module Button>
status = "loading"
State 3: <Succeed line 8, col 12 to line 8, col 49 of module Button>
status = "done"

这里 done 本来就是终点，不算 bug，所以前面的例子都把死锁检查关了。

练习

练习 4.1：想让成功后还能再点一次，该加什么动作？

答案：Again == status = "done" /\ status' = "idle"，再把它加进 Next。这样 done 之后有动作可做，就不会再报死锁。

练习 4.2：Click == status' = "loading"（去掉守卫）意味着什么？

答案：任何时候都能点，包括已经在 loading 时，相当于按钮没有 disabled。状态数不变，但图里每个状态都会多一条通往 loading 的线。