Почему 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). Красный цвет не означает, что состояния недействительны!
• Префикс (бесконечного) поведения, сообщаемого проводником трассировки как трассировка ошибки, не удовлетворяет свойству (безопасность) TypeInvariant потому как TypeInvariantэто не позволяет q=4.

Кстати, группа TLA+ - гораздо лучшее место, чтобы задавать вопросы.