Spinroot

A forum for Spin users

You are not logged in.

#1 2011-06-08 04:48:19

sudakshina
Member
Registered: 2011-06-08
Posts: 7

Dubious use of else

I have written a code in promela, the loop in the model is as follows:

active [N] proctype P
{
again:
statements;

do
  :: (i == turn) -> receive msg1 from ith_process;
                        calculations;
                        if (result of calculations) -> send msg2 to
ith_process; fi;
                        turn++;
  :: (receive msg2 from process(s)) -> calculations;
  :: else -> i++;
           if (i == N) -> i = 0; break;
od;

goto again;
}

Here, it is showing an error "dubious use of else combined with i/o".

I have run the code on jSPIN and iSPIN, both are giving the same error.
Output of the simulation run is as follows:
1st time (i.e. 1st run in the do loop):: All pid(s) executes the loop
(with either option1 or 2) successfully
2nd time ::
if they have to execute either option1 or option2, then they will execute
if they have to execute the  last option (i.e. else option) then
they will execute, but, for the 3rd time, they are not able to enter
into the loop
(i.e. once after executing the else option, Processes are not able
to enter into the loop for the next time)
and thus, the Process which has stared 1st, is supposed to receive
the 'msg2' from all other processes, is not able to do so and its
'timeout'.

please help me, how to resolve the problem.

Thanks,
Sudakshina

Offline

#2 2011-06-08 05:07:29

spinroot
forum
Registered: 2010-11-18
Posts: 695
Website

Re: Dubious use of else

the construct is flagged as an error because it implies a race condition.
you can avoid the error by using a normal expression as a guard for the 2nd option, instead of a receive operation.
for instance, you can write something like :: nempty(q) -> q?mesg2
or perhaps still better: :: atomic { nempty(q) -> q?mesg2 }

Offline

#3 2011-06-08 07:38:26

sudakshina
Member
Registered: 2011-06-08
Posts: 7

Re: Dubious use of else

Thanks a lot Sir,

The 'dubious use of else' problem is solved by using the 'atomic{nmpty(q)->q?msg2}'.
The recent scenario (i.e.  simulation output) is as follows:

P0 has started 1st, followed by P2, then P3 and then P1.
Now, all the 4 Ps have executed the 1st option of the 'do loop'
(i.e. i==0 and so, all Ps have received msg1 from P0 and send msg2 to P0.)
(So, P0 is having 4 no. of msg2 in its receiving channel.)
P2 is executed :: since its receiving channel is empty, so executed the else option (i.e. i++)
P0 :: receives msg2
P3 :: i++
p1 :: i++
timeout

Why the loop is not executing for the next time? and why timeout?

The expected output in the 2nd run would be:
P0 :: receives msg2 (upto total 4 times)
P1 :: received msg1 from P1 and sends msg2
p2 :: received msg1 from P1 and do not sends msg2
p3 :: received msg1 from P1 and do not sends msg2

Please help.


Thanks,
Sudakshina

Last edited by sudakshina (2011-06-08 07:39:05)

Offline

#4 2011-06-09 03:42:29

spinroot
forum
Registered: 2010-11-18
Posts: 695
Website

Re: Dubious use of else

in a nondeterministic do or if selection
*all* executable guards are equally likely to be taken -- so it may not be the one you had in mind.
but apart from that, if execution blocks, and no process can execute anymore, that means that all guards are false
to give a more precise answer please show the exact promela model you're working on.
the example has too many syntactical errors to be helpful for us

Offline

#5 2011-06-09 05:04:39

sudakshina
Member
Registered: 2011-06-08
Posts: 7

Re: Dubious use of else

Sir,

the code is not completely mine, so i do not have authority to share (2 more seniors are working on this), but I can assure you one thing that, there is no syntactic error, otherwise it would not run for the 1st time also. but, there may be any logical error, which I am not able to find out.

as per do loop I hae mentioned in my 1st post

i=0; turn=0;
do
:: (i == turn) -> the P (i.e. P0/1/2/3) will receive msg1 from Pi;
                      if Pi has started 1st, then P will send msg2 to Pi;
                       turn++;
:: when (i != turn) and P's receiving channel is not empty
                       then P will receive msg2
:: else ( i.e. when ( i != turn) and P's receiving channel is empty
                        then i++; (so for the next run  i will be equal to turn, and again the 1st option will be executed)
od

Offline

#6 2011-06-09 07:26:04

sudakshina
Member
Registered: 2011-06-08
Posts: 7

Re: Dubious use of else

Sir,

Thanks a lot for your kind and continuous guidance, I am able to solve the problem, I was facing.
I had to mention a 'else' condition for each 'if' condition, along with a 'goto' statement to direct the pointer to the starting of the 'do' loop.

Regards,
sudakshina

Offline

Board footer

Powered by FluxBB