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.