(* Completion of an automaton *)

let (complete_with: 'state -> 'state automaton -> 'state automaton) = 
  fun black_hole aut ->
	{ aut with 
	  name = "FS(" ^ aut.name ^ ")" ;
	  transitions = 
	    (List.map (fun symbol -> (black_hole,symbol,black_hole)) aut.alphabet)
	    @
            (foreach_in (all_states_of aut) (fun src -> 
		foreach_in aut.alphabet (fun symbol ->
		      let 
			  src_transitions_on_symbol = get_transitions (On[symbol]) (get_transitions (From[src]) aut.transitions) 
		      in
			if src_transitions_on_symbol = [] 
			then [ (src,symbol,black_hole) ]
			else src_transitions_on_symbol  ))
 	    )
	} 


(* The complementary automaton *)

let (complementary_of_deterministic_automaton: 'state automaton -> ('state set) automaton) =
  fun aut ->
	let fs_aut (* fully_specified *) =  complete_with [] (lift_states_with (fun state -> [state]) aut)
	in
	  { fs_aut with 
            name = "C(" ^ fs_aut.name ^ ")" ;
	    accepting = Set.minus (all_states_of fs_aut) fs_aut.accepting
          }  

let (*USER*) (explained_complementary: 'state automaton -> ('state set) automaton) = 
  fun aut ->
	let dcfa =  (complete_with [] (determinization_using_set_of_states aut))
	in
	  { dcfa with 
            name = "C(" ^ dcfa.name ^ ")" ;
	    accepting = Set.minus (all_states_of dcfa) dcfa.accepting
          }  

let (*USER*)(complementary: 'state automaton -> 'state automaton) = 
  fun aut ->
	let dcfa =  normalize (complete_with [] (determinization_using_set_of_states aut))
	in
	  { dcfa with 
            name = "C(" ^ dcfa.name ^ ")" ;
	    accepting = Set.minus (all_states_of dcfa) dcfa.accepting
          }