#DEFINE N 4
#DEFINE K 4

server:		quarter(agents car[N];servers prevq:quarter,nextq:quarter,in:road,out:road),  
services	{trye[K],oke[K],takee[K],tryi[K],takei[K],occupy[K]},
states		{free,freew,rese,resew,resi,occ,occw},								
actions{
<i=1..N><j=1..K>{car[i].quarter.tryi[j], quarter.free} -> {car[i].in.oki[j], quarter.resi},
<i=1..N><j=1..K>{car[i].quarter.tryi[j], quarter.freew} -> {car[i].in.oki[j], quarter.resi},
<i=1..N><j=1..K>{car[i].quarter.tryi[j], quarter.rese} -> {car[i].quarter.tryi[j], quarter.resew},
<i=1..N><j=1..K>{car[i].quarter.takei[j], quarter.resi} -> {car[i].quarter.occupy[j], quarter.occ},

<i=1..N><j=1..K-1>{car[i].quarter.trye[j], quarter.free} -> {car[i].prevq.oke[j+1], quarter.rese},
<i=1..N><j=1..K-1>{car[i].quarter.takee[j], quarter.rese} -> {car[i].quarter.occupy[j], quarter.occ},
<i=1..N><j=1..K-1>{car[i].quarter.takee[j], quarter.resew} -> {car[i].quarter.occupy[j], quarter.occw},

<i=1..N>	{car[i].quarter.occupy[1], quarter.occ} -> {car[i].out.leave, quarter.free},
<i=1..N>	{car[i].quarter.occupy[1], quarter.occw} -> {car[i].out.leave, quarter.freew},
<i=1..N><j=2..K>{car[i].quarter.occupy[j], quarter.occ} -> {car[i].nextq.trye[j-1], quarter.occ},
<i=1..N><j=2..K>{car[i].quarter.occupy[j], quarter.occw} -> {car[i].nextq.trye[j-1], quarter.occw},

<i=1..N><j=2..K>{car[i].quarter.oke[j], quarter.occ} -> {car[i].nextq.takee[j-1], quarter.free},
<i=1..N><j=2..K>{car[i].quarter.oke[j], quarter.occw} -> {car[i].nextq.takee[j-1], quarter.freew},
}

server:		road(agents car[N]; servers qin:quarter),
services	{leave,oki[K]},
states		{idle,tries},
actions{
//j=1 right, j=2 straight, j=3 left, j=4 turn back
<i=1..N><j=1..K>{car[i].road.leave, road.idle} -> {car[N].qin.tryi[j], road.tries},
<i=1..N><j=1..K>{car[i].road.oki[j], road.tries} -> {car[N].qin.takei[j], road.idle},
}


servers 	quarter[K],road[K];
agents	 	car[N];	
 
init	->	{ 
		quarter[1](car[1..N],quarter[4,2],road[1,2]).free,
	        quarter[2](car[1..N],quarter[1,3],road[2,3]).free,
		quarter[3](car[1..N],quarter[2,4],road[3,4]).free,
		quarter[4](car[1..N],quarter[3,1],road[4,1]).free,

	<j=1..4>road[j](car[1..N],quarter[j]).idle,

	<i=1..N>car[i].road[1].leave, 	
	}.