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 (file)
--- a/src/ata.ml
+++ b/src/ata.ml
@@ -227,7 +227,14 @@ let get_trans a tag states =
   ) states TransList.nil
 
 
   ) 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
 
 (*
   [complete transitions a] ensures that for each state q

diff --git a/src/ata.mli b/src/ata.mli
index eada8d0..aa28abf 100644 (file)
--- 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
 (** 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.
  *)
 
     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 *)
 
 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 (file)
--- a/src/run.ml
+++ b/src/run.ml
@@ -60,34 +60,40 @@ module Make (T : Tree.S) =
    end
 
    type node_status = {
    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 *)
 
    }
 (* 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;
 
    let dummy_status =
      NodeStatus.make { sat = StateSet.empty;

-                       unsat = StateSet.empty;
-                       todo = Ata.TransList.nil;
+                       todo = StateSet.empty;

                        summary = NodeSummary.dummy;
                      }
 
                        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 *)
      (* 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 *)
      (* 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
    }
 
    let pass r = r.pass


@@ -116,11 +122,7 @@ module Make (T : Tree.S) =
    let tree r = r.tree
 
 
    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
 
    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;
        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 =
      }
 
    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
    let html tree node i config msg =
      let config = config.NodeStatus.node in
      Html.trace (T.preorder tree node) i

-       "node: %i<br/>%s<br/>sat: %a<br/>unsat: %a<br/>todo: %around: %i<br/>"
+       "node: %i<br/>%s<br/>sat: %a<br/>todo: %a<br/>round: %i<br/>"

        (T.preorder tree node)
        msg
        StateSet.print config.sat
        (T.preorder tree node)
        msg
        StateSet.print config.sat

-       StateSet.print config.unsat
-       (Ata.TransList.print ~sep:"<br/>") config.todo i
+       StateSet.print config.todo
+       i

 
 
    let debug msg tree node i config =
      let config = config.NodeStatus.node in
      eprintf
 
 
    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
        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
      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
 
 
    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) ->
            | 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
                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
 
 
            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;
      let { sat = old_sat;

-           unsat = old_unsat;

            todo = old_todo;
            todo = old_todo;

-           summary = old_summary } = old_config.NodeStatus.node
+           summary = old_summary } as os_node = old_status.NodeStatus.node

      in
      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
      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 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 =

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

-       if res == old_config then res else loop res
+       if res == old_status then res else loop res

      in
      loop ss
 
      in
      loop ss
 


@@ -283,7 +301,7 @@ END
     let auto = run.auto in
     let status = run.status in
     let cache2 = run.cache2 in
     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
     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 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;
             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 *)
                 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
               }
           else c
         in

-

         TRACE(html tree node _i config0 "Entering node");
 
         (* get the node_statuses for the first child, next sibling and parent *)
         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 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 *)
         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 *)
            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
 
         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)");
 
 
         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
              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
         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 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
     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;
       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 *)
             summary = NodeSummary.make
               (node == T.first_child tree parent) (* is_left *)
               (node == T.next_sibling tree parent) (* is_right *)