THANK YOU
]]>if
:: q?msg
:: else
fi
then you should get a warning from spin that this is a dubious control construct,
basically building in a race condition
but you may have something else in mind?
'if' by itself is not a statement in promela, but 'else' is
Basically I have two processes say LH process and RH process. The LH process writes a msg on channel CH1 and the RH process reads it to make a decision about the received msg . ' if ' / ' else ' clause used to check the received msg and send the decision back to LH process on another channel CH2 , in my model I found both statements in ' if ' and ' else ' are executable at the same time !!!.
Any help to resolve this will be much appreciated - Thanks
]]>