module FSA = struct (* Finite State Modules *) module OrderedStates = struct type t = int let compare x y = if x > y then 1 else if x = y then 0 else -1 end;; module StateSet = Set.Make(OrderedStates);; module OrderedPStates = struct type t = int * int let compare x y = if ((fst x) > (fst y)|| (fst x = fst y) && (snd x > snd y)) then 1 else if x = y then 0 else -1 end;; module StatePSet = Set.Make(OrderedPStates);; type trans = {first: int; symbol: char; second: int};; module OChar = struct type t = char let compare x y = if x > y then 1 else if x = y then 0 else -1 end;; module CharSet = Set.Make(OChar);; (* HashedTrans defined the hash function on integers * chars *) module HashedTrans = struct type t = int * char let equal x y = (((fst x = fst y) && (snd x = snd y))) let hash x = ((256 * (fst x)) + (int_of_char (snd x))) end;; module HTrans = Hashtbl.Make(HashedTrans);; let add_transition_entry htbl elt = HTrans.add htbl (elt.first,elt.symbol) elt.second;; (* list_converts converts a transition hash table into a list of transitions *) let list_convert htb = let conv c n = {first = (fst c); symbol = (snd c); second = n} in let conv_add c n tlist = if (List.mem n (HTrans.find_all htb c)) then (conv c n)::tlist else tlist in HTrans.fold conv_add htb [];; (* Class automaton lets you create and manipulate automata It sets the initial automaton to all sets empty and the initial state to 0. Beware! *) class automaton = object val mutable i = 0 val mutable x = StateSet.empty val mutable y = StateSet.empty val mutable z = CharSet.empty val mutable t = HTrans.create 0 method get_initial = i method get_states = x method get_astates = y method get_alph = z method get_transitions = t method initialize_alph = z <- CharSet.empty method initialize_states = x <- StateSet.empty method initialize_astates = y <- StateSet.empty method initialize_transitions n = t <- HTrans.create n method state_change s = i <- s method add_alph d = z <- CharSet.add d z method add_state d = x <- StateSet.add d x method add_astate d = y <- StateSet.add d y method add_transition d = add_transition_entry t d method remove_alph d = z <- CharSet.remove d z method remove_state d = x <- StateSet.remove d x method remove_astate d = y <- StateSet.remove d y method remove_transition d = HTrans.remove t d method make_initial d = i <- d method make_alph d = z <- d method make_states d = x <- d method make_astates d = y <- d method make_transitions d = t <- d method iniset = StateSet.add i StateSet.empty method list_alph = CharSet.elements z method list_states = StateSet.elements x method list_astates = StateSet.elements y method list_transitions = list_convert t end;; (* aut_copy aut aut1 copies aut to aut1 *) let aut_copy aut aut1 = aut1#make_initial aut#get_initial; aut1#make_alph aut#get_alph; aut1#make_states aut#get_states; aut1#make_astates aut#get_astates; aut1#make_transitions aut#get_transitions;; (* nice output *) let rec int_prt ls = match ls with [] -> Format.print_string("") | hd::[] -> (Format.print_int(hd)) | hd::tl -> (Format.print_int(hd); Format.print_string(", ");int_prt tl);; let rec char_prt ls = match ls with [] -> Format.print_string("") | hd::[] -> (Format.print_char(hd)) | hd::tl -> (Format.print_char(hd); Format.print_string(", ");char_prt tl);; let entry_print tr = Format.print_string("\123out: "); Format.print_int(tr.first); Format.print_string("; letter: "); Format.print_char(tr.symbol); Format.print_string("; in: "); Format.print_int(tr.second); Format.print_string("\125");; let rec tr_prt ls = match ls with [] -> Format.print_string("") | hd::[] -> entry_print(hd) | hd::tl -> (entry_print(hd); Format.print_string(", "); Format.print_newline (); Format.print_string(" "); tr_prt tl);; let list_print ls = Format.open_box 0; Format.print_char('\123'); int_prt ls; Format.print_char('\125'); Format.close_box (); Format.print_newline ();; let alist_print ls = Format.open_box 0; Format.print_char('\123'); char_prt ls; Format.print_char('\125'); Format.close_box (); Format.print_newline ();; let trlist_print ls = Format.open_box 0; Format.print_string(" \123"); tr_prt ls; Format.print_char('\125'); Format.close_box (); Format.print_newline ();; let show aut = print_string("States: "); list_print aut#list_states; print_string("Accepting States: "); list_print aut#list_astates; print_string("Initial State: "); Format.open_box 0; Format.print_int(aut#get_initial); Format.close_box (); Format.print_newline (); print_string("Alphabet: "); alist_print aut#list_alph; print_string("Transitions: "); Format.print_newline (); trlist_print aut#list_transitions;; (* arrows aut returns a list of pairs (m,n) such that there is a transition from m to n *) let arrows aut = let st = ref StatePSet.empty in let gc set (left,right) entry = if not (StatePSet.mem (left,entry) !set) then set := StatePSet.add (left,entry) !set in HTrans.iter (gc st) aut#get_transitions; !st;; (* closure S R computes the closure of the set S under the relation R *) let rec flip set flag lrela1 lrela = match (lrela,flag) with ([],false) -> set | ([],true) -> flip set false [] lrela1 | ((h,d)::tl,_) when (StateSet.mem h set) -> (flip (StateSet.add d set) true lrela1 tl) | (hd::tl,f) -> (flip set f (hd::lrela1) tl);; let closure set rela = flip set false [] (StatePSet.elements rela);; (* is_empty aut checks whether aut accepts no input *) let is_empty aut = let f = closure aut#iniset (arrows aut) in StateSet.is_empty (StateSet.inter f aut#get_astates);; (* close_sets adds for each transition the arguments to the list of states and the alphabet. *) let close_sets aut = let fc (m,a) n = aut#add_state m; aut#add_state n; aut#add_alph a in HTrans.iter fc aut#get_transitions;; (* assoc_make numbers the members of a list in ascending order *) let rec assc slist = match slist with [] -> [] | hd::tl -> (hd,(List.length tl))::(assc tl);; let assoc_make slist = assc (List.rev slist);; (* totalize aut checks whether aut is partial and if so adds a trash state *) let not_bound aut = let trs = aut#get_transitions in let lst = ref [] in let bad_list i chr = if HTrans.mem trs (i,chr) then lst := !lst else lst := (i,chr)::!lst in let state_check i = CharSet.iter (bad_list i) aut#get_alph in StateSet.iter state_check aut#get_states; !lst;; let partial aut = not ([] = not_bound aut);; let rec complete_trans trs elt lst = let add_entry t e pair = HTrans.add t pair e in List.iter (add_entry trs elt) lst;; let totalize aut = let trs = aut#get_transitions in let lst = not_bound aut in if lst = [] then (Format.print_string("This automaton is already total."); Format.print_newline()) else let m = (StateSet.max_elt aut#get_states)+1 in complete_trans trs m lst; let trash x ch = HTrans.add trs (x,ch) x in CharSet.iter (trash m) aut#get_alph; aut#make_transitions trs; ;; (* compactify renames the transitions and states *) let trsl tlist aslist = let remap aslist hd = {first = (List.assoc hd.first aslist); symbol = hd.symbol; second = (List.assoc hd.second aslist)} in List.map (remap aslist) tlist;; let compactify aut = close_sets aut; let tlist = aut#list_transitions and st = aut#get_states and ast = aut#get_astates in let ntbl = HTrans.create (List.length tlist) and slist = (assoc_make (StateSet.elements st)) in let ttlist = trsl tlist slist in List.iter (add_transition_entry ntbl) ttlist; aut#make_transitions ntbl; aut#make_initial (List.assoc (aut#get_initial) slist); aut#initialize_states; aut#initialize_astates; let state_add n = (aut#add_state (List.assoc n slist)) in (StateSet.iter state_add st); let astate_add n = (aut#add_astate (List.assoc n slist)) in (StateSet.iter astate_add ast);; (* make_empty aut makes aut the empty automaton *) let make_empty aut = aut#initialize_transitions 0; aut#make_initial 0; aut#initialize_states; aut#add_state 0; aut#initialize_astates;; (* restrict_to_accessible removes inaccessible states *) let restrict_to_accessible aut = close_sets aut; (* first we define the accessible states *) let acc_states = (closure aut#iniset (arrows aut)) in (* and then restrict the states sets *) aut#make_states acc_states; aut#make_astates (StateSet.inter aut#get_astates acc_states); (* next we remove inaccessible transitions *) let htbl = aut#get_transitions and ctbl = HTrans.create ((StateSet.cardinal (aut#get_states))*(StateSet.cardinal (aut#get_states))*256) in let add_to_htbl c n = if (StateSet.mem n acc_states) && (StateSet.mem (fst c) acc_states) then HTrans.add ctbl c n in HTrans.iter add_to_htbl htbl; aut#make_transitions ctbl; (* we check whether there is an accessible accepting state if so, the automaton is set to the null automaton *) if ((StateSet.is_empty aut#get_astates) || not (StateSet.mem aut#get_initial aut#get_states)) then (print_endline("Warning: This automaton accepts the empty language!"); make_empty aut) else ();; (* clean_fsa performs all normalizations at once *) let clean_fsa aut = restrict_to_accessible aut; compactify aut;; (* runs_to htbl st x is that number y such that string st leads from state x to state y via the hash table htbl. *) let rec runs_to g st x = if st = "" then x else let b = ref x in for i = 0 to (String.length st)-1 do b := HTrans.find g#get_transitions (!b,st.[i]) done; !b;; (* accepts g sta looks whether starting at g's initial state one ends in an accepting state of g following the transitions on st. *) let accepts g st = StateSet.mem (runs_to g st g#get_initial) g#get_astates;; (* exp_state htb states set chr creates the successor state in the exponentiated machine *) let exp_state htb states set chr = let is_succ n m = (List.mem n (HTrans.find_all htb (m,chr))) in let succ_set n = (StateSet.exists (is_succ n) set) in StateSet.filter succ_set states;; let rec cut_off q elt = match q with [] -> elt | ht::[] -> elt | hd::tl when ((List.hd tl) = elt) -> hd | hd::tl when not (hd = elt) -> (cut_off tl elt) | _ -> elt;; let next_in_line elt lstr = cut_off (fst (List.split lstr)) elt;; let rec follow aut ast set i n alph lstr sts htb ntb = let next = (next_in_line set lstr) in if i=n then if (set = next) then ntb else (follow aut ast next 0 n alph lstr sts htb ntb) else let chr = (List.nth alph i) in let set2 = (exp_state htb sts set chr) in let lstr1 = if not (List.mem_assoc set2 lstr) then ((set2,(List.length lstr))::lstr) else lstr in if not (List.mem_assoc set2 lstr) && not (StateSet.is_empty (StateSet.inter set2 ast)) then aut#add_astate (List.assoc set2 lstr1); let plus = {first = (List.assoc set lstr1); symbol = chr; second = (List.assoc set2 lstr1)} in (follow aut ast set (i+1) n alph lstr1 sts htb (plus::ntb));; let exponentiate aut aut1 = (* clean_fsa aut; *) let htb = aut#get_transitions and ast = aut#get_astates and i = aut#iniset in aut1#initialize_astates; aut1#make_initial 0; let ntb = HTrans.create (List.length (list_convert htb)) in let tlist = (follow aut ast i 0 (List.length aut#list_alph) aut#list_alph [(i,0)] aut#get_states htb []) in List.iter (add_transition_entry ntb) tlist; aut1#make_transitions ntb; close_sets aut1;; (* We define sets of sets of states *) module OStateSetSet = struct type t = StateSet.t let compare x y = StateSet.compare x y end;; module StateSetSet = Set.Make(OStateSetSet);; (* Next we implement the refinement of such a set via an arbitrary set Y. The refinement will not add any empty sets *) let set_refine aset set = let sct = StateSet.inter aset set in if ((StateSet.subset aset set) || (StateSet.is_empty sct)) then (StateSetSet.singleton aset) else (StateSetSet.add sct (StateSetSet.singleton (StateSet.diff aset set)));; let part_refine pset set = if ((StateSetSet.is_empty pset) || (StateSet.is_empty set)) then pset else let add_refined set iset rset = StateSetSet.union rset (set_refine iset set) in StateSetSet.fold (add_refined set) pset StateSetSet.empty;; let char_refine states trans set ch pset = let goes_to set trans ch elt = ((HTrans.mem trans (elt,ch)) && (StateSet.mem (HTrans.find trans (elt,ch)) set)) in let preset = StateSet.filter (goes_to set trans ch) states in part_refine pset preset;; let all_char_refine states alph trans set pset = CharSet.fold (char_refine states trans set) alph pset;; let one_step_refine states alph trans pset = StateSetSet.fold (all_char_refine states alph trans) pset pset;; let rec totally_refine states alph trans pset = let part = (one_step_refine states alph trans pset) in if (pset = part) then pset else (totally_refine states alph trans part);; (* finds the index of the first occurrence in the reverse list *) let rec associate_number elt lyst = if lyst = [] then 1 else if (List.hd lyst) = elt then 0 else (associate_number elt (List.tl lyst))+1;; (* compress aut part compresses each set of the partition of aut into one element. It does not check whether the automaton is refined! *) let compress aut part = let hl = StateSetSet.elements part in aut#initialize_states; let smb = (List.find (StateSet.mem aut#get_initial) hl) in aut#make_initial (associate_number smb (List.rev hl)); let ast = aut#get_astates in aut#initialize_astates; let trs = aut#get_transitions in (aut#initialize_transitions ((List.length hl) * (List.length hl) * 256)); let adt x y a = if ((HTrans.mem trs ((StateSet.min_elt (List.nth hl x)),a))) && (StateSet.mem (HTrans.find trs ((StateSet.min_elt (List.nth hl x)),a)) (List.nth hl y)) then (aut#add_transition {first = x; symbol = a; second = y}) else () in for i = 0 to ((List.length hl)-1) do aut#add_state i; if StateSet.subset (List.nth hl i) ast then aut#add_astate i; for j = 0 to ((List.length hl)-1) do CharSet.iter (adt i j) aut#get_alph done; done; ;; (* automaton_refine aut refines the automaton if needed. Reports if the automaton has no accepting states. First however the automaton is totalized. *) let automaton_refine aut = let ast = aut#get_astates in let fst = aut#get_states in let trs = aut#get_transitions in if (StateSet.is_empty ast) then (Format.print_string("This automaton has no accepting states!"); Format.print_newline()) else let split = if (fst = ast) then (StateSetSet.singleton fst) else (StateSetSet.add ast (StateSetSet.singleton (StateSet.diff fst ast))) in (compress aut (totally_refine fst aut#get_alph trs split));; (* end of module*) end;;