(* The states of the deterministic automaton under construction are
 set of states of the origninal non-deterministic automaton.  A set of
 states (called a configuration) represents the concurrent execution
 of several copies of the original automaton at different current
 states. Each copy trying to recognize the word from one state of the configuration.
 The word is recognized if (at least) one of the concurrent copy accepts it.
*)
	      
let (enumerate_transitions_from: 'state automaton -> 'state set -> (('state set) transition) list) =
  fun aut initial_configuration ->
	let transitions_from = fun configurations ->
	      foreach_in configurations (fun config ->
		    foreach_in aut.alphabet (fun symbol ->
			  make_if_useful_transition (config, symbol, targets aut config symbol) 
              ))
	and configurations_from = fun transitions -> targets_of transitions
	and deja_vu = []
	and inputs  = [ initial_configuration ]
	and outputs = []
	in
	  accumulating_fixpoint (transitions_from,configurations_from) (deja_vu, inputs, outputs)


let (*USER*) (determinization_using_set_of_states: 'state automaton -> ('state set) automaton) =
  fun aut ->
	let initial_configuration = aut.initial
	in let 
	    transitions_between_configurations = enumerate_transitions_from aut initial_configuration
	in 
	  { aut with 
	    name = "D(" ^ aut.name ^ ")" ;
	    initial   = [ initial_configuration ] ;
	    accepting = List.filter (fun config -> Set.intersect config aut.accepting) 
	      (states_of transitions_between_configurations) ;
            transitions = List.rev transitions_between_configurations
	  } 

let (*USER*) (determinization: std automaton -> std automaton) = 
  fun aut -> normalize (determinization_using_set_of_states aut)

let (*USER*) (explained_determinization: std automaton -> std automaton) = 
  fun aut ->
	let (indexed_configs,dfa) = rename (determinization_using_set_of_states aut)
	in
	  begin
	    print_string (String.concat " " 
                [ "\n Renaming of configurations:"  
                ; Set.pretty_indexed_set pretty_std_states indexed_configs 
		; "\n\n"
                ]) ;
	    dfa 
	  end


(* The blow up example of Sakoda-Sipser 1978, Birget 1993 *)

let blow_up_ndfa n =
  let rec generate_transitions = 
    fun n -> if n=0 then [] else (generate_transitions (n-1)) @ [ (n,"a",n+1) ; (n,"b",n+1) ]
  in
    { name = "Blowup." ^ (string_of_int n)
    ; alphabet = [ "a" ; "b"] 
    ; initial = [0]
    ; accepting = [ n+2 ]
    ; transitions = 
      [ (0,"a",0) ; (0,"a",1) ;                 (n+2,"a",n+2) ;
	(0,"b",0) ;             (n+1,"b",n+2) ; (n+2,"b",n+2) ] @ (generate_transitions n)
    } ;;