--      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 VERSION2:Interface types and connections are refined.


--------      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 Pump is interface
  action in  On(), Off(), Activate(Cost : Dollars);
         out     Report(Amount : Gallons;
                          Cost : Dollars);
  behavior
      Reading, Limit : var Dollars := 0;
      action Ready(), In_Use(), Done();
  begin 
     Start => Ready;;
     (?X : Dollars)  Ready ~ On ~ Activate(?X) => Limit := ?X;
                                                       In_Use;;
     In_Use => Reading := $Limit; Done;;
     Off or Done  => Ready || Report($Reading);;
--  constraint
-- foo
  end Pump;

  type Customer is interface
  action out Pre_Pay(Id : Customer; Cost : Dollars),
             Get_Refund(Id : Customer),
             Turn_On(), Walk(), Turn_Off();
         in  Okay(), Stop(), Change(Cost : Dollars);
  behavior
     Id : Customer is self;     -- notice this!
     D : Dollars is 10;
--   Trying : var Boolean := false; -- this doesn't protect.
     action Trying();               -- this does protect, change the
  begin                             -- action back to the var,
     start => Pre_Pay(Id, D);;      -- and see what happens.
     Okay  => Walk;;
     Walk  => Turn_On;;
     Turn_On => Trying;;            -- Trying := True;;
     Stop ~ Trying => Get_Refund(Id);;
--   Stop where $Trying => Trying := False; Get_Refund(Id);;
--  constraint

  end Customer;

  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_station3() 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.Turn_On ||> P.On;
    (?C : Customer) ?C.Turn_Off ||> P.Off;
    (?C : Customer) ?C.Get_Refund(?C) ||> O.Cash_Back(?C);
    (?X : Gallons; ?Y : Dollars)P.Report(?X, ?Y) ||> O.Result(?Y);
    (?X : Gallons; ?Y : Dollars)P.Report(?X, ?Y) ||> C1.Stop;
    (?X : Gallons; ?Y : Dollars)P.Report(?X, ?Y) ||> C2.Stop;
    (?C : Customer; ?X : Dollars)O.Remit(?C,?X) ||> ?C.Change(?X);
  end gas_station3;