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