module inv2p_new_p1_r2_a2 (DATAP, ORDERS_NEW, STOCKS) is !nat_bits 9 -- to allow sums that overflow 255 -- maximal number of products M_p = 1 -- maximal number of references M_r = 2 -- maximal amount M_a = 2 process MAIN [Request : RequestChan, Cancel : CancelChan, Deposit : DepositChan, Invoice : InvoiceChan] is hide Withdraw : WithdrawChan in par Withdraw in par Order_p1_r0 [Request, Cancel, Invoice, Withdraw] (2 of Amount) || Order_p1_r1 [Request, Cancel, Invoice, Withdraw] (2 of Amount) || Order_p1_r2 [Request, Cancel, Invoice, Withdraw] (2 of Amount) end par || par Stock_p0 [Deposit, Withdraw] (2 of Amount) || Stock_p1 [Deposit, Withdraw] (2 of Amount) end par end par end hide end process end module