CONSTANTS
  Items = {a, b}
  Pushers = {p1, p2}
  MaxCommits = 4
  MaxChanges = 1
  NoObs = NoObs

SPECIFICATION Spec
INVARIANT TypeOK
INVARIANT AppliedMatchesMainAfterReconcile
INVARIANT CallSeesOneRelease
INVARIANT NothingDropped
INVARIANT RefNeverDangles
INVARIANT NoLostPush
CHECK_DEADLOCK FALSE