\* Client-declared holdings (shipped): every reconnect — resumed or
\* re-established — is diffed against the client's own statement of its
\* replica, with lost pushes and a wiped replica both in play.
\* EXPECTED: all invariants HOLD — a reconnect converges the replica and
\* re-delivers nothing it holds.
SPECIFICATION Spec
CHECK_DEADLOCK FALSE
CONSTANTS
  Docs = {"d1", "d2"}
  MaxWrites = 3
  MaxLoss = 1
  AllowReset = TRUE
  Mode = "holdings"
INVARIANT TypeOK
INVARIANT ReconnectConverges
INVARIANT NoRedundantDelivery