const
	NumOfForks	:	5;
	NumOfPhilosophers	:	5;
	MININT	:	-32768;
	MAXINT	:	32767;
type
	PhilosopherState	:	enum { thinking,eating };
	ForkState	:	enum { available,nonavailable };
var
	forks	:	array [0..NumOfForks-1] of ForkState;
	philosophers	:	array [0..NumOfPhilosophers-1] of PhilosopherState;
	p0	:	MININT..MAXINT;
	p1	:	MININT..MAXINT;
	p2	:	MININT..MAXINT;
	p3	:	MININT..MAXINT;
	p4	:	MININT..MAXINT;

Rule "ReturnForks"
philosophers [ p0 ] =eating
==>
begin
  philosophers [ p0 ] :=thinking;
  forks [ p0 ] :=available;
  forks [ (p0 + 1) NumOfForks ] :=available;
end;

Rule "PickUpForks"
((philosophers [ p0 ] =thinking) & (forks [ p0 ] =available) & (forks [ (p0 + 1) NumOfForks ] =available))
==>
begin
  philosophers [ p0 ] :=eating;
  forks [ p0 ] :=nonavailable;
  forks [ (p0 + 1) NumOfForks ] :=nonavailable;
end;

Rule "PickUpForks_Philosopher"
((philosophers [ p1 ] =thinking) & (forks [ p1 ] =available) & (forks [ (p1 + 1) NumOfForks ] =available))
==>
begin
  philosophers [ p1 ] :=eating;
  forks [ p1 ] :=nonavailable;
  forks [ (p1 + 1) NumOfForks ] :=nonavailable;
end;

Rule "ReturnForks_Philosopher"
philosophers [ p1 ] =eating
==>
begin
  philosophers [ p1 ] :=thinking;
  forks [ p1 ] :=available;
  forks [ (p1 + 1) NumOfForks ] :=available;
end;

Rule "PickUpForks_Philosopher_Philosopher"
((philosophers [ p2 ] =thinking) & (forks [ p2 ] =available) & (forks [ (p2 + 1) NumOfForks ] =available))
==>
begin
  philosophers [ p2 ] :=eating;
  forks [ p2 ] :=nonavailable;
  forks [ (p2 + 1) NumOfForks ] :=nonavailable;
end;

Rule "ReturnForks_Philosopher_Philosopher"
philosophers [ p2 ] =eating
==>
begin
  philosophers [ p2 ] :=thinking;
  forks [ p2 ] :=available;
  forks [ (p2 + 1) NumOfForks ] :=available;
end;

Rule "PickUpForks_Philosopher_Philosopher_Philosopher"
((philosophers [ p3 ] =thinking) & (forks [ p3 ] =available) & (forks [ (p3 + 1) NumOfForks ] =available))
==>
begin
  philosophers [ p3 ] :=eating;
  forks [ p3 ] :=nonavailable;
  forks [ (p3 + 1) NumOfForks ] :=nonavailable;
end;

Rule "ReturnForks_Philosopher_Philosopher_Philosopher"
philosophers [ p3 ] =eating
==>
begin
  philosophers [ p3 ] :=thinking;
  forks [ p3 ] :=available;
  forks [ (p3 + 1) NumOfForks ] :=available;
end;

Rule "PickUpForks_Philosopher_Philosopher_Philosopher_Philosopher"
((philosophers [ p4 ] =thinking) & (forks [ p4 ] =available) & (forks [ (p4 + 1) NumOfForks ] =available))
==>
begin
  philosophers [ p4 ] :=eating;
  forks [ p4 ] :=nonavailable;
  forks [ (p4 + 1) NumOfForks ] :=nonavailable;
end;

Rule "ReturnForks_Philosopher_Philosopher_Philosopher_Philosopher"
philosophers [ p4 ] =eating
==>
begin
  philosophers [ p4 ] :=thinking;
  forks [ p4 ] :=available;
  forks [ (p4 + 1) NumOfForks ] :=available;
end;

startstate
begin
  p4:=4;
  p3:=3;
  p2:=2;
  p1:=1;
  p0:=0;
  for i_1:= 0 to NumOfPhilosophers-1 Do
	  philosophers[i_1]:=thinking
	endfor;
  for i_1:= 0 to NumOfForks-1 Do
	  forks[i_1]:=available
	endfor;
end;