/* The Dining Philosophers problem
* the treatment follows that in:
* "Communicating Sequential Processes" by C.A.R. Hoare
* Prentice-Hall International Series in Computer Science
*/

PHIL = (sitdown -> left.get 
                -> right.get -> left.put 
                             -> right.put -> arise -> PHIL).

FORK = (left.get-> left.put -> FORK 
        | right.get -> right.put -> FORK
       ).

// Check Safety - produces trace to deadlock
// Run - reproduce deadlock
||COLLEGE(N=5) = ( phil[0..N-1]:PHIL || fork[0..N-1]:FORK )/
		  { phil[i:0..N-1].left  / fork[i].left,
		    phil[i:0..N-1].right / fork[((i-1)+N)%N].right}.

// FOOTMAN allows only N-1 philosophers to sitdown at the same time
FOOTMAN(N=5) 	= FOOT[0],
FOOT[0] 	= (phil[0..N-1].sitdown->FOOT[1]),
FOOT[i:1..N-2] 	= (phil[0..N-1].sitdown->FOOT[i+1]|phil[0..N-1].arise->FOOT[i-1]),
FOOT[N-1]	= (phil[0..N-1].arise->FOOT[N-2]).

//it better to disable minimisation (Options) when checking this
||NEWCOLLEGE(N=5) = (COLLEGE(N) || FOOTMAN(N)).