Second fixpoint of TP_Max is now hconsed.

diff --git a/src/run.ml b/src/run.ml
index b5dbc84..1dfb6a8 100644 (file)
--- a/src/run.ml
+++ b/src/run.ml
@@ -122,7 +122,7 @@ let rec bu_oracle asta run tree tnode hashOracle=
     end
 
 (* Build the over-approx. of the maximal run *)
-let rec bu_over_max asta run tree tnode hashRun =
+let rec bu_over_max asta run tree tnode hashOver =
   if (Tree.is_leaf tree tnode)      (* BU_oracle has already created the map *)
   then
     ()
@@ -130,8 +130,8 @@ let rec bu_over_max asta run tree tnode hashRun =
     let tfnode = Tree.first_child_x tree tnode
     and tnnode = Tree.next_sibling tree tnode in
     begin
-      bu_over_max asta run tree tfnode hashRun;
-      bu_over_max asta run tree tnnode hashRun;
+      bu_over_max asta run tree tfnode hashOver;
+      bu_over_max asta run tree tnnode hashOver;
       let (fnode,nnode) =
         (Tree.preorder tree tfnode, Tree.preorder tree tnnode)
       and node = Tree.preorder tree tnode in          
@@ -152,9 +152,9 @@ let rec bu_over_max asta run tree tnode hashRun =
           then result (StateSet.add q set) qf qn 1 list_tr tl
           else result set qf qn 0 list_tr tl in
       let result_set () =
-        try HashRun.find hashRun ((StateSet.empty,resultr),qf,qn,list_tr,lab)
+        try HashRun.find hashOver ((StateSet.empty,resultr),qf,qn,list_tr,lab)
         with _ -> let res = result StateSet.empty qf qn 0 list_tr list_tr in
-                  HashRun.add hashRun
+                  HashRun.add hashOver
                     ((StateSet.empty,resultr), qf,qn,list_tr,lab) res;
                   res in
       (* we keep the old recognizing states set *)
@@ -163,7 +163,7 @@ let rec bu_over_max asta run tree tnode hashRun =
 
 
 (* Build the maximal run *)
-let rec tp_max asta run tree tnode hashRun =
+let rec tp_max asta run tree tnode hashMax =
   if (Tree.is_leaf tree tnode)      (* BU_oracle has already created the map *)
   then
     ()
@@ -212,7 +212,7 @@ let rec tp_max asta run tree tnode hashRun =
           end
           else result_st_q self_q queue flag tl in
       let rec comp_acc_self self_q_i queue = (* compute the fixed point *)
-        if Queue.is_empty queue
+        if Queue.is_empty queue              (* todo: to be hconsigned? *)
         then self_q_i
         else
           let q = Queue.pop queue in
@@ -224,15 +224,19 @@ let rec tp_max asta run tree tnode hashRun =
       let self,queue_init = result_q self_q (Queue.create()) list_tr in
       let self_q = comp_acc_self self_q queue_init in
       NodeHash.replace run node (self_q,self_r);
-      (* From now, the correct set of states is mapped to node! *)
-      let rec result = function
+      (* From now, the correct set of states is mapped to (self) node! *)
+      let rec result self qf qn = function
         | [] -> []
         | (q,form) :: tl ->
-          if (StateSet.mem q self) &&  (* infers & trans. can start here *)
-            (Formula.infer_form (self_q,self_r) qf qn form)
-          then form :: (result tl)
-          else result tl in      
-      let list_form = result list_tr in (* tran. candidates *)
+          if (StateSet.mem q (fst self)) && (* infers & trans. can start here *)
+            (Formula.infer_form self qf qn form)
+          then form :: (result self qf qn tl)
+          else result self qf qn tl in      
+      let list_form =
+        try HashRun.find hashMax ((self_q,self_r),qf,qn,list_tr,lab) 
+        with _ -> let res = result (self_q,self_r) qf qn list_tr in
+                  HashRun.add hashMax ((self_q,self_r),qf,qn,list_tr,lab) res;
+                  res in
       (* compute states occuring in transition candidates *)
       let rec add_st (ql,qr) = function
         | [] -> ql,qr
@@ -253,8 +257,8 @@ let rec tp_max asta run tree tnode hashRun =
         then ()
         else NodeHash.replace run nnode (StateSet.inter qnq qr,qnr);
         (* indeed we delete all states from self transitions!  *)
-        tp_max asta run tree tfnode hashRun;
-        tp_max asta run tree tnnode hashRun;
+        tp_max asta run tree tfnode hashMax;
+        tp_max asta run tree tnnode hashMax;
       end;
     end
         
@@ -268,13 +272,15 @@ let compute tree asta =
   bu_oracle asta map tree (Tree.root tree) hashOracle;
   HashOracle.clear hashOracle;
   if flag > 0 then begin
-    let hashRun = HashRun.create(size_hcons_M) in
-    bu_over_max asta map tree (Tree.root tree) hashRun;
+    let hashOver = HashRun.create(size_hcons_M) in
+    let hashMax = HashRun.create(size_hcons_M) in
+    bu_over_max asta map tree (Tree.root tree) hashOver;
     if flag = 2
     then
-      tp_max asta map tree (Tree.root tree) hashRun
+      tp_max asta map tree (Tree.root tree) hashMax
     else ();
-    HashRun.clear hashRun;
+    HashRun.clear hashOver;
+    HashRun.clear hashMax;
   end
   else ();
   map