Spinroot

I am using iSpin 1.0.4 and Spin 6.0.1 which I recently downloaded and installed. I ran iSpin on a simple mutual exclusion protocol below. The verification produced an error trail which I then simulated in the simulator. At about the 4th step of the simulation, the variable want0 is shown with value 1, which seems wrong to me.

I had noticed a similar discrepancy earlier. Is there a problem with iSpin's display of variables?

If needed I can send the trail file as well.

Thanks,

Deepak.

---------------------------------------------------------------------
byte turn = 0;
bool want0 = false;
bool want1 = false;
bool CS0 = false;
bool CS1 = false;

proctype process0(){

         do
         :: want0 = true;
            ((!want1) || (turn == 0));  /* block till condition is true */
            turn = 0;
            CS0 = true;   /* enter CS */
            CS0 = false;
            want0 = false;
            turn = 1;
         od
}

proctype process1(){

         do
         :: want1 = true;
            ((!want0) || (turn == 1));  /* block till condition is true */
            turn = 1;
            CS1 = true;   /* enter CS */
            CS1 = false;
            want1 = false;
            turn = 0;
         od
}

init {
    run process0();
    run process1();
}     

ltl mutualex {
     always (!(CS0 && CS1));
}

ltl nostarv0 {
     always (want0 -> eventually (CS0));
}