RULE = always (EVENT_A imply eventually EVENT_B)