X-Git-Url: http://git.nguyen.vg/gitweb/?p=tatoo.git;a=blobdiff_plain;f=src%2Fauto%2Fata.ml;h=f4f11db7a96cc612cca4629eefa01dd4e82c2466;hp=aa4fb385a2d80c3244b180f42ad99f5753a9e3d8;hb=8026ca9faaa968ced3c2e75ca1d6b55f7270ca50;hpb=f49a93deba13602e16a3923695281e9a20215ac8 diff --git a/src/auto/ata.ml b/src/auto/ata.ml index aa4fb38..f4f11db 100644 --- a/src/auto/ata.ml +++ b/src/auto/ata.ml @@ -14,7 +14,7 @@ (***********************************************************************) (* - Time-stamp: + Time-stamp: *) INCLUDE "utils.ml" @@ -29,6 +29,12 @@ type state_ctx = { mutable left : StateSet.t; mutable epsilon : StateSet.t} type pred_ = move * bool * State.t +let make_ctx a b c d e = + { left = a; right = b; up1 = c; up2 = d; epsilon = e } + +let print_ctx fmt c = fprintf fmt "{ left : %a; right : %a; up1: %a ; up2 : %a; epsilon : %a }" + StateSet.print c.left StateSet.print c.right StateSet.print c.up1 StateSet.print c.up2 + StateSet.print c.epsilon module Move : (Formula.PREDICATE with type data = pred_ and type ctx = state_ctx ) = struct @@ -42,14 +48,16 @@ struct type ctx = state_ctx - let make_ctx a b c d e = - { left = a; right = b; up1 = c; up2 = d; epsilon = e } - include Hcons.Make(Node) + include Hcons.Make(Node) + let _pr_buff = Buffer.create 10 + let _str_fmt = formatter_of_buffer _pr_buff + let _flush_str_fmt () = pp_print_flush _str_fmt (); + let s = Buffer.contents _pr_buff in + Buffer.clear _pr_buff; s let print ppf a = - let _ = flush_str_formatter() in - let fmt = str_formatter in + let _ = _flush_str_fmt () in let m, b, s = a.node in let dir,num = @@ -60,9 +68,9 @@ struct | `Up1 -> Pretty.up_arrow, Pretty.subscript 1 | `Up2 -> Pretty.up_arrow, Pretty.subscript 2 in - fprintf fmt "%s%s" dir num; - State.print fmt s; - let str = flush_str_formatter() in + fprintf _str_fmt "%s%s" dir num; + State.print _str_fmt s; + let str = _flush_str_fmt () in if b then fprintf ppf "%s" str else Pretty.pp_overline ppf str @@ -72,7 +80,7 @@ struct exception NegativeAtom of (move*State.t) let eval ctx p = let l, b, s = p.node in - if b then raise (NegativeAtom(l,s)); + if not b then raise (NegativeAtom(l,s)); StateSet.mem s begin match l with `Left -> ctx.left @@ -87,8 +95,8 @@ module SFormula = Formula.Make(Move) type t = { id : Uid.t; mutable states : StateSet.t; -(* mutable top_states : StateSet.t; - mutable bottom_states: StateSet.t; *) + mutable top_states : StateSet.t; + mutable bottom_states: StateSet.t; mutable selection_states: StateSet.t; transitions: (State.t, (QNameSet.t*SFormula.t) list) Hashtbl.t; } @@ -97,13 +105,22 @@ let next = Uid.make_maker () let create () = { id = next (); states = StateSet.empty; -(* top_states = StateSet.empty; - bottom_states = StateSet.empty; *) + top_states = StateSet.empty; + bottom_states = StateSet.empty; selection_states = StateSet.empty; transitions = Hashtbl.create 17; } +let get_trans a states tag = + 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 (q,phi)::acc1 else acc1) acc0 trs + with Not_found -> acc0 + ) states [] + (* [add_trans a q labels f] adds a transition [(q,labels) -> f] to the automaton [a] but ensures that transitions remains pairwise disjoint @@ -132,17 +149,24 @@ let add_trans a q s f = in Hashtbl.replace a.transitions q ntrs +let _pr_buff = Buffer.create 50 +let _str_fmt = formatter_of_buffer _pr_buff +let _flush_str_fmt () = pp_print_flush _str_fmt (); + let s = Buffer.contents _pr_buff in + Buffer.clear _pr_buff; s let print fmt a = fprintf fmt - "Unique ID: %i@\n\ - States %a@\n\ + "\nInternal UID: %i@\n\ + States: %a@\n\ + Top states: %a@\n\ + Bottom states: %a@\n\ Selection states: %a@\n\ Alternating transitions:@\n" (a.id :> int) StateSet.print a.states -(* StateSet.print a.top_states - StateSet.print a.bottom_states *) + StateSet.print a.top_states + StateSet.print a.bottom_states StateSet.print a.selection_states; let trs = Hashtbl.fold @@ -150,25 +174,30 @@ let print fmt a = a.transitions [] in - let sorted_trs = List.stable_sort (fun (q1, s1, phi1) (q2, s2, phi2) -> + let sorted_trs = List.stable_sort (fun (q1, s1, _) (q2, s2, _) -> let c = State.compare q1 q2 in - (if c == 0 then QNameSet.compare s1 s2 else c)) trs in - let sfmt = str_formatter in - let _ = flush_str_formatter () in - let strs_strings, maxs = List.fold_left (fun (accl, accm) (q, s, f) -> - let s1 = State.print sfmt q; flush_str_formatter () in - let s2 = QNameSet.print sfmt s; flush_str_formatter () in - let s3 = SFormula.print sfmt f; flush_str_formatter () in - ( (s1, s2, s3) :: accl, - max - accm (2 + String.length s1 + String.length s2)) - ) ([], 0) sorted_trs + let _ = _flush_str_fmt () in + let strs_strings, max_pre, max_all = List.fold_left (fun (accl, accp, acca) (q, s, f) -> + let s1 = State.print _str_fmt q; _flush_str_fmt () in + let s2 = QNameSet.print _str_fmt s; _flush_str_fmt () in + let s3 = SFormula.print _str_fmt f; _flush_str_fmt () in + let pre = Pretty.length s1 + Pretty.length s2 in + let all = Pretty.length s3 in + ( (q, s1, s2, s3) :: accl, max accp pre, max acca all) + ) ([], 0, 0) sorted_trs in - List.iter (fun (s1, s2, s3) -> - fprintf fmt "%s, %s" s1 s2; - fprintf fmt "%s" (Pretty.padding (maxs - String.length s1 - String.length s2 - 2)); - fprintf fmt "%s %s@\n" Pretty.right_arrow s3) strs_strings + let line = Pretty.line (max_all + max_pre + 6) in + let prev_q = ref State.dummy in + List.iter (fun (q, s1, s2, s3) -> + if !prev_q != q && !prev_q != State.dummy then fprintf fmt " %s\n%!" line; + prev_q := q; + fprintf fmt " %s, %s" s1 s2; + fprintf fmt "%s" (Pretty.padding (max_pre - Pretty.length s1 - Pretty.length s2)); + fprintf fmt " %s %s@\n%!" Pretty.right_arrow s3; + ) strs_strings; + fprintf fmt " %s\n%!" line (* [complete transitions a] ensures that for each state q @@ -195,7 +224,7 @@ let complete_transitions a = complementing the sub-automaton in the negative states. [TODO check the meaning of negative upward arrows] *) -let normalize_negations a = +let normalize_negations auto = let memo_state = Hashtbl.create 17 in let todo = Queue.create () in let rec flip b f = @@ -214,7 +243,7 @@ let normalize_negations a = either we have a positive state deep below a negation or we have a negative state in a positive formula b' = sign of the state - b = sign of the containing formula + b = sign of the enclosing formula *) let not_q = try @@ -224,6 +253,10 @@ let normalize_negations a = Not_found -> (* create a new state and add it to the todo queue *) let nq = State.make () in + if not (StateSet.mem q auto.bottom_states) then + auto.bottom_states <- StateSet.add nq auto.bottom_states; + if not (StateSet.mem q auto.top_states) then + auto.top_states <- StateSet.add nq auto.top_states; Hashtbl.add memo_state (q, false) nq; Queue.add (q, false) todo; nq in @@ -231,7 +264,9 @@ let normalize_negations a = end end in - StateSet.iter (fun q -> Queue.add (q, true) todo) a.selection_states; + (* states that are not reachable from a selection stat are not interesting *) + StateSet.iter (fun q -> Queue.add (q, true) todo) auto.selection_states; + while not (Queue.is_empty todo) do let (q, b) as key = Queue.pop todo in let q' = @@ -239,10 +274,17 @@ let normalize_negations a = Hashtbl.find memo_state key with Not_found -> - let nq = if b then q else State.make () in + let nq = if b then q else + let nq = State.make () in + if not (StateSet.mem q auto.bottom_states) then + auto.bottom_states <- StateSet.add nq auto.bottom_states; + if not (StateSet.mem q auto.top_states) then + auto.top_states <- StateSet.add nq auto.top_states; + nq + in Hashtbl.add memo_state key nq; nq in - let trans = Hashtbl.find a.transitions q in + let trans = Hashtbl.find auto.transitions q in let trans' = List.map (fun (lab, f) -> lab, flip b f) trans in - Hashtbl.replace a.transitions q' trans' + Hashtbl.replace auto.transitions q' trans' done