docs: def nfa_to_afw_conversion(nfa: dict) -> dict:
      """ Returns a AFW reading the same language of input NFA.
  
      Let :math:`A = (Σ,S,S^0, ρ,F)`  be an nfa. Then we define the
      afw AA such that :math:`L(AA) = L(A)` as follows
      :math:`AA = (Σ, S ∪ {s_0}, s_0 , ρ_A , F )` where :math:`s_0`
      is a new state and :math:`ρ_A` is defined as follows:
  
       • :math:`ρ_A(s, a)= ⋁_{(s,a,s')∈ρ}s'`, for all :math:`a ∈ Σ`
         and :math:`s ∈ S`
       • :math:`ρ_A(s^0, a)= ⋁_{s∈S^0,(s,a,s')∈ρ}s'`, for all
         :math:`a ∈ Σ`
  
      We take an empty disjunction in the definition of AA to be
      equivalent to false. Essentially,
      the transitions of A are viewed as disjunctions in AA . A
      special treatment is needed for the
      initial state, since we allow a set of initial states in
      nondeterministic automata, but only a
      single initial state in alternating automata.
  
      :param dict nfa: input NFA.
      :return: *(dict)* representing a AFW.
      """
      afw = {
          'alphabet': nfa['alphabet'].copy(),
          'states': nfa['states'].copy(),
          'initial_state': 'root',
          'accepting_states': nfa['accepting_states'].copy(),
          'transitions': dict()
      }
  
      # Make sure "root" node doesn't already exists, in case rename it
      i = 0
      while afw['initial_state'] in nfa['states']:
          afw['initial_state'] = 'root' + str(i)
          i += 1
      afw['states'].add(afw['initial_state'])
  
      for (state, action) in nfa['transitions']:
          boolean_formula = str()
          for destination in nfa['transitions'][state, action]:
              boolean_formula += destination + ' or '
          # strip last ' or ' from the formula string
          boolean_formula = boolean_formula[0:-4]
          afw['transitions'][state, action] = boolean_formula
          if state in nfa['initial_states']:
              afw['transitions'][afw['initial_state'], action] = boolean_formula
  
      return afw