def explain_all_succ(fsm, state, sat):
    """
    Give all the successors of state belonging to sat.
    The returned value is a set of tuples (action, successor)
    where successor is a successor of state through action belonging to sat.
    
    fsm -- the fsm;
    state -- a state of fsm able to reach sat in one step;
    sat -- a BDD representing a set of states of fsm.    
    """
    successors = set()
    for next in fsm.pick_all_states(fsm.post(state) & sat):
        inputs = fsm.pick_one_inputs(fsm.get_inputs_between_states(state, next)
            )
        successors.add((inputs, next))
    return successors
