From: Kim Nguyễn Date: Fri, 26 Jul 2013 14:01:29 +0000 (+0200) Subject: Drastically improve performances by simplifying the book-keeping X-Git-Tag: v0.1~54 X-Git-Url: http://git.nguyen.vg/gitweb/?p=tatoo.git;a=commitdiff_plain;h=021fdd8af4067ec57cdbf5c2dbc903252cbd4707 Drastically improve performances by simplifying the book-keeping of pending transitions during a topdown run. Before: - we were keeping for each node (1) sat: the set of states satisfied at that node (2) unsat: the set of states unsatisfied at that node (3) todo: the hashconsed list of pending transitions (of the form q, {a,b,c} -> f where f has been simplified w.r.t to sat and unsat (that is atoms containing states in either have been simplified to True or False) and q is neither in sat nor unsat. - during each run, for each node, we were scanning todo and rebuilding it removing satisfied or unsatisfied transitions. This lead to excessive hashconsing, and a lot of time spent in the hashconsing module (in turn spending a lot of time in the GC) After: - we keep for each node: (1) sat: the set of states satisfied at that node (2) todo: the set of undetermined *states* - we perform the book-keeping as before but do not materialize the simplified transitions. Also unsat is made inplicit (a state is unsat if it is neither in sat nor todo). --- diff --git a/src/ata.ml b/src/ata.ml index add2775..2f20b14 100644 --- a/src/ata.ml +++ b/src/ata.ml @@ -227,7 +227,14 @@ let get_trans a tag states = ) states TransList.nil - +let get_form a tag q = + try + let trs = Hashtbl.find a.transitions q in + List.fold_left (fun aphi (labs, phi) -> + if QNameSet.mem tag labs then Formula.or_ aphi phi else aphi + ) Formula.false_ trs + with + Not_found -> Formula.false_ (* [complete transitions a] ensures that for each state q diff --git a/src/ata.mli b/src/ata.mli index eada8d0..aa28abf 100644 --- a/src/ata.mli +++ b/src/ata.mli @@ -98,11 +98,16 @@ val get_selecting_states : t -> StateSet.t (** return the set of selecting states of the automaton *) val get_trans : t -> QNameSet.elt -> StateSet.t -> TransList.t -(** [get_trans auto l q] return the list of transitions taken by [auto] +(** [get_trans auto l q] returns the list of transitions taken by [auto] for label [l] in state [q]. Takes time proportional to the number of transitions in the automaton. *) +val get_form : t -> QNameSet.elt -> State.t -> Formula.t +(** [get_form auto l q] returns a single formula for label [l] in state [q]. + Takes time proportional to the number of transitions in the automaton. + *) + val print : Format.formatter -> t -> unit (** Pretty printing of the automaton *) diff --git a/src/run.ml b/src/run.ml index cb2ea3b..726a483 100644 --- a/src/run.ml +++ b/src/run.ml @@ -60,34 +60,40 @@ module Make (T : Tree.S) = end type node_status = { - sat : StateSet.t; - unsat : StateSet.t; - todo : Ata.TransList.t; - summary : NodeSummary.t; + sat : StateSet.t; (* States that are satisfied at the current node *) + todo : StateSet.t; (* States that remain to be proven *) + (* For every node_status and automaton a: + a.states - (sat U todo) = unsat *) + summary : NodeSummary.t; (* Summary of the shape of the node *) } (* Describe what is kept at each node for a run *) - module NodeStatus = Hcons.Make(struct - type t = node_status - let equal c d = - c == d || - c.sat == d.sat && - c.unsat == d.unsat && - c.todo == d.todo && - c.summary == d.summary - - let hash c = - HASHINT4((c.sat.StateSet.id :> int), - (c.unsat.StateSet.id :> int), - (c.todo.Ata.TransList.id :> int), - c.summary) - end - ) + module NodeStatus = + struct + include Hcons.Make(struct + type t = node_status + let equal c d = + c == d || + c.sat == d.sat && + c.todo == d.todo && + c.summary == d.summary + + let hash c = + HASHINT3((c.sat.StateSet.id :> int), + (c.todo.StateSet.id :> int), + c.summary) + end + ) + let print ppf s = + fprintf ppf + "{ sat: %a; todo: %a; summary: _ }" + StateSet.print s.node.sat + StateSet.print s.node.todo + end let dummy_status = NodeStatus.make { sat = StateSet.empty; - unsat = StateSet.empty; - todo = Ata.TransList.nil; + todo = StateSet.empty; summary = NodeSummary.dummy; } @@ -105,9 +111,9 @@ module Make (T : Tree.S) = (* A boolean indicating whether the run is incomplete *) mutable pass : int; (* The number of times this run was updated *) - mutable cache2 : Ata.TransList.t Cache.N2.t; + mutable cache2 : Ata.Formula.t Cache.N2.t; (* A cache from states * label to list of transitions *) - mutable cache4 : NodeStatus.t Cache.N4.t; + mutable cache5 : NodeStatus.t Cache.N5.t; } let pass r = r.pass @@ -116,11 +122,7 @@ module Make (T : Tree.S) = let tree r = r.tree - let dummy_trl = - Ata.(TransList.cons - (Transition.make - (State.dummy,QNameSet.empty, Formula.false_)) - TransList.nil) + let dummy_form = Ata.Formula.stay State.dummy let make auto tree = let len = T.size tree in @@ -131,8 +133,8 @@ module Make (T : Tree.S) = unstable = Bitvector.create ~init:true len; redo = true; pass = 0; - cache2 = Cache.N2.create dummy_trl; - cache4 = Cache.N4.create dummy_status; + cache2 = Cache.N2.create dummy_form; + cache5 = Cache.N5.create dummy_status; } let get_status a i = @@ -151,127 +153,143 @@ END let html tree node i config msg = let config = config.NodeStatus.node in Html.trace (T.preorder tree node) i - "node: %i
%s
sat: %a
unsat: %a
todo: %around: %i
" + "node: %i
%s
sat: %a
todo: %a
round: %i
" (T.preorder tree node) msg StateSet.print config.sat - StateSet.print config.unsat - (Ata.TransList.print ~sep:"
") config.todo i + StateSet.print config.todo + i let debug msg tree node i config = let config = config.NodeStatus.node in eprintf - "DEBUG:%s node: %i\nsat: %a\nunsat: %a\ntodo: %around: %i\n" + "DEBUG:%s node: %i\nsat: %a\ntodo: %a\nround: %i\n" msg (T.preorder tree node) StateSet.print config.sat - StateSet.print config.unsat - (Ata.TransList.print ~sep:"\n") config.todo i - + StateSet.print config.todo + i - let get_trans cache2 auto tag states = - let trs = - Cache.N2.find cache2 - (tag.QName.id :> int) (states.StateSet.id :> int) + let get_form cache2 auto tag q = + let phi = + Cache.N2.find cache2 (tag.QName.id :> int) (q :> int) in - if trs == dummy_trl then - let trs = Ata.get_trans auto tag states in - (Cache.N2.add - cache2 - (tag.QName.id :> int) - (states.StateSet.id :> int) trs; trs) - else trs - - - - let simplify_atom atom pos q { NodeStatus.node = status; _ } = - if (pos && StateSet.mem q status.sat) - || ((not pos) && StateSet.mem q status.unsat) then Ata.Formula.true_ - else if (pos && StateSet.mem q status.unsat) - || ((not pos) && StateSet.mem q status.sat) then Ata.Formula.false_ - else atom + if phi == dummy_form then + let phi = Ata.get_form auto tag q in + let () = + Cache.N2.add + cache2 + (tag.QName.id :> int) + (q :> int) phi + in phi + else phi + + type trivalent = False | True | Unknown + let of_bool = function false -> False | true -> True + let or_ t1 t2 = + match t1 with + False -> t2 + | True -> True + | Unknown -> if t2 == True then True else Unknown + + let and_ t1 t2 = + match t1 with + False -> False + | True -> t2 + | Unknown -> if t2 == False then False else Unknown + + (* Define as macros to get lazyness *) +DEFINE OR_(t1,t2) = + let __t1 = (t1) in + match t1 with + False -> (t2) + | True -> True + | Unknown -> if (t2) == True then True else Unknown + +DEFINE AND_(t1,t2) = + let __t1 = (t1) in + match t1 with + False -> False + | True -> (t2) + | Unknown -> if (t2) == False then False else Unknown let eval_form phi fcs nss ps ss summary = let open Ata in let rec loop phi = begin match Formula.expr phi with - Boolean.True | Boolean.False -> phi + | Boolean.False -> False + | Boolean.True -> True | Boolean.Atom (a, b) -> begin let open NodeSummary in match a.Atom.node with | Move (m, q) -> - let states = match m with - `First_child -> fcs - | `Next_sibling -> nss - | `Parent | `Previous_sibling -> ps - | `Stay -> ss - in simplify_atom phi b q states - | Is_first_child -> Formula.of_bool (b == is_left summary) - | Is_next_sibling -> Formula.of_bool (b == is_right summary) - | Is k -> Formula.of_bool (b == (k == kind summary)) - | Has_first_child -> Formula.of_bool (b == has_left summary) - | Has_next_sibling -> Formula.of_bool (b == has_right summary) + let { NodeStatus.node = n_sum; _ } as sum = + match m with + `First_child -> fcs + | `Next_sibling -> nss + | `Parent | `Previous_sibling -> ps + | `Stay -> ss + in + if sum == dummy_status || StateSet.mem q n_sum.todo then + Unknown + else + of_bool (b == StateSet.mem q n_sum.sat) + | Is_first_child -> of_bool (b == is_left summary) + | Is_next_sibling -> of_bool (b == is_right summary) + | Is k -> of_bool (b == (k == kind summary)) + | Has_first_child -> of_bool (b == has_left summary) + | Has_next_sibling -> of_bool (b == has_right summary) end - | Boolean.And(phi1, phi2) -> Formula.and_ (loop phi1) (loop phi2) - | Boolean.Or (phi1, phi2) -> Formula.or_ (loop phi1) (loop phi2) + | Boolean.And(phi1, phi2) -> AND_ (loop phi1, loop phi2) + | Boolean.Or (phi1, phi2) -> OR_ (loop phi1, loop phi2) end in loop phi - let eval_trans_aux cache4 fcs nss ps ss old_config = + let eval_trans_aux auto cache2 cache4 tag fcs nss ps old_status = let { sat = old_sat; - unsat = old_unsat; todo = old_todo; - summary = old_summary } = old_config.NodeStatus.node + summary = old_summary } as os_node = old_status.NodeStatus.node in - let sat, unsat, removed, kept, todo = - Ata.TransList.fold - (fun trs acc -> - let q, lab, phi = Ata.Transition.node trs in - let a_sat, a_unsat, a_rem, a_kept, a_todo = acc in - if StateSet.mem q a_sat || StateSet.mem q a_unsat then acc else - let new_phi = - eval_form phi fcs nss ps old_config old_summary - in - if Ata.Formula.is_true new_phi then - StateSet.add q a_sat, a_unsat, StateSet.add q a_rem, a_kept, a_todo - else if Ata.Formula.is_false new_phi then - a_sat, StateSet.add q a_unsat, StateSet.add q a_rem, a_kept, a_todo - else - let new_tr = Ata.Transition.make (q, lab, new_phi) in - (a_sat, a_unsat, a_rem, StateSet.add q a_kept, (Ata.TransList.cons new_tr a_todo)) - ) old_todo (old_sat, old_unsat, StateSet.empty, StateSet.empty, Ata.TransList.nil) + let sat, todo = + StateSet.fold (fun q ((a_sat, a_todo) as acc) -> + let phi = + get_form cache2 auto tag q + in + let v = eval_form phi fcs nss ps old_status old_summary in + match v with + True -> StateSet.add q a_sat, a_todo + | False -> acc + | Unknown -> a_sat, StateSet.add q a_todo + ) old_todo (old_sat, StateSet.empty) in - (* States that have been removed from the todo list and not kept are now - unsatisfiable *) - 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 = NodeStatus.make { old_config.NodeStatus.node with sat; unsat; todo; } in - new_config + if old_sat != sat || old_todo != todo then + NodeStatus.make { os_node with sat; todo } + else old_status - let eval_trans cache4 fcs nss ps ss = + let eval_trans auto cache2 cache5 tag fcs nss ps ss = let fcsid = (fcs.NodeStatus.id :> int) in let nssid = (nss.NodeStatus.id :> int) in let psid = (ps.NodeStatus.id :> int) in - let rec loop old_config = - let oid = (old_config.NodeStatus.id :> int) in + let tagid = (tag.QName.id :> int) in + let rec loop old_status = + let oid = (old_status.NodeStatus.id :> int) in let res = - let res = Cache.N4.find cache4 oid fcsid nssid psid in + let res = Cache.N5.find cache5 tagid oid fcsid nssid psid in if res != dummy_status then res else - let new_config = - eval_trans_aux cache4 fcs nss ps ss old_config + let new_status = + eval_trans_aux auto cache2 cache5 tag fcs nss ps old_status in - Cache.N4.add cache4 oid fcsid nssid psid new_config; - new_config + Cache.N5.add cache5 tagid oid fcsid nssid psid new_status; + new_status in - if res == old_config then res else loop res + if res == old_status then res else loop res in loop ss @@ -283,7 +301,7 @@ END let auto = run.auto in let status = run.status in let cache2 = run.cache2 in - let cache4 = run.cache4 in + let cache5 = run.cache5 in let unstable = run.unstable in let rec loop node = let node_id = T.preorder tree node in @@ -300,11 +318,11 @@ END let c = unsafe_get_status status node_id in if c == dummy_status then (* first time we visit the node *) - let ltrs = get_trans cache2 auto tag (Ata.get_states auto) in NodeStatus.make { sat = StateSet.empty; - unsat = Ata.get_starting_states auto; - todo = ltrs; + todo = StateSet.diff + (Ata.get_states auto) + (Ata.get_starting_states auto); summary = NodeSummary.make (node == T.first_child tree parent) (* is_left *) (node == T.next_sibling tree parent) (* is_right *) @@ -314,7 +332,6 @@ END } else c in - TRACE(html tree node _i config0 "Entering node"); (* get the node_statuses for the first child, next sibling and parent *) @@ -322,8 +339,7 @@ END let fcs = unsafe_get_status status fc_id in let nss = unsafe_get_status status ns_id in (* evaluate the transitions with all this statuses *) - let status1 = eval_trans cache4 fcs nss ps status0 in - + let status1 = eval_trans auto cache2 cache5 tag fcs nss ps status0 in TRACE(html tree node _i config1 "Updating transitions"); (* update the cache if the status of the node changed *) @@ -335,14 +351,14 @@ END get the new status of the first child *) let fcs1 = unsafe_get_status status fc_id in (* update the status *) - let status2 = eval_trans cache4 fcs1 nss ps status1 in + let status2 = eval_trans auto cache2 cache5 tag fcs1 nss ps status1 in TRACE(html tree node _i config2 "Updating transitions (after first-child)"); if status2 != status1 then status.(node_id) <- status2; let unstable_right = loop ns in let nss1 = unsafe_get_status status ns_id in - let status3 = eval_trans cache4 fcs1 nss1 ps status2 in + let status3 = eval_trans auto cache2 cache5 tag fcs1 nss1 ps status2 in TRACE(html tree node _i config3 "Updating transitions (after next-sibling)"); @@ -353,7 +369,7 @@ END pending, the current node is unstable *) unstable_left || unstable_right - || Ata.TransList.nil != status3.NodeStatus.node.todo + || StateSet.empty != status3.NodeStatus.node.todo in Bitvector.unsafe_set unstable node_id unstable_self; TRACE((if not unstable_self then @@ -456,18 +472,15 @@ END let tree = run.tree in let auto = run.auto in let status = run.status in - let cache2 = run.cache2 in List.iter (fun node -> let parent = T.parent tree node in let fc = T.first_child tree node in let ns = T.next_sibling tree node in - let tag = T.tag tree node in - let status0 = NodeStatus.make { sat = Ata.get_starting_states auto; - unsat = StateSet.empty; - todo = get_trans cache2 auto tag (Ata.get_states auto); + todo = + StateSet.diff (Ata.get_states auto) (Ata.get_starting_states auto); summary = NodeSummary.make (node == T.first_child tree parent) (* is_left *) (node == T.next_sibling tree parent) (* is_right *)