/** dining philosophers - abstract model
 *  
 *  each philosopher picks up both forks concurrently, in a single action
 *  
 *  Gregor v. Bochmann, December 2008 */

const N=10     //number of philosophers and of forks  --  on my computer the composition of the system works for up to N = 10

PHILO(I=0)  = ( think[I] -> get[I]  -> eat[I] ->  put[I] -> PHILO ).

FORK(J=0)  = ( get[J] ->  put[J] -> FORK | get[(J+1)%N] -> put[(J+1)%N] -> FORK ).
// fork j can be used by philosopher i=j or by philosopher i=j+1 modulo N

||TABLE = forall[i:0..N-1] ( PHILO(i) || FORK(i) ).