SPECIFICATION Spec
CHECK_DEADLOCK FALSE
CONSTANTS
  Envs = {"web", "host", "orphan"}
  MaxCalls = 2
  Hold = TRUE
INVARIANTS
  TypeOK
  NoWebCallInFrame
  CallsUseFinalTransport
  ReadyTransportIsFinal
  ReadyMeansSettled
  SessionOnFinalTransport
  UserReadIsSettled