Quelle  HeadMeetBeaconEvent.vdmpp

\section{The HeadMeetBeaconEvent Test Class}

The HeadMeetBeaconEvent class implements a test event where the head
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 HeadMeetBeaconEvent is subclass of Event

instance variables

  beacon : Beacon;

operations

  public
  HeadMeetBeaconEvent: Beacon ==> HeadMeetBeaconEvent 
  HeadMeetBeaconEvent(b) ==
    beacon := b;

  public
  execute : KLV ==> Test`TestResult
  execute (klv) ==
    ( klv.headMeetsBeacon(beacon); 
      let anns = klv.getAnnouncements(),
          restr = klv.getSpeedRestrictions() in
      return mk_Test`BeaconsMet(
            [ mk_Test`TIVD(a.getTargetSpeed()) | a in seq anns ],
            [ mk_Test`TIVE(r.getSpeedRestriction()) | r in seq restr ]) );

pure public getBeacon: () ==> Beacon
getBeacon() ==
  return beacon;
  
end HeadMeetBeaconEvent
\end{vdm_al}