Dubious use of 'else' combined with i/o, saw ';' near 'if'

model-checking, multithreading, promela, spin

Solution

The reason this occurs is because the Spin compiler translates the `else` into the negation of all the `if` options and then, because one of your options has `nempty()`, the translated `if` ends up with a `!nempty()` which is disallowed. For example:

if
:: (p1) -> …
:: (p2) -> … 
:: else -> … 
if

is translated to

if
:: (p1) -> … 
:: (p2) -> … 
:: (!p1 && !p2) -> … 
if

When `p1` or `p2` contains any of `full()`, `nfull()`, `empty()`, or `nempty()` the expression of `!p1` or `!p1` will negate one of those queue full/empty predicates. It is illegal to do that negation. See www.spinroot.com for documentation of these predicates.

The solution is to do the `else` translation yourself and then when you see a negation replace it with the matching predicate. For example, if you want:

if
:: a == b && nempty(q) -> …
:: else
fi

then replace `else` with (working it out):

!(a==b &&  nempty(q))   => DeMorgan's Laws
 (a!=b || !nempty(q))   
 (a!=b ||  empty(q))

and thus `!nempty()` no longer exists in the final 'by hand' translation:

if
:: a == b && nempty(q) -> …
:: a != b ||  empty(q))-> …
fi

If your case, with multiple complicated options, doing the 'by hand' translation of `else` will be prone to errors. But, that is what you need to do.

Problem

Following is the code causing this. ``` if :: ((fromProc[0] == MSG_SLEEP) && nempty(proc2clk[0])) -> proc2clk[0] ? fromProc[0]; // Woke up :: (!(fromProc[0] == MSG_SLEEP) && !(fromProc[0] == MSG_FIN)) -> clk2proc[0] ! 0; ::else -> time = time + 1; // just for debugging fi; ``` If I remove the nempty call in the first condition, the error is gone. From what I've read, you can not use the else statement, if you use a receive or send statement in a condition, but from what I know, nempty is not a sending or receiving statement, but just to check whether a channel is not empty. So, what mistake am I doing, and how can I solve this.

Original source