CONSTANTS Fixed = TRUE PublishUnready = TRUE Scenario = "ports"
SPECIFICATION Spec
INVARIANTS TypeOK HealthyObservation PortContinuity
PROPERTIES TransportRecovery ServingRecovery LossReported