Блог

У меня есть следующая спецификация для очереди:

 ------------------------------- 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 .

• Красная ячейка указывает, что значение переменной изменилось в этом состоянии по сравнению с ее предыдущим значением (см. https://tla.msr-inria.inria.fr/tlatoolbox/doc/model/executing-tlc.html ). Красный не указывает, что состояния недопустимы!
• Префикс (бесконечного) поведения, сообщаемый проводником трассировки как трассировка ошибки, не удовлетворяет свойству (safety) TypeInvariant , поскольку TypeInvariant не разрешает q=4 .

Кстати, группа TLA — гораздо лучшее место для вопросов.