在我的规范中，我试图检查序列中的更改是否为 -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.
最佳答案
waitingRoomP' 是 waitingRoomP 在下一个状态中的值，这意味着 PVariance 现在是一个操作。不变量不能是 Action ，它们只能是“纯”运算符。
您可以通过编写 [][PVariance]_waitingRoomP 将 PVariance 作为操作属性进行检查。这需要作为工具箱中的时间属性进行检查，而不是不变量。
关于specifications - TLA+错误: The invariant Invariants is not a state predicate，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/66464077/