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 PickUpForks1:
		enable: ((i = 1) /\ (philosophers[1] = thinking) /\ (forks[1] = available) /\ 
			 (forks[2]= available));
		assign: philosophers[1]' := eating;
			forks[1]' := nonavailable;
			forks[2]' := nonavailable;

	TRANS PickUpForks2:
		enable: ((i = 2) /\ (philosophers[2]= thinking) /\ (forks[2] = available) /\ 
			 (forks[3]= available));
		assign: philosophers[2]' := eating;
			forks[2]' := nonavailable;
			forks[3]' := nonavailable;


	TRANS PickUpForks3:
		enable: ((i = 3) /\ (philosophers[3] = thinking) /\ (forks[3] = available) /\ 
			 (forks[4]= available));
		assign: philosophers[3]' := eating;
			forks[3]' := nonavailable;
			forks[4]' := nonavailable;

	TRANS PickUpForks4:
		enable: ((i = 4) /\ (philosophers[4] = thinking) /\ (forks[4] = available) /\ 
			 (forks[0]= available));
		assign: philosophers[4]' := eating;
			forks[4]' := nonavailable;
			forks[0]' := nonavailable;

	TRANS PickUpForks0:
		enable: ((i = 0) /\ (philosophers[0] = thinking) /\ (forks[0] = available) /\ 
			 (forks[1]= available));
		assign: philosophers[0]' := eating;
			forks[0]' := nonavailable;
			forks[1]' := nonavailable;

	TRANS ReturnForks1:
		enable: ((i = 1) /\ (philosophers[1] = eating));
		assign: philosophers[1]' := thinking;
			forks[1]' := available;
			forks[2]' := available;

	TRANS ReturnForks2:
		enable: ((i = 2) /\ (philosophers[2] = eating));
		assign: philosophers[2]' := thinking;
			forks[2]' := available;
			forks[3]' := available;

	TRANS ReturnForks3:
		enable: ((i = 3) /\ (philosophers[3] = eating));
		assign: philosophers[3]' := thinking;
			forks[3]' := available;
			forks[4]' := available;

	TRANS ReturnForks4:
		enable: ((i = 4) /\ (philosophers[4] = eating));
		assign: philosophers[4]' := thinking;
			forks[4]' := available;
			forks[0]' := available;

	TRANS ReturnForks0:
		enable: ((i = 0) /\ (philosophers[0] = eating));
		assign: philosophers[0]' := thinking;
			forks[0]' := available;
			forks[1]' := 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)) 
}