为什么 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）。红色 not 表示状态无效！
（无限）行为的前缀 - 由跟踪资源管理器报告为错误跟踪 - 不满足（安全）属性 TypeInvariant 因为 TypeInvariant 确实 不允许允许q=4.

顺便说一句，TLA+ group 是提问的好地方。

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

Why is TLC reporting errors on valid states?

specifications

formal-verification

tla+

tlc