Returns the minimization of the DFA in input through a
    greatest fix-point method.

    Given a completed DFA :math:`A = (Σ, S, s_0 , ρ, F )` there
    exists a single minimal DFA :math:`A_m`
    which is equivalent to A, i.e. reads the same language
    :math:`L(A) = L(A_m)` and with a minimal number of states.
    To construct such a DFA we exploit bisimulation as a suitable
    equivalence relation between states.

    A bisimulation relation :math:`E ∈ S × S` is a relation
    between states that satisfies the following condition:
    if :math:`(s, t) ∈ E` then:

     • s ∈ F iff t ∈ F;
     • For all :math:`(s_X,a)` such that :math:`ρ(s, a) = s_X`,
       there exists :math:`t_X` such that :math:`ρ(t, a) = t_X`
       and :math:`(s_X , t_X ) ∈ E`;
     • For all :math:`(t_X,a)` such that :math:`ρ(t, a) = t_X` ,
       there exists :math:`s_X` such that :math:`ρ(s, a) = s_X`
       and :math:`(s_X , t_X ) ∈ E`.

    :param dict dfa: input DFA.
    :return: *(dict)* representing the minimized DFA.

def dfa_minimization(dfa: dict) -> dict:
    """ Returns the minimization of the DFA in input through a
    greatest fix-point method.

    Given a completed DFA :math:`A = (Σ, S, s_0 , ρ, F )` there
    exists a single minimal DFA :math:`A_m`
    which is equivalent to A, i.e. reads the same language
    :math:`L(A) = L(A_m)` and with a minimal number of states.
    To construct such a DFA we exploit bisimulation as a suitable
    equivalence relation between states.

    A bisimulation relation :math:`E ∈ S × S` is a relation
    between states that satisfies the following condition:
    if :math:`(s, t) ∈ E` then:

     • s ∈ F iff t ∈ F;
     • For all :math:`(s_X,a)` such that :math:`ρ(s, a) = s_X`,
       there exists :math:`t_X` such that :math:`ρ(t, a) = t_X`
       and :math:`(s_X , t_X ) ∈ E`;
     • For all :math:`(t_X,a)` such that :math:`ρ(t, a) = t_X` ,
       there exists :math:`s_X` such that :math:`ρ(s, a) = s_X`
       and :math:`(s_X , t_X ) ∈ E`.

    :param dict dfa: input DFA.
    :return: *(dict)* representing the minimized DFA.
    """
    dfa = dfa_completion(deepcopy(dfa))

    ################################################################
    ### Greatest-fixpoint

    z_current = set()
    z_next = set()

    # First bisimulation condition check (can be done just once)
    # s ∈ F iff t ∈ F
    for state_s in dfa['states']:
        for state_t in dfa['states']:
            if (
                            state_s in dfa['accepting_states']
                    and state_t in dfa['accepting_states']
            ) or (
                            state_s not in dfa['accepting_states']
                    and state_t not in dfa['accepting_states']
            ):
                z_next.add((state_s, state_t))

    # Second and third condition of bisimularity check
    while z_current != z_next:
        z_current = z_next
        z_next = z_current.copy()
        for (state_1, state_2) in z_current:
            # for all s0,a s.t. ρ(s, a) = s_0 , there exists t 0
            # s.t. ρ(t, a) = t 0 and (s_0 , t 0 ) ∈ Z i ;
            for a in dfa['alphabet']:
                if (state_1, a) in dfa['transitions'] \
                        and (state_2, a) in dfa['transitions']:
                    if (
                            dfa['transitions'][state_1, a],
                            dfa['transitions'][state_2, a]
                    ) not in z_current:
                        z_next.remove((state_1, state_2))
                        break
                else:
                    # action a not possible in state element[0]
                    # or element[1]
                    z_next.remove((state_1, state_2))
                    break

    ################################################################
    ### Equivalence Sets

    equivalence = dict()
    for (state_1, state_2) in z_current:
        equivalence.setdefault(state_1, set()).add(state_2)

    ################################################################
    ### Minimal DFA construction

    dfa_min = {
        'alphabet': dfa['alphabet'].copy(),
        'states': set(),
        'initial_state': dfa['initial_state'],
        'accepting_states': set(),
        'transitions': dfa['transitions'].copy()
    }

    # select one element for each equivalence set
    for equivalence_set in equivalence.values():
        if dfa_min['states'].isdisjoint(equivalence_set):
            e = equivalence_set.pop()
            dfa_min['states'].add(e)  # TODO highlight this instruction
            equivalence_set.add(e)

    dfa_min['accepting_states'] = \
        dfa_min['states'].intersection(dfa['accepting_states'])

    for t in dfa['transitions']:
        if t[0] not in dfa_min['states']:
            dfa_min['transitions'].pop(t)
        elif dfa['transitions'][t] not in dfa_min['states']:
            dfa_min['transitions'][t] = \
                equivalence[dfa['transitions'][t]]. \
                    intersection(dfa_min['states']).pop()

    return dfa_min