| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/VDM/VDMPP/CMConcPP/ (Wiener Entwicklungsmethode ©) Datei vom 13.4.2020 mit Größe 998 B |
|
Quelle sensor.vdmpp Sprache: VDM |
|||||||||
|
\begin{vdm_al}
class Sensor is subclass of GLOBAL instance variables -- the missile detector this sensor is connected to private detector : MissileDetector; -- the left hand-side of the viewing angle of the sensor private aperture : Angle; operations public Sensor: MissileDetector * Angle ==> Sensor Sensor (pmd, psa) == ( detector := pmd; aperture := psa); -- get the left hand-side start point and opening angle pure public getAperture: () ==> GLOBAL`Angle * GLOBAL`Angle getAperture () == return mk_ (aperture, SENSOR_APERTURE); -- trip is called asynchronously from the environment to -- signal an event. the sensor triggers if the event is -- in the field of view. the event is stored in the -- missile detector for further processing public trip: EventId * MissileType * Angle ==> () trip (evid, pmt, pa) == -- log and time stamp the observed threat detector.addThreat(evid, pmt,pa,World`timerRef.GetTime()) pre canObserve(pa, aperture, SENSOR_APERTURE) end Sensor \end{vdm_al} ¤ Dauer der Verarbeitung: 0.11 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28