Commentaries

[tatoo.git] / src / run.ml

diff --git a/src/run.ml b/src/run.ml
index 9ece6ee..482a749 100644 (file)
--- a/src/run.ml
+++ b/src/run.ml
@@ -33,7 +33,6 @@ exception Max_fail
 
 (* Mapped sets for leaves *)
 let map_leaf asta = (Asta.bot_states_s asta, StateSet.empty)
-let empty = (StateSet.empty,StateSet.empty)
 
 (* Build the Oracle *)
 let rec bu_oracle asta run tree tnode =
@@ -46,21 +45,21 @@ let rec bu_oracle asta run tree tnode =
   else
     let tfnode = Tree.first_child tree tnode (* first child *)
     and tnnode = Tree.next_sibling tree tnode in (* next-sibling *)
-    let fnode,nnode =
+    let fnode,nnode =                            (* their preorders *)
       (Tree.preorder tree tfnode, Tree.preorder tree tnnode) in
     begin
       bu_oracle asta run tree tfnode;
       bu_oracle asta run tree tnnode;
-      let q_rec n =
+      let q_rec n =                     (* compute the set for child/sibling *)
         try NodeHash.find run n
         with Not_found -> map_leaf asta in
       let (_,qfr),(_,qnr) = q_rec fnode,q_rec nnode (* computed in rec call *)
       and lab = Tree.tag tree tnode in
-      let _,list_tr = Asta.transitions_lab asta lab in (* only take reco. *)
+      let _,list_tr = Asta.transitions_lab asta lab in (* only reco. tran.*)
       let rec result set = function
         | [] -> set
         | (q,form) :: tl ->
-          if Formula.eval_form (qfr,qnr) form
+          if Formula.eval_form (qfr,qnr) form (* evaluates the formula *)
           then result (StateSet.add q set) tl
           else result set tl in
       let result_set = result StateSet.empty list_tr in
@@ -90,14 +89,14 @@ let rec bu_over_max asta run tree tnode =
       let rec result set = function
         | [] -> set
         | (q,form) :: tl ->
-          if Formula.infer_form (qfq,qnq) (qfr,qnr) form
+          if Formula.infer_form (qfq,qnq) (qfr,qnr) form (* infers the formula*)
           then result (StateSet.add q set) tl
           else result set tl in
       let _,resultr = try NodeHash.find run node
         with _ -> raise Over_max_fail in      
       let result_set = result StateSet.empty list_tr in
+      (* we keep the old recognizing states set *)
       NodeHash.replace run node (result_set, resultr)
-    (* Never remove elt in Hash (the old one would appear) *)
     end
 
 
@@ -113,7 +112,7 @@ let rec tp_max asta run tree tnode =
     let (fnode,nnode) =
       (Tree.preorder tree tfnode, Tree.preorder tree tnnode) in
     begin
-      if tnode == Tree.root tree        (* we must intersectt with top states *)
+      if tnode == Tree.root tree        (* we must intersect with top states *)
       then let setq,_  = try NodeHash.find run node
         with _ -> raise Max_fail in
            NodeHash.replace run node
@@ -131,10 +130,11 @@ let rec tp_max asta run tree tnode =
         | [] -> []
         | (q,form) :: tl ->
           if (Formula.infer_form (qfq,qnq) (qfr,qnr) form) &&
-            (StateSet.mem q set_node)
+            (StateSet.mem q set_node)   (* infers & trans. can start here *)
           then form :: (result tl)
           else result tl in
-      let list_form = result list_tr in
+      let list_form = result list_tr in (* tran. candidates *)
+      (* compute states occuring in transition candidates *)
       let rec add_st (ql,qr) = function
         | [] -> ql,qr
         | f :: tl -> let sql,sqr = Formula.st f in
@@ -160,7 +160,7 @@ let rec tp_max asta run tree tnode =
         
 let compute tree asta =
   let flag = 2 in                       (* debug  *)
-  let size_tree = 10000 in              (* todo *)
+  let size_tree = 10000 in              (* todo (Tree.size ?) *)
   let map = NodeHash.create size_tree in
   bu_oracle asta map tree (Tree.root tree);
   if flag > 0 then begin