|
\begin{vdm_al}
class FlareController is subclass of GLOBAL, BaseThread
instance variables
-- the left hand-side of the working angle
private aperture : Angle;
-- maintain a link to each dispenser
ranges : map nat to (Angle * Angle) := {|->};
dispensers : map nat to FlareDispenser := {|->};
inv dom ranges = dom dispensers;
-- the relevant events to be treated by this controller
threats : seq of (EventId * MissileType * Angle * Time) := [];
-- the status of the controller
busy : bool := false
operations
public FlareController: Angle * [ThreadDef] ==> FlareController
FlareController (papp, tDef) ==
(aperture := papp;
if tDef <> nil
then (period := tDef.p;
isPeriodic := tDef.isP;
);
BaseThread(self);
);
public addDispenser: FlareDispenser ==> ()
addDispenser (pfldisp) ==
let angle = aperture + pfldisp.GetAngle() in
(dcl id : nat := card dom ranges + 1;
atomic
(ranges := ranges munion
{id |-> mk_(angle, DISPENSER_APERTURE)};
dispensers := dispensers munion {id |-> pfldisp}
);
);
-- get the left hand-side start point and opening angle
pure public getAperture: () ==> GLOBAL`Angle * GLOBAL`Angle
getAperture () == return mk_(aperture, FLARE_APERTURE);
-- addThreat is a helper operation to modify the event
-- list. currently events are stored first come first served.
-- one could imagine using a different ordering instead
public addThreat: EventId * MissileType * Angle * Time ==> ()
addThreat (evid,pmt,pa,pt) ==
(threats := threats ^ [mk_ (evid,pmt,pa,pt)];
busy := true );
-- getThreat is a local helper operation to modify the event list
private getThreat: () ==> EventId * MissileType * Angle * Time
getThreat () ==
(dcl res : EventId * MissileType * Angle * Time := hd threats;
threats := tl threats;
return res );
public isFinished: () ==> ()
isFinished () ==
for all id in set dom dispensers do
dispensers(id).isFinished();
protected Step: () ==> ()
Step() ==
(if threats <> []
then (def mk_ (evid,pmt, pa, pt) = getThreat() in
for all id in set dom ranges do
def mk_(papplhs, pappsize) = ranges(id) in
if canObserve(pa, papplhs, pappsize)
then dispensers(id).addThreat(evid,pmt,pt);
busy := len threats > 0 );
);
sync
-- addThreat and getThreat modify the same instance variables
-- therefore they need to be declared mutual exclusive
mutex (addThreat,getThreat);
mutex (Step);
-- getThreat is used as a 'blocking read' from the main
-- thread of control of the missile detector
per getThreat => len threats > 0;
per isFinished => len threats = 0 --not busy
end FlareController
\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.
|
