The NoBeaconMetEvent class implements the event that an announced
TIV\_E was not met in the distance it was supposed tobe located. It
provides an execute operation that returns the status of the Cab
Display andof the Emergency Break.
\begin{vdm_al} class NoBeaconMetEvent issubclassof Event
operations
public
execute : KLV ==> Test`TestResult
execute (klv) ==
( klv.noBeaconMet(); let mk_(a,e,g) = klv.getCabDisplay().getDisplay(),
e' = klv.getEmergencyBreak().getEmergencyBreak() in return mk_Test`KLVstate(mk_Test`CabDisp(a,e,g),
mk_Test`EmerBreak(e')) );
end NoBeaconMetEvent
\end{vdm_al}
¤ Dauer der Verarbeitung: 0.24 Sekunden
(vorverarbeitet)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
