Quelle  environment.vdmpp   Sprache: VDM

\begin{vdm_al}
class Environment is subclass of GLOBAL

types

public inline  = EventId * MissileType * Angle * Time;
public outline = EventId * FlareType * Angle * Time * Time;

instance variables

-- access to the VDMTools stdio
io : IO := new IO();

-- the input file to process
inlines : seq of inline := [];

-- the output file to print
outlines : seq of outline := [];

-- maintain a link to all sensors
ranges : map nat to (Angle * Angle) := {|->};
sensors : map nat to Sensor := {|->};
inv dom ranges = dom sensors;

-- information about the latest event that has arrived
evid : [EventId] := nil;

busy : bool := true;

operations

public Environment: seq of char ==> Environment
Environment (fname) ==
  def mk_ (-,input) = io.freadval[seq of inline](fname) in
    inlines := input;

public addSensor: Sensor ==> ()
addSensor (psens) ==
  (dcl id : nat := card dom ranges + 1;
   atomic (
    ranges := ranges munion {id |-> psens.getAperture()};
    sensors := sensors munion {id |-> psens} 
   )
  );

public Run: () ==> ()
Run () == 
 (while not (isFinished() and CM`detector.isFinished()) do
    (evid := createSignal();
     CM`detector.Step();
     World`timerRef.StepTime();
    );
 showResult()
 );

private createSignal: () ==> [EventId]
createSignal () ==
  (if len inlines > 0
   then (dcl curtime : Time := World`timerRef.GetTime(), 
             done : bool := false;
         while not done do
           def mk_ (eventid, pmt, pa, pt) = hd inlines in
             if pt <= curtime
             then (for all id in set dom ranges do
                     def mk_(papplhs,pappsize) = ranges(id) in
                       if canObserve(pa,papplhs,pappsize)
                       then sensors(id).trip(eventid,pmt,pa);
                   inlines := tl inlines;
                   done := len inlines = 0;
                   return eventid )
             else (done := true;
                   return nil ))
   else (busy := false;
         return nil));

public handleEvent: EventId * FlareType * Angle * Time * Time ==> ()
handleEvent (newevid,pfltp,angle,pt1,pt2) ==
  (outlines := outlines ^ [mk_ (newevid,pfltp, angle,pt1, pt2)] );

public showResult: () ==> ()
showResult () ==
  def - = io.writeval[seq of outline](outlines) in skip;

public isFinished : () ==> bool
isFinished () == 
  return inlines = [] and not busy;

pure public getAperture: () ==> Angle * Angle
getAperture () == return mk_(0,0);

end Environment
\end{vdm_al}