X-Git-Url: http://git.nguyen.vg/gitweb/?p=tatoo.git;a=blobdiff_plain;f=src%2Fata.ml;h=df433926b41d263b3ec105f449d02b5fa043d59f;hp=9fe128ae92a27b9b6883ae46bb5205e8b50994f3;hb=41dd1fed04cabad212f10fce3484545f6e9d9444;hpb=556c8805fcfd27f485bdd63cd704e4df7eac8a06 diff --git a/src/ata.ml b/src/ata.ml index 9fe128a..df43392 100644 --- a/src/ata.ml +++ b/src/ata.ml @@ -13,10 +13,6 @@ (* *) (***********************************************************************) -(* - Time-stamp: -*) - INCLUDE "utils.ml" open Format @@ -199,7 +195,6 @@ type config = { unsat : StateSet.t; todo : TransList.t; summary : node_summary; - mutable round : int; } module Config = Hcons.Make(struct @@ -236,12 +231,12 @@ let dummy2 = TransList.cons -let dummy_config = Config.make { sat = StateSet.empty; - unsat = StateSet.empty; - todo = TransList.nil; - summary = dummy_summary; - round = 0 - } +let dummy_config = + Config.make { sat = StateSet.empty; + unsat = StateSet.empty; + todo = TransList.nil; + summary = dummy_summary + } let create s ss = @@ -258,20 +253,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 -> @@ -296,82 +298,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_ @@ -442,7 +368,7 @@ let eval_trans auto fcs nss ps ss = let unsat = StateSet.union unsat (StateSet.diff removed kept) in (* States that were found once to be satisfiable remain so *) let unsat = StateSet.diff unsat sat in - let new_config = Config.make { sat; unsat; todo ; summary = old_summary ; round = 0 } in + let new_config = Config.make { old_config.Config.node with sat; unsat; todo; } in Cache.N4.add auto.cache4 oid fcsid nssid psid new_config; new_config in