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