\* The identity-commit acceptance composed with delayed verdict delivery:
\* an elided commit's verdict is processed by Deliver like any accept, its
\* layer stands in the stack until Integrate, and builds in that window
\* name it as a dependency. Brings INV-6 (AcceptedVersusDropped) into scope
\* for elided acceptances. Writes are restricted to single paths, as in
\* PendingStacks_Filtered5.cfg: two values under channel delivery at
\* MaxTotal = 4 with multi-path writes runs past 680M distinct states
\* without finishing in half an hour, and a single-path write is all an
\* identity needs. EXPECTED: all invariants HOLD.
SPECIFICATION Spec
CHECK_DEADLOCK FALSE
CONSTANTS
  Sessions = {"s1", "s2"}
  Paths = {"p1", "p2"}
  Values = {"a", "b"}
  MaxTotal = 4
  DepMode = "fullstack"
  BasisMode = "confirmed"
  DeliveryMode = "channel"
  IdentityMode = "elide"
  ViewMode = "replay"
WriteChoices <- SingletonWrites
INVARIANT TypeOK
INVARIANT ContentCoherence
INVARIANT ElidedUnchanged
INVARIANT CascadeTotality
INVARIANT MonotonicResolution
INVARIANT AcceptedVersusDropped