Spinroot

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

I have founded the following message about my error message:

https://spinroot.com/fluxbb/viewtopic.php?id=115

I'm going to translate this solution to my model.

Thanks.