|
\begin{vdm_al}
class FlareDispenser is subclass of GLOBAL
values
responseDB : map MissileType to Plan =
{<MissileA> |-> [mk_(<FlareOneA>,900),
mk_(<FlareTwoA>,500),
mk_(<DoNothingA>,100),
mk_(<FlareOneA>,500)],
<MissileB> |-> [mk_(<FlareTwoB>,500),
mk_(<FlareTwoB>,700)],
<MissileC> |-> [mk_(<FlareOneC>,400),
mk_(<DoNothingC>,100),
mk_(<FlareTwoC>,400),
mk_(<FlareOneC>,500)] };
missilePriority : map MissileType to nat =
{<None> |-> 0,
<MissileA> |-> 1,
<MissileB> |-> 2,
<MissileC> |-> 3 }
types
public Plan = seq of PlanStep;
public PlanStep = FlareType * Time;
instance variables
public curplan : Plan := [];
curprio : nat := 0;
busy : bool := false;
aperture : Angle;
eventid : [EventId];
operations
public FlareDispenser: nat ==> FlareDispenser
FlareDispenser(ang) ==
aperture := ang;
public Step: () ==> ()
Step() ==
if len curplan > 0
then (dcl curtime : Time := World`timerRef.GetTime(),
first : PlanStep := hd curplan,
next : Plan := tl curplan;
let mk_(fltp, fltime) = first in
(if fltime <= curtime
then (releaseFlare(eventid,fltp,fltime,curtime);
curplan := next;
if len next = 0
then (curprio := 0;
busy := false ) )
)
);
pure public GetAngle: () ==> nat
GetAngle() ==
return aperture;
public addThreat: EventId * MissileType * Time ==> ()
addThreat (evid, pmt, ptime) ==
if missilePriority(pmt) > curprio
then (dcl newplan : Plan := [],
newtime : Time := ptime;
-- construct an absolute time plan
for mk_(fltp, fltime) in responseDB(pmt) do
(newplan := newplan ^ [mk_ (fltp, newtime)];
newtime := newtime + fltime );
-- immediately release the first action
def mk_(fltp, fltime) = hd newplan;
t = World`timerRef.GetTime() in
releaseFlare(evid,fltp,fltime,t);
-- store the rest of the plan
curplan := tl newplan;
eventid := evid;
curprio := missilePriority(pmt);
busy := true )
pre pmt in set dom missilePriority and
pmt in set dom responseDB;
private releaseFlare: EventId * FlareType * Time * Time ==> ()
releaseFlare (evid,pfltp, pt1, pt2) ==
World`env.handleEvent(evid,pfltp,aperture,pt1,pt2);
public isFinished: () ==> bool
isFinished () ==
return not busy;
pure public getAperture: () ==> Angle * Angle
getAperture () == return mk_(0,0);
end FlareDispenser
\end{vdm_al}
[ zur Elbe Produktseite wechseln0.16Quellennavigators
Analyse erneut starten
]
|
