Quelle DepartureTMI.vdmsl Sprache: VDM

/*
  A model of an Air Traffic Flow Management (ATFM) departure Traffic Management Initiative
  (TMI) with the constraints:
  - a set of flights wish to depart an airport;
  - each flight may only take off from certain runways;
  - each flight has a preferred take off time;
  - each flight has an acceptable take off window;
  - only certain runways are available;
  - runways have a maximum rate at which departures can take place;
  - the TMI runs for a specific time interval.

  Within these constraints, the goal is to allocate a take off time and runway to flights
  in an optimal manner.

  This module depends on modules Set, Seq and ISO8601 contained in the ISO8601 example located at

    http://overturetool.org/download/examples/VDMSL/
*/
module DepartureTMI
imports from ISO8601 all,
        from Seq all,
        from Set all
exports types AirportDesig
              FlightId
              RunwayDesig
              struct FlightInfo
              struct RunwayRates
              Rate
              struct TMIConfig
              struct Allocation
              DepartureTMI
        functions departureTMI: TMIConfig +> DepartureTMI * set of FlightId

definitions

types

  -- An airport designator.
  AirportDesig = token;

  -- A flight identifier.
  FlightId = token;

  -- A runway designator.
  RunwayDesig = token;

  -- Information on when a flight can take off and what runways it can use.
  FlightInfo :: canUse   : set1 of RunwayDesig -- The runways the flight can use
                preferred: ISO8601`DTG         -- The preferred take off time
                window   : ISO8601`Interval    -- The acceptable take off window
  inv flight == -- The preferred time falls in the take off window
                ISO8601`inInterval(flight.preferred, flight.window);

  -- The rate for each available runway.
  -- The domain of the map is the set of available runways.
  RunwayRates = map RunwayDesig to Rate
  inv rr == -- At least one runway is available.
            dom rr <> {};

  -- The minimum duration between consecutive departures.
  Rate = ISO8601`Duration;

  -- A TMI configuration for departures at an airport.
  TMIConfig :: airport: AirportDesig                -- The airport location designator
               period : ISO8601`Interval            -- The period over which the TMI runs
               flight :-map FlightId to FlightInfo  -- The flights that wish to depart
               rates  :-RunwayRates                 -- The runway rates
  inv tmiCfg == -- Every flight window overlaps the TMI period
                (forall f in set rng tmiCfg.flight & ISO8601`overlap(f.window, tmiCfg.period)) and
                -- Every flight can use at least one of the available runways
                (forall f in set rng tmiCfg.flight & f.canUse inter dom tmiCfg.rates <> {});

  -- An allocated runway and take off time.
  Allocation :: rwy : RunwayDesig   -- The allocated runway
                ttot: ISO8601`DTG;  -- The target take off time

  -- A departure TMI is a mapping from flights to their allocated runways and departure times.
  DepartureTMI = inmap FlightId to Allocation;

functions

  -- Run the TMI: determine a runway and take off time for each flight.
  -- Highlight those flights that could not be accommodated.
  departureTMI(config:TMIConfig) res:DepartureTMI * set of FlightId
  post -- The result is a solution.
       satisfies(config, res.#1) and
       -- Of all solutions, the result is one with the least cost.
       (forall tmi:DepartureTMI
             & satisfies(config, tmi) => cost(config, res.#1) <= cost(config, tmi)) and
       -- Those flights that could not be accommodated in the TMI are returned.
       res.#2 = dom config.flight \ dom res.#1;

  -- Does a TMI satisfy the constraints with respect to a configuration?
  satisfies: TMIConfig * DepartureTMI +> bool
  satisfies(config,tmi) ==
    -- Only candidate flights are allocated.
    dom tmi subset dom config.flight and
    -- The flight can use the allocated runway.
    (forall f in set dom tmi & tmi(f).rwy in set config.flight(f).canUse) and
    -- An allocated runway is in the set of available runways.
    (forall f in set dom tmi & tmi(f).rwy in set dom config.rates) and
    -- The allocated take off time falls within the acceptable take off window.
    (forall f in set dom tmi & ISO8601`inInterval(tmi(f).ttot, config.flight(f).window)) and
    -- The allocated take off time falls within the period of the TMI.
    (forall f in set dom tmi & ISO8601`inInterval(tmi(f).ttot, config.period)) and
    -- Two flights allocated the same runway depart at least the required duration apart.
    (forall f,g in set dom tmi
          & f <> g and tmi(f).rwy = tmi(g).rwy
            => ISO8601`durGeq(ISO8601`diff(tmi(f).ttot, tmi(g).ttot), config.rates(tmi(f).rwy)));

  -- The cost of a TMI as a function of the deviations of the individual flights.
  -- The ideal solution is where every flight is allocated its preferred time.
  cost: TMIConfig * DepartureTMI -> nat
  cost(config,tmi) == ISO8601`durToSeconds(ISO8601`sumDuration(deviations(config, tmi)));

  -- The deviation of each flight expressed as a duration of time.
  -- Flights that could not be accommodated are also assigned a deviation.
  deviations: TMIConfig * DepartureTMI -> seq of ISO8601`Duration
  deviations(config,tmi) ==
    let allFlights = Set`toSeq[FlightId](dom config.flight)
    in [ if f in set dom tmi
         then allocatedDeviation(config.flight(f), tmi(f))
         else omittedDeviation(config.period, config.flight(f).window)
       | f in seq allFlights
       ];

  -- The deviation of a flight from an allocated time.
  allocatedDeviation: FlightInfo * Allocation +> ISO8601`Duration
  allocatedDeviation(flight,alloc) == ISO8601`diff(flight.preferred, alloc.ttot);

  -- The deviation of a flight that is omitted from a TMI.
  omittedDeviation: ISO8601`Interval * ISO8601`Interval +> ISO8601`Duration
  omittedDeviation(period, flightWindow) ==
    let dur = ISO8601`durFromInterval(flightWindow)
    in if ISO8601`within(flightWindow, period) then dur else ISO8601`durDivide(dur, 2);

end DepartureTMI

quality87%

¤ Dauer der Verarbeitung: 0.15 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.