CONSTANTS Fixed = TRUE PublishUnready = FALSE Scenario = "health"
SPECIFICATION Spec
INVARIANTS TypeOK HealthyObservation PortContinuity
PROPERTY ServingRecovery