|
class Radar is subclass of GLOBAL, BaseThread
types
instance variables
busy : bool := true;
location : Coordinates;
range : nat1;
detected : map FOId to FO;
priority : seq of FO := [];
inv forall foid in set dom detected & detected(foid).getId() = foid
operations
public Radar : int * int * nat1 * nat1 * bool ==> Radar
Radar(x,y,r, p, isP) ==
(location := mk_Coordinates(x,y);
range := r;
detected := {|->};
period := p;
isPeriodic := isP;
);
public Scan : AirSpace ==> ()
Scan(as) ==
(detected := { x.getId() |-> x | x in set as.getAirspace() & InRange(x) };
UpdatePriorityList()
);
pure private InRange : FO ==> bool
InRange(fo) ==
let foLocation = fo.getCoordinates()
in
return isPointInRange(location,range,foLocation);
pure public getDetected : () ==> set of FO
getDetected() ==
return rng detected;
pure public getDetectedMap : () ==> map FOId to FO
getDetectedMap() ==
return detected;
pure public saturatedRadar : () ==> bool
saturatedRadar() ==
return card dom detected > range / 4;
pure public getSaturatingFOs : () ==> set of FOId
getSaturatingFOs() ==
return {priority(i).getId() | i in set inds priority & i > floor(range/4)};
pure public getLocation : () ==> Coordinates
getLocation() ==
return location;
pure public getRange : () ==> nat1
getRange() ==
return range;
private UpdatePriorityList : () ==> ()
UpdatePriorityList() ==
let notDetect = elems priority \ rng detected,
newlyDet = detected :-> elems priority
in
( removeNotDetected(notDetect);
addNewlyDetected(newlyDet);
busy := false
);
private removeNotDetected : set of FO ==> ()
removeNotDetected(fos) ==
priority := [p | p in seq priority & p in set fos];
private addNewlyDetected : map FOId to FO ==> ()
addNewlyDetected(newlyDetect) ==
priority := priority ^ set2seqFO(rng newlyDetect);
public isFinished: () ==> ()
isFinished() == skip;
public Step: () ==> ()
Step() ==
let as = MSAW`airspace
in
(detected := { x.getId() |-> x | x in set as.getAirspace() & InRange(x) };
UpdatePriorityList();
--World`timerRef.WaitRelative(TimeStamp`stepLength);
)
functions
set2seqFO : set of FO -> seq of FO
set2seqFO(fos) ==
if fos = {}
then []
else
let fo in set fos
in
[fo] ^ set2seqFO(fos\{fo})
measure set2seqFOm;
set2seqFOm : set of FO -> nat
set2seqFOm(fos) == card fos;
--thread
--while true do
-- (
-- let as = MSAW`airspace
-- in
-- (detected := { x.getId() |-> x | x in set as.getAirspace() & InRange(x) };
-- UpdatePriorityList();
-- World`timerRef.WaitRelative(TimeStamp`stepLength);
-- )
-- )
sync
mutex(Step);
--mutex(InRange);
mutex(UpdatePriorityList);
per isFinished => not busy;
mutex(removeNotDetected);
mutex (addNewlyDetected);
mutex(UpdatePriorityList)
end Radar
¤ Dauer der Verarbeitung: 0.13 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.
|
