如何从 PROMELA/SPIN 中的“任何”频道接收消息答案

【问题标题】：How to receive message from 'any' channel in PROMELA/SPIN如何从 PROMELA/SPIN 中的“任何”频道接收消息
【发布时间】：2014-01-28 20:31:01
【问题描述】：

我正在为 Spin 中的算法建模。我有一个有多个渠道的流程，并且在某些时候，我知道一条消息将会到来，但不知道来自哪个渠道。因此，希望等待（阻止）该过程，直到消息来自任何通道。我该怎么做？

【问题讨论】：

标签： spin

【解决方案1】：

我认为您需要 Promela 的 if 构造（请参阅 http://spinroot.com/spin/Man/if.html）。

在您所指的过程中，您可能需要以下内容：

byte var;
if
:: ch1?var -> skip
:: ch2?var -> skip
:: ch3?var -> skip
fi

如果通道上没有任何内容，则“选择结构作为一个整体块”（引用手册），这正是您想要的行为。

更全面地引用手册的相关部分： “一个选项 [每个 :: 行] 只能在其保护语句可执行时选择执行 [保护语句是 -> 之前的部分]。如果多个保护语句是可执行的，则其中一个将是非确定性选择。如果没有一个守卫是可执行的，则选择结构作为一个整体阻塞。"

顺便说一句，我没有在 Spin 中检查或模拟上述语法。希望是对的。我对 Promela 和 Spin 自己很陌生。

【讨论】：

请注意，'-> 跳过'不是必需的。
如果通道数为 n 怎么办？意思是一开始就有一个定义的价值..有人可能会改变它的价值......？这样你将不得不修改你的代码......还有其他方法吗？

【解决方案2】：

如果你想让你的通道数可变而不必更改发送和接收部分的实现，你可以使用以下生产者-消费者示例的方法：

#define NUMCHAN 4

chan channels[NUMCHAN];

init {
    chan ch1 = [1] of { byte };
    chan ch2 = [1] of { byte };
    chan ch3 = [1] of { byte };
    chan ch4 = [1] of { byte };

    channels[0] = ch1;
    channels[1] = ch2;
    channels[2] = ch3;
    channels[3] = ch4;
    // Add further channels above, in
    // accordance with NUMCHAN

    // First let the producer write
    // something, then start the consumer
    run producer();
    atomic { _nr_pr == 1 ->
        run consumer();
    }
}

proctype consumer() {
    byte var, i;
    chan theChan;

    i = 0;
    do
        :: i == NUMCHAN -> break
        :: else ->
             theChan = channels[i];
             if
               :: skip // non-deterministic skip
               :: nempty(theChan) ->
                  theChan ? var;
                  printf("Read value %d from channel %d\n", var, i+1)
             fi;
             i++
    od
}

proctype producer() {
    byte var, i;
    chan theChan;

    i = 0;
    do
        :: i == NUMCHAN -> break
        :: else ->
             theChan = channels[i];
             if
               :: skip;
               :: theChan ! 1;
                  printf("Write value 1 to channel %d\n", i+1)
             fi;
             i++
    od
}

消费者进程中的do 循环不确定地选择0 和NUMCHAN-1 之间的索引并从相应的通道读取，如果有要读取的内容，则始终跳过该通道。自然，在使用 Spin 进行模拟期间，从通道 NUMCHAN 读取的概率远小于通道 0 的概率，但这在模型检查中没有任何区别，因为模型检查会探索任何可能的路径。

【讨论】：