Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: ADTSL.launch Sprache: VDM

Original von: VDM^©

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.16 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.