Promela: how to use a for loop for an array of type typedef

Question

I would like to be able use a for loop to loop through an array of typedef values as demonstrated below:

typedef chanArray {
    chan ch[5] = [1] of {bit};
}
chanArray comms[5];

active proctype Reliable() {
    chanArray channel;
    for ( channel in comms ) {
        channel.ch[0] ! 0;
    }   
}

Spin gives the following error:

spin: test2.pml:8, Error: for ( channel in .channel_name ) { ... }

Is it possible to use a for loop in this form to loop through the array instead of having to use a for loop with an index pointer?

Answer 1

Try:

active proctype Reliable () {
  byte index;

  index = 0;
  do
  :: index < 5 -> channel.ch[index] ! 0; index++
  :: else -> break
  od
}

this is the only way. So the answer to your 'is it possible ...' question is 'no, it is not possible ...'

Answer 2

I'm new to Promela, but it seems that you are using

for '(' varref in channel ')' '{' sequence '}'

instead of

for '(' varref ':' expr '..' expr ')' '{' sequence '}' 

Try with something like

int i;
for (i : 0..4 ) {...}