// Unsafe because reject and ship conflict on outcome
// Nonlive because gameover cannot occur in accept occurs

Purchase Unsafe Nonlive {
  roles Buyer, Seller, Shipper
  parameters out ID key, out item, out price, out outcome, out gameover
  private address, resp, shipped

  Buyer → Seller: rfq[out ID,out item]
  Seller → Buyer: quote[in ID, in item, out price]

  Buyer → Seller: accept[in ID, in item, in price, out resp, out address]
  Buyer → Seller: reject[in ID, in item, in price, out resp, out outcome, out gameover]

  Seller → Shipper: ship[in ID, in item, out outcome, out shipped]
  Shipper → Buyer: deliver[in ID, in item, in address, out gameover]
}