server:	fork (servers chair[2]:chair; agents ph[2]:ph),
services	{take_first,take_second,release_first,release_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_sec, fork.free},
	<j=1..2>{ph[j].fork.release_second, fork.taken}	-> {ph[j].chair[j].aft_release_sec, fork.free},
};
server:	butler (servers chair[3]:chair; agents ph[3]:ph),
services	{take,release},
states	{v0,v[2]},
actions {
	<j=1..3>{ph[j].butler.take, butler.v0}	-> {ph[j].chair[j].may_take_first, butler.v[1]},
	<i=1..1><j=1..3>{ph[j].butler.take, butler.v[i]}	-> {ph[j].chair[j].may_take_first, butler.v[i+1]},
	<i=2..2><j=1..3>{ph[j].butler.release, butler.v[i]}	-> {ph[j].chair[j].aft_release, butler.v[i-1]},
	<j=1..3>{ph[j].butler.release, butler.v[1]}	-> {ph[j].chair[j].aft_release, butler.v0},
};
server:	chair (servers fork[2]:fork,butler[2]:butler; agents ph:ph),
services	{may_eat,may_think,may_take_first,may_take_second,may_release_first,may_release_sec,aft_release,aft_release_sec},
states	{think,first_left,first_right,after_eat},
actions {
	{ph.chair.may_think, chair.think}	-> {ph.butler[1].take, chair.first_left},
	{ph.chair.may_think, chair.think}	-> {ph.butler[2].take, 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.fork[1].release_first, chair.first_left},
	{ph.chair.may_eat, chair.first_right}	-> {ph.fork[2].release_first, chair.first_right},
	{ph.chair.may_release_first, chair.first_left}	-> {ph.fork[1].release_first, chair.first_left},
	{ph.chair.may_release_first, chair.first_right}	-> {ph.fork[2].release_first, chair.first_right},
	{ph.chair.may_release_sec, chair.first_left}	-> {ph.fork[2].release_second, chair.first_left},
	{ph.chair.may_release_sec, chair.first_right}	-> {ph.fork[1].release_second, chair.first_right},
	{ph.chair.aft_release_sec, chair.first_left}	-> {ph.butler[1].release, chair.first_left},
	{ph.chair.aft_release_sec, chair.first_right}	-> {ph.butler[2].release, chair.first_right},
	{ph.chair.aft_release, chair.first_left}	-> {ph.chair.may_think, chair.think},
	{ph.chair.aft_release, chair.first_right}	-> {ph.chair.may_think, chair.think},
};
agent:	ph;
agents	ph[3]:ph;
servers	fork[3]:fork,chair[3]:chair,butler[2]:butler;
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],butler[1,2],ph[1]).think,
	chair[2](fork[2,3],butler[1,2],ph[2]).think,
	chair[3](fork[3,1],butler[1,2],ph[3]).think,
	butler[1](chair[1..3],ph[1..3]).v0,
	butler[2](chair[1..3],ph[1..3]).v0,
}