为什么TLC在有效状态上报告错误？

Question

对于队列，我有以下规范：

------------------------------- 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上没有显示红灯。

Answer 1

• 红细胞表示变量的值在此状态下与以前的值相比发生了变化(请参阅https://tla.msr-inria.inria.fr/tlatoolbox/doc/model/executing-tlc.html)。红色并不表示状态无效！
• 跟踪资源管理器作为错误跟踪的(无限)行为-reported的前缀-不满足(安全)属性TypeInvariant，因为TypeInvariant不允许q=4。

顺便说一句，TLA+群是一个问问题的好地方。