Quelle Environment.vdmpp Sprache: VDM

-----------------------------------------------
-- Class: Environment
-- Description: Environment class in the VeMo project
-----------------------------------------------

--
-- class definition
--
class Environment

instance variables

public city : City;
private io : IO := new IO();
private inlines : seq of inline := [];
private outlines : seq of char := [];
private busy : bool := true;
private simulating : bool := false;

private passengersTransported : nat := 0;
private passengersAnnoyed : nat := 0;
private passengersCount : nat :=0;
private passengersAnnoyedStops :  map Waypoint`WaypointsEnum to nat := {|->};

types
inline  = Types`Event;
InputTP   = seq of inline;

operations

public Environment: seq of char ==> Environment
Environment(filename) ==
(
  city := new City();

  def mk_(-,input) = io.freadval[InputTP](filename) in
  (
   inlines := input;
  );

  --BuildCityMap();
);

private BuildCityMap : () ==> ()
BuildCityMap() ==
(
  dcl a : Busstop, b : Busstop, c : Busstop, d : Busstop, e : Busstop, f :Busstop;
  dcl wp1 : Waypoint, wp2 : Waypoint, wp3 : Waypoint, wp4 : Waypoint;

  a := city.addBusstop(<A>);
  b := city.addBusstop(<B>);
  c := city.addBusstop(<C>);
  d := city.addBusstop(<D>);
  e := city.addBusstop(<E>);
  f := city.addBusstop(<F>);

  wp1 := city.addWaypoint(<WP1>);
  wp2 := city.addWaypoint(<WP2>);
  wp3 := city.addWaypoint(<WP3>);
  wp4 := city.addWaypoint(<WP4>);

  city.addRoad(a, b, <R1>, 40);
  city.addRoad(b, wp1, <R2>, 80);
  city.addRoad(b, wp2, <R3>, 50);
  city.addRoad(a, wp2, <R4>, 90);
  city.addRoad(wp2, c, <R5>, 60);
  city.addRoad(c, d, <R6>, 40);
  city.addRoad(c, f, <R7>, 60);
  city.addRoad(f, city.getCentralStation(), <R8>, 100);
  city.addRoad(city.getCentralStation(), wp3, <R9>, 50);
  city.addRoad(wp3, wp4, <R10>, 30);
  city.addRoad(d, wp4, <R11>, 40);
  city.addRoad(wp3, e, <R12>, 40);
  city.addRoad(e, wp1, <R13>, 40);
  city.addRoad(wp1, d, <R14>, 30);
  city.addRoad(f, wp4, <R15>, 20);
  city.addRoad(wp1, wp3, <R16>, 40);
  city.addRoad(a, city.getCentralStation(), <HW1>, 310, Config`DefaultRoadSpeedLimit + 10);
);

public Events: () ==> ()
Events() ==
(
    if inlines <> []
    then
    (
     dcl done : bool := false,
     eventOccurred : bool := false,
     curtime : Types`Time := World`timerRef.GetTime();

  while not done do
  (
      def event = hd inlines in
   cases event:
    mk_Types`BusRoute(-,-,-) ->
    (
     if event.t <= curtime
     then
     (
         Printer`OutWithTS("Environment: Bus route "
                ^ Printer`natToString(event.ID));

      let b = city.addBus(event.ID, event.route) in
      (
       Printer`Out("Waypoints:");
       let wps = b.GetWaypoints() in
        let wpsIds = [wp.GetId() | wp in seq wps] in
         IO`print(wpsIds);

       Printer`Out("\nStops:");

       let wps = b.GetStops() in
        let wpsIds = [wp.GetId() | wp in seq wps] in
         IO`print(wpsIds);
       Printer`Out("\n");

       if simulating then
       (
        start(b);
       );

      );

          eventOccurred := true;
     )
       ),
       mk_Types`Inflow(-,-) ->
       (
        if event.t <= curtime
     then
     (
      SetInflow(event.flow);

          eventOccurred := true;
         )
       ),
       mk_Types`Simulate(-) ->
       (
        if event.t <= curtime
     then
     (
      if not simulating then
      (
       Printer`OutWithTS("Environment: "
               ^ "Simulation started");
       simulating := true;
       start(city);
       city.WaitForThreadStart();
       for all bus in set city.getBuses() do
       (
        start(bus);
        bus.WaitForThreadStart();
       );

      );
      eventOccurred := true;
     )
       ),
       mk_Types`WasteTime(-) ->
       (
        if event.t <= curtime
     then
     (
      Printer`OutWithTS("Environment: Wasting time");
         eventOccurred := true;
        )
       ),
       others -> Printer`OutWithTS("Environment: No match found")
   end;

   if eventOccurred then
     (
      inlines := tl inlines;
      done := len inlines = 0;
     )
     else
    done := true;

   eventOccurred := false;
      );
    )
       else busy := false;
);

public handleEvent : seq of char ==> ()
handleEvent(s) ==
(
    Printer`OutWithTS("#Environment handled System Event: " ^ s);
    outlines := outlines ^ Printer`natToString(World`timerRef.GetTime()) ^ ": " ^ s ^ "\n";
);

