Spinroot

amirzol

Member

Registered: 2010-12-25

Posts: 4

if and else both are executable !!!

Does Promela allow ' if ' and ' else ' to be executable  at the same time??

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

spinroot

forum

Registered: 2010-11-18

Posts: 700

Website

Re: if and else both are executable !!!

can you show the actual piece of code?
if you mean:

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

amirzol

Member

Registered: 2010-12-25

Posts: 4

Re: if and else both are executable !!!

what I meant is similar to this chunck of code, I found this clarification very useful, the problem sorted out.

THANK YOU