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.