2

In my spec, I'm trying to check if a change in a sequence is either -1, 0 or 1.

I described this invariant as below :


PVariance == Len(waitingRoomP') - Len(waitingRoomP) \in {-1,0,1}
CVariance == Len(waitingRoomC') - Len(waitingRoomC) \in {-1,0,1}

Invariants ==
    /\ TypeInv
    /\ \/ PVariance 
       \/ CVariance

The TLC model checker outputs this :

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.
devio
  • 1,147
  • 5
  • 15
  • 41

1 Answers1

3

waitingRoomP' is the value of waitingRoomP in the next state, meaning PVariance is now an action. Invariants can't be actions, they can only be "pure" operators.

You can instead check PVariance as an action property by writing [][PVariance]_waitingRoomP. This will need to be checked as a temporal property in the toolbox, not an invariant.

Hovercouch
  • 1,962
  • 12
  • 12