在 SPIN/Promela 中，如何以正确的方式从频道接收 MSG？答案

【问题标题】：In SPIN/Promela, how to receive a MSG from a channel in the correct way?在 SPIN/Promela 中，如何以正确的方式从频道接收 MSG？
【发布时间】：2013-06-12 17:06:34
【问题描述】：

我阅读了旋转指南，但以下问题没有答案：

我的代码中有一行如下：

Ch?x

其中 Ch 是频道，x 是频道类型（接收 MSG）如果 Ch 为空会发生什么？它会等待味精到达吗？是否需要先检查 Ch 是否为空？

基本上我想要的是，如果 Ch 是空的，那么等到 MSG 到达，当它到达时继续......

【问题讨论】：

标签： spin promela

【解决方案1】：

是的，当前的proctype 将阻塞，直到有消息到达Ch。此行为在receive 语句下的Promela Manual 中进行了描述。 [因为您提供了一个变量x（如Ch?x），Ch 中的任何消息都将导致该语句可执行。也就是说，receive 的模式匹配方面不适用。]

【讨论】：

【解决方案2】：

底线：Promela 的语义保证了您想要的行为，即接收操作阻塞，直到可以接收到消息。

来自receive man page

可执行性
语句的第一种和第三种形式，用单个问号，如果频道中的第一条消息是可执行的匹配接收语句中的模式。

这会告诉您接收操作何时是可执行的。

semantics of Promela 然后告诉你为什么可执行性很重要：

只要有可执行的转换（对应于 Promela 的基本语句），语义引擎将选择其中之一随机执行。

当然，引号并没有说得很清楚，但它意味着当前不可执行的语句将阻塞执行过程，直到它变为可执行。

这是一个演示接收操作行为的小程序。

chan ch = [1] of {byte};
  /* Must be a buffered channel. A non-buffered, i.e., rendezvous channel,
   * won't work, because it won't be possible to execute the atomic block
   * around ch ! 0 atomically since sending over a rendezvous channel blocks
   * as well.
   */

short n = -1;

proctype sender() {
  atomic  {
    ch ! 0;
    n = n + 1;
  }
}

proctype receiver() {
  atomic  {
    ch ? 0;
    n = -n;
  }
}

init {
  atomic {
    run sender();
    run receiver();
  }

  _nr_pr == 1;

  assert n == 0;
    /* Only true if both processes are executed and if sending happened
     * before receiving.
     */
}

【讨论】：