PlusCal：为什么公平算法仍然卡顿？

Question

我使用 PlusCal 对接受与正则表达式 (X*)(Y).

匹配的字符串的普通状态机建模

(*--fair algorithm stateMachine
variables
    state = "start";

begin

Loop:    
while state /= "end" do
    either
        \* we got an X, keep going
        state := "reading"
    or
        \* we got a Y, terminate
        state := "end"
    end either;
end while;


end algorithm;*)

即使我已经标记了算法 fair，但由于卡顿，以下时间条件失败了......模型检查器允许状态机吸收 X 然后只是停在 Loop 上，不再做任何其他事情。

MachineTerminates == <>[](state = "end")

在像这样的简单过程中，公平实际上意味着什么？有没有办法告诉模型检查器状态机永远不会运行输入不足，因此总是会终止？

Answer 1

好吧，这很奇怪，应该通过，但不是你想的那样。要理解为什么，我们首先要谈谈公平的 "usual" 定义，然后是技术定义。

弱公平说，如果一个动作永远不会被禁用，它最终会发生。您可能期望的是以下内容：

循环可以选择 "end" 但不能。
循环可以选择 "end" 但没有。这种情况发生了任意次数。
由于循环是公平的*，它被迫选择"end"。
我们完成了。

但事实并非如此。在 pluscal 中，公平是在标签级别。它没有说明标签中发生了什么，只是标签本身必须发生。所以这是一个完全有效的行为：

因为循环永远不会被禁用，所以它最终会发生。它选择 "reading".
因为循环永远不会被禁用，所以它最终会发生。它选择 "reading".
因为循环永远不会被禁用，所以它最终会发生。它选择 "reading".
这会一直持续下去。

这相当于您输入了一个无限长的字符串，仅由 X 组成。如果你只想要有限的字符串，你必须明确地表达它，要么作为规范的一部分，要么作为你想要的时间属性的先决条件之一。例如，你可以让你的时间属性 state = "end" ~> Termination，你可以为输入字符串建模，你可以为 "how many x's before the y" 添加一个计数等等。不过规格设计不错。

这是正常情况。但这是一个非常、非常的规则例外。那是因为"fairness is defined"。正式地，WF_vars(A) == <>[](Enabled <<A>>_v) => []<><<A>>_v。我们通常将其翻译为

If the system is always able to do A, then it will keep on doing A.

这是我到现在为止一直在使用的解释。但它在一个非常大的方面是错误的。 <<A>>_vars == A /\ (vars' /= vars)，或者说“A发生了，vars发生了变化。所以我们的定义实际上是

If the system is always able to do A in a way that changes its state, then it will keep on doing A in a way that changes its state.

一旦你有 pc = "Loop" /\ state = "reading"，做 state := "reading" 不会改变系统状态，所以它不算作 <<Next>>_vars.所以 <<Next>>_vars 实际上并没有发生，但出于不公平的考虑，它最终一定会发生。 <<Next>>_vars 发生的唯一方法是循环设置 state := "reading，这允许 while 循环终止。

这是一个非常不稳定的情况。我们对规范所做的任何细微更改都可能将我们推回到更熟悉的领域。例如，以下规范不会按预期终止：

variables
    state = "start";
    foo = TRUE;        
begin
Loop:    
while state /= "end" do
    foo := ~foo;
    either
        \* we got an X, keep going
        state := "reading"
    or
        \* we got a Y, terminate
        state := "end"
    end either;
end while;
end algorithm;*)

即使 foo 不影响其余代码，它允许我们拥有 vars' /= vars 而无需更新 state。类似地，将 WF_vars(Next) 替换为 WF_pc(Next) 会使规范失败，因为我们可以达到禁用 <<Next>>_pc 的状态（也就是 state = "reading" 的任何状态）。

*循环不公平，整个算法是。这在某些情况下会产生很大的不同，这就是我们指定的原因。但在这种情况下更容易谈论循环，因为它是唯一的动作。

PlusCal：为什么公平算法仍然卡顿？

PlusCal: Why does fair algorithm still stutter?

tla+

pluscal