Strange error on Promela - Error: syntax error saw 'keyword: do' near 'do'

Question

为什么以下 Promela 代码仅在 N >= 34 时返回错误？

#define N 34
active proctype proc1() {

    byte i;
    select(i: 1 .. N);    //line 5

    do
        :: true ->
            printf("Hi");
        :: true -> 
            break;
    od
}

错误是：

spin: prova.pml:5, Error: syntax error  saw 'keyword: do' near 'do'

我真的找不到错误。使用 N <= 33 它可以正常工作。

这是一个错误吗？

Answer 1

是的，这是一个错误。

将您的 Spin 版本更新为 6.4.7 或更高版本。

版本6.4.7的release notes提到：

fixed a bug in the parsing of select (...) statements that could cause unwarranted syntax errors when larger ranges are used

我无法用版本 6.4.8 重现您的问题，尽管它确实存在于版本 6.4.6.

中

Strange error on Promela - Error: syntax error saw 'keyword: do' near 'do'

Strange error on Promela - Error: syntax error saw 'keyword: do' near 'do'

spin

promela