Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: atc.vdmpp Sprache: VDM

Original von: VDM^©

class AirTrafficController is subclass of GLOBAL

instance variables

radars    : set of Radar    := {};
obstacles : set of Obstacle := {};
history   : map FOId to (seq of Position) := {|->};

operations

public getDirectionVectors : FOId ==> seq of Vector
getDirectionVectors(id) ==
  let hist = history(id),
      p1 = hist(3),
      p2 = hist(2),
      p3 = hist(1)
  in
    return [mk_Vector(p1.coord.X - p2.coord.X,
                      p1.coord.Y - p2.coord.Y),
            mk_Vector(p2.coord.X - p3.coord.X,
                      p2.coord.Y - p3.coord.Y)]
pre id in set dom history and len history(id) = 3;

public getAltitudeHistory : FOId ==> seq of nat
getAltitudeHistory(id) ==
  let hist = history(id),
      lastHist = hist(1,...,2)
  in
    return [lastHist(i).altitude | i in set inds lastHist]
pre id in set dom history and len history(id) = 3;

public updateHistory : () ==> ()
updateHistory() ==
(
   cleanUpHistory();
   for all r in set radars
   do
    (for all fo in set r.getDetected()
     do
      registerHistory(fo);
    )
);

private registerHistory : FO ==> ()
registerHistory(fo) ==
(let id = fo.getId(),
      coor = fo.getCoordinates(),
      alt = fo.getAltitude()
  in
    if id in set dom history
    then history := history ++
                    {id |-> addHistory(history(id),coor,alt)}
    else history := history munion
                    {id |-> addHistory([],coor,alt)}
);

public cleanUpHistory : () ==> ()
cleanUpHistory() ==
(let alldetected = dunion {r.getDetected() | r in set radars},
      allids = { fo.getId() | fo in set alldetected }
  in
    history := allids <: history
);

functions
private addHistory : History * Coordinates * Altitude  -> History
addHistory(hist,coord,alt) ==
  if(len hist < 3)
  then hist ^ [mk_Position(coord,alt)]
  else tl hist ^ [mk_Position(coord,alt)];

operations

public addRadar : Radar ==> ()
addRadar(r) ==
  radars := {r} union radars;

public addObstacle : Obstacle ==> ()
addObstacle(ob) ==
  obstacles := {ob} union obstacles;

public findThreats : () ==> ()
findThreats() ==
  let allFOs = dunion { r.getDetected() | r in set radars }
  in
   (for all fo in set allFOs
    do
      for all ob in set obstacles
      do
        if not isFOSafe(ob,fo.getPosition())
        then writeObjectWarning(ob,fo)
        else
          if len history(fo.getId()) = 3
          then willFObeSafe(ob,fo);
    for all r in set radars
    do
      if r.saturatedRadar()
      then writeRadarWarning(r)
   );

public detectedByTwoRadars : set of Radar ==> set of FO
detectedByTwoRadars(r) ==
  return dunion {a.getDetected() inter b.getDetected()
                 | a,b in set r & a <> b};

public detectedByAllRadars : set of Radar ==> set of FO
detectedByAllRadars(r) ==
  return dinter {rad.getDetected() | rad in set r};

public Step : () ==> ()
Step() ==
( for all r in set radars
  do
    r.Scan(MSAW`airspace);
  updateHistory();
  findThreats();
);

functions

isFOatSafeAltitude : MinimumSafetyAltitude * Position -> bool
isFOatSafeAltitude(msa,pos) ==
  msa <> <NotAllowed> and msa < pos.altitude;

operations

isFOSafe : Obstacle * Position ==> bool
isFOSafe(obs,pos) ==
  let obsloc      = obs.getCoordinates(),
      secureRange = obs.getSecureRange(),
      foloc       = pos.coord
  in
    if isPointInRange(obsloc,secureRange,foloc)
    then isFOatSafeAltitude(obs.getMSA(),pos)
    else return false;

willFObeSafe : Obstacle * FO ==> ()
willFObeSafe(obs,fo) ==
  let pred = isPredictPossible(fo)
  in
    for all p in set pred
    do
      if not isFOSafe(obs,p)
      then
        let id   = fo.getId(),
            cs   = fo.getCoordinates(),
            alt  = fo.getAltitude(),
            type = <EstimationWarning>,
            msa  = obs.getMSA(),
            t    = World`timerRef.GetTime()
        in
         (World`env.handleFOWarningEvent(id, cs, alt, type, msa, t);
          return
         )
pre fo.getId() in set dom history and  len history(fo.getId()) = 3;


private writeObjectWarning : Obstacle * FO ==> ()
writeObjectWarning(obs,fo) ==
  let id   = fo.getId(),
      cs   = fo.getCoordinates(),
      alt  = fo.getAltitude(),
      type = obs.getType(),
      msa  = obs.getMSA(),
      t    = World`timerRef.GetTime()
  in
    World`env.handleFOWarningEvent(id, cs, alt, type, msa, t);

private writeRadarWarning : Radar ==> ()
writeRadarWarning(r) ==
  let coord   = r.getLocation(),
      range   = r.getRange(),
      radWarn = <Saturated>,
      num     = card r.getDetected(),
      t       = World`timerRef.GetTime()
  in
    World`env.handleRadarWarningEvent(coord,range,radWarn,num,t);


private isPredictPossible : FO ==> [set of Position]
isPredictPossible(fo)==
  let hist = history(fo.getId())
  in
    if len hist < 3
    then return nil
    else return predictPosition(fo)
pre fo.getId() in set dom history ;


private predictPosition : FO ==> set of Position
predictPosition(fo) ==
  let foid   = fo.getId(),
      vs     = getDirectionVectors(foid),
      estVec = vectorRotate(vs(1),signedVectorAngle(vs(2),vs(1))),
      estAlt = predictAltitude(getAltitudeHistory(foid)),
      estCoo = addVectorToPoint(estVec,history(foid)(3)),
      estPos = mk_Position(estCoo,estAlt)

  in
    return calculateNeighborhood(estPos)
pre fo.getId() in set dom history and len history(fo.getId()) = 3;

functions
private calculateNeighborhood : Position -> set of Position
calculateNeighborhood(pos) ==
{pos,
  mk_Position(addVectorToPoint(mk_Vector(2,0),pos),pos.altitude),
  mk_Position(addVectorToPoint(mk_Vector(-2,0),pos),pos.altitude),
  mk_Position(addVectorToPoint(mk_Vector(0,2),pos),pos.altitude),
  mk_Position(addVectorToPoint(mk_Vector(0,-2),pos),pos.altitude)
};

private predictAltitude : seq of nat -> nat
predictAltitude(alts) ==
  alts(1) + (alts(1) - alts(2))
pre len alts = 2;

end AirTrafficController

¤ Dauer der Verarbeitung: 0.18 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.