Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/Sources/formale Sprachen/VDM/VDMPP/BuslinesPP/ (Wiener Entwicklungsmethode ^©) Datei vom 13.4.2020 mit Größe 1 kB

Quelle Passenger.vdmpp Sprache: 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

quality97%

¤ Dauer der Verarbeitung: 0.14 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.