私の仕様では、シーケンスの変更が -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.