Why is TLC reporting errors on valid states?

Question

I have the following specification for a queue:

------------------------------- MODULE queue -------------------------------
EXTENDS Naturals

CONSTANT L (* The fixed max length of the queue *)
VARIABLE q (* Represents the queue as the number of items in it *)
----------------------------------------------------------------------------
TypeInvariant == q >= 0 /\ q <= L
----------------------------------------------------------------------------
Init == q = 0

NoOp == q' = q (* Queue unchanged *)

Enqueue == q' = q + 1 (* Element added *)

Dequeue == q' = IF q = 0 THEN q ELSE q - 1 (* Element removed *)

Next == NoOp \/ Enqueue \/ Dequeue
----------------------------------------------------------------------------
Spec == Init /\ [][Next]_q
----------------------------------------------------------------------------
THEOREM Spec => TypeInvariant
============================================================================

When I run TLC with the following values for constants:

L <- 3

And these contraints:

INVARIANT
TypeInvariant

It reports these errors:

But the specification allows values in (0 .. L), so why is TLC reporting q=1, q=2, q=3, q=4 as invalid states?

---

The error trace output is the following:

<<
[
 _TEAction |-> [
   position |-> 1,
   name |-> "Initial predicate",
   location |-> "Unknown location"
 ],
q |-> 0
],
[
 _TEAction |-> [
   position |-> 2,
   name |-> "Enqueue",
   location |-> "line 18, col 12 to line 18, col 21 of module queue"
 ],
q |-> 1
],
[
 _TEAction |-> [
   position |-> 3,
   name |-> "Enqueue",
   location |-> "line 18, col 12 to line 18, col 21 of module queue"
 ],
q |-> 2
],
[
 _TEAction |-> [
   position |-> 4,
   name |-> "Enqueue",
   location |-> "line 18, col 12 to line 18, col 21 of module queue"
 ],
q |-> 3
],
[
 _TEAction |-> [
   position |-> 5,
   name |-> "Enqueue",
   location |-> "line 18, col 12 to line 18, col 21 of module queue"
 ],
q |-> 4
]
>>

How is one supposed to recognize those that are considered errors and those which are not from this trace? The interface shows no red light on q=0.

Answer 1

• A red cell indicates that the value of the variable changed in this state compared to its previous value (see https://tla.msr-inria.inria.fr/tlatoolbox/doc/model/executing-tlc.html). Red does not indicate that states are not valid!
• The prefix of an (infinite) behavior -reported by the trace explorer as an error trace- does not satisfy the (safety) property TypeInvariant because TypeInvariant does not allow q=4.

By the way, the TLA+ group is a much better place to ask questions.