| products/Sources/formale Sprachen/VDM/VDMPP/CMSeqPP/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei:
Interaktion und
|
|
||||||
|
\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} ¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.16Angebot Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können ¤ |
Lebenszyklus
Die hierunter aufgelisteten Ziele sind für diese Firma wichtig
ZieleEntwicklung einer Software für die statische QuellcodeanalyseBot Zugriff |
