|
\begin{vdm_al}
class Environment is subclass of GLOBAL, BaseRTThread
types
public inline = EventId * MissileType * Angle * Time;
public outline = EventId * FlareType * Angle * nat * 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;
operations
public getAperture: () ==> Angle * Angle
getAperture () == is not yet specified;
public Environment: seq of char * [ThreadDef] ==> Environment
Environment (fname, tDef) ==
(def mk_ (-,input) = io.freadval[seq of inline](fname) in
inlines := input;
if tDef <> nil
then (period := tDef.p;
jitter := tDef.j;
delay := tDef.d;
offset := tDef.o;
);
BaseRTThread(self);
);
public addSensor: Sensor ==> ()
addSensor (psens) ==
duration (0)
(dcl id : nat := card dom ranges + 1;
atomic (
ranges := ranges munion {id |-> psens.getAperture()};
sensors := sensors munion {id |-> psens}
)
);
private createSignal: () ==> ()
createSignal () ==
duration (0)
(if len inlines > 0
then (dcl curtime : Time := time, 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)
else done := true)
else busy := false);
public handleEvent: EventId * FlareType * Angle * Time * Time ==> ()
handleEvent (evid,pfltp,angle,pt1,pt2) ==
duration (0)
(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 GetAndPurgeOutlines: () ==> seq of outline
GetAndPurgeOutlines() ==
let res = outlines
in
(outlines := [];
return res);
public Step : () ==> ()
Step() ==
(createSignal();
);
sync
mutex (handleEvent);
mutex (createSignal);
per isFinished => not busy;
end Environment
\end{vdm_al}
\begin{rtinfo}[Environment`GetAndPurgeOutlines]
{vdm.tc}[Environment]
\end{rtinfo}
¤ Dauer der Verarbeitung: 0.16 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.
|
