TLA+ 序列未使用 Append 或 Tail 调用更新

Question

问题

我正在研究 TLA+，并认为我会在 PlusCal 中编写以下明显错误的规范：

---- MODULE transfer ----
EXTENDS Naturals, TLC, Sequences

(* --algorithm transfer

\* Simple algorithm:
\*  1. Start with a shared-memory list with one element.
\*  2. A process adds arbitrary numbers of elements to the list.
\*  3. Another process removes arbitrary numbers of elements from the list, 
\*     but only if the list has more than one item in it. This check is 
\*     applied just before trying to removing an element. 
\* Is it true that the list will always have a length of 1? 
\* You would expect this to be false, since the adder process can add more elements 
\* than the remover process can consume.

variables stack = <<0>>

process Adder = 0
  begin
      AddElement:
        stack := Append(stack, Len(stack));
        either goto AddElement
        or skip
        end either;
end process;

process Remover = 1
  begin
      RemoveElement:
        \* Pop from the front of the stack
        if Len(stack) > 1 then
            stack := Tail(stack);
        end if;
        either goto RemoveElement
        or skip
        end either;
end process;

end algorithm *)

IsStackAlwaysUnitLength == Len(stack) = 1

====

检查 IsStackAlwaysUnitLength 作为要报告的时间属性之一后，我希望 TLA+ 将此属性标记为失败。

然而，所有州都通过了！为什么它没有失败？

调试尝试

在使用 print 语句进行调试时，我注意到以下奇怪的行为：

process Adder = 0
  begin
      AddElement:
        print stack;
        print "Adder applied!";
        stack := Append(stack, Len(stack));
        print stack;
        print "Adder task complete!";
        \* Force 
        either goto AddElement
        or skip
        end either;
end process;

process Remover = 1
  begin
      RemoveElement:
        \* Pop from the front of the stack
        print stack;
        print "Remover applied!";
        if Len(stack) > 1 then
            stack := Tail(stack);
            print stack;
            print "Remover task complete!";
        else
            print "Remover task complete!";
        end if;
        either goto RemoveElement
        or skip
        end either;
end process;

调试面板中的产量

<<0>>
"Adder applied!"
<<0>>
"Adder task complete!"
<<0>>
<<0>>
"Remover applied!"
"Remover applied!"
"Remover task complete!"
"Remover task complete!"
<<0>>
"Adder applied!"
<<0>>
"Adder task complete!"

我不确定为什么 stack := Append(stack, Len(stack)); 和 stack := Tail(stack); 没有更新全局 stack 变量。

已生成完整的 TLA 规范

---- MODULE transfer ----
EXTENDS Naturals, TLC, Sequences

(* --algorithm transfer

variables stack = <<0>>

process Adder = 0
  begin
      AddElement:
        stack := Append(stack, Len(stack));
        either goto AddElement
        or skip
        end either;
end process;

process Remover = 1
  begin
      RemoveElement:
        \* Pop from the front of the stack
        if Len(stack) > 1 then
            stack := Tail(stack);
        end if;
        either goto RemoveElement
        or skip
        end either;
end process;

end algorithm *)
\* BEGIN TRANSLATION
VARIABLES stack, pc

vars == << stack, pc >>

ProcSet == {0} \cup {1}

Init == (* Global variables *)
        /\ stack = <<0>>
        /\ pc = [self \in ProcSet |-> CASE self = 0 -> "AddElement"
                                        [] self = 1 -> "RemoveElement"]

AddElement == /\ pc[0] = "AddElement"
              /\ stack' = [stack EXCEPT ![0] = Append(stack, Len(stack))]
              /\ \/ /\ pc' = [pc EXCEPT ![0] = "AddElement"]
                 \/ /\ TRUE
                    /\ pc' = [pc EXCEPT ![0] = "Done"]

Adder == AddElement

RemoveElement == /\ pc[1] = "RemoveElement"
                 /\ IF Len(stack) > 1
                       THEN /\ stack' = [stack EXCEPT ![1] = Tail(stack)]
                       ELSE /\ TRUE
                            /\ stack' = stack
                 /\ \/ /\ pc' = [pc EXCEPT ![1] = "RemoveElement"]
                    \/ /\ TRUE
                       /\ pc' = [pc EXCEPT ![1] = "Done"]

Remover == RemoveElement

Next == Adder \/ Remover
           \/ (* Disjunct to prevent deadlock on termination *)
              ((\A self \in ProcSet: pc[self] = "Done") /\ UNCHANGED vars)

Spec == Init /\ [][Next]_vars

Termination == <>(\A self \in ProcSet: pc[self] = "Done")

\* END TRANSLATION

IsStackAlwaysUnitLength == Len(stack) = 1

====

Answer 1

恭喜，您遇到了 PlusCal 错误！还有一个不是错误但仍然不直观的边缘情况。让我们从错误开始。

有时在使用 PlusCal 时我们希望多个进程共享标签。我们使用过程来做到这一点。为了使其全部正常工作，PlusCal 翻译器添加了一个名为 stack 的额外簿记变量。通常，如果用户定义的变量foo 与生成的变量foo 冲突，翻译会将其中一个重命名为foo_。在这种情况下，因为没有冲突，所以没有任何重命名。*错误是翻译者混淆了并将变量翻译成好像它应该是簿记stack。你可以看到这个，因为它把追加变成了

stack' = [stack EXCEPT ![0] = Append(stack, Len(stack))]

什么时候应该

stack' = Append(stack, Len(stack))

您可以通过 将 stack 重命名为 mystack 来解决此问题。 这应该使规范正常运行。但它仍然会通过：那是因为你把 IsStackAlwaysUnitLength 作为属性而不是 不变的 。作为时间属性，如果在初始状态下为真，则 IsStackAlwaysUnitLength 为真。作为不变量，如果在所有状态下为真，则 IsStackAlwaysUnitLength 为真。** 您可以通过 更改 IsStackAlwaysUnitLength 使规范正确失败从属性到 "what is the model" 页面中的不变 。

*实际上在这种情况下，如果您添加过程，翻译器不会重命名 stack，它只会抛出一个错误。但这仍然是安全的。

**这是因为 TLC（模型检查器）将不变量 P 视为时间属性 []P。它基本上是语法糖。

TLA+ 序列未使用 Append 或 Tail 调用更新

TLA+ sequence not being updated with Append or Tail calls

tla+

问题

调试尝试

已生成完整的 TLA 规范