(*****************************************************************************

  "inv2p.lotos"   K. J. Turner   14/12/1997

  This LOTOS specification in process-oriented style describes case 2 of the
  invoicing case study by Henri Habrias <habrias@irin.univ-nantes.fr>.

  Modified by M. Sighireanu to obtain a parameterized description on the
  maximal number of Reference (M_r), Product (M_p), Amount (M_a) and to
  test the state of an order (Invoice action).

  Case M_p=1, M_r=1, M_a=2

*****************************************************************************)

specification Invoicing [Request, Cancel, Deposit, Invoice] : noexit

  library
    Boolean, NaturalNumber, DATAP
  endlib

  behaviour
    hide Withdraw in
      (Order_p1_r0 [Request, Cancel, Invoice, Withdraw] (Succ (Succ (0)) of Amount)
        |||
       Order_p1_r1 [Request, Cancel, Invoice, Withdraw] (Succ (Succ (0)) of Amount)
      )
    |[Withdraw]|
      (Stock_p0 [Deposit, Withdraw] (Succ (Succ (0)) of Amount)
        |||
       Stock_p1 [Deposit, Withdraw] (Succ (Succ (0)) of Amount)
      )

  where

   library ORDERS_NEW, STOCKS endlib

endspec (* Invoicing *)