Impressum Radar.vdmpp

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