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