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

どのチャネルにも何も含まれていない場合は、「ブロック全体としての選択構造」(マニュアルを引用)、これはまさにあなたが望む動作です。

マニュアルの関連部分をより完全に引用すると、次のようになります。 1 つのガード ステートメントが実行可能である場合、そのうちの 1 つが非決定論的に選択されます。実行可能なガードがない場合、選択構造全体がブロックされます。

ちなみに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の間のインデックスを非決定論的に選択し、それぞれのチャネルから読み取ります。読み取るものがあれば、このチャネルは常にスキップされます。当然のことながら、Spin を使用したシミュレーション中、 channel から読み取る確率は channel の確率よりもはるかに小さくなりますが、これは可能なパスが探索されるモデル チェックでは何の違いもありません。0NUMCHAN-1NUMCHAN0

于 2014-01-28T12:19:10.833 に答える