Concurrent Elevator (1)

package Elevator is

   -- the range of the floors in the building
   NumberFloors : constant Integer := 5;
   type FloorNumber is new Integer range 1..NumberFloors;
   type FloorList is array (FloorNumber) of Boolean;

   -- the direction of moving
   type DirectionType is (Up, Down);

   function GetActionId return Integer;

   task Controller is
      entry Approaching (F : in FloorNumber);
      entry StoppedAt (F : in FloorNumber);
      entry CarReady (F : in FloorNumber);
      entry CarReadyEmpty (F : in FloorNumber);
      entry NewDestination (F : in FloorNumber);
   end Controller;

   task Car is
      entry Stop;
      entry Continue;
      entry DoorsOpen;
      entry DoorsClose;
      entry MoveUp;
      entry MoveDown;
   end Car;

end Elevator;



package body Elevator is

task body Controller is

   CallsUp, CallsDown, Stops : FloorList;

   PeoplePresent : Boolean := False;
   DirectionUP : boolean;
   Random : Integer;
   Floor : FloorNumber;
   Dummy : Boolean := False;

   function GetCallFloor return FloorNumber;
   function IsDestination (Floor : in FloorNumber) return Boolean;
   function isInCallsUp (Floor : in FloorNumber) return Boolean;
   function isInCallsDown (Floor : in FloorNumber) return Boolean;
   function ThereAreRequestsAbove (Floor : in FloorNumber) return Boolean;

begin
   DirectionUP := true; --event[{directionup=t}]
   loop
      -- obtain a random number that is supposed to model obtaining the
      -- code for a particular real-time event
      Random := GetActionId;
      case Random is
	 when 1 => 
	    -- someone pushed the call Up button on one of the floors
	    Floor := GetCallFloor;

	    -- enter the floor in the list of calls Up
	    CallsUp(Floor) := True;
	 when 2 => 
	    -- someone pushed the call Up button on one of the floors
	    Floor := GetCallFloor;

	    -- enter the floor in the list of calls Up
	    CallsDown(Floor) := True;
	 when 3 => 
	    -- the car is approaching a certain floor
	    accept Approaching(F : in FloorNumber) do
	       Floor := F; --event[{reporting_approach}]
	       null;
	    end Approaching;

	    -- stop there only if this floor was requested as a destination
	    -- by one of the people in the car or has a person waiting who
	    -- is going in the direction the car is currently going
	    if IsDestination(Floor) or 
	       ((DirectionUp) and then IsInCallsUp(Floor)) or
	       ((not DirectionUp) and then IsInCallsDown(Floor)) then
	       Car.Stop; --event[{ordered_to_stop}]
	       null;
	    -- also stop if the floor is the top or first floor
	    elsif ((DirectionUp) and then (Floor = FloorNumber'last)) or
		  ((not DirectionUp) and then (Floor = FloorNumber'first)) then
	       Car.Stop; --event[{ordered_to_stop}]
	       null;
	    else
	       Car.Continue;
	    end if;
	 when 4 => 
	    -- the car has stopped at a certain floor
	    accept StoppedAt(F : in FloorNumber) do
	       Floor := F; --event[{not_moving}]
	       null;
	    end StoppedAt;

	    -- open the doors
	    Car.DoorsOpen; -- event[{open_doors}]

	    -- no more people should be waiting for this car on this floor
	    if DirectionUp then
	       CallsUp(Floor) := False;
	    else
	       CallsDown(Floor) := False;
	    end if;

	    -- set the direction to Up if the car is on the first floor and
	    -- to Down if it is on the top floor
	    if Floor = FloorNumber'First then
	       DirectionUp := true; --event[{directionup=t}]
	       null;
	    end if;

	    if Floor = FloorNumber'Last then
	       DirectionUp := false; --event[{directionup=f}]
	       null;
	    end if;
	 when 5 =>
	    -- the car is ready to move (people are not standing in the
	    -- doors)
	    accept CarReady(F : in FloorNumber) do
	       Floor := F;
	    end CarReady;

	    -- all people who wanted should have exited by now
	    Stops(Floor) := False;
	    -- close the doors
	    Car.DoorsClose; -- event[{close_doors}]

	    -- move the car in the same direction unless there are no 
	    -- desired destinations in that direction
	    if (DirectionUp) then
	       null; --event[{directionupis=t}]
	       if ThereAreRequestsAbove(Floor) then
		  Car.MoveUp; --event[{ordered_to_move}]
		  null; --event[{ordered_to_move_up}]
		  null;
	       else
		  DirectionUp := false; --event[{directionup=f}]
		  Car.MoveDown; --event[{ordered_to_move}]
		  null; --event[{ordered_to_move_down}]
		  null;
	       end if;
	    else
	       null; --event[{directionupis=f}]
	       Car.MoveDown; --event[{ordered_to_move}]
	       null; --event[{ordered_to_move_down}]
	       null;
	    end if;
	 when 6 => 
	    -- someone pushed a button while in the car
	    accept NewDestination(F : in FloorNumber) do
	       Floor := F;
	    end NewDestination;

	    Stops(Floor) := True;
	 when 7 => 
	    -- the car is open and empty
	    accept CarReadyEmpty(F : in FloorNumber) do
	       Floor := F;
	    end CarReadyEmpty;

	    -- clear all the stops now because there's nobody in the car
	    for I in FloorNumber loop
	       Stops(I) := False;
	    end loop;

	    -- this line is added only for the benefit of FLAVERS, in
	    -- general the controller does not have to be terminating
	    -- the exit from the loop may only occur here, when there are
	    -- no people in the car and the doors are open
	    exit when Dummy;

	    -- close the doors
	    Car.DoorsClose; --event[{close_doors}]

	    -- of course it's unfair, but start moving to the first floor
	    Car.MoveDown;  --event[{ordered_to_move}]
	    null; --event[{ordered_to_move_down}]
	    null;
	 when others =>
	    null;
      end case;
      null;
   end loop;
end Controller;

task body Car is

   CurrentFloor : FloorNumber := FloorNumber'First;
   Random : Integer;
   Dummy : Boolean := False;
   WaitForResponse : Duration := 10.0;
   WaitWithDoorsOpen : Duration := 100.0;

begin
   loop
      Random := GetActionId;
      case Random is
	 when 1 => 
	    -- the car is approaching the CurrentFloor
	    Controller.Approaching(CurrentFloor);

	    -- wait for the response from the controller, if none then stop
	    -- to be on the safe side
	    select
	       accept Stop;
	       Controller.StoppedAt(CurrentFloor);
	    or
	       accept Continue;
	    or
	       delay WaitForResponse;
	       Controller.StoppedAt(CurrentFloor);
	    end select;
	 when 2 => 
	    -- receive the order to open the doors
	    accept DoorsOpen;

	    -- wait for a predefined amount of time and then either report
	    -- that the car is ready or that it is empty and ready
	    -- (make a non-deterministic choice)
	    delay WaitWithDoorsOpen;
	    if Dummy then
	       Controller.CarReady(CurrentFloor);
	    else
	       Controller.CarReadyEmpty(CurrentFloor);
	       exit when Dummy;
	    end if;
	 when 3 => 
	    accept DoorsClose;
	 when 4 => 
	    accept MoveUp;
	 when 5 => 
	    accept MoveDown;
	 when others => 
	    -- report to the controller that a new destination button was
	    -- pushed from inside the car
	    Controller.NewDestination(CurrentFloor);
      end case;
      null;
   end loop;
end Car;

end Elevator;