| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/VDM/VDMPP/KLVPP/ (Wiener Entwicklungsmethode ©) Datei vom 13.4.2020 mit Größe 1 kB |
|
Quelle TailMeetBeaconEvent.vdmpp Sprache: VDM |
|||||||||
|
\section{The TailMeetBeaconEvent Test Class}
The TailMeetBeaconEvent class implements a test event where the tail of a train meets a beacon. It provides a setBeacon and an execute operation. The execute operation returns the current announcements and speed restrictions. \begin{vdm_al} class TailMeetBeaconEvent is subclass of Event instance variables beacon : Beacon; operations public TailMeetBeaconEvent: Beacon ==> TailMeetBeaconEvent TailMeetBeaconEvent (b) == beacon := b; public execute : KLV ==> Test`TestResult execute (klv) == ( klv.tailMeetsBeacon(beacon); let anns = klv.getAnnouncements(), restr = klv.getSpeedRestrictions() in return mk_Test`BeaconsMet( [ mk_Test`TIVD(anns(i).getTargetSpeed()) | i in set inds anns ], [ mk_Test`TIVE(restr(i).getSpeedRestriction()) | i in set inds restr ]) ) pre isofclass(TIV_E, beacon) => (klv.getFirstSpeedRestriction() or klv.getSpeedRestrictions() <> []); pure public getBeacon: () ==> Beacon getBeacon() == return beacon; end TailMeetBeaconEvent \end{vdm_al} ¤ Dauer der Verarbeitung: 0.23 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28