Checks if the input NFA reads any language other than the
    empty one, returning True/False.

    The language L(A) recognized by the automaton A is nonempty iff
    there are states :math:`s ∈ S_0` and :math:`t ∈ F` such that
    t is connected to s.
    Thus, automata nonemptiness is equivalent to graph reachability.

    A breadth-first-search algorithm can construct in linear time
    the set of all states connected to a state in :math:`S_0`. A
    is nonempty iff this set intersects F nontrivially.

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

def nfa_nonemptiness_check(nfa: dict) -> bool:
    """ Checks if the input NFA reads any language other than the
    empty one, returning True/False.

    The language L(A) recognized by the automaton A is nonempty iff
    there are states :math:`s ∈ S_0` and :math:`t ∈ F` such that
    t is connected to s.
    Thus, automata nonemptiness is equivalent to graph reachability.

    A breadth-first-search algorithm can construct in linear time
    the set of all states connected to a state in :math:`S_0`. A
    is nonempty iff this set intersects F nontrivially.

    :param dict nfa: input NFA.
    :return: *(bool)*, True if the input nfa is nonempty, False
             otherwise.
    """
    # BFS
    queue = list()
    visited = set()
    for state in nfa['initial_states']:
        visited.add(state)
        queue.append(state)
    while queue:
        state = queue.pop(0)
        visited.add(state)
        for a in nfa['alphabet']:
            if (state, a) in nfa['transitions']:
                for next_state in nfa['transitions'][state, a]:
                    if next_state in nfa['accepting_states']:
                        return True
                    if next_state not in visited:
                        queue.append(next_state)
    return False