Spinroot

Hi,

I'm kind of new to Spin and I was hoping for some help on a problem I'm having. I have a pretty basic state machine with only 6 states and two threads working in these states. Threads can move from state to state by hearing messages from other threads or on its own. All in all, this seems like a perfect application for Spin.

The problem is when I run the verifier on my pml file (i.e, I do the commands "spin -a twothreads.pml", "cc pan.c", "./a.out", "spin -t twothreads.pml"), I'm getting deadlocked in my program and I'm not sure why. It prints out the final state of the program where it claims there are no more executable actions:

        queue 1 (threadBuffers[0]): [CLAUSE][CLAUSE][CLAUSE][CLAUSE][CLAUSE][CLAUSE][CLAUSE][CLAUSE]
        queue 2 (threadBuffers[1]): [CLAUSE][CLAUSE][CLAUSE][CLAUSE][CLAUSE][CLAUSE][CLAUSE][CLAUSE]
        states[0] = 0
        states[1] = 0

However in my pml file I have (inside a do loop, and i is either 0 or 1 depending on the thread):

         ::  (states[i] == 0)  -> /*read something from the buffer*/             
             threadBuffers[1-i] ? msg;                                             
             if                                                                   
                 ::(msg == CLAUSE) ->                                             
                      skip; /*do nothing*/

                  ...(other code down here)

So shouldn't it at least have the option of dequeuing one of these CLAUSE messages from the queue? I guess I must not understand completely what the verifier is doing. Here is the link to the entire pml file if that will help:

https://dl.dropbox.com/u/68065978/twothreads.pml

Sorry if the terminology I'm using isn't quite right or if I didn't make sense! Thanks for any help, I appreciate it!

-Max