def explain_ex(fsm, state, p):
    """
    Return a path explaining why state of fsm satisfies EX phi.
    
    fsm -- a MAS
    state -- a State of fsm satisfying EX phi
    p -- a BDD representing the set of states of fsm satisfying the property phi
    
    Return a triple (s, i, s') where
        s is state,
        s' is a state of p that is a successor of s,
        i is one possible input between s and s' in fsm
    The returned value represents a two-states path in fsm starting at state
    and ending with a successor of state from p.
    """
    nexts = fsm.post(state)
    sp = fsm.pick_one_state(nexts & p)
    return state, fsm.pick_one_inputs(fsm.get_inputs_between_states(state, sp)
        ), sp
