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