server:	fork (servers chair[2]:chair; agents ph[2]:ph),
services	{take_first,take_second,release_first,release_second,check_first,check_second},
states	{taken,free},
actions {
	<j=1..2>{ph[j].fork.take_first, fork.free}	-> {ph[j].chair[j].may_take_second, fork.taken},
	<j=1..2>{ph[j].fork.take_second, fork.free}	-> {ph[j].chair[j].may_eat, fork.taken},
	<j=1..2>{ph[j].fork.release_first, fork.taken}	-> {ph[j].chair[j].may_release_second, fork.free},
	<j=1..2>{ph[j].fork.release_second, fork.taken}	-> {ph[j].chair[j].may_think, fork.free},
	<j=1..2>{ph[j].fork.check_first, fork.free}	-> {ph[j].chair[j].may_check_second, fork.free},
	<j=1..2>{ph[j].fork.check_second, fork.free}	-> {ph[j].chair[j].may_take_first, fork.free},
	<j=1..2>{ph[j].fork.check_first, fork.taken}	-> {ph[j].chair[j].occupied, fork.taken},
	<j=1..2>{ph[j].fork.check_second, fork.taken}	-> {ph[j].chair[j].occupied, fork.taken},
};
server:	locker (servers chair[3]:chair; agents ph[3]:ph),
services	{lock,unlock,unlock_fail},
states	{locked,unlocked},
actions {
	<j=1..3>{ph[j].locker.lock, locker.unlocked}	-> {ph[j].chair[j].may_check_first, locker.locked},
	<j=1..3>{ph[j].locker.unlock, locker.locked}	-> {ph[j].chair[j].may_eat, locker.unlocked},
	<j=1..3>{ph[j].locker.unlock_fail, locker.locked}	-> {ph[j].chair[j].may_think, locker.unlocked},
};
server:	chair (servers fork[2]:fork,locker:locker; agents ph:ph),
services	{may_eat,may_think,may_check_first,may_check_second,may_take_first,may_take_second,may_release_first,may_release_second,occupied},
states	{think,eat,first_left,first_right},
actions {
	{ph.chair.may_think, chair.think}	-> {ph.chair.may_think, chair.think},
	{ph.chair.may_think, chair.think}	-> {ph.locker.lock, chair.first_left},
	{ph.chair.may_think, chair.think}	-> {ph.locker.lock, chair.first_right},
	{ph.chair.may_check_first, chair.first_left}	-> {ph.fork[1].check_first, chair.first_left},
	{ph.chair.may_check_first, chair.first_right}	-> {ph.fork[2].check_first, chair.first_right},
	{ph.chair.may_check_second, chair.first_left}	-> {ph.fork[2].check_second, chair.first_left},
	{ph.chair.may_check_second, chair.first_right}	-> {ph.fork[1].check_second, chair.first_right},
	{ph.chair.may_take_first, chair.first_left}	-> {ph.fork[1].take_first, chair.first_left},
	{ph.chair.may_take_first, chair.first_right}	-> {ph.fork[2].take_first, chair.first_right},
	{ph.chair.may_take_second, chair.first_left}	-> {ph.fork[2].take_second, chair.first_left},
	{ph.chair.may_take_second, chair.first_right}	-> {ph.fork[1].take_second, chair.first_right},
	{ph.chair.may_eat, chair.first_left}	-> {ph.locker.unlock, chair.eat},
	{ph.chair.may_eat, chair.first_right}	-> {ph.locker.unlock, chair.eat},
	{ph.chair.may_eat, chair.eat}	-> {ph.chair.may_eat, chair.eat},
	{ph.chair.may_eat, chair.eat}	-> {ph.fork[1].release_first, chair.first_left},
	{ph.chair.may_eat, chair.eat}	-> {ph.fork[2].release_first, chair.first_right},
	{ph.chair.may_release_second, chair.first_left}	-> {ph.fork[2].release_second, chair.think},
	{ph.chair.may_release_second, chair.first_right}	-> {ph.fork[1].release_second, chair.think},
	{ph.chair.occupied, chair.first_left}	-> {ph.locker.unlock_fail, chair.think},
	{ph.chair.occupied, chair.first_right}	-> {ph.locker.unlock_fail, chair.think},
};
agent:	ph;
agents	ph[3]:ph;
servers	fork[3]:fork,chair[3]:chair,locker:locker;
init	-> {
	<j=1..3>ph[j].chair[j].may_think,
	fork[1](chair[3,1],ph[3,1]).free,
	fork[2](chair[1,2],ph[1,2]).free,
	fork[3](chair[2,3],ph[2,3]).free,
	chair[1](fork[1,2],locker,ph[1]).think,
	chair[2](fork[2,3],locker,ph[2]).think,
	chair[3](fork[3,1],locker,ph[3]).think,
	locker(chair[1..3],ph[1..3]).unlocked,
}