6. 不变式：绝不能发生的事

“不变式”（invariant）是一条在每个状态都必须成立的规则，也叫“安全性”（safety）规则：坏事绝不能发生。TLC 每走到一个状态就检查一次；只要有一个状态不成立，它就停下，打印从起点到这个坏状态的完整路径，这条路径叫“反例”或“轨迹”（trace）。

例子：两个标签页登录。每个页面先“看”有没有会话（Check），再“建”（Create）。这两步之间，另一个页面可以插进来。这个规格是故意写坏的。

---- MODULE Login ----
\* 两个标签页同时登录。每个标签页先“看”有没有会话，再“建”会话。
\* 看和建是两步，中间可以被另一个标签页插进来。
EXTENDS Naturals
VARIABLES sessions, seen, pc
vars == <<sessions, seen, pc>>
Tabs == {"t1", "t2"}

Init == /\ sessions = 0
        /\ seen = [t \in Tabs |-> 0]
        /\ pc = [t \in Tabs |-> "start"]

Check(t) == /\ pc[t] = "start"
            /\ seen' = [seen EXCEPT ![t] = sessions]
            /\ pc' = [pc EXCEPT ![t] = "checked"]
            /\ UNCHANGED sessions

Create(t) == /\ pc[t] = "checked"
             /\ sessions' = IF seen[t] = 0 THEN sessions + 1 ELSE sessions
             /\ pc' = [pc EXCEPT ![t] = "done"]
             /\ UNCHANGED seen

Next == \E t \in Tabs : Check(t) \/ Create(t)
Spec == Init /\ [][Next]_vars

\* 绝不允许出现两个会话
AtMostOneSession == sessions <= 1
====

SPECIFICATION Spec
INVARIANT AtMostOneSession
CHECK_DEADLOCK FALSE

pc 记录每个页面走到哪一步（start、checked、done），seen 记录它当时看到的会话数。

stateDiagram-v2
  [*] --> S1: 会话0, 两页都没开始
  S1 --> S2: t1 看(看到0)
  S2 --> S3: t2 看(也看到0)
  S3 --> S4: t1 建, 会话=1
  S4 --> S5: t2 建, 会话=2 (违反)

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

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

Error: Invariant AtMostOneSession is violated.
Error: The behavior up to this point is:
State 1: <Initial predicate>
/\ seen = [t1 |-> 0, t2 |-> 0]
/\ sessions = 0
/\ pc = [t1 |-> "start", t2 |-> "start"]

State 2: <Check line 13, col 13 to line 16, col 33 of module Login>
/\ seen = [t1 |-> 0, t2 |-> 0]
/\ sessions = 0
/\ pc = [t1 |-> "checked", t2 |-> "start"]

State 3: <Check line 13, col 13 to line 16, col 33 of module Login>
/\ seen = [t1 |-> 0, t2 |-> 0]
/\ sessions = 0
/\ pc = [t1 |-> "checked", t2 |-> "checked"]

State 4: <Create line 18, col 14 to line 21, col 30 of module Login>
/\ seen = [t1 |-> 0, t2 |-> 0]
/\ sessions = 1
/\ pc = [t1 |-> "done", t2 |-> "checked"]

State 5: <Create line 18, col 14 to line 21, col 30 of module Login>
/\ seen = [t1 |-> 0, t2 |-> 0]
/\ sessions = 2
/\ pc = [t1 |-> "done", t2 |-> "done"]

13 states generated, 12 distinct states found, 3 states left on queue.

读这条轨迹：State 2 里 t1 看到 0 个会话；State 3 里 t2 也看到 0；然后两边都去建，最后 sessions = 2。这就是前端常说的“先检查再操作”（check-then-act）竞态，和两个 tab 同时读 localStorage 是同一类问题。

练习

练习 6.1：怎么修？

答案：把“看”和“建”合成不可打断的一步（比如交给服务端用一个原子操作完成，或用 Web Locks 这类锁）。配套文件里的 LoginFixed.tla 只用一个动作：

Login(t) == /\ pc[t] = "start"
            /\ sessions' = IF sessions = 0 THEN 1 ELSE sessions
            /\ pc' = [pc EXCEPT ![t] = "done"]

真实输出：

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

练习 6.2：TLC 一共只找到 12 个状态就停了，为什么还剩 “3 states left on queue”？

答案：找到第一个坏状态它就停了，队列里还有没来得及检查的状态。安全性错误不需要把整张图走完。