system nDiningPhilosophers
{
	top record Object
	{
	}
	
	record Fork extends Object
	{
		boolean isHeld;
	}
	
	const MAX
	{
		PHILOSOPHERS = 3;
		//PHILOSOPHERS = 5;
		//PHILOSOPHERS = 7;
		//PHILOSOPHERS = 10;
	}
	
	thread Philosopher(Fork fork1, Fork fork2)
	{
		loc loc0: live {}
			when !fork1.isHeld do
			{
				fork1.isHeld := true;
			}
			goto loc1;
		loc loc1: live {}
			when !fork2.isHeld do
			{
				fork2.isHeld := true;
			}
			goto loc2;
		loc loc2: live {}
			when true do
			{
				fork2.isHeld := false;
			}
			goto loc3;
		loc loc3: live {}
			when true do
			{
				fork1.isHeld := false;
			}
			goto loc0;
	}
	
	main thread MAIN()
	{
		int counter;
		Fork[] forks;
		
		loc loc0: live { forks }
			when MAX.PHILOSOPHERS > 1 do invisible
			{
				forks := new Fork[MAX.PHILOSOPHERS];
			}
			goto loc1;
			when MAX.PHILOSOPHERS <= 1 do
			{
			}
			return;
		loc loc1: live { counter, forks }
			when counter == 0 do invisible
			{
				forks[counter] := new Fork;
				counter := counter + 1;
			}
			goto loc1;
			when counter < MAX.PHILOSOPHERS
				 && counter != 0 do invisible
			{
				forks[counter] := new Fork;
				start Philosopher(forks[counter - 1], forks[counter]);
				counter := counter + 1;
			}
			goto loc1;
			when counter == MAX.PHILOSOPHERS do invisible
			{
				start Philosopher(forks[counter -1], forks[0]);
				//start Philosopher(forks[0], forks[counter -1]);
			}
			return;
	}
}