def ex(fsm, phi):
    """
    Return the set of states of fsm satisfying EX phi.
    
    fsm -- a MAS representing the system
    phi -- a BDD representing the set of states of fsm satisfying phi
    """
    return fsm.pre(phi)
