SPECIFICATION Spec
CONSTANT MaxTid = 6
INVARIANTS
  TypeOK
  NoTransportFailure
  RespTidMatchesOutstanding
  AtMostOneOutstanding
  SessionOpsOnlyWhenOpen
  TidMonotonic
  SingleDataPhase
  DataDirectionOK
  SendObjectPaired
CHECK_DEADLOCK FALSE