Spinroot

A forum for Spin users

You are not logged in.

#1 2011-06-10 05:33:53

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

iSPIN

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

Offline

#2 2011-06-10 07:05:59

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

Re: iSPIN

are you maybe following a trail (guided simulation) ?
or are you always using the same seed for the random number generator?
if you change the seed, you get a different run

Offline

#3 2011-06-10 10:30:16

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

Re: iSPIN

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.

Offline

#4 2011-06-11 20:07:36

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

Re: iSPIN

You may not be generating random numbers, but Spin is doing just that to make nondeterministic choices in simulation.  You can set the seed for the random number generator that Spin uses in the simulation panel.
(Using a fixed seed makes it possible to have a reproducible run, so that you can recreate an interesting scenario that you see in simulations -- without it, every simulation run would be different and it would become quite difficult to recreate an earlier run.)

Offline

#5 2011-06-13 09:44:36

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

Re: iSPIN

Ya
Thnks sir, its workin now

Offline

Board footer

Powered by FluxBB