promelaspin

Trying to match to a typedef value in a receive statement causes "bad node type 44" error message


When I try to match a message in a receive statement I get a "bad node type 44" error message. This happens when the message's type is a typedef. The error message is rather cryptic and doesn't give much insight.

typedef t {
    int i
}
init {
    chan c = [1] of {t}
    t x;
    !(c ?? [eval(x)]) // <--- ERROR
}

Solution

  • Apparently it's a bug, link to github issue: https://github.com/nimble-code/Spin/issues/17

    Update: Bug is now fixed.

    Update 2: Bug was actually partially fixed, there are still some edge cases where it's behaving weirdly.

    Update 3: As far as I can tell bug looks fixed now. The only downside is that it seems that now there is a strict restriction on what you put in the receive args. They have to match exactly the types declared in the channel. No more partial matches or unrolling struct fields.