\* A positional op shown as the result its writer computed, for every own
\* layer whatever it read (ViewMode "intended"): a build over such a layer
\* observes the confirmed state at the layer's basis while declaring the
\* current one. A layer whose commit did not read the path is accepted as it
\* stands, and the build that sat on it is then accepted having missed the
\* foreign write the substitution hid. EXPECTED: ReadCoherence VIOLATED
\* (the regression witness for the review finding on #8698).
SPECIFICATION Spec
CHECK_DEADLOCK FALSE
CONSTANTS
  Sessions = {"s1", "s2"}
  Paths = {"p1", "p2"}
  MaxTotal = 4
  DepMode = "fullstack"
  BasisMode = "confirmed"
  Values = {"v"}
  DeliveryMode = "channel"
  IdentityMode = "none"
  ViewMode = "intended"
INVARIANT TypeOK
INVARIANT ReadCoherence
INVARIANT CascadeTotality
INVARIANT MonotonicResolution
INVARIANT AcceptedVersusDropped