带有内联的 select() 语句中的错误?

Question

我会在 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'

Answer 1

错误：

事实上，它看起来像是Spin版本6.4.6的错误。(该错误已在版本6.4.7中修复(

有趣的是，您可以通过简单地编写temp :而不是temp:来使其消失。

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

---

建议：

我不完全乐意创建一个别名变量来解决带有结构字段的内置选择函数的问题。由于 select 的实现相当微不足道，可以在文档中找到，我将引入一个新颖的内联函数来替换内置的 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("%dn", st.field);
}