\* Regression witness for the form of INV-1 the identity mode is held to:
\* the same run as PendingStacks_Identity.cfg checked against the writer-set
\* coherence of every commit that wrote something, instead of
\* ContentCoherence. (Unrestricted ReadCoherence fails one step sooner, on
\* the elided commit's own stale observation, which is the recorded
\* exemption rather than a finding.) EXPECTED: ReadCoherenceOfWrites
\* VIOLATED - a commit sitting on its session's elided layer observes that
\* layer as a contributor where durable history holds the foreign write
\* carrying the same value, a difference of writers and not of content. A
\* clean exit here means elision stopped being observable and the model
\* needs examining.
SPECIFICATION Spec
CHECK_DEADLOCK FALSE
CONSTANTS
  Sessions = {"s1", "s2"}
  Paths = {"p1", "p2"}
  Values = {"a", "b"}
  MaxTotal = 4
  DepMode = "fullstack"
  BasisMode = "confirmed"
  DeliveryMode = "atomic"
  IdentityMode = "elide"
  ViewMode = "replay"
INVARIANT TypeOK
INVARIANT ReadCoherenceOfWrites