system BUF;
server:	buf,
services	{put, get}
states	{elem0, elem[3]}
;
server:	Sprod,
services	{doSth, ok_put}
states	{neutral, prod}
;
server:	Scons,
services	{doSth, ok_get}
states	{neutral, cons}
;
agent:	Aprod (servers buf:buf,Sprod:Sprod),
actions {
	<j=1..2>{Aprod.buf.put, buf.elem[j]}	-> {Aprod.Sprod.ok_put, buf.elem[j+1]},
	{Aprod.buf.put, buf.elem0}	-> {Aprod.Sprod.ok_put, buf.elem[1]},
	{Aprod.Sprod.doSth, Sprod.neutral}	-> {Aprod.buf.put, Sprod.prod},
	{Aprod.Sprod.ok_put, Sprod.prod}	-> {Aprod.Sprod.doSth, Sprod.neutral},
};
agent:	Acons (servers buf:buf,Scons:Scons),
actions {
	{Acons.buf.get, buf.elem[1]}	-> {Acons.Scons.ok_get, buf.elem0},
	<j=2..3>{Acons.buf.get, buf.elem[j]}	-> {Acons.Scons.ok_get, buf.elem[j-1]},
	{Acons.Scons.ok_get, Scons.cons}	-> {Acons.Scons.doSth, Scons.neutral},
	{Acons.Scons.doSth, Scons.neutral}	-> {Acons.buf.get, Scons.cons},
};
agents	Aprod[3]:Aprod,Acons[3]:Acons;
servers	buf:buf,Sprod[3]:Sprod,Scons[3]:Scons;
init	-> {
	Aprod[1](buf,Sprod[1]).Sprod[1].doSth,
	Aprod[2](buf,Sprod[2]).Sprod[2].doSth,
	Aprod[3](buf,Sprod[3]).Sprod[3].doSth,
	Acons[1](buf,Scons[1]).Scons[1].doSth,
	Acons[2](buf,Scons[2]).Scons[2].doSth,
	Acons[3](buf,Scons[3]).Scons[3].doSth,
	buf.elem0,
	<j=1..3>Sprod[j].neutral,
	<j=1..3>Scons[j].neutral,
}