CONSTANTS
  Replicas = {r1, r2, r3}
  MaxLsn = 3
  MaxSyncCount = 2

INIT Init
NEXT Next

CHECK_DEADLOCK FALSE

INVARIANTS
  TypeOk
  AcksRemovePending
  PendingAreKnown
  AppliedLteCurrent

PROPERTIES
  MonotonicLsn
SYMMETRY Symmetry