Gas Station with No Queueing (1)

procedure gas;


procedure gas is

  N : constant natural := 1;         -- number of customers
  type cust_range is range 0 .. N;
  type pump_range is range 1 .. 2;   -- two pumps

  task operator is
    entry prepay_1_pump_1;
    entry prepay_1_pump_2;
    entry charge_1_pump_1;
    entry charge_1_pump_2;
  end operator;

  task pump_1 is
    entry activate;
    entry start_pumping;
    entry stop_pumping_1;
  end pump_1;

  task pump_2 is
    entry activate;
    entry start_pumping;
    entry stop_pumping_1;
  end pump_2;

  task customer_1 is
    entry change;
  end customer_1;


  task body operator is
    Pump_1_ActiveCustomers : cust_range;
    Pump_2_ActiveCustomers : cust_range;
    done            : boolean;

  begin		-- Operator

    Pump_1_ActiveCustomers := 0;   --event[{p1ac=0}]
    Pump_2_ActiveCustomers := 0;   --event[{p2ac=0}]
    null;

    -- infinite loop
    loop

      select

         -- can accept a prepayment from customer 1 for pump 1
         accept prepay_1_pump_1 do

            -- check for this as the first customer
            if Pump_1_ActiveCustomers = 0 then

               -- activate the pump
               gas.pump_1.activate;   --eventb[{p1acis=0}]
               null;

            end if;

            -- increment the number of active customers on pump 1
            Pump_1_ActiveCustomers := 
                   Pump_1_ActiveCustomers + 1;  --event[{p1acinc}]
            null;

         end prepay_1_pump_1;

      or

         -- can accept a prepayment from customer 1 for pump 2
         accept prepay_1_pump_2 do

            -- check for this as the first customer for pump 2
            if Pump_2_ActiveCustomers = 0 then

               -- activate the pump
               gas.pump_2.activate;   --eventb[{p2acis=0}]
               null;

            end if;

            -- increment the number of active customers on pump 2
            Pump_2_ActiveCustomers := 
                   Pump_2_ActiveCustomers + 1;  --event[{p2acinc}]
            null;

         end prepay_1_pump_2;

      or 

         -- can accept charge for customer_1 from pump 1
         accept charge_1_pump_1;

         -- decrement number of active customers on pump 1
         Pump_1_ActiveCustomers := 
                 Pump_1_ActiveCustomers - 1; --event[{p1acdec}]
         null;

         -- check for more customers
         if Pump_1_ActiveCustomers > 0 then
                                   
            -- more customers, so activate pump again
            gas.pump_1.activate;   --eventb[{p1acis>0}]
            null;

         end if;

         -- give change to customer 1
         gas.customer_1.change;    --eventb[{cust_1_pump_1_change}]
         null;

      or 

         -- can accept charge for customer_1 from the pump 2
         accept charge_1_pump_2;

         -- decrement number of active customers on pump 2
         Pump_2_ActiveCustomers := 
                 Pump_2_ActiveCustomers - 1; --event[{p2acdec}]
         null;

         -- check for more customers
         if Pump_2_ActiveCustomers > 0 then
                                   
            -- more customers, so activate pump again
            gas.pump_2.activate;   --eventb[{p2acis>0}]
            null;

         end if;

         -- give change to customer 1
         gas.customer_1.change;    --eventb[{cust_1_pump_2_change}]
         null;

      end select;

      exit when done;

    end loop;
  end operator;

  task body pump_1 is 
    done : boolean;
  begin		-- Pump

    -- infinite loop
    loop
      accept activate;
      accept start_pumping;
      accept stop_pumping_1 do
         gas.operator.charge_1_pump_1; 
      end stop_pumping_1;
      exit when done;
    end loop;
  end pump_1;

  task body pump_2 is
    done : boolean; 
  begin		-- Pump

    -- infinite loop
    loop
      accept activate;
      accept start_pumping;
      accept stop_pumping_1 do
         gas.operator.charge_1_pump_2;
      end stop_pumping_1; 
      exit when done;
    end loop;
  end pump_2;


  task body customer_1 is
    done : boolean;
  begin		-- Customer_1

    -- infinite loop
    loop

      -- either pump on pump 1 or pump 2
      select
         gas.operator.prepay_1_pump_1;
         gas.pump_1.start_pumping;     --event[{cust_1_start_pumping}]
         gas.pump_1.stop_pumping_1;    --eventb[{cust_1_stop_pumping}]
         null;
      else
         gas.operator.prepay_1_pump_2;
         gas.pump_2.start_pumping;
         gas.pump_2.stop_pumping_1;
      end select;
      accept change;
      exit when done;
    end loop;
  end customer_1;

begin
  null;
end gas;