\* Legacy shape, kept as the regression witness: full-stack dependency
\* recording (#4606), staleness scan based at the highest dependency's
\* resolution seq. This is the path servers still serve to pending reads
\* that carry no basisSeq.
\* EXPECTED: ReadCoherence VIOLATED (CT-1910 pending-read basis over-advance).
SPECIFICATION Spec
CHECK_DEADLOCK FALSE
CONSTANTS
  Sessions = {"s1", "s2"}
  Paths = {"p1", "p2"}
  MaxTotal = 4
  DepMode = "fullstack"
  BasisMode = "maxdep"
  Values = {"v"}
  DeliveryMode = "atomic"
  IdentityMode = "none"
  ViewMode = "replay"
INVARIANT TypeOK
INVARIANT ReadCoherence
INVARIANT CascadeTotality
INVARIANT MonotonicResolution