PROMELA/SPINの 'any'チャンネルからメッセージを受け取る方法

Question

私はSpinでアルゴリズムをモデリングしています。 私はいくつかのチャンネルを持っているプロセスを持っています。そしてある時点で、メッセージが来るが、どのチャンネルからメッセージが来るのか分からないことを知っています。したがって、メッセージがいずれかのチャネルから来るまでプロセスを待機（ブロック）したい。どうやってやるの？

Answer 1

プロンプラのif構造が必要だと思います（http://spinroot.com/spin/Man/if.html参照）。

あなたが参照しているプロセスでは、あなたはおそらく以下のものが必要です。

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

チャンネルのどれもが彼らに何も持っていない場合は、「選択はブロック全体としての構築は、」（手を引用）、これはまさにあなたが望むふるまいです。

"[各::行]オプションは、そのガードステートメントが実行可能な場合にのみ実行するように選択することができます[ガードステートメントは、 ]複数のガードステートメントが実行可能な場合、そのうちの1つは非決定論的に選択されます。ガードが実行可能でない場合、選択構造全体がブロックされます。

ところで、私は上記のSpinで構文チェックやシミュレーションを行っていません。うまくいけばそれは正しい。私はプロメラとスピンには全く新しいです。

Answer 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のそれよりもはるかに小さいですが、これは可能なパスを調べるモデル検査では何の違いもありません。