Spinroot

A forum for Spin users

You are not logged in.

#1 2011-05-17 14:08:53

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

Offline

#2 2011-05-18 01:49:27

spinroot
forum
Registered: 2010-11-18
Posts: 691
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

Offline

#3 2011-05-19 07:56:18

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

Offline

Board footer

Powered by FluxBB