/** Concurrency: State Models and Java Programs
 *             Jeff Magee and Jeff Kramer
 *  
 */

PHIL(I=0) = (when (I%2==0)
                 sitdown->left.get->right.get
                   ->eat->left.put->right.put->arise->PHIL
            |when (I%2==1)
                 sitdown->right.get->left.get
                   ->eat->left.put->right.put->arise->PHIL
            ).

FORK = (get -> put -> FORK).

||DINERS(N=5)= 
   forall [i:0..N-1] 
   (phil[i]:PHIL(i) 
   ||{phil[i].left,phil[((i-1)+N)%N].right}::FORK).