--      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 VERSION4:
--      Constraints are added to the architecture to check that customers
--      access the pump in the order intended by the operator.




--------      types of objects in the problem  ----------------

  type Dollars is integer;
  type Gallons is integer;
  type Operator_Stack is array[integer] of ref(integer);-- should be
                                                        -- hidden in Operator.
  type Customer_Pump(type T) is interface
  action out Turn_On(Id : T);
         in  On(Id : T);
  end;


  type Customer is interface
  action out Pre_Pay(Id : Customer; Cost : Dollars),
             Get_Refund(Id : Customer),
             Walk(), Turn_Off(Id : Customer);
         in  Okay(), Stop(Id : Customer), Change(Cost : Dollars);
  service  To_Pump : Customer_Pump(Customer);
  behavior
     Id : Customer is self;
     D : Dollars is 10;
     action Trying();
  begin                           
     start => Pre_Pay(Id, D);;    
     Okay  => Walk;;
     Walk  => To_Pump.Turn_On(Id);;
     (?C : Customer) To_Pump.Turn_On(?C) ~ To_Pump.On(?C) => Trying;;
     (?C : Customer) (Stop(?C) where ?C == Id) ~ Trying => 
                                                        Get_Refund(Id);;
--  constraint

  end Customer;

  type Pump is interface
  action in  Off(Id : Customer), Activate(Cost : Dollars);
         out     Report(Id : Customer;
                        Amount : Gallons;
                        Cost : Dollars);
  service  From_Pump : dual Customer_Pump(Customer);
  behavior
      Reading, Limit : var Dollars := 0;
      action Ready(), In_Use(Id : Customer), Done(Id : Customer);
  begin 
     Start => Ready;;
     (?X : Dollars; ?C : Customer) Ready ~ From_Pump.Turn_On(?C) ~
                                   Activate(?X) => 
                      Limit := ?X; From_Pump.On(?C); In_Use(?C);;
     (?C : Customer) In_Use(?C) => Reading := $Limit; Done(?C);;
     (?C : Customer) Off(?C) or Done(?C) =>
                        Ready || Report(?C, $Reading, $Reading);;
--  constraint
-- foo
  end Pump;

  type Operator is interface
  action in  Request(Id : Customer; Cost : Dollars),
             Result(Cost : Dollars),
             Cash_Back(Id : Customer);
         out Schedule(Id : Customer; Cost : Dollars),
             Remit(C : Customer; Change : Dollars);
  behavior
     In_Pointer, Out_Pointer : var integer := 0;
     Stack : Operator_Stack is (1..2, default is ref_to(integer,0));
  begin
    (?X : Dollars; ?I : Customer)Request(?I,?X) => 
                                  Stack[$In_Pointer+1] := ?X; 
                                  In_Pointer := ($In_Pointer+1) mod 2;
                                  Schedule(?I,?X);;
     (?C : Customer; ?X : Dollars)Result(?X) ~ Cash_Back(?C) => 
                                  Remit(?C, $(Stack[$Out_Pointer+1]) - ?X);
                                  Out_Pointer := ($Out_Pointer+1) mod 2;;
--  constraint

  end;

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

  architecture gas_station5() return root
  is
     O : Operator;
     P : Pump;
     C1, C2 : Customer;
  connect
    (?C : Customer; ?X : Dollars) ?C.Pre_Pay(?C,?X) ||> O.Request(?C,?X);
    (?X : Dollars; ?I : Customer) O.Schedule(?I,?X) ||> P.Activate(?X);
    (?X : Dollars; ?I : Customer)O.Schedule(?I,?X) ||> ?I.Okay;
--  (?C : Customer) ?C.To_Pump to  P.From_Pump; -- this is "fan-out" on ?C
                                                 -- and wont compile.
                   C1.To_Pump to  P.From_Pump;   -- fan-in Customers to Pump,
                   C2.To_Pump to  P.From_Pump;   -- fan-out Pump to Customers.
    (?C : Customer) ?C.Get_Refund(?C) ||> O.Cash_Back(?C);
    (?C : Customer; ?X : Gallons; ?Y : Dollars)P.Report(?C, ?X, ?Y) ||> 
                                                               O.Result(?Y);
    (?C : Customer; ?X : Gallons; ?Y : Dollars)P.Report(?C, ?X, ?Y) ||> 
                                                               C1.Stop(?C);
    (?C : Customer; ?X : Gallons; ?Y : Dollars)P.Report(?C, ?X, ?Y) ||> 
                                                               C2.Stop(?C);
    (?C : Customer; ?X : Dollars)O.Remit(?C,?X) ||> ?C.Change(?X);

  constraint
     never (?C1 : Customer; ?C2 : Customer) 
           (?C1.To_Pump.Turn_On ||  ?C2.To_Pump.Turn_On) where ?C1 /== ?C2;

--  never (?C1 : Customer; ?C2 : Customer) 
--        ( O.Schedule(?C1) -> O.Schedule(?C2)) where ?C1 /== ?C2  ~
--        ( O.Schedule(?C1) -> ?C1.To_Pump.Turn_On) and
--        ( O.Schedule(?C2) -> ?C2.To_Pump.Turn_On) and
--        ((?C2.To_Pump.Turn_On -> ?C1.To_Pump.Turn_On) );

  end gas_station5;