Checks if the input DFA is nonempty (i.e. if it recognizes a
    language except the empty one), returning True/False.

    An automaton A is nonempty if :math:`L(A) ≠ ∅`. L(A) is
    nonempty iff there are states :math:`s_0 and t ∈ F` such
    that t is connected to :math:`s_0`. Thus, automata
    nonemptiness is equivalent to graph reachability, where a
    breadth-first-search algorithm can construct in linear time
    the set of all states connected to initial state
    :math:`s_0`.
    A is nonempty iff this set intersects F nontrivially.

    :param dict dfa: input DFA.
    :return: *(bool)*, True if the DFA is nonempty, False otherwise

def dfa_nonemptiness_check(dfa: dict) -> bool:
    """ Checks if the input DFA is nonempty (i.e. if it recognizes a
    language except the empty one), returning True/False.

    An automaton A is nonempty if :math:`L(A) ≠ ∅`. L(A) is
    nonempty iff there are states :math:`s_0 and t ∈ F` such
    that t is connected to :math:`s_0`. Thus, automata
    nonemptiness is equivalent to graph reachability, where a
    breadth-first-search algorithm can construct in linear time
    the set of all states connected to initial state
    :math:`s_0`.
    A is nonempty iff this set intersects F nontrivially.

    :param dict dfa: input DFA.
    :return: *(bool)*, True if the DFA is nonempty, False otherwise
    """
    # BFS
    queue = [dfa['initial_state']]
    visited = set()
    visited.add(dfa['initial_state'])
    while queue:
        state = queue.pop(0)  # TODO note that this pop is applied to a list
        # not like in sets
        visited.add(state)
        for a in dfa['alphabet']:
            if (state, a) in dfa['transitions']:
                if dfa['transitions'][state, a] in dfa['accepting_states']:
                    return True
                if dfa['transitions'][state, a] not in visited:
                    queue.append(dfa['transitions'][state, a])
    return False