|
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)
¤
|
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.
|
