CONSTANTS Fixed = FALSE PublishUnready = FALSE Scenario = "proxy"
SPECIFICATION Spec
INVARIANT TypeOK
PROPERTY TransportRecovery