1

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

我的代码中有一行如下：

Ch?x

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

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

4

2 回答 2

2

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

从接收手册页

可执行
性 如果通道中的第一条消息与接收语句中的模式匹配，则语句的第一种和第三种形式（用一个问号编写）是可执行的。

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

然后，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.
     */
}
于 2013-06-17T08:06:16.523 回答
1

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

于 2013-06-18T14:10:24.620 回答