/** Concurrency: State Models and Java Programs
 *             Jeff Magee and Jeff Kramer
 *  modified for SEG-2106 course by Gregor v. Bochmann
 *  
 *  with counter to limit number of concurrently active philosophers
 *         ( in order to avoid deadlocks )
 */

PHIL = (think -> incr -> right.get -> left.get -> decr
          -> eat -> left.put -> right.put -> PHIL).
         
FORK = (get -> put -> FORK).

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