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