Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Passenger.vdmpp Sprache: VDM

Original von: VDM^©

class Passenger

instance variables
  static nextPassengerId : nat := 1;

  passengerId : nat;
  goal :  Waypoint;
  inv goal.IsStop() = true;

  annoyanceLimit : nat;
  pickedUp : bool;
  alreadyAnnoyed : bool;

operations
  public Passenger : Busstop==> Passenger
  Passenger(destination) ==
  (
   passengerId := GetNextId();
   goal := destination;
   annoyanceLimit := World`timerRef.GetTime() + Config`PassengerAnnoyanceLimit;
   pickedUp := false;
   alreadyAnnoyed := false;

   World`env.PassengerCount();
  )
  pre destination.IsStop() = true;

  pure public GetDestination : () ==>  Waypoint
  GetDestination()==
   return goal;

  public GotOnBus : () ==> ()
  GotOnBus()==
  (
   World`graphics.passengerGotOnBus(passengerId);
   pickedUp := true;
  );

  public IsAnnoyedOfWaiting : () ==> bool
  IsAnnoyedOfWaiting() == return annoyanceLimit < World`timerRef.GetTime()
         and not pickedUp;

  -- report to environment when  passenger becomes annoyed.
  public AnnoyedOfWaiting : () ==> ()
  AnnoyedOfWaiting() ==
  (
   if(IsAnnoyedOfWaiting() and not alreadyAnnoyed) then
   (
    alreadyAnnoyed := true;
    World`env.handleEvent("Passenger " ^ Printer`natToString(passengerId) ^ " heading for " ^
     VDMUtil`val2seq_of_char[Waypoint`WaypointsEnum](goal.GetId()) ^ " is annoyed of waiting.");
    World`env.AnnoyedPassenger(1, goal.GetId());
    World`graphics.passengerAnnoyed(passengerId);
   )
  );

  pure public Id : () ==> nat
  Id()==
   return passengerId;

  private GetNextId : () ==> nat
  GetNextId() ==
  (
   let pid = nextPassengerId
   in
   (
    nextPassengerId := nextPassengerId +1;
    return pid;
   )

  );

sync
  mutex(GotOnBus, AnnoyedOfWaiting);

end Passenger

¤ Dauer der Verarbeitung: 0.20 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

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.