1

问题

我正在玩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

====
4

1 回答 1

3

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

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

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

什么时候应该

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

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

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

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

于 2019-01-07T02:56:48.460 回答