115: Tail Assignment

language Essence 1.3
$ prob115.essence: Tail Assignment
$ Problem details available in:
$   A Constraint Programming Model for Tail Assignment
$   M. Gronkvist
$   Proc. First International Conference on Integration of AI and OR Techniques
$   in Constraint Programming for Combinatorial Optimization Problems (CPAIOR
$   2004), LNCS 3011, pp. 287-301, 2004.

$ n_flights: the number of flights
$ n_planes: the number of aircraft
$ maint_freq: how many flights an aircraft may make before needing maintenance
given n_flights, n_planes, maint_freq : int(1..)

$ Flight: flight identifiers
$ Plane: aircraft identifiers
letting Flight be domain int(1..n_flights),
        Plane be domain int(1..n_planes)

$ network: the flight network. which flights can follow from which other flights
$ can_fly: which aircraft can make which flights
$ carry_in: the last flight made by each aircraft
$ maint: the set of flights that have a maintenance facility at their
$        destination
given network : relation of (Flight*Flight),
      can_fly : relation of (Plane*Flight),
      carry_in : function (total) Plane --> Flight,
      maint : set of Flight

$ route: the route for each aircraft
find route : function (total) Plane --> function int(1..n_flights) --> Flight

such that
$ all elements of the range of the function 'route' are valid sequences
    forAll s in range(route) . forAll i in defined(s) . i=1 \/ (i-1) in defined(s),
$ the route for each aircraft begins with a flight that may follow on from the
$ last flight that it made
    forAll p : Plane . (carry_in(p), route(p)(1)) in network,
$ each aircraft is able to make the flights on its route
    forAll p : Plane . forAll a in range(route(p)) . tuple (a) in can_fly(p,_),
$ flights are made in the correct order
    forAll s in range(route) . forAll i : int(1..n_flights) , i <= |s|-1 .
        (s(i),s(i+1)) in network,
$ every flight is made exactly once
    forAll f : Flight . exists p : Plane . f in range(route(p)),
    forAll p1,p2 : Plane . |range(route(p1)) intersect range(route(p2))| = 0,
$ every aircraft visits a maintenance depot frequently enough
    forAll s in range(route) . forAll i : int(1..n_flights - maint_freq) , i <= |s| - maint_freq .
        exists j : int(i..i+maint_freq) . s(j) in maint