Rewrite the HTML debugging output to generate an svg file directly instead going

[tatoo.git] / src / run.ml

diff --git a/src/run.ml b/src/run.ml
index 53cecb4..d7f4ba7 100644 (file)
--- a/src/run.ml
+++ b/src/run.ml
@@ -153,12 +153,11 @@ END
    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/>todo: %a<br/>round: %i<br/>"
+       "node: %i<br/>%s<br/>sat: %a<br/>todo: %a<br/>_______________________<br/>"
        (T.preorder tree node)
        msg
        StateSet.print config.sat
        StateSet.print config.todo
-       i
 
 
    let debug msg tree node i config =
@@ -293,6 +292,7 @@ DEFINE AND_(t1,t2) =
 
 
   let top_down run =
+    let _i = run.pass in
     let tree = run.tree in
     let auto = run.auto in
     let status = run.status in
@@ -327,7 +327,7 @@ DEFINE AND_(t1,t2) =
               }
           else c
         in
-        TRACE(html tree node _i config0 "Entering node");
+        TRACE(html tree node _i status0 "Entering node");
 
         (* get the node_statuses for the first child, next sibling and parent *)
         let ps = unsafe_get_status status (T.preorder tree parent) in
@@ -335,7 +335,7 @@ DEFINE AND_(t1,t2) =
         let nss = unsafe_get_status status ns_id in
         (* evaluate the transitions with all this statuses *)
         let status1 = eval_trans auto cache2 cache5 tag fcs nss ps status0 in
-        TRACE(html tree node _i config1 "Updating transitions");
+        TRACE(html tree node _i status1 "Updating transitions");
 
         (* update the cache if the status of the node changed *)
 
@@ -348,14 +348,14 @@ DEFINE AND_(t1,t2) =
         (* update the status *)
         let status2 = eval_trans auto cache2 cache5 tag fcs1 nss ps status1 in
 
-        TRACE(html tree node _i config2 "Updating transitions (after first-child)");
+        TRACE(html tree node _i status2 "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 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 status3 "Updating transitions (after next-sibling)");
 
         if status3 != status2 then status.(node_id) <- status3;
 
@@ -371,50 +371,13 @@ DEFINE AND_(t1,t2) =
             Html.finalize_node
               node_id
               _i
-              Ata.(StateSet.intersect config3.Config.node.sat auto.selection_states)));
+              Ata.(StateSet.intersect status3.NodeStatus.node.sat (get_selecting_states auto))));
         unstable_self
       end
     in
     run.redo <- loop (T.root tree);
     run.pass <- run.pass + 1
 
-(*
-  let stats run =
-    let count = ref 0 in
-    let len = Bitvector.length run.unstable in
-    for i = 0 to len - 1 do
-      if not (Bitvector.unsafe_get run.unstable i) then
-        incr count
-    done;
-    Logger.msg `STATS
-      "%i nodes over %i were skipped in iteration %i (%.2f %%), redo is: %b"
-      !count len run.pass (100. *. (float !count /. float len))
-      run.redo
-
-
-  let eval auto tree node =
-    let len = T.size tree in
-    let run = { config = Array.create len Ata.dummy_config;
-                unstable = Bitvector.create ~init:true len;
-                redo = true;
-                pass = 0
-              }
-    in
-    while run.redo do
-      run.redo <- false;
-      Ata.reset auto; (* prevents the .cache2 and .cache4 memoization tables from growing too much *)
-      run.redo <- top_down_run auto tree node run;
-      stats run;
-      run.pass <- run.pass + 1;
-    done;
-    at_exit (fun () -> Logger.msg `STATS "%i iterations" run.pass);
-    at_exit (fun () -> stats run);
-    let r = get_results auto tree node run.config in
-
-    TRACE(Html.gen_trace (module T : Tree.S with type t = T.t) (tree));
-
-    r
-*)
 
   let get_results run =
     let cache = run.status in
@@ -469,6 +432,7 @@ DEFINE AND_(t1,t2) =
        (fun q acc -> (q, Cache.N1.find res_mapper (q :> int))::acc)
        (Ata.get_selecting_states auto) [])
 
+
   let prepare_run run list =
     let tree = run.tree in
     let auto = run.auto in
@@ -494,23 +458,21 @@ DEFINE AND_(t1,t2) =
       status.(node_id) <- status0) list
 
 
-  let eval full auto tree nodes =
+  let compute_run auto tree nodes =
     let run = make auto tree in
     prepare_run run nodes;
     while run.redo do
       top_down run
     done;
-    if full then `Full (get_full_results run)
-    else `Normal (get_results run)
+    TRACE(Html.gen_trace auto (module T : Tree.S with type t = T.t) tree);
+    run
 
   let full_eval auto tree nodes =
-    match eval true auto tree nodes with
-      `Full l -> l
-    | _ -> assert false
+    let r = compute_run auto tree nodes in
+    get_full_results r
 
   let eval auto tree nodes =
-    match eval false auto tree nodes with
-      `Normal l -> l
-    | _ -> assert false
+    let r = compute_run auto tree nodes in
+    get_results r
 
 end