没有通过追加或尾调用更新TLA+序列
问题
我正在玩弄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
====回答 1
Stack Overflow用户
发布于 2019-01-07 02:56:48
恭喜你，你碰到了一个PlusCal错误！这也是一种边缘情况，它不是一个bug，但仍然是不直观的。让我们从窃听器开始。
有时，当使用PlusCal时，我们希望有多个进程共享标签。我们使用一个过程来完成这个任务。为了使其全部工作，PlusCal转换器添加了一个额外的簿记变量，名为stack。通常，如果用户定义一个与生成的变量foo冲突的变量foo，则转换将一个重命名为foo_。在这种情况下，由于没有冲突，所以没有任何改名。*错误在于，翻译人员混淆并翻译了变量，就好像它应该是簿记stack。您可以看到这一点，因为它将附件转换为
stack' = [stack EXCEPT ![0] = Append(stack, Len(stack))]当它应该是
stack' = Append(stack, Len(stack))您可以通过将stack mystack**.重命名为mystack**.来修复这个问题，这将使规范运行正常。但是它还是会过去的:这是因为您将IsStackAlwaysUnitLength作为一个属性而不是一个不变变量。作为一个时态属性，如果IsStackAlwaysUnitLength在初始状态为true，则它是true。作为一个不变量，如果在所有状态中都是正确的，则IsStackAlwaysUnitLength是正确的。** YOu可以通过将**YOu属性中的**更改为“什么是模型”页面中的不变来使规范正确失败。
*实际上，在这种情况下，如果添加一个过程，翻译器不会重命名stack，它只是抛出一个错误。但这仍然是不安全的。
**这是因为TLC (模型检查器)将不变的P视为时态属性[]P。基本上是语法糖。
https://stackoverflow.com/questions/54067207
复制相似问题
腾讯云开发者
