Spinroot

KeesPronk

Member

Registered: 2011-01-04

Posts: 12

Possible bug in spin 6.2.5 interpreter?

It seems there is a problem with the spin interpreter and with iSpin (spin version 6.2.5)

Please note the following excerpt from a larger program:

//
#define p   1   
#define q   2   
#define r   4   

  byte    i0205 = 0;
  byte    i0305 = p;
  byte    i0404 = 0;
  byte    i0405 = q;
  byte    i0505 = 0;

init {
  do

  :: ( ((i0404 & p) == p) && ((i0405 & r) != r) ) -> d_step{ i0404 =  i0404 & (~p); i0405 =  i0405 | p }; 

  :: ( ((i0405 & p) == p) && ((i0404 & r) != r) ) -> d_step{ i0405 =  i0405 & (~p); i0404 =  i0404 | p }; 

  :: ( ((i0305 & p) == p) && ((i0405 & r) != r) ) -> d_step{ i0305 =  i0305 & (~p); i0405 =  i0405 | p }; 

  :: ( ((i0505 & p) == p) && ((i0405 & r) != r) ) -> d_step{ i0505 =  i0505 & (~p); i0405 =  i0405 | p };

  :: ( ((i0405 & p) == p) && ((i0505 & r) != r) ) -> d_step{ i0405 =  i0405 & (~p); i0505 =  i0505 | p }; 

  :: ( ((i0405 & p) == p) && ((i0305 & r) != r) ) -> d_step{ i0405 =  i0405 & (~p); i0305 =  i0305 | p }; 

  :: ( ((i0305 & p) == p) && ((i0205 & r) != r) ) -> d_step{ i0305 =  i0305 & (~p); i0205 =  i0205 | p }; 
  od;
}

Start the program from the command line with 'spin -i test.pml'.
You start in position 0305; there are 2 transitions enabled (OK).
Take choice 3; this brings you from position 0305 to position 0405.
Note that there are 3 transitions enabled now (OK).
Take choice 2: this brings you from position 0405 to 0404.
As there exists only one transition out of 0404 (back to 0405) the interpreter will proceed automatically to 0405.

However, there are now _4_ transitions enabled; 3 from 0405 (OK) one from 0404 (not OK).

The wrong transition probably is the one from the 0404 position you have just left, which is still enabled (try to take it).

When running the same program with iSpin in interpretative mode, one also sees 4 transitions being enabled.
When running in iSPin it seems that some "instruction pointer" in the interpreter is staying behind (the yellow line#).

Is it a bug, or is it a misinterpretation?

Regards, Kees Pronk

PS
I haven't checked if the verifyer works correctly on this example.