SPECIFICATION Spec
CHECK_DEADLOCK FALSE
CONSTANTS
  Invocations = {i1, i2}
  MaxVersion = 3
  ReadsPerInvocation = 2
  Snapshot = TRUE
INVARIANTS
  TypeOK
  OneVersionPerInvocation
  CurrentAtStart