Promela: как использовать цикл for для массива типа typedef

Question

Я хотел бы иметь возможность использовать цикл for для цикла через массив значений typedef, как показано ниже:

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: test2.pml:8, Error: for ( channel in .channel_name ) { ... }

Можно ли использовать цикл for в этой форме для циклического прохождения массива вместо необходимости использовать цикл for с указателем индекса?

Answer 1

Пытаться:

active proctype Reliable () {
  byte index;

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

это единственный способ. Таким образом, ответ на ваш вопрос "возможно ли это?" - "нет, это невозможно..."

Answer 2

Я новичок в Promela, но кажется, что вы используете

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

вместо

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

Попробуйте что-то вроде

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