1

我使用 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;*)

即使我已经标记了 algorithm fair，以下时间条件由于口吃而失败......模型检查器允许状态机吸收 anX然后简单地停止Loop而不再做任何其他事情的情况。

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

在这样一个简单过程的背景下，公平实际上意味着什么？有没有办法告诉模型检查器状态机永远不会用完输入，因此总是会终止？

4

1 回答 1

5

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

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

  1. 循环可以选择“结束”，但不会。
  2. 循环可以选择“结束”，但不会。这发生了任意次数。
  3. 由于循环是公平的*，它被迫选择“结束”。
  4. 我们完成了。

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

  1. 因为循环永远不会被禁用，它最终会发生。它选择“阅读”。
  2. 因为循环永远不会被禁用，它最终会发生。它选择“阅读”。
  3. 因为循环永远不会被禁用，它最终会发生。它选择“阅读”。
  4. 这一直持续下去。

这对应于您输入一个无限长的字符串，仅由 X 组成。如果你只想要有限的字符串，你必须明确地表达出来，要么作为规范的一部分，要么作为你想要的时间属性的先决条件之一。例如，您可以制作您的时间属性state = "end" ~> Termination，您可以对输入字符串进行建模，您可以添加“y 之前有多少个 x”的计数，等等。不过，这会脱离实际错误并进入良好的规范设计。

这是正常情况。但这是该规则的一个非常非常具体的例外。那是因为“公平是如何定义的”。正式地，WF_vars(A) == <>[](Enabled <<A>>_v) => []<><<A>>_v. 我们通常将其翻译为

如果系统总是能够做 A，那么它将继续做 A。

这就是我到现在为止使用的解释。但这在一个很大的方面是错误的。<<A>>_vars == A /\ (vars' /= vars)，或“A发生并vars改变。所以我们的定义实际上是

如果系统总是能够以改变其状态的方式执行 A ，那么它将继续以改变其状态的方式执行A。

一旦拥有pc = "Loop" /\ state = "reading"，doingstate := "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"）。

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

于 2019-03-12T22:16:40.923 回答