标签: pluscal

我使用 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，以下时间条件由于口吃而失败......模型检查器允许状态机吸收 anX然后简单地停止Loop而不做任何其他事情的情况。

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

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