"When A and B ... " 的逻辑评估

Question

给定一个语句"When the CM is idle and receives update request from the WCP, it will set ...."。 一些上下文：频道中只能有一种类型的消息，即它只会包含来自 wcp 的更新请求。

我可以想到 2 种可能的实现方式。但是，我不太确定哪种方法是正确的。

第一种方式：

    do
    :: CM_STATUS == IDLE && nempty(wcpOut) -> // remove msg from channel and set something;
    od;

第二种方式

    mtype receivedMessage;
    do
    :: CM_STATUS == IDLE -> 
        if
        :: wcpOut?receivedMessage -> // set something;
        fi;
    od;

Answer 1

这两个例子略有不同。

do
    :: CM_STATUS == IDLE && nempty(wcpOut) -> // read msg
od;

在这里，如果您的状态是 idle 并且频道 wcpOut 不为空，您承诺阅读消息。但是，如果进程在 nempty(wcpOut) 的评估之前被抢占，并且消息被其他人读取，会发生什么情况？在那种情况下，该过程可能最终被阻止。

mtype receivedMessage;
do
:: CM_STATUS == IDLE -> 
    if
    :: wcpOut?receivedMessage -> // set something;
    fi;
od;

在这里，您承诺在状态 idle 时阅读一条消息，因此在阅读消息之前您无法对状态更改做出反应。

我不会使用任何一种方法，除了简单的例子。

第一种方法的缺陷在于它不是原子地执行这两个操作。第二种方法的缺陷在于，它很难通过添加更多条件来扩展控制器在空闲 state 中的行为。（例如，您会得到 "dubious use of 'else' combined with i/o" error message if you tried to add an else branch）。

恕我直言，更好的选择是

do
    :: atomic{ nempty(my_channel) -> my_channel?receiveMessage; } ->
        ...
    :: empty(my_channel) -> // do something else

od;

相反，当您想使用 message filtering, you can use message polling:

do
    :: atomic{ my_channel?[MESSAGE_TYPE] -> my_channel?MESSAGE_TYPE } ->
        ...
    :: else -> // do something else
od;

是否选择使用 CM_STATUS == IDLE 加入这些条件，或者您更喜欢使用嵌套方法，完全取决于您，除非您有理由相信 CM_STATUS 变量可以被其他一些过程改变。当可以提高可读性时，我几乎总是使用第二种样式。

"When A and B ... " 的逻辑评估

Logical evaluation of "When A and B ... "

model-checking

spin

promela