“ A和B……的逻辑评估”

Question

给出一条语句“当CM空闲并从WCP接收更新请求时，它将设置....”。某些上下文：通道中只能存在一种类型的味精，即，它将仅包含来自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）。

IMHO，更好的选择是

else

相反，当您想使用

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变量可以通过其他过程进行更改。如果可以提高可读性，我几乎总是使用第二种样式。