A forum for Spin users
You are not logged in.
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
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
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