module INVOICE (DATAD, CHANNELS) is

!update "2021-b"  -- use standard operator priority

-------------------------------------------------------------------------------

-- Invoice process parameterized by M_p, M_r, M_a

process Invoice_p_r_a [Request: RequestChan, Cancel: CancelChan, Deposit: DepositChan]
                      (M_p:Product, M_r:Reference, M_a:Amount,
                       in var ords:Orders, in var stks:Stocks) is
   var ref: Reference, prd: Product, amt: Amount, newords: Orders, newstks: Stocks in
      loop
         alt
            Request (?ref, ?prd, ?amt) where
               ref <= M_r and prd <= M_p and amt <= M_a and
     	       StatOrder (ref, ords) == None and amt > 0 of Amount;
            ords := AddOrder (MkOrder (ref, prd, amt, Pending), ords)
         []
            Cancel (?ref) where
               ref <= M_r and StatOrder (ref, ords) == Pending;
            ords := RemOrder (MkOrder (ref, 0 of Product, 0 of Amount, Pending), ords)
         []
            Deposit (?prd, ?amt) where
               prd <= M_p and amt <= M_a and amt > 0 of Amount;
            stks := AddStock (MkStock (prd, amt), stks)
         end alt;
         i; -- to mimick the ">>" operator in the original LOTOS specification
         newords := UpdateOrders (ords, stks);
         newstks := UpdateStocks (ords, stks);
         ords := newords;
         stks := newstks
      end loop
   end var
end process

-------------------------------------------------------------------------------

-- Invoice process parameterized by M_p, M_r, M_a and modfied to
-- have safety equivalence with the process-oriented description

process Invoice_safety_p_r_a [Request: RequestChan, Cancel: CancelChan, Deposit: DepositChan]
                             (M_p:Product, M_r:Reference, M_a:Amount,
                             in var ords:Orders, in var stks:Stocks) is
   var ref: Reference, prd: Product, amt: Amount, newords: Orders, newstks: Stocks in
      loop
         alt
            Request (?ref, ?prd, ?amt) where
               ref <= M_r and prd <= M_p and amt <= M_a and
     	       StatOrder (ref, ords) == None and amt > 0 of Amount;
            ords := AddOrder (MkOrder (ref, prd, amt, Pending), ords)
         []
            Cancel (?ref) where
               ref <= M_r and StatOrder (ref, ords) == Pending;
            ords := RemOrder (MkOrder (ref, 0 of Product, 0 of Amount, Pending), ords)
         []
            Deposit (?prd, ?amt) where
               prd <= M_p and amt <= M_a and amt > 0 of Amount;
            stks := AddStock (MkStock (prd, amt), stks)
         []
            newords := UpdateOrders (ords, stks);
            newstks := UpdateStocks (ords, stks);
            ords := newords;
            stks := newstks
         end alt;
         i
      end loop
   end var
end process

-------------------------------------------------------------------------------

end module