CONSTANTS
  Users = {u1, u2, u3}
  MaxAmt = 2
  MaxExpenses = 2
  PaymentIds = {p1, p2}
  NULL = NULL

SPECIFICATION Spec
INVARIANT TypeOK
INVARIANT Conservation
INVARIANT SharesExact
INVARIANT SettlementSound
INVARIANT IdempotentPayments
PROPERTY NoOverwrite
CHECK_DEADLOCK FALSE