\* As ChannelIntended, but the computed result stands in only for a layer
\* whose commit read the path (ViewMode "intendedRead"). Such a layer is
\* refused once a foreign write moves the path and a build that named it is
\* refused with it, so what the substitution hides never reaches an accepted
\* observation; a layer that did not read the path replays as the server
\* applies it. 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 = "channel"
  IdentityMode = "none"
  ViewMode = "intendedRead"
INVARIANT TypeOK
INVARIANT ReadCoherence
INVARIANT CascadeTotality
INVARIANT MonotonicResolution
INVARIANT AcceptedVersusDropped