AG((starv.state = NOT_OK) -> AF (starv.state =OK));