SPIN reprots "dubious use of 'else' combined with i/o" but not always

awesan · 2011-11-19 22:20:32

Please look at the following PROMELA fragment:
****************************************
do
:: state == A ->
if
:: chx?? [id] ->
chx ?? id ->
ch1?msg;
:: else -> skip; // SPIN does NOT throw syntax error
fi

:: state == B ->
if
:: some_condition_1 -> ....
:: some_condition_2 -> ....
:: nempty(ch1) ->
ch1?msg;
:: else -> skip; //SPIN throws syntax error : dubious use of 'else' combined with i/o, saw 'token: ::'
//SPIN reports error at line number that has " :: state == C ->" which is a few lines below, instead of at the line above. Seems to be a minor BUG.
fi

:: state == C ->

od;
****************************************
Q-1. As mentioned in the comments, SPIN accepts "else" on a random-receive boolean function but throws syntax error on a boolean function "nempty". It looks a bit inconsistent to have different behaviors on these two cases and it would be more clear if the behavior is consistent one way or the other. I see in the documentation that !empty is not allowed and that's why SPIN has both empty and nempty. If that is the reason for syntax error on "else" case, that sounds reasonable. However, it does limit one from using "else" in an "if" statement that has several conditions with one of them being "nempty" on a channel. I understand that the model can be written with some extra lines of code and checks and worked-around, but it would be a syntactic sugar to allow "else" in an "if" statement that has "nempty" as one of the conditions, even though !nempty is not allowed by SPIN. I think it is possible that this is done for all valid reasons and limitations by design and implementation.

Q-2. The line number reported by SPIN for the syntax error "dubious use of 'else'" is incorrect as mentioned in the comments. Again, it is not a big deal and I can obviously easily spot the offending line and fix it. However, if you would like to fix this and cannot reproduce this, please let me know.

spinroot · 2011-11-20 00:56:14

the reason that there's no complaint for the first else is that it is combined with a channel poll, not a channel send or receive.
I agree that it's not fully consistent to reject a nempty, but accept a poll
For better or worse, this change was introduced in Spin Version 2.7.4 on 25 September 1995. The V2.Updates log says:
===== 2.7.4 - 25 September 1995 ====
...
- allowed `else' to be combined with boolean channel references
such as len and receive-poll
...

I can't reconstruct what the reasoning was behind this change.

Q2: I know, the line number reporting is annoying, but hard to get right

awesan · 2011-11-20 02:34:57

I misspoke. By "random-receive boolean function", I meant "random-poll". I am not quite "SPIN"ning right yet

Thanks for looking at the change log. Given the fact that "else" can be combined with "len", I can define the following macros and use these instead of the built-in "empty" and "nempty" and this would allow me to keep the model more crisp and terse. So, I can use "else" on all channel poll's and empty/nempty conditions, which is sweet.
************************************************
#define _empty(_ch) (len(_ch) == 0)
#define _nempty(_ch) (len(_ch) != 0)
************************************************
I am happy with this work-around. If you choose to make it consistent, I would recommend allowing "empty" and "nempty" to be combined with "else" than disallowing channel poll, if there are no strong reasons to do the other way around.

Thanks again for all the help.

Last edited by awesan (2011-11-20 06:18:17)

Spinroot

#1 2011-11-19 22:20:32

SPIN reprots "dubious use of 'else' combined with i/o" but not always

#2 2011-11-20 00:56:14

Re: SPIN reprots "dubious use of 'else' combined with i/o" but not always

#3 2011-11-20 02:34:57

Re: SPIN reprots "dubious use of 'else' combined with i/o" but not always

Board footer