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

Question

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.

Answer 1

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.