TLA+错误:不变量不变量不是状态谓词

Question

在我的规范中，我尝试检查序列中的更改是否为-1、0或1。

我对这个不变量的描述如下：

PVariance == Len(waitingRoomP') - Len(waitingRoomP) \in {-1,0,1}
CVariance == Len(waitingRoomC') - Len(waitingRoomC) \in {-1,0,1}

Invariants ==
    /\ TypeInv
    /\ \/ PVariance 
       \/ CVariance

TLC模型检查器输出以下内容：

The invariant Invariants is not a state predicate (one with no primes or temporal operators).
Note that a bug can cause TLC to incorrectly report this error.
If you believe your TLA+ or PlusCal specification to be correct,
please check if this bug described in LevelNode.java starting at line 590ff affects you.

Answer 1

waitingRoomP'是下一个状态下的waitingRoomP的值，这意味着PVariance现在是一个动作。不变量不能是动作，它们只能是“纯”运算符。

相反，您可以通过编写[][PVariance]_waitingRoomP将PVariance作为操作属性进行检查。这将需要在工具箱中作为时态属性进行检查，而不是不变量。