module ORDERS (DATAP, CHANNELS, STOCKS) is
!update "2021-b" -- use standard operator priority
-------------------------------------------------------------------------------
-- Order process parameterized by M_p and M_a and the fixed reference ref
process Order_p [Request: RequestChan, Cancel: CancelChan, Withdraw: WithdrawChan]
(M_p: Product, M_a: Amount, ref: Reference, in var prd: Product,
in var amt: Amount, in var sta: Status) is
loop
if sta == None then
Request (ref, ?prd, ?amt) where
prd <= M_p and amt <= M_a and amt > 0 of Amount;
sta := Pending
elsif sta == Pending then
alt
Cancel (ref);
amt := 0 of Amount;
sta := None
[]
Withdraw (prd, amt) where amt > 0 of Amount;
sta := Invoiced
end alt
end if
end loop
end process
-------------------------------------------------------------------------------
-- Order process for ref=0, M_p=0
process Order_p0_r0 [Request: RequestChan, Cancel: CancelChan,
Withdraw: WithdrawChan] (M_a: Amount) is
Order_p [Request, Cancel, Withdraw] (0 of Product, M_a, 0 of Reference,
0 of Product, 0 of Amount, None)
end process
-------------------------------------------------------------------------------
-- Order process for ref=1, M_p=0
process Order_p0_r1 [Request: RequestChan, Cancel: CancelChan,
Withdraw: WithdrawChan] (M_a: Amount) is
Order_p [Request, Cancel, Withdraw] (0 of Product, M_a, 1 of Reference,
0 of Product, 0 of Amount, None)
end process
-------------------------------------------------------------------------------
-- Order process for ref=2, M_p=0
process Order_p0_r2 [Request: RequestChan, Cancel: CancelChan,
Withdraw: WithdrawChan] (M_a: Amount) is
Order_p [Request, Cancel, Withdraw] (0 of Product, M_a, 2 of Reference,
0 of Product, 0 of Amount, None)
end process
-------------------------------------------------------------------------------
-- Order process for ref=0, M_p=1
process Order_p1_r0 [Request: RequestChan, Cancel: CancelChan,
Withdraw: WithdrawChan] (M_a: Amount) is
Order_p [Request, Cancel, Withdraw] (1 of Product, M_a, 0 of Reference,
0 of Product, 0 of Amount, None)
end process
-------------------------------------------------------------------------------
-- Order process for ref=1, M_p=1
process Order_p1_r1 [Request: RequestChan, Cancel: CancelChan,
Withdraw: WithdrawChan] (M_a: Amount) is
Order_p [Request, Cancel, Withdraw] (1 of Product, M_a, 1 of Reference,
0 of Product, 0 of Amount, None)
end process
-------------------------------------------------------------------------------
-- Order process for ref=2, M_p=1
process Order_p1_r2 [Request: RequestChan, Cancel: CancelChan,
Withdraw: WithdrawChan] (M_a: Amount) is
Order_p [Request, Cancel, Withdraw] (1 of Product, M_a, 2 of Reference,
0 of Product, 0 of Amount, None)
end process
-------------------------------------------------------------------------------
end module