CONSTANTS Fixed = FALSE PublishUnready = FALSE Scenario = "health"
SPECIFICATION Spec
INVARIANTS TypeOK HealthyObservation