| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/VDM/VDMRT/MSAWRT/ (Wiener Entwicklungsmethode ©) Datei vom 13.4.2020 mit Größe 6 kB |
|
Quelle 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 ¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28