promela - 配列内のすべての値がPromelaで等しいかどうかを確認するにはどうすればよいですか?

Question

配列のすべての値が等しいかどうか、Promela でどのようにチェックしますか?

このコードをアトミ​​ックで実行可能にしたいのですが（すべてが等しくなるまで待機中）。

for ループを使用する方法はありますか? (配列の長さはパラメータとして与えられます)

Answer 1

次のスニペットのようなものを試すことができます (配列は空でないと想定されています)。

#define N 3
int arr[N];

proctype Test(int length) {
  int i, val;
  bool result = true;

  do
    :: atomic {
         /* check for equality */
         val = arr[0];
         for (i : 1 .. length-1) {
           if
            :: arr[i] != val ->
                 result = false;
                 break
            :: else -> skip
           fi
         }

         /* Leave loop if all values are equal,
            else one more iteration (active waiting).
            Before the next entrance into the atomic
            block, other proctypes will have the chance
            to interleave and change the array values */
         if
           :: result -> break;
           :: else -> result = true
         fi
       }
  od

  /* will end up here iff result == true */
}

init {  
  arr[0] = 2;
  arr[1] = 2;
  arr[2] = 2;

  run Test(N);
}

アトミック ブロック内のコードはブロックされないため、継続的に実行できます。

/edit (2019-01-24):resultアトミックステートメントの後の条件ブロックのelse部分でtrueに設定。そうしないと、値が最初に等しくない場合、チェックは成功しません。