2

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

4

2 回答 2

4

我认为您需要 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 很陌生。

于 2012-04-02T23:41:47.983 回答
0

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

#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，但这在模型检查中没有任何区别，在模型检查中探索了任何可能的路径。

于 2014-01-28T12:19:10.833 回答