Hashcons transition evaluation based on node configuration.

diff --git a/src/ata.ml b/src/ata.ml
index 62be713..d6aeaec 100644 (file)
--- a/src/ata.ml
+++ b/src/ata.ml
@@ -14,7 +14,7 @@
 (***********************************************************************)
 
 (*
 (***********************************************************************)
 
 (*

-  Time-stamp: <Last modified on 2013-04-22 14:46:08 CEST by Kim Nguyen>
+  Time-stamp: <Last modified on 2013-04-22 15:27:36 CEST by Kim Nguyen>

 *)
 
 INCLUDE "utils.ml"
 *)
 
 INCLUDE "utils.ml"


@@ -159,13 +159,72 @@ end =
   end
 
 
   end
 
 

+
+type node_summary = int
+let dummy_summary = -1
+(*
+4444444444443210
+4 -> kind
+3 -> is_left
+2 -> is_right
+1 -> has_left
+0 -> has_right
+*)
+
+let has_right (s : node_summary) : bool =
+  Obj.magic (s land 1)
+let has_left (s : node_summary) : bool =
+  Obj.magic ((s lsr 1) land 1)
+
+let is_right (s : node_summary) : bool =
+  Obj.magic ((s lsr 2) land 1)
+
+let is_left (s : node_summary) : bool =
+  Obj.magic ((s lsr 3) land 1)
+
+let kind (s : node_summary ) : Tree.NodeKind.t =
+  Obj.magic (s lsr 4)
+
+let node_summary 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)
+
+
+
+type config = {
+  sat : StateSet.t;
+  unsat : StateSet.t;
+  todo : TransList.t;
+  summary : node_summary;
+}
+
+module Config = Hcons.Make(struct
+  type t = config
+  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.TransList.id :> int),
+             c.summary)
+end
+)
+

 type t = {
   id : Uid.t;
   mutable states : StateSet.t;
   mutable selection_states: StateSet.t;
   transitions: (State.t, (QNameSet.t*SFormula.t) list) Hashtbl.t;
   mutable cache2 : TransList.t Cache.N2.t;
 type t = {
   id : Uid.t;
   mutable states : StateSet.t;
   mutable selection_states: StateSet.t;
   transitions: (State.t, (QNameSet.t*SFormula.t) list) Hashtbl.t;
   mutable cache2 : TransList.t Cache.N2.t;

-  mutable cache6 : (TransList.t*StateSet.t) Cache.N6.t;
+  mutable cache4 : Config.t Cache.N4.t;

 }
 
 let next = Uid.make_maker ()
 }
 
 let next = Uid.make_maker ()


@@ -174,7 +233,13 @@ let dummy2 = TransList.cons
   (Transition.make (State.dummy,QNameSet.empty, SFormula.false_))
   TransList.nil
 
   (Transition.make (State.dummy,QNameSet.empty, SFormula.false_))
   TransList.nil
 

-let dummy6 = (dummy2, StateSet.empty)
+
+
+let dummy_config = Config.make { sat = StateSet.empty;
+                                 unsat = StateSet.empty;
+                                 todo = TransList.nil;
+                                 summary = dummy_summary
+                               }

 
 
 let create s ss =
 
 
 let create s ss =


@@ -183,27 +248,27 @@ let create s ss =
                selection_states = ss;
                transitions = Hashtbl.create 17;
                cache2 = Cache.N2.create dummy2;
                selection_states = ss;
                transitions = Hashtbl.create 17;
                cache2 = Cache.N2.create dummy2;

-               cache6 = Cache.N6.create dummy6;
+               cache4 = Cache.N4.create dummy_config;

              }
   in
   at_exit (fun () ->
              }
   in
   at_exit (fun () ->

-    let n6 = ref 0 in
+    let n4 = ref 0 in

     let n2 = ref 0 in
     Cache.N2.iteri (fun _ _ _ b -> if b then incr n2) auto.cache2;
     let n2 = ref 0 in
     Cache.N2.iteri (fun _ _ _ b -> if b then incr n2) auto.cache2;

-    Cache.N6.iteri (fun _ _ _ _ _ _ _ b -> if b then incr n6) auto.cache6;
+    Cache.N4.iteri (fun _ _ _ _ _ b -> if b then incr n4) auto.cache4;

     Format.eprintf "INFO: automaton %i, cache2: %i entries, cache6: %i entries\n%!"
     Format.eprintf "INFO: automaton %i, cache2: %i entries, cache6: %i entries\n%!"

-      (auto.id :> int) !n2 !n6;
+      (auto.id :> int) !n2 !n4;

     let c2l, c2u = Cache.N2.stats auto.cache2 in
     let c2l, c2u = Cache.N2.stats auto.cache2 in

-    let c6l, c6u = Cache.N6.stats auto.cache6 in
+    let c4l, c4u = Cache.N4.stats auto.cache4 in

     Format.eprintf "INFO: cache2: length: %i, used: %i, occupation: %f\n%!" c2l c2u (float c2u /. float c2l);
     Format.eprintf "INFO: cache2: length: %i, used: %i, occupation: %f\n%!" c2l c2u (float c2u /. float c2l);

-    Format.eprintf "INFO: cache6: length: %i, used: %i, occupation: %f\n%!" c6l c6u (float c6u /. float c6l)
+    Format.eprintf "INFO: cache4: length: %i, used: %i, occupation: %f\n%!" c4l c4u (float c4u /. float c4l)

 
   );
   auto
 
 let reset a =
 
   );
   auto
 
 let reset a =

