X-Git-Url: http://git.nguyen.vg/gitweb/?p=tatoo.git;a=blobdiff_plain;f=src%2Fata.ml;h=add27752c0a75530d254e0b5d8af01b71d149732;hp=70213fd4fd7ae13ed151c36bfcc600385ec19cf7;hb=6ca42ffbd541cede6afcc473b563e54b848ee534;hpb=398ce5dca1bee23f5137a3eba21df17d7aaaf1fa diff --git a/src/ata.ml b/src/ata.ml index 70213fd..add2775 100644 --- a/src/ata.ml +++ b/src/ata.ml @@ -116,13 +116,23 @@ struct end -module Transition = Hcons.Make (struct +module Transition = + struct + include Hcons.Make (struct type t = State.t * QNameSet.t * Formula.t let equal (a, b, c) (d, e, f) = a == d && b == e && c == f let hash (a, b, c) = HASHINT4 (PRIME1, a, ((QNameSet.uid b) :> int), ((Formula.uid c) :> int)) end) + let print ppf t = + let q, l, f = t.node in + fprintf ppf "%a, %a %s %a" + State.print q + QNameSet.print l + Pretty.double_right_arrow + Formula.print f + end module TransList : sig @@ -147,24 +157,12 @@ type t = { transitions: (State.t, (QNameSet.t*Formula.t) list) Hashtbl.t; } - +let uid t = t.id let get_states a = a.states let get_starting_states a = a.starting_states let get_selecting_states a = a.selecting_states -let get_trans a tag states = - StateSet.fold (fun q acc0 -> - try - let trs = Hashtbl.find a.transitions q in - List.fold_left (fun acc1 (labs, phi) -> - if QNameSet.mem tag labs then - TransList.cons (Transition.make (q, labs, phi)) acc1 - else acc1) acc0 trs - with Not_found -> acc0 - ) states TransList.nil - - let _pr_buff = Buffer.create 50 let _str_fmt = formatter_of_buffer _pr_buff @@ -173,6 +171,7 @@ let _flush_str_fmt () = pp_print_flush _str_fmt (); Buffer.clear _pr_buff; s let print fmt a = + let _ = _flush_str_fmt() in fprintf fmt "Internal UID: %i@\n\ States: %a@\n\ @@ -215,6 +214,21 @@ let print fmt a = ) strs_strings; fprintf fmt "%s@\n" line + +let get_trans a tag states = + StateSet.fold (fun q acc0 -> + try + let trs = Hashtbl.find a.transitions q in + List.fold_left (fun acc1 (labs, phi) -> + if QNameSet.mem tag labs then + TransList.cons (Transition.make (q, labs, phi)) acc1 + else acc1) acc0 trs + with Not_found -> acc0 + ) states TransList.nil + + + + (* [complete transitions a] ensures that for each state q and each symbols s in the alphabet, a transition q, s exists. @@ -444,16 +458,30 @@ let concat a1 a2 = let link_phi = StateSet.fold (fun q phi -> Formula.(or_ (stay q) phi)) - a1.selecting_states Formula.true_ + a1.selecting_states Formula.false_ in + Hashtbl.iter (fun q trs -> Hashtbl.add a1.transitions q trs) + a2.transitions; StateSet.iter (fun q -> - Hashtbl.add a1.transitions q [(QNameSet.any, link_phi)]) + Hashtbl.replace a1.transitions q [(QNameSet.any, link_phi)]) a2.starting_states; - Hashtbl.iter (fun q trs -> Hashtbl.add a1.transitions q trs) - a2.transitions; { a1 with states = StateSet.union a1.states a2.states; selecting_states = a2.selecting_states; transitions = a1.transitions; } + +let merge a1 a2 = + let a1 = copy a1 in + let a2 = copy a2 in + { a1 with + states = StateSet.union a1.states a2.states; + selecting_states = StateSet.union a1.selecting_states a2.selecting_states; + starting_states = StateSet.union a1.starting_states a2.starting_states; + transitions = + let () = + Hashtbl.iter (fun k v -> Hashtbl.add a1.transitions k v) a2.transitions + in + a1.transitions + }