From: Kim Nguyễn Date: Sat, 16 Mar 2013 10:32:08 +0000 (+0100) Subject: - Reorder the keys used to cache transitions X-Git-Tag: v0.1~109 X-Git-Url: http://git.nguyen.vg/gitweb/?p=tatoo.git;a=commitdiff_plain;h=3d06334f6539fb3376427b7cf063d2b330142b87 - Reorder the keys used to cache transitions - Use a new stop condition (gives optimal traversal for filter less queries) - Reorder a variant type so that the hash of some variant becomes smaller --- diff --git a/src/auto/ata.ml b/src/auto/ata.ml index 419ab57..2710465 100644 --- a/src/auto/ata.ml +++ b/src/auto/ata.ml @@ -14,7 +14,7 @@ (***********************************************************************) (* - Time-stamp: + Time-stamp: *) INCLUDE "utils.ml" @@ -262,15 +262,13 @@ let int_of_conf is_left is_right has_left has_right kind = (Obj.magic has_right) let eval_trans auto ltrs fcs nss ps ss is_left is_right has_left has_right kind = - let i = int_of_conf 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 - + and m = (ps.StateSet.id :> int) in let rec loop ltrs ss = - let j = (ltrs.TransList.id :> int) - and n = (ss.StateSet.id :> int) in + 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 diff --git a/src/auto/eval.ml b/src/auto/eval.ml index e4def93..f51e0d5 100644 --- a/src/auto/eval.ml +++ b/src/auto/eval.ml @@ -14,7 +14,7 @@ (***********************************************************************) (* - Time-stamp: + Time-stamp: *) INCLUDE "utils.ml" @@ -96,7 +96,12 @@ END TRACE(Html.trace (T.preorder tree node) _i "Right BU States: %a
Right BU Trans: %a
" StateSet.print states3 (Ata.TransList.print ~sep:"
") _trans3) in if states3 != states2 then set cache tree node states3; - if states0 != states3 && (not !redo) then redo := true + (*if states0 != states3 && (not !redo) then redo := true *) + if (not !redo) + && not (Ata.TransList.nil == _trans3) + && (states1 != states3) + && not (StateSet.intersect states3 auto.Ata.selection_states) + then redo := true end in loop node; @@ -122,6 +127,7 @@ END let iter = ref 0 in Ata.reset auto; while !redo do + redo := false; redo := top_down_run auto tree node cache !iter; incr iter; done; diff --git a/src/tree/common.ml b/src/tree/common.ml index 099d751..76e6dc2 100644 --- a/src/tree/common.ml +++ b/src/tree/common.ml @@ -14,13 +14,13 @@ (***********************************************************************) (* - Time-stamp: + Time-stamp: *) module NodeKind = struct type t = - Document | Element | Text | Comment | Attribute | ProcessingInstruction + Document | Element | Text | Attribute | Comment | ProcessingInstruction | Node let to_string =