-  a.cache2 <- Cache.N2.create dummy2;
-  a.cache6 <- Cache.N6.create dummy6
+  a.cache2 <- Cache.N2.create (Cache.N2.dummy a.cache2);
+  a.cache4 <- Cache.N4.create (Cache.N4.dummy a.cache4)

 
 
 let get_trans_aux a tag states =
 
 
 let get_trans_aux a tag states =


@@ -230,7 +295,7 @@ let get_trans a tag states =
   else 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
 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


@@ -290,7 +355,7 @@ let eval_trans auto ltrs fcs nss ps ss is_left is_right has_left has_right kind
               else if SFormula.is_false new_phi then
                 (acct, accs)
               else
               else if SFormula.is_false new_phi then
                 (acct, accs)
               else

-                let new_tr = Transition.make (q, lab, new_phi) in
+                 let new_tr = Transition.make (q, lab, new_phi) in

                 (TransList.cons new_tr acct, accs)
           ) ltrs (TransList.nil, ss)
         in
                 (TransList.cons new_tr acct, accs)
           ) ltrs (TransList.nil, ss)
         in


@@ -303,64 +368,8 @@ let eval_trans auto ltrs fcs nss ps ss is_left is_right has_left has_right kind
   in
   loop ltrs ss
 
   in
   loop ltrs ss
 

-type node_summary = int
-let dummy_summary = -1
-(*
-4444444444443210
-4 -> kind
-3 -> is_left
-2 -> is_right
-1 -> has_left
-0 -> has_right

 *)
 
 *)
 

-let has_right (s : node_summary) : bool =
-  Obj.magic (s land 1)
-let has_left (s : node_summary) : bool =
-  Obj.magic ((s lsr 1) land 1)
-
-let is_right (s : node_summary) : bool =
-  Obj.magic ((s lsr 2) land 1)
-
-let is_left (s : node_summary) : bool =
-  Obj.magic ((s lsr 3) land 1)
-
-let kind (s : node_summary ) : Tree.NodeKind.t =
-  Obj.magic (s lsr 4)
-
-let node_summary 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)
-
-
-
-type config = {
-  sat : StateSet.t;
-  unsat : StateSet.t;
-  todo : TransList.t;
-  summary : node_summary;
-}
-
-module Config = Hcons.Make(struct
-  type t = config
-  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.TransList.id :> int),
-             c.summary)
-end
-)
-

 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_
 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_


@@ -369,7 +378,7 @@ let simplify_atom atom pos q { Config.node=config; _ } =
   else atom
 
 
   else atom
 
 

-let eval_form2 phi fcs nss ps ss summary =
+let eval_form phi fcs nss ps ss summary =

   let rec loop phi =
     begin match SFormula.expr phi with
       Formula.True | Formula.False -> phi
   let rec loop phi =
     begin match SFormula.expr phi with
       Formula.True | Formula.False -> phi


@@ -395,38 +404,48 @@ let eval_form2 phi fcs nss ps ss summary =
 
 
 let eval_trans auto fcs nss ps ss =
 
 
 let eval_trans auto fcs nss ps ss =

+  let fcsid = (fcs.Config.id :> int) in
+  let nssid = (nss.Config.id :> int) in
+  let psid = (ps.Config.id :> int) in

   let rec loop old_config =
   let rec loop old_config =

