1

スピン ガイドを読みましたが、次の質問に対する回答がありません。

コードに次のような行があります。

Ch?x

ここで、Ch はチャネル、x はチャネル タイプ (MSG を受信するため) です。Ch が空の場合はどうなりますか? MSG が到着するのを待ちますか? Ch が空でないかどうかを最初に確認する必要がありますか?

基本的に私が望むのは、Chが空の場合、MSGが到着するまで待ち、到着したら続行することです...

4

2 に答える 2

2

結論: Promela のセマンティクスは、メッセージを受信できるようになるまで受信操作がブロックされるという、目的の動作を保証します。

受信のマニュアルページから

EXECUTABILITY
チャネル内の最初のメッセージが receive ステートメントのパターンと一致する場合、単一の疑問符で記述されたステートメントの最初と 3 番目の形式は実行可能です。

これは、受信操作がいつ実行可能かを示します。

Promelaのセマンティクスは、実行可能性が重要な理由を示しています。

実行可能なトランジション (Promela の基本的なステートメントに対応) がある限り、セマンティクス エンジンはその中からランダムに 1 つを選択して実行します。

確かに、この引用はそれを明確にするものではありませんが、現在実行可能でないステートメントは、実行可能になるまで実行プロセスをブロックすることを意味します。


これは、受信操作の動作を示す小さなプログラムです。

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変数を提供しているため、 のメッセージによってステートメントが実行可能になります。つまり、 のパターン マッチングの側面は適用されません。]xCh?xChreceive

于 2013-06-18T14:10:24.620 に答える