Как проверить, равны ли все значения в массиве в Promela?

Вы можете попробовать что-то вроде следующего фрагмента (где массив считается непустым):

#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 в true в else части условного блока после атомарного оператора. В противном случае проверка никогда не будет успешной, если значения изначально не равны.