\* The reconnect before client-declared holdings, with a perfectly
\* absorbing client and no replica wipe: correctness holds, but a session
\* the server no longer holds is re-established with the whole union.
\* EXPECTED: ReconnectConverges HOLDS; NoRedundantDelivery VIOLATED — the
\* witness for the full re-download on a lapsed session.
SPECIFICATION Spec
CHECK_DEADLOCK FALSE
CONSTANTS
  Docs = {"d1", "d2"}
  MaxWrites = 3
  MaxLoss = 0
  AllowReset = FALSE
  Mode = "memory"
INVARIANT TypeOK
INVARIANT ReconnectConverges
INVARIANT NoRedundantDelivery