\* Full-stack dependency recording plus the CT-1910 repair (shipped): the
\* pending-read staleness scan runs from the reader's declared confirmed
\* basis. The model excludes the reader's whole session from the scan; the
\* shipped SQL exclusion is the DECLARED SET (own-session commits the read's
\* array names), and the two coincide on every reachable state of this
\* model because Build always records the full stack (see tla/README.md,
\* "Scope of the certification"). EXPECTED: all invariants HOLD.
SPECIFICATION Spec
CHECK_DEADLOCK FALSE
CONSTANTS
  Sessions = {"s1", "s2"}
  Paths = {"p1", "p2"}
  MaxTotal = 4
  DepMode = "fullstack"
  BasisMode = "confirmed"
  Values = {"v"}
  DeliveryMode = "atomic"
  IdentityMode = "none"
  ViewMode = "replay"
INVARIANT TypeOK
INVARIANT ReadCoherence
INVARIANT CascadeTotality
INVARIANT MonotonicResolution