TLA+ error : The invariant Invariants is not a state predicate
TLA+ error : The invariant Invariants is not a state predicate
在我的规范中,我试图检查序列中的变化是 -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
现在是一个动作。不变量不能是动作,它们只能是“纯”运算符。
您可以通过编写 [][PVariance]_waitingRoomP
来检查 PVariance
作为一个动作 属性。这需要在工具箱中作为时间 属性 检查,而不是不变量。
在我的规范中,我试图检查序列中的变化是 -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
现在是一个动作。不变量不能是动作,它们只能是“纯”运算符。
您可以通过编写 [][PVariance]_waitingRoomP
来检查 PVariance
作为一个动作 属性。这需要在工具箱中作为时间 属性 检查,而不是不变量。