Spinroot

A forum for Spin users

You are not logged in.

#1 2017-04-11 21:45:00

xueying
Member
Registered: 2017-04-11
Posts: 3

generate random initiation value for the variables

I am an almost new user of SPIN, and in the verification of SPIN.

for example I create a new variable a  the type is byte
Does SPIN go over all random initiate values for a during the exhaustive verification .

like, a range is [0...255]
SPIN Checks all possible value of a ?

And I am also confused with the seed value when do the simulation.
What does it mean?


Thanks a lot.

Offline

#2 2017-04-11 22:01:21

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

Re: generate random initiation value for the variables

Spin will only check the values you assign. By default this will be 0.
You can non-deterministically assign other values with an if statements or a select statement
See the manual pages online.
http://spinroot.com/spin/Man

Offline

#3 2017-04-11 23:36:02

xueying
Member
Registered: 2017-04-11
Posts: 3

Re: generate random initiation value for the variables

Thanks a lot smile

Offline

#4 2017-05-11 16:53:55

salcaraz
Member
Registered: 2017-02-26
Posts: 7

Re: generate random initiation value for the variables

Following with this question....

From the code below:

----------------------------------
active proctype P () {
  byte i,v;

  for (i : 0 .. 20) {
     select (v : 50..100); printf("v(%d)=%d\n",i,v)
  }
}
----------------------------------------


and the output:

$ spin p.pml
      v(0)=51
      v(1)=51
      v(2)=50
      v(3)=53
      v(4)=51
      v(5)=50
      v(6)=50
      v(7)=50
      v(8)=51
      v(9)=50
      v(10)=50
      v(11)=55
      v(12)=51
      v(13)=50
      v(14)=50
      v(15)=50
      v(16)=50
      v(17)=52
      v(18)=51
      v(19)=50
      v(20)=51
1 process created


The cuestion is: is correct the behaviour above, because it seems 'a little bit' non-deterministic??

Thank you in advance.

/salva

Last edited by salcaraz (2017-05-11 18:08:36)

Offline

#5 2017-05-11 22:00:53

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

Re: generate random initiation value for the variables

that sample does look a little biased, yes
but you can only judge the randomness after doing thousands of samples
(law of big numbers)

Offline

Board footer

Powered by FluxBB