server:	fork,
services	{take_first, take_second, release_first, release_second}
states	{taken, free}
;
server:	chair,
services	{may_eat, may_think, may_take_second, may_release_second}
states	{think, waits_eat, eat, first_left, first_right}
;
agent:	ph (servers fork[2]:fork,chair:chair),
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_release_second, chair.first_left}	-> {ph.fork[2].release_second, chair.think},
	{ph.chair.may_take_second, chair.first_left}	-> {ph.fork[2].take_second, chair.waits_eat},
	{ph.chair.may_release_second, chair.first_right}	-> {ph.fork[1].release_second, chair.think},
	{ph.chair.may_take_second, chair.first_right}	-> {ph.fork[1].take_second, chair.waits_eat},
	{ph.chair.may_think, chair.think}	-> {ph.fork[1].take_first, chair.first_left},
	{ph.chair.may_think, chair.think}	-> {ph.fork[2].take_first, chair.first_right},
	{ph.chair.may_think, chair.think}	-> {ph.chair.may_think, chair.think},
	{ph.chair.may_eat, chair.waits_eat}	-> {ph.chair.may_eat, chair.eat},
	{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].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].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].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},
};
agent:	ph__1 (servers fork[2]:fork,chair:chair),
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_release_second, chair.first_left}	-> {ph__1.fork[1].release_second, chair.think},
	{ph__1.chair.may_take_second, chair.first_left}	-> {ph__1.fork[1].take_second, chair.waits_eat},
	{ph__1.chair.may_release_second, chair.first_right}	-> {ph__1.fork[2].release_second, chair.think},
	{ph__1.chair.may_take_second, chair.first_right}	-> {ph__1.fork[2].take_second, chair.waits_eat},
	{ph__1.chair.may_think, chair.think}	-> {ph__1.fork[2].take_first, chair.first_left},
	{ph__1.chair.may_think, chair.think}	-> {ph__1.fork[1].take_first, chair.first_right},
	{ph__1.chair.may_think, chair.think}	-> {ph__1.chair.may_think, chair.think},
	{ph__1.chair.may_eat, chair.waits_eat}	-> {ph__1.chair.may_eat, chair.eat},
	{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].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].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].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},
};
agents	ph[2]:ph,ph__1:ph__1;
servers	fork[3]:fork,chair[3]:chair;
init	-> {
	ph[1](fork[1,2],chair[1]).chair[1].may_think,
	ph[2](fork[2,3],chair[2]).chair[2].may_think,
	ph__1(fork[1,3],chair[3]).chair[3].may_think,
	<j=1..3>fork[j].free,
	<j=1..3>chair[j].think,
}