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

Я хотел бы иметь возможность использовать цикл 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 выдает следующую ошибку:

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

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


promela spin
person Crux    schedule 15.02.2013    source источник

Ответы (2)


arrow_upward
2
arrow_downward

Пытаться:

active proctype Reliable () {
  byte index;

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

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

person GoZoner    schedule 02.03.2013

arrow_upward
1
arrow_downward

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

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

вместо

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

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

int i;
for (i : 0..4 ) {...}
person Javier    schedule 19.02.2013