SPECIFICATION Spec
CONSTANT MaxTid = 4
INVARIANTS
  TypeOK
  NoTransportFailure
  RespTidMatchesOutstanding
  AtMostOneOutstanding
  SessionOpsOnlyWhenOpen
  TidMonotonic
  SingleDataPhase
CHECK_DEADLOCK FALSE