spin - Promela：如何对 typedef 类型的数组使用 for 循环

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 ) {...}