products/sources/formale Sprachen/Delphi/Bille 0.71/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: atc.vdmrt   Sprache: VDM

class AirTrafficController is subclass of GLOBAL

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

operations

 
OverviewAllRadars: () ==> map FOId to FO
OverviewAllRadars() ==
  return merge {r.getDetectedMap() | r in set radars};

private 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()
  in 
    if id in set dom history 
    then history := history ++ {id |-> addHistory(history(id),
                                                  fo.getCoordinates(),
                                                  fo.getAltitude())}
    else history := history munion {id |-> addHistory([],
                                                      fo.getCoordinates(),
                                                      fo.getAltitude())}
 );

private 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 > 0 
  then 
    let lastValue = last(hist)
    in
     if lastValue = mk_Position(coord,alt)
      then hist
      else
        if(len hist < 3)
        then hist ^ [mk_Position(coord,alt)]
        else tl hist ^ [mk_Position(coord,alt)]
  else hist ^ [mk_Position(coord,alt)];
     
private last : History -> Position
last(hist) ==
  hist(len hist)
pre len hist > 0;

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 fo.getId() in set dom history and len history(fo.getId()) = 3 
          then willFObeSafe(ob,fo);       
    for all r in set radars
    do 
      if r.saturatedRadar()
      then writeRadarWarning(r)
   );

public UpdatesPresent:() ==> ()
UpdatesPresent() ==
  busy := true;

functions

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


functions

isFOSafe : Obstacle * Position -> bool
isFOSafe(obs,pos) ==
  let obsloc      = obs.getCoordinates(),
      secureRange = obs.getSecureRange(),
      foloc       = pos.coord
  in
    isPointInRange(obsloc,secureRange,foloc) => 
    isFOatSafeAltitude(obs.getMSA(),pos);
    
       
isFOatSafeAltitude : MinimumSafetyAltitude * Position -> bool
isFOatSafeAltitude(msa,pos) == 
  msa <> <NotAllowed> and msa < pos.altitude;
  
operations
 
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    = time
        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    = time
  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       = time
  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;  
 
 
operations  
public isFinished : () ==> ()
isFinished() ==
  for all r in set radars do
    r.isFinished(); 
 
public Step : () ==> ()
Step() == 
( busy := true;
  --for all r in set radars 
  --do 
  --  r.Scan(MSAW`airspace);
  updateHistory();
  findThreats();
  busy := false
);   
 
thread

periodic (1600E6,0,0,0) (Step)

sync 
per isFinished => not busy;

 
end AirTrafficController

[ Seitenstruktur0.25Drucken  etwas mehr zur Ethik  ]