A forum for Spin users
You are not logged in.
Pages: 1
Ya
Thnks sir, its workin now
Sir,
I am not generating random number, I have created 4 independent Processes :
active [4] proctype p()
{
.........
}
with the same code jSPIN is showing the 4 processes randomly (in any sequence) for each simulation run,
but iSPIN is showing a same sequence (P3, P2, P0, P1) all the time.
I have ran my promela code on both jSIPN and iSPIN.
but when i run the simulation run in iSPIN, always is shows the same sequence of processes,
i.e. P2 is started 1st followed by P3 then P0 and then P1.
Please tell me how to change that sequence, I want to see the output when P0 will start 1st.
Thanks,
sudakshina
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
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
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
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
Pages: 1