SPECIFICATION Spec
CONSTANTS
  Users = {a, b}
  Msgs = {m1, m2}
  MaxWrites = 2
INVARIANTS
  TypeOK
  NoLostNotes
  RightRecipient
  NoWriteAfterAck
CHECK_DEADLOCK FALSE