def explain_eax(fsm, state, alpha, phi):
    """
    Explain why state of fsm satisfies E<a>X p.
    
    fsm -- the BddFsm of the model;
    state -- a State of fsm satisfying E<a>X p;
    alpha -- a BDD of fsm representing the inputs satisfying a;
    phi -- a BDD of fsm representing the states satisfying p.
    
    Return a tuple (state, inputs, state') where
        inputs belongs to alpha
        state' belongs to phi
        state' is reachable from state through inputs.
    """
    nexts = fsm.post(state, alpha)
    next = fsm.pick_one_state(nexts & phi)
    inputs = fsm.get_inputs_between_states(state, next)
    inputs = fsm.pick_one_inputs(inputs & alpha)
    return state, inputs, next
