How do you check if all values in array are equal in Promela?

Question

How do you check in Promela if all values of an array are equal?

I want this piece of code to atomic and and executable if they are (busy waiting until all are equal).

Is there any way to use a for loop? (The length of the array is given as a parameter)

Answer 1

You could try something like in the following snippet (where the array is assumed to be non-empty):

#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);
}

The code inside the atomic block will not block and is therefore continuously executable.

/edit (2019-01-24): Setting result to true in else part of conditional block after the atomic statement. Otherwise, the check would never succeed if the values are not equal initially.