0

以下に示すように、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 ループを使用して配列をループすることは可能ですか?

4

2 に答える 2

2

試す：

active proctype Reliable () {
  byte index;

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

これが唯一の方法です。したがって、「可能ですか...」という質問に対する答えは、「いいえ、不可能です...」です。

于 2013-03-02T14:06:48.503 に答える
1

Promelaは初めてですが、使用しているようです

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

それ以外の

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

次のようなもので試してください

int i;
for (i : 0..4 ) {...}
于 2013-02-19T15:47:11.500 に答える