|
\begin{vdm_al}
class Environment is subclass of GLOBAL, BaseThread
types
public InputTP = (Time * seq of inline);
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;
busy : bool := true;
-- Amount of time we want to simulate
simtime : Time;
operations
public Environment: seq of char * [ThreadDef] ==> Environment
Environment (fname, tDef) ==
(def mk_ (-,mk_(timeval,input)) = io.freadval[InputTP](fname) in
(inlines := input;
simtime := timeval);
if tDef <> nil
then (period := tDef.p;
isPeriodic := tDef.isP;
);
BaseThread(self);
);
public addSensor: Sensor ==> ()
addSensor (psens) ==
(dcl id : nat := card dom ranges + 1;
atomic (
ranges := ranges munion {id |-> psens.getAperture()};
sensors := sensors munion {id |-> psens}
)
);
private createSignal: () ==> ()
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)
else (done := true;
return))
else (busy := false;
return));
public handleEvent: EventId * FlareType * Angle * Time * Time ==> ()
handleEvent (evid,pfltp,angle,pt1,pt2) ==
(outlines := outlines ^ [mk_ (evid,pfltp,angle,pt1,pt2)] );
public showResult: () ==> ()
showResult () ==
def - = io.writeval[seq of outline](outlines) in skip;
public isFinished : () ==> ()
isFinished () == skip;
public Step : () ==> ()
Step() ==
(if World`timerRef.GetTime() < simtime
then createSignal()
else busy := false;
);
sync
mutex (handleEvent);
mutex (createSignal);
per isFinished => not busy;
end Environment
\end{vdm_al}
¤ Dauer der Verarbeitung: 0.15 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.
|
