Spinroot

deepakdsouza

Member

Registered: 2011-04-25

Posts: 1

iSpin variable display

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));
}

spinroot

forum

Registered: 2010-11-18

Posts: 700

Website

Re: iSpin variable display

you can reproduce these trails from the command line to see more clearly what happens when you execute the model

for the counter example that you get with a default run of the verifier (./pan) the first few steps from the traceback from the command line look like this

$ spin -a tryme
$ cc -o pan pan.c
$ ./pan
[.....]
$ spin -t -v -p -l -g tryme
ltl mutualex: [] (! ((CS0) && (CS1)))
ltl nostarv0: [] ((! (want0)) || (<> (CS0)))
spin: couldn't find claim 3 (ignored)
        2 = :init:
        1 = process1
        0 = process0
Starting process0 with pid 2
  2:    proc  0 (:init:) tryme:36 (state 1)     [(run process0())]
Starting process1 with pid 3
  4:    proc  0 (:init:) tryme:37 (state 2)     [(run process1())]
  6:    proc  2 (process1) tryme:23 (state 1)   [want1 = 1]
                want1 = 1
  8:    proc  2 (process1) tryme:24 (state 2)   [((!(want0)||(turn==1)))]

You can see that in step 6 here the value of want1 is set to 1 (since it's symmetric, it could just as easily bee want0, as in your case).
Hope that helps!