PROMELA：如何通過的typedef值的數組使用for循環類型的數組的typedef

Question

我想是for循環來循環能夠使用如下面所示：

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