/** 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 )
 */

const Number = 5
range Int = 0..Number-1

PHIL(I=0) = 
(think[I] -> up[I] -> get_l[I] -> get_r[((I-1)+Number)%Number] -> down[I]  
          -> eat[I] -> put_l[I] -> put_r[((I-1)+Number)%Number] -> PHIL).

FORK(I=0) 
= (get_l[I] -> put_l[I] -> FORK | get_r[I] -> put_r[I] -> FORK).
        
||DINERS(N=Number)= 
   forall [i:0..N-1] 
       (PHIL(i) ||FORK(i)).


// Counter with minimum and maximum value (0 and Number-1, respectively)
// -- like the counter for a limited-size queue 

// The interactions are up (for increment) and down (for decrement)
// Since it has to count interactions coming from different philosophers, 
//     there there are transitions for each philosopher, distinguished by the index (only values from 0 through 4 are supported)

COUNTER(N=0) = C[N],
C[v:Int]    = (when(v<(Number-1)) up[0] -> C[v+1] | when(v<(Number-1)) up[1] -> C[v+1] | when(v<(Number-1)) up[2] -> C[v+1] 
             | when(v<(Number-1)) up[3] -> C[v+1] | when(v<(Number-1)) up[4] -> C[v+1]  
             | when(v>0) down[0] -> C[v-1] | when(v>0) down[1] -> C[v-1] | when(v>0) down[2] -> C[v-1]
             | when(v>0) down[3] -> C[v-1] | when(v>0) down[4] -> C[v-1] ). 


||COUNTED_DINERS = (DINERS || COUNTER).