Ошибка 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. Это нужно будет проверить как временное свойство в наборе инструментов, а не как инвариант.