\begin{vdm_al}class Environment is subclass of GLOBALtypes public inline = EventId * MissileType * Angle * Time ;public outline = EventId * FlareType * Angle * Time * Time ;instance variables -- access to the VDMTools stdio new IO();-- the input file to process seq of inline := [];-- the output file to print seq of outline := [];-- maintain a link to all sensors map nat to (Angle * Angle) := {|->};map nat to Sensor := {|->};inv dom ranges = dom sensors;-- information about the latest event that has arrived nil ;bool := true ;operations public Environment: seq of char ==> Environmentdef mk_ (-,input) = io.freadval[seq of inline](fname) in public addSensor: Sensor ==> ()dcl id : nat := card dom ranges + 1;atomic (munion {id |-> psens.getAperture()};munion {id |-> psens} public Run: () ==> ()while not (isFinished() and CM`detector.isFinished()) do private createSignal: () ==> [EventId]if len inlines > 0then (dcl curtime : Time := World`timerRef.GetTime(), bool := false ;while not done do def mk_ (eventid, pmt, pa, pt) = hd inlines in if pt <= curtimethen (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);tl inlines;len inlines = 0;return eventid )else (done := true ;return nil ))else (busy := false ;return nil ));public handleEvent: EventId * FlareType * Angle * Time * Time ==> ()public showResult: () ==> ()def - = io.writeval[seq of outline](outlines) in skip ;public isFinished : () ==> bool return inlines = [] and not busy;public getAperture: () ==> Angle * Anglereturn mk_(0,0);end Environmentend {vdm_al}quality 97%
¤ Dauer der Verarbeitung: 0.12 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
