“当A和B……”的逻辑评价答案

【问题标题】：Logical evaluation of "When A and B ... "“当A和B……”的逻辑评价
【发布时间】：2020-02-20 18:25:00
【问题描述】：

给定一个语句“当CM空闲并收到来自WCP的更新请求时，它将设置....”。 一些上下文：频道中只能有一种类型的 msg，即它只会包含来自 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;

【问题讨论】：

【解决方案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时，你可以使用message polling：

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

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

【讨论】：