3. 状态

“状态”就是某一刻所有变量的取值，相当于 React 里某一刻 state 的完整快照。这个按钮只有一个变量 status，它能取 4 个值，所以最多有 4 个状态。

---- MODULE Button ----
\* 一个提交按钮：空闲 -> 加载中 -> 成功 或 失败
VARIABLE status

Init == status = "idle"

Click   == status = "idle"    /\ status' = "loading"
Succeed == status = "loading" /\ status' = "done"
Fail    == status = "loading" /\ status' = "error"
Reset   == status = "error"   /\ status' = "idle"

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

TypeOK == status \in {"idle", "loading", "done", "error"}
====

SPECIFICATION Spec
INVARIANT TypeOK
CHECK_DEADLOCK FALSE

读法：Init 是起点（status 一开始是 “idle”）。TypeOK 是一条检查：status 永远只能是这 4 个值之一。CHECK_DEADLOCK FALSE 先关掉“死锁”检查，第 4 节会解释。

Mermaid 状态图（可以贴到任何支持 Mermaid 的地方，比如 GitHub 的 Markdown）：

stateDiagram-v2
  [*] --> idle
  idle --> loading: Click
  loading --> done: Succeed
  loading --> error: Fail
  error --> idle: Reset

命令：

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

真实输出：

Model checking completed. No error has been found.
5 states generated, 4 distinct states found, 0 states left on queue.
The depth of the complete state graph search is 3.

“4 distinct states found” 就是 4 个不同的状态：idle、loading、done、error。“5 states generated” 比 4 多，是因为有一条路（error 再回到 idle）走到了已经见过的状态，TLC 不会重复存它。

练习

练习 3.1：如果再加一个变量 retries，取值 0、1、2，最多有几个状态？

答案：最多 4 × 3 = 12 个。状态是所有变量取值的组合，实际能走到的可能更少。

练习 3.2：把 TypeOK 改成 status \in {"idle", "loading", "done"}（漏掉 "error"），TLC 会怎样？

答案：它会报 Invariant TypeOK is violated，并给出 idle → loading → error 这条路。我实际跑过这个改动，真实输出的第一行是 Error: Invariant TypeOK is violated.，轨迹正是 idle、loading、error。