Bug in select() statement with inlining?

Question

I would have posted this in the spinroot Bug Reports, but the spinroot forum is not currently accepting new users... If someone out there in charge of that is reading this, please let me in :)

Something very odd is happening when I try to use the select statement. Promela does not allow select() to be called on the field of a struct, so I have to make a temporary variable like this:

typedef someStruct {
    int someField;
}

someStruct struct;

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

init{
    SetSelect();
}

This runs fine. I tested it and struct.someField is correctly set to either -1, 0, or 1. However, when I try to just put the inlined code straight into the init() process, I get a syntax error. The code looks like this:

typedef someStruct {
    int someField;
}

someStruct struct;

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

And the error message is:

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

Answer 1

BUG:

Indeed, it looks like a bug for version 6.4.6 of Spin. (The bug is fixed in version 6.4.7)

Interestingly, You can make it go away by simply writing temp : instead of temp:.

I suggest you to contact Gerard Holzmann for filing a bug report. I would also mention the fact that select does not seem to work with a struct field, perhaps that can be fixed too (even if it might be by design).

---

SUGGESTION:

I am not entirely happy of creating an alias variable to get around the issue of the built-in select function with struct fields. Since the implementation of select is rather trivial, as can be found in the docs, I would introduce a novel inline function to replace the built-in select function:

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);
}