// Optimisation ATC KB
// Marjolein Deryck (KULeuven, Eavise)
// Optimise the landing order for 4 out of 5 aircraft
// To test : copy-paste code in online IDE : http://adams.cs.kuleuven.be/idp/server.html
// to do : generalise for other number of landing aircraft

vocabulary V {				
    type Aircraft constructed from {a319,a388,b788,be9l,e190}
    type NM isa int
    Boogfunct(Aircraft, Aircraft): NM
    Som : NM
    Leader : Aircraft
    Follower1 : Aircraft
    Follower2 : Aircraft
    Follower3 : Aircraft
    Waiting1 : Aircraft
    Waiting2 : Aircraft
    Waiting3 : Aircraft
    Waiting4 : Aircraft
    				
    Next(Aircraft):Aircraft
}				
				
theory T:V{		

    ? l : l = Leader <=> ? w : w = Waiting1.
    ? f : f = Follower1 <=> ? w : w = Waiting2.
  	? f : f = Follower2 <=> ? w : w = Waiting3.
    ? f : f = Follower3 <=> ? w : w = Waiting4.


    Leader = Waiting1 | Leader = Waiting2 | Leader = Waiting3 | Leader = Waiting4.
  	Follower1 = Waiting1 | Follower1 = Waiting2 | Follower1 = Waiting3 | Follower1 = Waiting4.
	Follower2 = Waiting1 | Follower2 = Waiting2 | Follower2 = Waiting3 | Follower2 = Waiting4.
	Follower3 = Waiting1 | Follower3 = Waiting2 | Follower3 = Waiting3 | Follower3 = Waiting4.

	! ac : Leader = ac => Follower1 ~= ac & Follower2 ~= ac & Follower3 ~= ac.
    ! ac : Follower1 = ac => Leader ~= ac & Follower2 ~= ac & Follower3 ~= ac.
    ! ac : Follower2 = ac => Leader ~= ac & Follower1 ~= ac & Follower3 ~= ac.
    ! ac : Follower3 = ac => Leader ~= ac & Follower2 ~= ac & Follower1 ~= ac.
    
    Boogfunct(Leader, Follower1) + Boogfunct(Follower1, Follower2) + Boogfunct(Follower2, Follower3) = Som.
    
    Next(Leader) = Follower1.
    Next(Follower1) = Follower2.
    Next(Follower2) = Follower3.
    
    }

structure S : V {				
   NM = {2..40}
   Boogfunct = {	a319	,	a319	,	3	;
	a319	,	a388	,	3	;
	a319	,	b788	,	3	;
	a319	,	be9l	,	5	;
	a319	,	e190	,	3	;
	a388	,	a319	,	7	;
	a388	,	a388	,	3	;
	a388	,	b788	,	6	;
	a388	,	be9l	,	8	;
	a388	,	e190	,	7	;
	b788	,	a319	,	5	;
	b788	,	a388	,	3	;
	b788	,	b788	,	4	;
	b788	,	be9l	,	6	;
	b788	,	e190	,	5	;
	be9l	,	a319	,	3	;
	be9l	,	a388	,	3	;
	be9l	,	b788	,	3	;
	be9l	,	be9l	,	3	;
	be9l	,	e190	,	3	;
	e190	,	a319	,	5	;
	e190	,	a388	,	3	;
	e190	,	b788	,	3	;
	e190	,	be9l	,	3	;
	e190	,	e190	,	3	}

     
   Waiting1	=	a319
Waiting2	=	a388
Waiting3	=	b788
Waiting4	=	be9l
}

term som:V{
    
    sum{ac: Leader = ac | Follower1 = ac | Follower2 = ac | Follower3 = ac : Boogfunct(ac,Next(ac))}
}

procedure main() {
    stdoptions.nbmodels = 1
    //stdoptions.xsb = false
    printmodels(modelexpand(T, S))
    printmodels(minimize(T, S, som))
    }