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

如何解决TLA+ 错误：不变的不变量不是状态谓词

在我的规范中，我试图检查序列中的变化是 -1、0 还是 1。

我将这个不变量描述如下：

PVariance == Len(waitingRoomP') - Len(waitingRoomP) \in {-1,1}
CVariance == Len(waitingRoomC') - Len(waitingRoomC) \in {-1,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.

解决方法

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

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