| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/VDM/VDMRT/CMRT/ (Wiener Entwicklungsmethode ©) Datei vom 13.4.2020 mit Größe 1 kB |
|
Quelle sensor.vdmrt 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 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 async public trip: EventId * MissileType * Angle ==> () trip (evid, pmt, pa) == -- log and time stamp the observed threat detector.addThreat(evid,pmt,pa,time) pre canObserve(pa, aperture, SENSOR_APERTURE) end Sensor \end{vdm_al} \begin{rtinfo}[Sensor`Sensor] {vdm.tc}[Sensor] \end{rtinfo} ¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28