// ATC KB IDP
// version 20190619
// Marjolein Deryck (KULeuven, Eavise)
// For online test : copy-paste code below in http://adams.cs.kuleuven.be/idp/server.html

vocabulary V {				
    type Icao constructed from {Light, Medium, Heavy, Super}				
    type Mtom isa int				
    type Aircraft isa string				
    type Separation isa int
    				
    AircraftIcaoCategory(Aircraft,Icao) 				
    MTOM(Aircraft, Mtom)
  				
    type Leader isa Aircraft				
    type Follower isa Aircraft				
    				
    IcaoSeparation(Leader, Follower) : Separation				
    MRS : Separation
    				
}				
				
theory T:V{				
    				
//*********Icao Regulations******************				
	    !a[Aircraft] w[Mtom]: 
    	AircraftIcaoCategory(a, Light) <= 				
	 	MTOM(a,w) 
    	& w =< 7000. 			
				
				
	 	!a[Aircraft] w[Mtom]: 
    	AircraftIcaoCategory(a, Medium) <= 				
		MTOM(a,w) 
    	& 7000 < w 
    	& w=< 136000.			
				
				
		!a[Aircraft] w[Mtom]: 
    	AircraftIcaoCategory(a, Heavy) <=				
	 	MTOM(a,w) 
    	& 136000 < w 
    	& a ~= a388
    	& a ~= a38f.		
        
    
		AircraftIcaoCategory("a388", Super). 
    	AircraftIcaoCategory("a38f", Super). 
    
				
    				
//******Icao Separation*************				
				
    	!l[Leader] f[Follower]:			
        IcaoSeparation(l,f) = MRS <=  //OK
    		AircraftIcaoCategory(l, Medium) 	
    		& AircraftIcaoCategory(f, Medium).			
				
        
    	!l[Leader] f[Follower]:	
    	IcaoSeparation(l,f) = MRS <= 
    		AircraftIcaoCategory(l, Medium) 
    		& AircraftIcaoCategory(f,Heavy).			
			
    
    	!l[Leader] f[Follower]:	
		IcaoSeparation(l,f) = MRS <=  //OK
    		AircraftIcaoCategory(l, Light).	
    
    
    	!l[Leader] f[Follower]:	
        IcaoSeparation(l,f) = MRS <=  //OK
    		AircraftIcaoCategory(f,Super).			
				
		
    	!l[Leader] f[Follower]:	
        IcaoSeparation(l,f) = 4 <= 	//OK
    		AircraftIcaoCategory(l, Heavy) 
    		& AircraftIcaoCategory(f, Heavy).			
				
		
        !l[Leader] f[Follower]:	
    	IcaoSeparation(l,f) = 5 <=	 
    		AircraftIcaoCategory(l, Heavy) 
    		& AircraftIcaoCategory(f, Medium).			
			
    
		!l[Leader] f[Follower]:	    
        IcaoSeparation(l,f) = 5 <= 	//OK
    		AircraftIcaoCategory(l, Medium) 
    		& AircraftIcaoCategory(f, Light).			
				
				
		!l[Leader] f[Follower]:	
    	IcaoSeparation(l,f) = 6 <=	 
    		AircraftIcaoCategory(l, Heavy) 
    		& AircraftIcaoCategory(f, Light).			
			
    
        !l[Leader] f[Follower]:	
    	IcaoSeparation(l,f) = 6 <= 	
    		AircraftIcaoCategory(l, Super) 
    		& AircraftIcaoCategory(f, Heavy).			
				
				
		!l[Leader] f[Follower]:			
        IcaoSeparation(l,f) = 7 <=	 //OK
    		AircraftIcaoCategory(l, Super) 
    		& AircraftIcaoCategory(f, Medium).			
				
				
		!l[Leader] f[Follower]:			
        IcaoSeparation(l,f) = 8 <= 	//OK
    		AircraftIcaoCategory(l, Super) 
    		& AircraftIcaoCategory(f, Light).		
    			
        }			
    				
structure S1 : V {				
    				
    //specific value assignments, can be changed by user:	
    Leader = {n262}				
    Follower = {s601}	
    				
    //Variable domains				
    Mtom = {0..575000}				
    Separation = {2..9}	
    MRS = 3
  	    			
    
   MTOM = 	{	
be91	,	4218	;
a388 	,  	575000	;        
a38f	, 	138000	;        
a500	,	3175	;	
sgup	,	77110	;	
l39		,  	4700	;	
ch7a	,	553		;	
n262	,	10301	;	
s601	,	6599	;	
s210	,	56000	;	
at3p1	,	2267	;	
at3p2	,	3492	;	
at3t	,	4159	}	
				
// MTOW, Wingspan and AppSpeed have been left out for performance reasons
}

procedure main() {
    stdoptions.nbmodels = 5
    printmodels(modelexpand(T, S1))  
   // printmodels(modelexpand(T, S2))  
    
}