Spinroot

A forum for Spin users

You are not logged in.

#1 2013-12-16 17:35:51

haozheng
Member
Registered: 2013-12-16
Posts: 8

Cannot find invalid end state in dinning philosopher

Hi, I am new to SPIN, and the following two Promela models for the dinning philosopher problem confuse me.  I attached the two models below.  To me, they are the same except the different ways on how processes are created. However, SPIN finds an invalid end state for model 1, but none for model 2.  The version of the SPIN I use is 6.2.5.  The commands used to compile the models are

../Src6.2.5/spin -a $1
gcc -O2 -DNOFAIR -DNOBOUNDCHECK -DSAFETY -o pan pan.c
./pan -m10000000 -n -Q5

Any insight and help would be very appreciated.

HZ 



/*
             Model 1
*/
byte fork[5];


active proctype phil_0() {

think: if
::  d_step {fork[0]==0;fork[0] = 1;}  goto one;

fi;
one: if
::  d_step {fork[1]==0;fork[1] = 1;}  goto eat;

fi;
eat: if
:: fork[0] = 0; goto finish;

fi;
finish: if
:: fork[1] = 0; goto think;

fi;
}

active proctype phil_1() {

think: if
::  d_step {fork[1]==0;fork[1] = 1;}  goto one;

fi;
one: if
::  d_step {fork[2]==0;fork[2] = 1;}  goto eat;

fi;
eat: if
:: fork[1] = 0; goto finish;

fi;
finish: if
:: fork[2] = 0; goto think;

fi;
}

active proctype phil_2() {

think: if
::  d_step {fork[2]==0;fork[2] = 1;}  goto one;

fi;
one: if
::  d_step {fork[3]==0;fork[3] = 1;}  goto eat;

fi;
eat: if
:: fork[2] = 0; goto finish;

fi;
finish: if
:: fork[3] = 0; goto think;

fi;
}

active proctype phil_3() {

think: if
::  d_step {fork[3]==0;fork[3] = 1;}  goto one;

fi;
one: if
::  d_step {fork[4]==0;fork[4] = 1;}  goto eat;

fi;
eat: if
:: fork[3] = 0; goto finish;

fi;
finish: if
:: fork[4] = 0; goto think;

fi;
}

active proctype phil_4() {

think: if
::  d_step {fork[4]==0;fork[4] = 1;}  goto one;

fi;
one: if
::  d_step {fork[0]==0;fork[0] = 1;}  goto eat;

fi;
eat: if
:: fork[4] = 0; goto finish;

fi;
finish: if
:: fork[0] = 0; goto think;

fi;
}




/* ================================================= */

/*
      Model 2
*/


byte fork[5];


proctype phil(byte left; byte right) {

think: if
::  d_step {left==0; left = 1;}  goto one;

fi;
one: if
::  d_step {right ==0; right = 1;}  goto eat;

fi;
eat: if
:: left = 0; goto finish;

fi;
finish: if
:: right = 0; goto think;

fi;
}

init {         atomic {run phil(fork[0], fork[1]);
                 run phil(fork[1], fork[2]);
            run phil(fork[2], fork[3]);
                 run phil(fork[3], fork[4]);
            run phil(fork[4], fork[0]) }
}

Offline

#2 2013-12-16 18:03:56

spinroot
forum
Registered: 2010-11-18
Posts: 695
Website

Re: Cannot find invalid end state in dinning philosopher

In the second version of the model you are passing the parameters by value, not by reference.
So in effect 'left' and 'right' are just local variables -- assigning to them does not change the value for any other process -- only for the local process that receives those parameters.
To make it work, you'd have to pass the indices into the fork array for each process -- so that they can indeed modify the shared global variables in the fork array.

Offline

#3 2013-12-23 18:00:48

haozheng
Member
Registered: 2013-12-16
Posts: 8

Re: Cannot find invalid end state in dinning philosopher

Thanks a lot for the comment.  I tried the revised model as suggested, and it worked with an invalid end state found for model 2.

Offline

Board footer

Powered by FluxBB