TLA+的Next中计算法AND操作符的算法如下
C /\ (\E i \in S : D(i) /\ E)；
计算过程是：
- 计算C
- 如果C为TRUE，把后边的\E i \in S : D(i) /\ E 根据S中的元素i拆分成多个表达式D(i) /\ E;
- 计算D(i) /\ E时，应用同样的规则，先计算D(i)
- 如果D(i)为TRUE，计算E
一个例子
------------------------------ MODULE TestAnd ------------------------------ EXTENDS Naturals, TLC VARIABLES wall, small, big S == <<wall, small, big>> Init == /\ Print("Init", TRUE) /\ wall = 0 /\ small = 0 /\ big = 0 /\ Print(S, TRUE) TypeOK == /\ Print("TypeOK", TRUE) /\ Print(S, TRUE) /\ wall \in 0..30 /\ small \in 0..10 /\ big \in 0..10 Tick == /\ Print("Tick", TRUE) /\ wall' = wall + 1 \* /\ UNCHANGED <<small, big>> /\ Print(S, TRUE) IncreSmall == /\ Print("IncreSmall", TRUE) /\ small' = small + 1 /\ UNCHANGED <<big>> IncreBig == /\ Print("IncreBig", TRUE) /\ big' = big + 2 /\ UNCHANGED <<small>> Next == /\ Tick /\ \/ IncreSmall \/ IncreBig ============================================================================= \* Modification History \* Last modified Wed Jul 18 16:36:02 CST 2018 by max \* Created Wed Apr 25 21:42:59 CST 2018 by max ============================================================================= \* Modification History \* Created Wed Jul 18 16:13:54 CST 2018 by max
debug信息如下：
======================== 这是第1轮 ======================== ==== 初始状态是<<0, 0>> ”Init" TRUE <<0, 0, 0>> TRUE "TypeOK" TRUE <<0, 0, 0>> TRUE 得到新状态<<0, 0, 0>> 第1轮总结：本轮新增状态<<0, 0, 0>> ======================== 开始第2轮 ======================== ==== 2.1 从sq中取出第一个状态<<0, 0, 0>>，开始计算Next ====计算AND操作符 "Tick" TRUE <<0, 0, 0>> TRUE ====如果Tick为TRUE，则进入IncreSmall，IncreBig========== "IncreSmall" TRUE "IncreBig" TRUE "TypeOK" TRUE <<1, 1, 0>> TRUE 通过Tick + IncreSmall得到新状态<<1, 1, 0>> "TypeOK" TRUE <<1, 0, 2>> TRUE 通过Tick + IncreBig得到新状态<<1, 0, 2>> ======================== 开始第3轮 ======================== ==== 3.1 从sq中取出第1个状态<<1, 1, 0>>，开始计算Next ====计算AND操作符 "Tick" TRUE <<1, 1, 0>> TRUE ============如果Tick为TRUE，则进入IncreSmall，IncreBig========== "IncreSmall" TRUE "IncreBig" TRUE "TypeOK" TRUE <<2, 2, 0>> TRUE 通过Tick + IncreSmall得到新状态<<2, 2, 0>> "TypeOK" TRUE <<2, 1, 2>> TRUE 通过Tick + IncreBig得到新状态<<2, 1, 2>> ==== 3.2 从sq中取出第2个状态<<1, 0, 2>>，开始计算Next ====计算AND操作符 "Tick" TRUE <<1, 0, 2>> TRUE ============如果Tick为TRUE，则进入IncreSmall，IncreBig========== "IncreSmall" TRUE "IncreBig" TRUE "TypeOK" TRUE <<2, 0, 4>> TRUE 通过Tick + IncreSmall得到新状态<<2, 0, 4>> "Tick" TRUE <<2, 2, 0>> TRUE 通过Tick + IncreBig得到新状态<<2, 2, 0>> ...
关于UNCHANGED
上面例子中如果在Tick中指定 UNCHANGED <<small, big>>
Tick == /\ Print("Tick", TRUE) /\ wall' = wall + 1 /\ UNCHANGED <<small, big>> /\ Print(S, TRUE) Next == /\ Tick /\ \/ IncreSmall \/ IncreBig
由于Next中Tick后面的IncreSmall和IncreBig其实是修改了small或者big的，那么计算Tick为TRUE后Tick /\ IncreSmall 和 Tick /\ IncreBig 就是False了，那么整个Next就不进行任何计算了。
因此，在Next中如果包含有AND运算符，那么一定要把UNCHANGED维护好。我的建议是：AND前面的子表达式只维护自己的变量，AND后面的子表达式不维护前面的子表达式的变量。