HOLD_PREVIOUS

CONST

NumOfPhilosophers: 5;
NumOfForks: 5;

TYPE

PhilosopherState: ENUM {thinking , eating};
ForkState: ENUM {available , nonavailable};

VAR

philosophers: ARRAY[NumOfPhilosophers] OF PhilosopherState INITVAL thinking;
forks: ARRAY[NumOfForks] OF ForkState INITVAL available;

MODULE Philosopher(i: INTEGER){
	
	TRANS PickUpForks:
		enable: ((philosophers[i] = thinking) /\ (forks[i] = available) /\ 
			 (forks[(i+1) % NumOfForks]= available));
		assign: philosophers[i]' := eating;
			forks[i]' := nonavailable;
			forks[(i+1) % NumOfForks]' := nonavailable;
	TRANS ReturnForks:
		enable: philosophers[i] = eating;
		assign: philosophers[i]' := thinking;
			forks[i]' := available;
			forks[(i+1) % NumOfForks]' := available;
}

MODULE SYSTEM(){
	VAR

	p0: integer INITVAL 0;
	p1: integer INITVAL 1;
	p2: integer INITVAL 2;
	p3: integer INITVAL 3;
	p4: integer INITVAL 4;
	
	((((Philosopher(p0) ||| Philosopher(p1)) ||| Philosopher(p2)) ||| Philosopher(p3)) ||| Philosopher(p4)) 
}