-    let { sat = old_sat;
-          unsat = old_unsat;
-          todo = old_todo;
-          summary = old_summary } = old_config.Config.node
-    in
-    let sat, unsat, removed, kept, todo =
-      TransList.fold
-        (fun trs acc ->
-          let q, lab, phi = 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_form2  phi fcs nss ps old_config old_summary
-            in
-            if SFormula.is_true new_phi then
-              StateSet.add q a_sat, a_unsat, StateSet.add q a_rem, a_kept, a_todo
-            else if SFormula.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 = Transition.make (q, lab, new_phi) in
-              (a_sat, a_unsat, a_rem, StateSet.add q a_kept, (TransList.cons new_tr a_todo))
-        ) old_todo (old_sat, old_unsat, StateSet.empty, StateSet.empty, TransList.nil)
+    let oid = (old_config.Config.id :> int) in
+    let res =
+      let res = Cache.N4.find auto.cache4 oid fcsid nssid psid in
+      if res != dummy_config then res
+      else
+        let { sat = old_sat;
+              unsat = old_unsat;
+              todo = old_todo;
+              summary = old_summary } = old_config.Config.node
+        in
+        let sat, unsat, removed, kept, todo =
+          TransList.fold
+            (fun trs acc ->
+              let q, lab, phi = 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 SFormula.is_true new_phi then
+                  StateSet.add q a_sat, a_unsat, StateSet.add q a_rem, a_kept, a_todo
+                else if SFormula.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 = Transition.make (q, lab, new_phi) in
+                  (a_sat, a_unsat, a_rem, StateSet.add q a_kept, (TransList.cons new_tr a_todo))
+            ) old_todo (old_sat, old_unsat, StateSet.empty, StateSet.empty, TransList.nil)
+        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 = Config.make { sat; unsat; todo ; summary = old_summary } in
+        Cache.N4.add auto.cache4 oid fcsid nssid psid new_config;
+        new_config

     in
     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 = Config.make { sat; unsat; todo ; summary = old_summary } in
-    if sat == old_sat && unsat == old_unsat && todo == old_todo then new_config
-    else loop new_config
+    if res == old_config then res else loop res

   in
   loop ss
 
   in
   loop ss
 

diff --git a/src/ata.mli b/src/ata.mli
index e2bf7e3..fd75e2e 100644 (file)
--- a/src/ata.mli
+++ b/src/ata.mli
@@ -14,7 +14,7 @@
 (***********************************************************************)
 
 (*
 (***********************************************************************)
 
 (*

-  Time-stamp: <Last modified on 2013-04-22 14:46:24 CEST by Kim Nguyen>
+  Time-stamp: <Last modified on 2013-04-22 15:08:54 CEST by Kim Nguyen>

 *)
 
 type predicate =
 *)
 
 type predicate =


@@ -66,13 +66,26 @@ module TransList : sig
 end
 
 
 end
 
 

+type node_summary = private int
+val node_summary : bool -> bool -> bool -> bool -> Tree.NodeKind.t -> node_summary
+val dummy_summary : node_summary
+type config = {
+  sat : StateSet.t;
+  unsat : StateSet.t;
+  todo : TransList.t;
+  summary : node_summary;
+}
+
+module Config : Hcons.S with type data = config
+
+

 type t = private {
   id : Uid.t;
   mutable states : StateSet.t;
   mutable selection_states: StateSet.t;
   transitions: (State.t, (QNameSet.t*SFormula.t) list) Hashtbl.t;
   mutable cache2 : TransList.t Cache.N2.t;
 type t = private {
   id : Uid.t;
   mutable states : StateSet.t;
   mutable selection_states: StateSet.t;
   transitions: (State.t, (QNameSet.t*SFormula.t) list) Hashtbl.t;
   mutable cache2 : TransList.t Cache.N2.t;

-  mutable cache6 : (TransList.t*StateSet.t) Cache.N6.t;
+  mutable cache4 : Config.t Cache.N4.t;

 }
 
 
 }
 
 


@@ -81,17 +94,6 @@ val create : StateSet.t -> StateSet.t -> t
 val reset : t -> unit
 val get_trans : t -> QNameSet.elt -> StateSet.t -> TransList.t
 
 val reset : t -> unit
 val get_trans : t -> QNameSet.elt -> StateSet.t -> TransList.t
 

-type node_summary = private int
-val node_summary : bool -> bool -> bool -> bool -> Tree.NodeKind.t -> node_summary
-val dummy_summary : node_summary
-type config = {
-  sat : StateSet.t;
-  unsat : StateSet.t;
-  todo : TransList.t;
-  summary : node_summary;
-}
-
-module Config : Hcons.S with type data = config

 
 val eval_trans : t -> Config.t -> Config.t -> Config.t -> Config.t -> Config.t
 
 
 val eval_trans : t -> Config.t -> Config.t -> Config.t -> Config.t -> Config.t
 

diff --git a/src/eval.ml b/src/eval.ml
index b48d129..e8e1d5a 100644 (file)
--- a/src/eval.ml
+++ b/src/eval.ml
@@ -14,7 +14,7 @@
 (***********************************************************************)
 
 (*
 (***********************************************************************)
 
 (*

-  Time-stamp: <Last modified on 2013-04-22 14:47:46 CEST by Kim Nguyen>
+  Time-stamp: <Last modified on 2013-04-22 15:31:24 CEST by Kim Nguyen>

 *)
 
 INCLUDE "utils.ml"
 *)
 
 INCLUDE "utils.ml"


@@ -134,6 +134,7 @@ END
     Ata.reset auto;
     while !redo do
       redo := false;
     Ata.reset auto;
     while !redo do
       redo := false;

+      Ata.reset auto;

       redo := top_down_run auto tree node cache !iter;
       incr iter;
     done;
       redo := top_down_run auto tree node cache !iter;
       incr iter;
     done;