If someone could explain to me why I am getting a timeout with the following code that would be great. I understand, or at least I think I do, the idea of a timeout, but with the do loops I thought this would stop this. Any advice is appreciated.
mtype wantp = false;
mtype wantq = false;
mtype turn = 1;
active proctype p()
{
do
:: printf ("non critical section for p\n");
wantp = true;
(wantq ==true);
if
:: (turn == 2)->
wantp = false;
/* wait for turn ==1*/
(turn ==1);
wantp = true;
fi;
printf("CRITICAL SECTION for P\n");
turn = 2;
wantp = false;
od
}
active proctype q()
{
do
:: printf("non critical section for q\n");
wantq = true;
(wantp ==true);
if
:: (turn == 1)->
wantq = false;
(turn ==2);
wantq = true;
fi;
printf("CRITICAL SECTION for Q\n");
turn = 1;
wantq = false;
od
}
When you perform a SPIN verification and a problem arises, such as a 'timeout', you have what is known as a 'trail' file. The trail file shows you the exact path through the program execution that leads to the problem.
Assuming the above file is called test.pml. You perform the following:
$ spin -a test.pml
$ gcc -o pan pan.c
$ ./pan
# info about verification, shows timeout
# view the detailed trail file
$ spin -p -t test.pml
Then, look at the details printed out to figure out how the timeout happened.