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 5 kB

Quelle Bus.vdmpp Sprache: VDM

class Bus

instance variables
  seats : set of Passenger;
  inv card seats <= Config`BusCapacity;

  --bus line number
  line : nat;

  -- the route of road the bus is moving along
  route : seq of Road;
  -- what roads are left in the current pass of the route
  curRoute : seq of Road;
  -- where are we heading
  nextWP : Waypoint;
  -- what road are we currently on
  currentRoad : Road;
  --waypoints passed by the bus
  wps : seq of Waypoint;

operations
  public Bus : nat * seq of Road * seq of Waypoint ==> Bus
  Bus(linenumber, busroute, waypoints)==
  (
   line := linenumber;
   route := busroute;
   curRoute := busroute;
   nextWP := hd waypoints;

   wps := waypoints;
   seats := {};
  )
  pre len waypoints > 1; --ensure bus has somewhere to go

  public GetOn : set of Passenger ==> ()
  GetOn(ps) ==
  (
   seats := seats union ps;
   World`graphics.busPassengerCountChanged(line, card seats);
  )
  pre card seats + card ps <= Config`BusCapacity;

  public GotOff : set of Passenger ==> ()
  GotOff(p) ==
  (
   seats := seats \ p;
   World`graphics.busPassengerCountChanged(line, card seats);
  )
  pre p inter seats <> {};

  pure public GetWaypoints : () ==> seq of Waypoint
  GetWaypoints()==
   return wps;

  pure public GetStops : () ==> seq of Busstop
  GetStops()==
   return [wp | wp in seq wps & wp.IsStop() ];


  private NextWaypoint : () ==> Waypoint
  NextWaypoint()==
  (
   --start route over
   if(len curRoute = 0) then
     curRoute := route;

   --next road
   let nextRoad = hd curRoute in
   (
    --move along route
    curRoute := tl curRoute;
    --what road are we on
    currentRoad := nextRoad;
    -- update waypoints
    let currentWp = nextWP  in
    (
     nextWP := currentRoad.OppositeEnd(currentWp);
     return currentWp;
    )
   );
  );

  --functionality to ensure thread start
  public WaitForThreadStart : () ==> ()
  WaitForThreadStart() == skip;

  private ThreadStarted : () ==> ()
  ThreadStarted() == skip;

sync
  per GetOn => card seats < Config`BusCapacity;
  per WaitForThreadStart => #fin(ThreadStarted) > 0

thread
(
  dcl passGettingOn : set of Passenger;
  ThreadStarted();
  let - = NextWaypoint() in skip; --prevent return

  --loop which moves bus along route, and lets passengers on and off at stops
  while true do
  (
   Printer`OutWithTS("%Bus " ^ Printer`natToString(line) ^ ": running on " ^
         VDMUtil`val2seq_of_char[Road`RoadNumber](currentRoad.GetRoadNumber()) ^
         " with length " ^ Printer`natToString(currentRoad.GetLength()) ^ " and speedlimit " ^
          Printer`natToString(currentRoad.GetSpeedLimit()) ^
          " Next: " ^ VDMUtil`val2seq_of_char[Waypoint`WaypointsEnum](nextWP.GetId()) ^
          " Time: " ^ Printer`natToString(currentRoad.GetTimePenalty())
       );

   World`graphics.busInRouteTo(line,
    VDMUtil`val2seq_of_char[Road`RoadNumber](currentRoad.GetRoadNumber()),
    VDMUtil`val2seq_of_char[Waypoint`WaypointsEnum](nextWP.GetId()),
    currentRoad.GetTimePenalty());

   --add to penalty for moving along road
   World`timerRef.WaitRelative(currentRoad.GetTimePenalty());
      World`timerRef.NotifyAll();
      World`timerRef.Awake();

   --next on bus route
   let next = NextWaypoint() in
   (
    Printer`OutWithTS("%Bus " ^ Printer`natToString(line) ^
    " arrived at " ^
    VDMUtil`val2seq_of_char[Waypoint`WaypointsEnum](next.GetId()));

    let nextId = next.GetId() in
    (
     --let passengers in at central station if
     --their destination is on the bus' route
     if nextId = <Central> then
     (
      --bus returned with passengers; in the current model this should not be possible
      --if(seats <> {}) then exit "Bus returned with passengers";

      let central : Busstop = next in
      (
       --find passengers for bus
       let potentialPassengers : set of Passenger = central.GetWaitingOn(wps) in
       (
        if(card potentialPassengers > 0) then
        (
         --count available sets in bus
         if((Config`BusCapacity - card seats) < card potentialPassengers) then
          --not room for all, select some
          passGettingOn := SelectSubset(potentialPassengers, Config`BusCapacity - card seats)
         else
          passGettingOn := potentialPassengers;

         -- leave busstop and enter bus seats
         central.PassengerLeft(passGettingOn);
         GetOn(passGettingOn);
         for all p in set passGettingOn do p.GotOnBus();

         Printer`OutWithTS("%Bus " ^ Printer`natToString(line) ^ ": " ^
          Printer`natToString(card passGettingOn) ^ " got on");

         --add to time penalty for stopping
         World`graphics.busStopping(line);
         World`timerRef.WaitRelative(3);
            World`timerRef.NotifyAll();
            World`timerRef.Awake();
        )
       );
      );
     );

     -- let passengers off at their destination
     let gettingOff = { p | p in set seats & p.GetDestination() = next} in
     (
       if(card gettingOff > 0) then
       (
        GotOff(gettingOff);
        Printer`OutWithTS("%Bus " ^ Printer`natToString(line) ^ ": " ^
         Printer`natToString(card gettingOff) ^ " got off");

        World`env.TransportedPassengers(card gettingOff);

        --add to time penalty for stopping
        World`graphics.busStopping(line);
        World`timerRef.WaitRelative(3);
           World`timerRef.NotifyAll();
           World`timerRef.Awake();
       );
     );
    );
   );

  );
);

operations
  pure private SelectSubset : set of Passenger * nat ==> set of Passenger
  SelectSubset(ps, limit)==
  (
   --base case
   if limit = 0 then
    return {};

   --smaller than limit, return
   if card ps <= limit then
    return ps;

   --recusive
   let sub in set ps in
     return {sub} union SelectSubset(ps \ {sub}, limit -1);
  )

end Bus

quality99%

¤ Dauer der Verarbeitung: 0.16 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.