specificationsformal-verificationtla+tlc

Why is TLC reporting errors on valid states?

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

enter image description here

It reports these errors:

enter image description here

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.

Solution

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