Promela 上的奇怪错误 - 错误：语法错误在 'do' 附近看到 'keyword: do'答案

【问题标题】：Strange error on Promela - Error: syntax error saw 'keyword: do' near 'do'Promela 上的奇怪错误 - 错误：语法错误在 'do' 附近看到 'keyword: do'
【发布时间】：2018-08-25 20:00:37
【问题描述】：

为什么下面的 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 可以正常工作。

这是一个错误吗？

【问题讨论】：

您使用的是哪个版本的Spin？我无法重现该问题，错误消息通常在do ... od 内没有任何分支时打印，但也可能是由于缺少;
macOS 版本 6.4.6
如果我删除定义并直接在选择中写入数字，也会出现同样的问题。
我会在周一在macos上测试并通知你

标签： spin promela

【解决方案1】：

是的，这是（曾经）一个错误。

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

6.4.7版本的release notes提及：

修复了解析 select (...) 语句中的一个错误，该错误可能会在使用较大范围时导致不必要的语法错误

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

【讨论】：