我有以下队列规范：
------------------------------- 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
============================================================================
当我使用以下常量值运行 TLC 时：
L <- 3
还有这些限制：
INVARIANT
TypeInvariant
它报告这些错误：
但是规范允许 中的值(0 .. L)，那么为什么 TLC 报告q=1, q=2, q=3,q=4作为无效状态？
错误跟踪输出如下：
<<
[
_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
]
>>
一个人应该如何识别那些被认为是错误的和那些不是来自这个跟踪的？界面不显示红灯q=0。