module inv2p_p1_r2_a1 (DATAP, CHANNELS, ORDERS, 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 = 1
process MAIN [Request: RequestChan, Cancel: CancelChan, Deposit: DepositChan] is
hide Withdraw: WithdrawChan in
par Withdraw in
par
Order_p1_r0 [Request, Cancel, Withdraw] (1 of Amount)
||
Order_p1_r1 [Request, Cancel, Withdraw] (1 of Amount)
||
Order_p1_r2 [Request, Cancel, Withdraw] (1 of Amount)
end par
||
par
Stock_p0 [Deposit, Withdraw] (1 of Amount)
||
Stock_p1 [Deposit, Withdraw] (1 of Amount)
end par
end par
end hide
end process
end module