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

  "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 added).

  Case M_p=0, M_r=1, M_a=1

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

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

  library
    Boolean, NaturalNumber, DATAP
  endlib

  behaviour
    hide Withdraw in
      (Order_p0_r0 [Request, Cancel, Invoice, Withdraw] (Succ (0) of Amount)
        |||
       Order_p0_r1 [Request, Cancel, Invoice, Withdraw] (Succ (0) of Amount)
      )
    |[Withdraw]|
      Stock_p0 [Deposit, Withdraw] (Succ (0) of Amount)

  where

   library ORDERS_NEW, STOCKS endlib

endspec (* Invoicing *)