--      Gas Station is a particular example of a general
--      problem of protecting resources. In this case, the
--      Pump is the resource, and the Operator is the
--      scheduler.
--      CHANGE FROM VERSION 5: One way to solve the race problem
--      is to turn the station into a Full Service Station.
--      There is an attendant that can accept customer's proxies
--      (Self) and prepayments, use the Pump on their behalf, and 
--      refund change to the correct customer.
--      If we had constructed the types in Version 5 carefully,
--      the attendant would be a subtype of Operator.
--      In this Full Service version, the interactions between the
--      components are simplified, so the number of actions and 
--      connections is reduced.

-------- types of objects and services in the model  ----------------

  type Dollars is integer;
  type Gallons is integer;


--------Customer type ----------------
  type Customer is interface
  action out Pre_Pay(Id : Root; Cost : Dollars);
         out Complain(Id : Customer);
         in  Change (Id : Root; Refund : Dollars);
  behavior
     Id : Customer is self;
     D : var Dollars := 10;
     action Leave(Id : Customer);
  begin                           
     start => Pre_Pay(Id, $D);;    
     (?C : Customer) (Change(?C) where ?C == Id) => Leave(Id);;
     (?C : Customer) (Change(?C) where ?C /== Id) =>Complain(Id);;
--  constraint

  end Customer;

-------------- Pump type ----------------

  type Attendant_to_Pump is interface
  action out Activate(Amnt : Dollars), Turn_On(), Turn_Off();
         in  Report (Quantity : Gallons;
                      Cost : Dollars), 
             On();
  end;

  type Pump is interface
  service  From_Pump : dual Attendant_to_Pump;
  behavior
      Reading, Limit : var Dollars := 0;
      Amount : var Gallons := 0;
      action Free(), In_Use(), Done();
  begin 
     Start => Free();;
     (?X : Dollars) Free ~ From_Pump.Turn_On ~ From_Pump.Activate(?X) => 
                      Limit := ?X; From_Pump.On(); In_Use;;
     In_Use => Reading := $Limit; Done;;
     From_Pump.Turn_Off ~ Done =>
                          Free() || From_Pump.Report($Reading, $Reading);;
--  constraint
  end Pump;

------- types for operators and Attendants ---------------
------- should be hidden in Operator or Attendant behavior ---

  
  type Customer_List is array[integer] of ref(Customer);
  type PrePay_List   is array[integer] of ref(Dollars);


------  Attendant, a simplified Operator---------------

  type Attendant is interface
  action  in Get_Pre_Pay(Id : Root; Cost : Dollars);
         out Remit(Id : Root; Refund : Dollars);

  service  To_Pump : Attendant_to_Pump;

  behavior
     In_Pointer, Out_Pointer : var integer := 0;
     Init_Customer : Customer;
     Cust_List: Customer_List is (1..2, default is ref_to(Customer,Init_Customer));
     Charge_List : PrePay_List is (1..2,default is ref_to(Integer,0));

     action Ready(), Serving(), Finished();
  begin
     Start => Ready;;
    (?X : Dollars; ?I : Customer) Get_Pre_Pay(?I,?X) => 
          Cust_List[$In_Pointer+1] := ?I;
          Charge_List[$In_Pointer+1] := ?X;
          In_Pointer := ($In_Pointer+1) mod 2;
          Serving;;
    Ready ~ Serving  =>
         To_Pump.Activate($(Charge_List[$Out_Pointer +1]));
         To_Pump.Turn_On(); To_Pump.Turn_Off();;
   (?Q : Gallons; ?X : Dollars; ?I : Customer)To_Pump.Report(?Q,?X) => 
          Remit($(Cust_List[$Out_Pointer+1]),
                  $(Charge_List[$Out_Pointer+1]) - ?X);
         Finished;;
   Finished => Out_Pointer := ($Out_Pointer+1) mod 2; Ready;;

--  constraint

  end;


-------------- main unit -------------------------

  architecture gas_station6() return root
  is
     O : Attendant;
     P : Pump;
     C1, C2 : Customer;
  connect
    (?C : Customer; ?X : Dollars) ?C.Pre_Pay(?C,?X) ||> O.Get_Pre_Pay(?C,?X);
    (?C : Customer; ?X : Dollars) O.Remit(?C,?X) ||> ?C.Change(?C, ?X);
     O.To_Pump to P.From_Pump;

  constraint
    never (?C : Customer) ?C.Complain;

  end gas_station6;