Returns a NFA reading the same language of input AFW.

    Let :math:`A = (Σ, S, s^0 , ρ, F )`  be an afw. Then we
    define the nfa :math:`A_N` such that :math:`L(A_N) = L(A)`
    as follows :math:`AN = (Σ, S_N , S^0_N , ρ_N , F_N )` where:

     • :math:`S_N = 2^S`
     • :math:`S^0_N= \{\{s^0 \}\}`
     • :math:`F_N=2^F`
     • :math:`(Q,a,Q') ∈ ρ_N` iff :math:`Q'` satisfies :math:`⋀_{
       s∈Q} ρ(s, a)`

     We take an empty conjunction in the definition of
     :math:`ρ_N` to be equivalent to true; thus, :math:`(∅, a,
     ∅) ∈ ρ_N`.

    :param dict afw: input AFW.
    :return: *(dict)* representing a NFA.

def afw_to_nfa_conversion(afw: dict) -> dict:
    """ Returns a NFA reading the same language of input AFW.

    Let :math:`A = (Σ, S, s^0 , ρ, F )`  be an afw. Then we
    define the nfa :math:`A_N` such that :math:`L(A_N) = L(A)`
    as follows :math:`AN = (Σ, S_N , S^0_N , ρ_N , F_N )` where:

     • :math:`S_N = 2^S`
     • :math:`S^0_N= \{\{s^0 \}\}`
     • :math:`F_N=2^F`
     • :math:`(Q,a,Q') ∈ ρ_N` iff :math:`Q'` satisfies :math:`⋀_{
       s∈Q} ρ(s, a)`

     We take an empty conjunction in the definition of
     :math:`ρ_N` to be equivalent to true; thus, :math:`(∅, a,
     ∅) ∈ ρ_N`.

    :param dict afw: input AFW.
    :return: *(dict)* representing a NFA.
    """

    nfa = {
        'alphabet': afw['alphabet'].copy(),
        'initial_states': {(afw['initial_state'],)},
        'states': {(afw['initial_state'],)},
        'accepting_states': set(),
        'transitions': dict()
    }

    # State of the NFA are composed by the union of more states of the AFW

    boundary = deepcopy(nfa['states'])
    possible_assignments = set(
        itertools.product([True, False], repeat=len(afw['states'])))

    while boundary:
        state = boundary.pop()
        # The state is accepting only if composed exclusively of final states
        if set(state).issubset(afw['accepting_states']):
            nfa['accepting_states'].add(state)

        for action in nfa['alphabet']:
            boolean_formula = 'True'
            # join the boolean formulas of the single states given the action
            for s in state:
                if (s, action) not in afw['transitions']:
                    boolean_formula += ' and False'
                else:
                    boolean_formula += \
                        ' and (' + \
                        afw['transitions'][s, action] + \
                        ')'

            for assignment in possible_assignments:
                mapping = dict(zip(afw['states'], assignment))

                # If the formula is satisfied
                if eval(boolean_formula, mapping):
                    # add the transition to the resulting NFA

                    evaluation = \
                        tuple(k for k in mapping if mapping[k] is True)

                    if evaluation not in nfa['states']:
                        nfa['states'].add(evaluation)
                        boundary.add(evaluation)
                    nfa['transitions'].setdefault(
                        (state, action), set()).add(evaluation)

    return nfa