1

我会在spinroot 错误报告中发布此内容，但 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'

4

1 回答 1

1

错误：

实际上，它看起来像是Spin6.4.6版本的错误。 （该错误已在版本中修复）6.4.7

有趣的是，您可以通过简单地编写temp :而不是temp:.

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

建议：

我不完全乐意创建一个别名变量来解决带有结构字段的内置选择函数的问题。由于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);
}
于 2017-08-03T07:25:49.850 回答