Add `Self direction in Formula + compute fixed point in Run.

[tatoo.git] / src / run.ml

diff --git a/src/run.ml b/src/run.ml
index 482a749..2e0cf95 100644 (file)
--- a/src/run.ml
+++ b/src/run.ml
@@ -25,7 +25,7 @@ module NodeHash = Hashtbl.Make (Node)
   
 type t = (StateSet.t*StateSet.t) NodeHash.t
 (** Map from nodes to query and recognizing states *)
-(* Note that we do not consider the nil nodes *)
+(* Note that we do not consider nil nodes *)
 
 exception Oracle_fail
 exception Over_max_fail
@@ -56,16 +56,22 @@ let rec bu_oracle asta run tree tnode =
       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 reco. tran.*)
-      let rec result set = function
-        | [] -> set
+      let rec result set flag = function (* add states which satisfy a transition *)
+        | [] -> set,flag
         | (q,form) :: tl ->
-          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
-      NodeHash.add run node (StateSet.empty, result_set)
+          if Formula.eval_form (set,qfr,qnr) form (* evaluates the formula*)
+          then
+            if StateSet.mem q set
+            then result set 0 tl
+            else result (StateSet.add q set) 1 tl
+          else result set 0 tl in
+      let rec fix_point set_i =  (* compute the fixed point of states of node *)
+        let set,flag = result set_i 0 list_tr in
+        if flag = 0 then set
+        else fix_point set in
+      NodeHash.add run node (StateSet.empty, fix_point StateSet.empty)
     end
-
+      
 (* Build the over-approx. of the maximal run *)
 let rec bu_over_max asta run tree tnode =
   if (Tree.is_leaf tree tnode)      (* BU_oracle has already created the map *)
@@ -83,18 +89,25 @@ let rec bu_over_max asta run tree tnode =
       let q_rec n =
         try NodeHash.find run n
         with Not_found -> map_leaf asta in
-      let (qfq,qfr),(qnq,qnr) = q_rec fnode,q_rec nnode in
+      let qf,qn = q_rec fnode,q_rec nnode in
       let lab = Tree.tag tree tnode in
-      let list_tr,_ = Asta.transitions_lab asta lab in (* only take query st. *)
-      let rec result set = function
-        | [] -> set
-        | (q,form) :: tl ->
-          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
+      let list_tr,_ = Asta.transitions_lab asta lab (* only take query st. *)
+      and _,resultr = try NodeHash.find run node
         with _ -> raise Over_max_fail in      
-      let result_set = result StateSet.empty list_tr in
+      let rec result set flag = function
+        | [] -> set,flag
+        | (q,form) :: tl ->
+          if Formula.infer_form (set,resultr) qf qn form (* infers the formula*)
+          then if StateSet.mem q set
+            then result set 0 tl
+            else result (StateSet.add q set) 1 tl
+          else result set 0 tl in
+      let rec fix_point set_i = 
+        let set,flag = result set_i 0 list_tr in
+        if flag = 0
+        then set
+        else fix_point set in
+      let result_set = fix_point StateSet.empty in
       (* we keep the old recognizing states set *)
       NodeHash.replace run node (result_set, resultr)
     end
@@ -121,15 +134,17 @@ let rec tp_max asta run tree tnode =
       let q_rec n =
         try NodeHash.find run n
         with Not_found -> map_leaf asta in
-      let (qfq,qfr),(qnq,qnr) = q_rec fnode,q_rec nnode in
+      let qf,qn = q_rec fnode,q_rec nnode in
       let lab = Tree.tag tree tnode in
       let list_tr,_ = Asta.transitions_lab asta lab in (* only take query. *)
       let set_node,_ = try NodeHash.find run node
         with _ -> raise Max_fail in
+      let self = try NodeHash.find run node
+        with Not_found -> raise Max_fail in
       let rec result = function
         | [] -> []
         | (q,form) :: tl ->
-          if (Formula.infer_form (qfq,qnq) (qfr,qnr) form) &&
+          if (Formula.infer_form self qf qn form) &&
             (StateSet.mem q set_node)   (* infers & trans. can start here *)
           then form :: (result tl)
           else result tl in