#include <stdlib.acsr>
// Define usefull macros
#define REP_ACT(ACTION,COUNT,NEXT)					    \
	 scope(rec X.(ACTION:X),dummy,(COUNT),NIL,(NEXT),NIL)

// Define constants
#define	Nt	3	// Number of taxiways

#define	Np	10	// Number of planes

#define	Tl	4	// Time to land a plane was 4

#define	Tt	2	// Time to move a plane to a taxiway

#define	Tc	2	// Time to cross from taxiway to a gate

#define	Td	3	// Time to take-off

#define Te	(Tl+Tt+1) //Time before sending an emergency
			// landing request Te > (Tl + Tt)

#define Tf	(Tl+Tt+Tc+Td+3) // Time to get perm. to land before crashing
			// Tf > (Tl + Tt + (Tc+1) + (Td+1))


/////////////////////////////////
LandingUnit	= UNTIL_INTRPT(ZOMBIE,
			       (landAsk,1).LdTry + (eLandAsk,3).ELdTry);
LdTry		= UNTIL_INTRPT(LandBusy,
			(eLandAsk,3).ELdTry +
			   ('taxi,2).('landGrant,1).Landing);
ELdTry		= UNTIL_INTRPT(LandBusy,
			('eTaxi,1).('eLandGrant,3).Landing);
Landing		= scope(LandBusy,
			dummy, Tl + Tt,
			NIL, LandingUnit, NIL);

LandBusy	= rec X. ({}:X + 
 		          (landAsk,1).('landDeny,1).X);

/////////////////////////////////
TakeOffUnit	= UNTIL_INTRPT(ZOMBIE, 
			(departAsk,1).UNTIL_INTRPT(TkOffBusy,
				scope(ReserveRWTaxi || TkOffBusy,
				      dummy, Td+1, 
				      NIL, TakeOffUnit, NIL) ));

ReserveRWTaxi	= {(DprtRwT[1],2),(DprtRwT[2],2),(DprtRwT[3],2)}:
		  ('departGrant,1).
		  rec X. {(DprtRwT[1],4),(DprtRwT[2],4),(DprtRwT[3],4)}:X;

TkOffBusy	= rec X. ({}:X + (departAsk,1).('departDeny,1).X);


/////////////////////////////////
TaxiManager	= TN || TE;

TN		= UNTIL_INTRPT(ZOMBIE, (taxi,1).REP_ACT({}, Tl+Tt, TW[1]));
TW[1]		= UNTIL_INTRPT(ZOMBIE, (taxi,1).REP_ACT({}, Tl+Tt, TW[2]) +
			       {(DprtRwT[1],1)}:('cross,1).TN);
TW[2]		= UNTIL_INTRPT(ZOMBIE, 
		{(DprtRwT[1],3),(DprtRwT[2],3)}:
				('cross,1).('cross,1).TN);

TE		= UNTIL_INTRPT(ZOMBIE, (eTaxi,1).REP_ACT({}, Tl+Tt, TW[3]));
TW[3]		= UNTIL_INTRPT(ZOMBIE, 
		   {(DprtRwT[3],3)}:('eCross,1).TE +
		   {(DprtRwT[1],3),(DprtRwT[3],3)}:('eCross,1).TE +
		   {(DprtRwT[1],3),(DprtRwT[2],3),(DprtRwT[3],3)}:
			('eCross,1).TE );

/////////////////////////////////
Controller	= LandingUnit || TakeOffUnit;

Airport		= (Controller || TaxiManager) \{taxi,eTaxi};
		

/////////////////////////////////
AirPlane[i]	= UNTIL_INTRPT(ZOMBIE, Arriving[i] + Departing[i]) {i,1,Np};

Arriving[i]	= ('landAsk,1).scope(LandAskR, 
			dummy, Te, 
			NIL, EPlaneLand[i], 
			(landGrant,2).PlaneLand[i]) {i, 1, Np};

LandAskR	= rec Y.({}:Y + (landDeny,1).{}:{}:
			rec X.({}:X + ('landAsk,1).Y));
			
PlaneLand[i]	= REP_ACT({(arrivalRW,1)}, Tl, TaxiStart[i]) {i, 1, Np};
TaxiStart[i]	= Choice[REP_ACT({(arrivalRW,1),(taxiway[j],1)}, 
			Tt, TaxiTry[i,j]), {j, 1, Nt-1}] {i,1, Np};
			
EPlaneLand[i]	= scope(ELandAsk,
			saved, Tf,
			ELand[i], NIL, NIL) {i,1,Np};
ELandAsk	= UNTIL_INTRPT(ZOMBIE, 
			('eLandAsk,1).UNTIL_INTRPT(ZOMBIE, 
					(eLandGrant,1).('saved,1).NIL));

ELand[i]	= REP_ACT({(arrivalRW,1)}, Tl, 
			  REP_ACT({(arrivalRW,1),(taxiway[Nt],1)}, 
				  Tt, TaxiTry[i,Nt])) {i, 1, Np};
TaxiTry[i,Nt]   = (eCross,1).
		  REP_ACT({(dprtRWT[Nt],4),(taxiway[Nt],1)}, Tc, AirPlane[i])
		+
		  {(taxiway[Nt],1)}:TaxiTry[i,Nt]  {i, 1, Np};
TaxiTry[i,j]	= (cross,1).
		  REP_ACT({(dprtRWT[j],4),(taxiway[j],1)}, Tc, AirPlane[i])
		+
		  {(taxiway[j],1)}:TaxiTry[i,j]  {i, 1, Np}, {j, 1, Nt-1};

/////////////////////////////////

Departing[i]	= ('departAsk,1).UNTIL_INTRPT(DepartAskR, 
			(departGrant,2).REP_ACT({(departRW,1)}, Td, 
				AirPlane[i])) {i,1,Np};
DepartAskR	= rec Y. ({}:Y + (departDeny,1).{}:{}:
 			rec X.({}:X + ('departAsk,1).Y));

/////////////////////////////////

System[i]	= [(Airport || Parallel[AirPlane[j], {j,1,i}])
		   \{landAsk, landGrant, landDeny,
		     eLandAsk, eLandGrant, 
		     departAsk, departGrant, departDeny,		
		     cross, eCross}
	          ] {arrivalRW,departRW,
		     taxiway[1],taxiway[2],taxiway[3],
		     DprtRwT[1],DprtRwT[2],DprtRwT[3]}
		  {i, 1, Np};