A forum for Spin users
You are not logged in.
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
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
Thanks a lot
Offline
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