private SetInflow : nat  ==> ()
SetInflow(flow)==
(
  Printer`OutWithTS("Environment: "
    ^ "Inflow changed to " ^ Printer`natToString(flow));

  city.setInflow(flow);
);

public IncreaseInflow : () ==> ()
IncreaseInflow() ==
(
  Printer`Out("Increase");
  let flow = city.getInflow() in
  (
   if(flow < Config`MaxInflow) then
    SetInflow(flow +1);
  )
);

public DecreaseInflow : () ==> ()
DecreaseInflow() ==
(
  let flow = city.getInflow() in
  (
   if(flow > 0) then
    SetInflow(flow -1);
  )
);

public TransportedPassengers : nat ==> ()
TransportedPassengers(number)==
  passengersTransported := passengersTransported + number;

public AnnoyedPassenger : nat * Waypoint`WaypointsEnum ==> ()
AnnoyedPassenger(number, goal)==
(
  passengersAnnoyed := passengersAnnoyed + number;

  if(goal not in set dom passengersAnnoyedStops) then
  (
   passengersAnnoyedStops := passengersAnnoyedStops ++ {goal |-> number};
  )
  else
   passengersAnnoyedStops := passengersAnnoyedStops ++ {goal |-> passengersAnnoyedStops(goal) + number};
);

public PassengerCount : () ==> ()
PassengerCount()==
  passengersCount := passengersCount + 1;

public report : () ==> ()
report() ==
(
  Printer`Out("\n\nHowever beautiful the strategy," ^
        " you should occasionally look at the results.");
    Printer`Out("**************RESULT**************");
    Printer`Out("**********************************");
    --Printer`Out(outlines);
    Printer`Out(" " ^ VDMUtil`val2seq_of_char[nat](passengersCount) ^ "\t passengers in total. (transported and at central)");
  Printer`Out(" " ^ VDMUtil`val2seq_of_char[nat](passengersTransported) ^ "\t passengers transported.");
  Printer`Out(" " ^ VDMUtil`val2seq_of_char[nat](passengersAnnoyed) ^ "\t passengers got annoyed.");


  for all waypoint in set dom passengersAnnoyedStops do
  (
   Printer`Out("\t" ^ VDMUtil`val2seq_of_char[Waypoint`WaypointsEnum](waypoint) ^ " : " ^ VDMUtil`val2seq_of_char[nat](passengersAnnoyedStops(waypoint)));

  );
    Printer`Out("\n**********************************");
  Printer`Out("**********************************");
);

public isFinished : () ==> ()
   isFinished() == skip;

   public goEnvironment : () ==> ()
goEnvironment() == skip;

public run : () ==> ()
run() ==
(
  start(new ClockTick());
     Events();
  World`graphics.move();
);

public step : () ==> ()
step() ==
(
     Events();
  World`timerRef.NotifyAndIncTime();
  World`timerRef.Awake();
  if(busy) then
  (
   World`graphics.move();
   World`graphics.sleep();
  )
  else
  (
   report();
  )
);

sync
per isFinished => not busy;
mutex(handleEvent)

end Environment

quality90%

¤ 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.0.17Bemerkung: (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.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.