From: Kim Nguyễn Date: Thu, 25 Apr 2013 13:35:52 +0000 (+0200) Subject: Add a clean logger infrastructure. X-Git-Tag: v0.1~83 X-Git-Url: http://git.nguyen.vg/gitweb/?p=tatoo.git;a=commitdiff_plain;h=969febf12344a3fe3bf793a323b2e88f7b20ebae Add a clean logger infrastructure. --- diff --git a/include/debug.ml b/include/debug.ml new file mode 100644 index 0000000..5a51787 --- /dev/null +++ b/include/debug.ml @@ -0,0 +1,13 @@ +IFNDEF DEBUG__ML__ +THEN +DEFINE DEBUG__ML__ + +IFDEF DEBUG +THEN + DEFINE DBG(e) = (e) +ELSE + DEFINE DBG(e) = () +END + + +END (* IFNDEF DEBUG__ML__ *) diff --git a/src/ata.ml b/src/ata.ml index 01fa639..19eb75d 100644 --- a/src/ata.ml +++ b/src/ata.ml @@ -14,7 +14,7 @@ (***********************************************************************) (* - Time-stamp: + Time-stamp: *) INCLUDE "utils.ml" @@ -260,20 +260,27 @@ let create s ss = let n2 = ref 0 in Cache.N2.iteri (fun _ _ _ b -> if b then incr n2) auto.cache2; Cache.N4.iteri (fun _ _ _ _ _ b -> if b then incr n4) auto.cache4; - Format.eprintf "STATS: automaton %i, cache2: %i entries, cache6: %i entries\n%!" + Logger.msg `STATS "automaton %i, cache2: %i entries, cache6: %i entries" (auto.id :> int) !n2 !n4; let c2l, c2u = Cache.N2.stats auto.cache2 in let c4l, c4u = Cache.N4.stats auto.cache4 in - Format.eprintf "STATS: cache2: length: %i, used: %i, occupation: %f\n%!" c2l c2u (float c2u /. float c2l); - Format.eprintf "STATS: cache4: length: %i, used: %i, occupation: %f\n%!" c4l c4u (float c4u /. float c4l) + Logger.msg `STATS + "cache2: length: %i, used: %i, occupation: %f" + c2l c2u (float c2u /. float c2l); + Logger.msg `STATS + "cache4: length: %i, used: %i, occupation: %f" + c4l c4u (float c4u /. float c4l) ); auto let reset a = - a.cache2 <- Cache.N2.create (Cache.N2.dummy a.cache2); a.cache4 <- Cache.N4.create (Cache.N4.dummy a.cache4) +let full_reset a = + reset a; + a.cache2 <- Cache.N2.create (Cache.N2.dummy a.cache2) + let get_trans_aux a tag states = StateSet.fold (fun q acc0 -> @@ -298,82 +305,6 @@ let get_trans a tag states = (states.StateSet.id :> int) trs; trs) else trs - -(* -let eval_form phi fcs nss ps ss is_left is_right has_left has_right kind = - let rec loop phi = - begin match SFormula.expr phi with - Formula.True | Formula.False -> phi - | Formula.Atom a -> - let p, b, q = Atom.node a in begin - match p with - | First_child -> - if b == StateSet.mem q fcs then SFormula.true_ else phi - | Next_sibling -> - if b == StateSet.mem q nss then SFormula.true_ else phi - | Parent | Previous_sibling -> - if b == StateSet.mem q ps then SFormula.true_ else phi - | Stay -> - if b == StateSet.mem q ss then SFormula.true_ else phi - | Is_first_child -> SFormula.of_bool (b == is_left) - | Is_next_sibling -> SFormula.of_bool (b == is_right) - | Is k -> SFormula.of_bool (b == (k == kind)) - | Has_first_child -> SFormula.of_bool (b == has_left) - | Has_next_sibling -> SFormula.of_bool (b == has_right) - end - | Formula.And(phi1, phi2) -> SFormula.and_ (loop phi1) (loop phi2) - | Formula.Or (phi1, phi2) -> SFormula.or_ (loop phi1) (loop phi2) - end - in - loop phi - -let int_of_conf is_left is_right has_left has_right kind = - ((Obj.magic kind) lsl 4) lor - ((Obj.magic is_left) lsl 3) lor - ((Obj.magic is_right) lsl 2) lor - ((Obj.magic has_left) lsl 1) lor - (Obj.magic has_right) - -let eval_trans auto ltrs fcs nss ps ss is_left is_right has_left has_right kind = - let n = int_of_conf is_left is_right has_left has_right kind - and k = (fcs.StateSet.id :> int) - and l = (nss.StateSet.id :> int) - and m = (ps.StateSet.id :> int) in - let rec loop ltrs ss = - let i = (ltrs.TransList.id :> int) - and j = (ss.StateSet.id :> int) in - let (new_ltrs, new_ss) as res = - let res = Cache.N6.find auto.cache6 i j k l m n in - if res == dummy6 then - let res = - TransList.fold (fun trs (acct, accs) -> - let q, lab, phi = Transition.node trs in - if StateSet.mem q accs then (acct, accs) else - let new_phi = - eval_form - phi fcs nss ps accs - is_left is_right has_left has_right kind - in - if SFormula.is_true new_phi then - (acct, StateSet.add q accs) - else if SFormula.is_false new_phi then - (acct, accs) - else - let new_tr = Transition.make (q, lab, new_phi) in - (TransList.cons new_tr acct, accs) - ) ltrs (TransList.nil, ss) - in - Cache.N6.add auto.cache6 i j k l m n res; res - else - res - in - if new_ss == ss then res else - loop new_ltrs new_ss - in - loop ltrs ss - -*) - let simplify_atom atom pos q { Config.node=config; _ } = if (pos && StateSet.mem q config.sat) || ((not pos) && StateSet.mem q config.unsat) then SFormula.true_ diff --git a/src/ata.mli b/src/ata.mli index 8a1119e..a0778a1 100644 --- a/src/ata.mli +++ b/src/ata.mli @@ -14,7 +14,7 @@ (***********************************************************************) (* - Time-stamp: + Time-stamp: *) type predicate = @@ -93,6 +93,7 @@ type t = private { val create : StateSet.t -> StateSet.t -> t val reset : t -> unit +val full_reset : t -> unit val get_trans : t -> QNameSet.elt -> StateSet.t -> TransList.t diff --git a/src/eval.ml b/src/eval.ml index d90be92..575ee09 100644 --- a/src/eval.ml +++ b/src/eval.ml @@ -14,7 +14,7 @@ (***********************************************************************) (* - Time-stamp: + Time-stamp: *) INCLUDE "utils.ml" @@ -145,7 +145,8 @@ END if not (Bitvector.unsafe_get run.unstable i) then incr count done; - eprintf "@[STATS: %i nodes over %i were skipped in iteration %i (%.2f %%), redo is: %b@]@." + Logger.msg `STATS + "%i nodes over %i were skipped in iteration %i (%.2f %%), redo is: %b" !count len run.pass (100. *. (float !count /. float len)) run.redo @@ -170,7 +171,7 @@ END stats run; run.pass <- run.pass + 1; done; - at_exit (fun () -> eprintf "@[STATS: %i iterations@]@." run.pass); + at_exit (fun () -> Logger.msg `STATS "%i iterations" run.pass); at_exit (fun () -> stats run); let r = get_results auto tree node run.config in diff --git a/src/logger.ml b/src/logger.ml new file mode 100644 index 0000000..aa9f6f5 --- /dev/null +++ b/src/logger.ml @@ -0,0 +1,54 @@ +(***********************************************************************) +(* *) +(* TAToo *) +(* *) +(* Kim Nguyen, LRI UMR8623 *) +(* Université Paris-Sud & CNRS *) +(* *) +(* Copyright 2010-2013 Université Paris-Sud and Centre National de la *) +(* Recherche Scientifique. All rights reserved. This file is *) +(* distributed under the terms of the GNU Lesser General Public *) +(* License, with the special exception on linking described in file *) +(* ../LICENSE. *) +(* *) +(***********************************************************************) + +INCLUDE "utils.ml" +open Format + +type level = [ `NORMAL (* regular output *) + | `STATS (* Statistics only given if -s *) + | `DEBUG] (* DEBUG STATEMENTS *) + +let string_of_level = function +| `NORMAL -> "NORMAL" +| `STATS -> "STATS" +| `DEBUG -> "DEBUG" + + +let _o = ref err_formatter + +let set_output o = _o := o + +IFDEF DEBUG +THEN +let debug = true +ELSE +let debug = false +END + +let kont fmt = fprintf fmt "@]@." + +let msg level msg = + let do_ = + match level with + `NORMAL -> true + | `DEBUG when debug -> true + | `STATS when !Options.stats -> true + | _ -> false + in + if do_ then begin + fprintf !_o "@[%s: " (string_of_level level); + kfprintf kont !_o msg + end else + ifprintf !_o msg diff --git a/src/options.ml b/src/options.ml index 142b709..61f0396 100644 --- a/src/options.ml +++ b/src/options.ml @@ -7,10 +7,10 @@ let query = ref "" let stats = ref false let specs = align [ - "-c", Set count, ""; - "--count", Set count, " write the number of results only"; - "-s", Set stats, ""; - "--stats", Set stats, " display timing and various statistics"; + "-c", Set count, " write the number of results only"; + "--count", Set count, " "; + "-s", Set stats, " display timing and various statistics"; + "--stats", Set stats, " "; ] let usage_msg = Printf.sprintf "usage: %s [options] input.xml query [output.xml]" Sys.argv.(0) diff --git a/src/tatoo.ml b/src/tatoo.ml index 2c32062..ca79411 100644 --- a/src/tatoo.ml +++ b/src/tatoo.ml @@ -14,7 +14,7 @@ (***********************************************************************) (* - Time-stamp: + Time-stamp: *) open Format @@ -24,7 +24,7 @@ let time f arg msg = let r = f arg in let t2 = Unix.gettimeofday () in let time = (t2 -. t1) *. 1000. in - if !Options.stats then fprintf err_formatter "@[STATS: %s: %fms@]@." msg time; + Logger.msg `STATS "%s: %fms" msg time; r @@ -50,10 +50,8 @@ let main () = | Some f -> open_out f in if !Options.stats then begin - fprintf err_formatter "@[STATS: Query: %a @]@." Xpath.Ast.print_path query; - fprintf err_formatter "@[STATS: @[Automaton: @\n"; - Ata.print err_formatter auto; - fprintf err_formatter "@]@]@."; + Logger.msg `STATS "Query: %a " Xpath.Ast.print_path query; + Logger.msg `STATS "@[Automaton: @\n%a@]" Ata.print auto; end; let module Naive = Eval.Make(Naive_tree) in