CONSTANTS
  Items = {a, b}
  Pushers = {p1, p2}
  MaxCommits = 5
  MaxChanges = 2
  NoObs = NoObs

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