X-Git-Url: http://git.nguyen.vg/gitweb/?p=tatoo.git;a=blobdiff_plain;f=src%2Frun.ml;fp=src%2Frun.ml;h=291faa49d530d17c1a5488c0ce9ca68d0c07eebc;hp=1824aebec8d311591cc88fe8a6c15f6908dfe900;hb=129708eaa5983b9463f96b714c00468602339b0a;hpb=c2c22bf0d75a390c2538b9fce44aae63c542119a

diff --git a/src/run.ml b/src/run.ml
index 1824aeb..291faa4 100644
--- a/src/run.ml
+++ b/src/run.ml
@@ -80,12 +80,28 @@ module Make (T : Tree.S) =
 
    let dummy_set = StateSet.singleton State.dummy
    open Bigarray
+
+IFDEF HTMLTRACE
+THEN
+   type sat_array = StateSet.t array list
+   DEFINE IFHTML(a,b) = (a)
+ELSE
+   type sat_array = StateSet.t array
+   DEFINE IFHTML(a,b) = (b)
+END
+   let unsafe_get a i =
+     if i < 0 then StateSet.empty else
+       Array.unsafe_get (IFHTML(List.hd a, a)) i
+   let unsafe_set a i v old_v =
+     if v != old_v then
+       Array.unsafe_set (IFHTML(List.hd a, a)) i v
+
    type run = {
      tree : T.t ;
      (* The argument of the run *)
      auto : Ata.t;
      (* The automaton to be run *)
-     sat: StateSet.t array;
+     mutable sat: sat_array;
      (* A mapping from node preorders to states satisfied at that node *)
      mutable pass : int;
      (* Number of run we have performed *)
@@ -107,7 +123,8 @@ module Make (T : Tree.S) =
      {
        tree = tree;
        auto = auto;
-       sat = Array.create len StateSet.empty;
+       sat = (let a = Array.create len StateSet.empty in
+             IFHTML([a], a));
        pass = 0;
        fetch_trans_cache = Cache.N2.create dummy_form;
        td_cache = Cache.N6.create dummy_set;
@@ -201,7 +218,6 @@ module Make (T : Tree.S) =
           new_sat
 
 
-   let unsafe_get a i = if i < 0 then StateSet.empty else Array.unsafe_get a i
 
    let top_down run =
     let i = run.pass in
@@ -214,7 +230,9 @@ module Make (T : Tree.S) =
         states_by_rank.(i+1)
     in
     let rec loop_td_and_bu node parent parent_sat =
-      if node == T.nil then StateSet.empty else begin
+      if node == T.nil
+      then StateSet.empty
+      else begin
         let node_id = T.preorder tree node in
         let fc = T.first_child tree node in
         let ns = T.next_sibling tree node in
@@ -243,19 +261,20 @@ module Make (T : Tree.S) =
             parent_sat
             status0 td_todo summary
         in
-        (* update the cache if the status of the node changed *)
-        if status1 != status0 then run.sat.(node_id) <- status1;
+        (* update the cache if the status of the node changed
+        unsafe_set run.sat node_id status1 status0;*)
         let fcs1 = loop_td_and_bu fc node status1 in
-        if bu_todo == StateSet.empty then
+        if bu_todo == StateSet.empty then begin
+          unsafe_set run.sat node_id status1 status0; (* write the td_states *)
           loop_td_and_bu ns node status1 (* tail call *)
-        else
+        end else
           let nss1 = loop_td_and_bu ns node status1 in
           let status2 =
             eval_trans auto run.fetch_trans_cache run.bu_cache tag fcs1 nss1
               parent_sat
               status1 bu_todo summary
           in
-          if status2 != status1 then run.sat.(node_id) <- status2;
+          unsafe_set run.sat node_id status2 status0;
           status2
       end
     in
@@ -264,7 +283,7 @@ module Make (T : Tree.S) =
 
 
   let get_results run =
-    let cache = run.sat in
+    let cache = IFHTML((List.hd run.sat), run.sat) in
     let auto = run.auto in
     let tree = run.tree in
     let sel_states = Ata.get_selecting_states auto in
@@ -283,7 +302,7 @@ module Make (T : Tree.S) =
 
 
   let get_full_results run =
-    let cache = run.sat(*tatus*) in
+    let cache = IFHTML((List.hd run.sat), run.sat) in
     let auto = run.auto in
     let tree = run.tree in
     let res_mapper = Hashtbl.create MED_H_SIZE in
@@ -320,10 +339,11 @@ module Make (T : Tree.S) =
   let prepare_run run list =
     let tree = run.tree in
     let auto = run.auto in
+    let sat = IFHTML((List.hd run.sat), run.sat) in
     let sat0 = Ata.get_starting_states auto in
     List.iter (fun node ->
       let node_id = T.preorder tree node in
-      run.sat.(node_id) <- sat0) list
+      sat.(node_id) <- sat0) list
 
   let tree_size = ref 0
   let pass = ref 0
@@ -335,11 +355,12 @@ module Make (T : Tree.S) =
     let rank = Ata.get_max_rank auto in
     while run.pass <= rank do
       top_down run;
+      IFHTML((run.sat <- (Array.copy (List.hd run.sat)) :: run.sat), ());
       run.td_cache <- Cache.N6.create dummy_set;
       run.bu_cache <- Cache.N6.create dummy_set;
     done;
     pass := Ata.get_max_rank auto + 1;
-
+    IFHTML(Html.gen_trace auto run.sat (module T : Tree.S with type t = T.t) tree ,());
     run
 
   let full_eval auto tree nodes =