select() 语句中的内联错误？

Question

我会在 spinroot Bug Reports 中发布此内容，但 spinroot 论坛目前不接受新用户...如果负责该论坛的人正在阅读此内容，请让我加入 :)

当我尝试使用 select 语句时发生了一些非常奇怪的事情。 Promela 不允许在结构的字段上调用 select()，所以我必须像这样创建一个临时变量：

typedef someStruct {
    int someField;
}

someStruct struct;

inline SetSelect() {
    int temp;
    select(temp: -1 .. 1);
    struct.someField = temp;
}

init{
    SetSelect();
}

这运行良好。我对其进行了测试，struct.someField 正确设置为 -1、0 或 1。但是， 当我尝试将内联代码直接放入 init() 过程中，我收到语法错误。代码如下所示：

typedef someStruct {
    int someField;
}

someStruct struct;

init{
    int temp;
    select(temp: -1 .. 1);
    struct.someField = temp;
}

错误信息是：

spin: select_test.pml:9, Error: syntax error saw ''-' = 45'

Answer 1

BUG:

确实，它看起来像是 Spin 版本 6.4.6 的错误。 （该错误已在版本 6.4.7 中修复）

有趣的是，你可以通过简单地写 temp : 而不是 temp: 来让它消失。

我建议您联系 Gerard Holzmann 提交错误报告。我还要提到 select 似乎不适用于 struct 字段 ，也许这也可以修复 （即使它可能是设计使然）.

建议：

我不太高兴创建一个别名变量来解决带有结构字段的内置 select 函数的问题。由于 select 的实现相当简单，可以在 docs 中找到，我将引入一个新颖的内联函数 来替换内置 select 函数：

typedef Struct
{
    int field;
}

inline my_select (var, lower, upper)
{
    var = lower;
    do
        :: var < upper -> var++;
        :: break;
    od;
}

init
{
    Struct st;
    my_select(st.field, -1, 1);
    printf("%d\n", st.field);
}

select() 语句中的内联错误？

Bug in select() statement with inlining?

model-checking

spin

promela