\* Deeper bound for the filtered mode: five commits allow a foreign write to
\* reject a MIDDLE pending layer underneath a reader, which is the scenario
\* where overlap-filtering actually drops a dependency the full-stack shape
\* would have kept. Writes are restricted to single paths to keep the state
\* space tractable. EXPECTED: all invariants HOLD.
SPECIFICATION Spec
CHECK_DEADLOCK FALSE
CONSTANTS
  Sessions = {"s1", "s2"}
  Paths = {"p1", "p2"}
  MaxTotal = 5
  DepMode = "filtered"
  BasisMode = "confirmed"
  Values = {"v"}
  DeliveryMode = "atomic"
  IdentityMode = "none"
  ViewMode = "replay"
WriteChoices <- SingletonWrites
INVARIANT TypeOK
INVARIANT ReadCoherence
INVARIANT CascadeTotality
INVARIANT MonotonicResolution