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

diff --git a/src/formula.ml b/src/formula.ml
index 8369571..2d9893c 100644 (file)
--- a/src/formula.ml
+++ b/src/formula.ml
@@ -15,7 +15,7 @@
 INCLUDE "utils.ml"
 
 open Format
-type move = [ `Left | `Right ]
+type move = [ `Left | `Right | `Self ]
 type 'hcons expr =
   | False | True
   | Or of 'hcons * 'hcons
@@ -73,30 +73,30 @@ let prio f =
     | Or _ -> 1
       
 (* Begin Lucca Hirschi *)
-let rec eval_form ss f = match expr f with
+let rec eval_form (q,qf,qn) f = match expr f with
   | False -> false
   | True -> true
-  | And(f1,f2) -> eval_form ss f1 && eval_form ss f2
-  | Or(f1,f2) -> eval_form ss f1 || eval_form ss f2
+  | And(f1,f2) -> eval_form (q,qf,qn) f1 && eval_form (q,qf,qn) f2
+  | Or(f1,f2) -> eval_form (q,qf,qn) f1 || eval_form (q,qf,qn) f2
   | Atom(dir, b, s) -> 
-    let set = match dir with |`Left -> fst ss | `Right -> snd ss in
+    let set = match dir with
+      |`Left -> qf | `Right -> qn | `Self -> q in
     if b then StateSet.mem s set
     else not (StateSet.mem s set)
 
-let rec infer_form ssq ssr f = match expr f with
+let rec infer_form sq sqf sqn f = match expr f with
   | False -> false
   | True -> true
-  | And(f1,f2) -> infer_form ssq ssr f1 && infer_form ssq ssr f2
-  | Or(f1,f2) -> infer_form ssq ssr f1 || infer_form ssq ssr f2
+  | And(f1,f2) -> infer_form sq sqf sqn f1 && infer_form sq sqf sqn f2
+  | Or(f1,f2) -> infer_form sq sqf sqn f1 || infer_form sq sqf sqn f2
   | Atom(dir, b, s) -> 
     let setq, setr = match dir with
-      |`Left -> fst ssq, fst ssr
-      | `Right -> snd ssq, snd ssr in
+      | `Left -> sqf | `Right -> sqn | `Self -> sq in
     (* WG: WE SUPPOSE THAT Q^r and Q^q are disjoint ! *)
     let mem =  StateSet.mem s setq || StateSet.mem s setr in
     if b then mem else not mem
 (* End *)
-
+      
 let rec print ?(parent=false) ppf f =
   if parent then fprintf ppf "(";
   let _ = match expr f with
@@ -117,6 +117,7 @@ let rec print ?(parent=false) ppf f =
           match  dir with
           | `Left ->  Pretty.down_arrow, Pretty.subscript 1
           | `Right -> Pretty.down_arrow, Pretty.subscript 2
+          | `Self -> Pretty.down_arrow, Pretty.subscript 0
         in
         fprintf fmt "%s%s" a_str d_str;
         State.print fmt s;
@@ -147,6 +148,7 @@ let atom_ d p s =
   let ss = match d with
     | `Left -> si, StateSet.empty
     | `Right -> StateSet.empty, si
+    | `Self -> si, StateSet.empty       (* TODO WHAT? *)
   in fst (cons (Atom(d,p,s)) (Atom(d,not p,s)) ss ss 1 1)
 
 let not_ f = f.Node.node.neg

diff --git a/src/formula.mli b/src/formula.mli
index 69bdb78..9ecf30a 100644 (file)
--- a/src/formula.mli
+++ b/src/formula.mli
@@ -15,7 +15,7 @@
 
 (** Implementation of hashconsed Boolean formulae *)
 
-type move = [ `Left |`Right ]
+type move = [ `Left |`Right | `Self ]
 (** Direction for automata predicates *)
 
 type 'hcons expr =
@@ -52,11 +52,11 @@ val compare : t -> t -> int
 val size : t -> int
 (** Syntactic size of the formula *)
 
-val eval_form : (StateSet.t * StateSet.t) -> t -> bool
-(** [eval_form (sf,sn) F] evaluates the formula [F] on [(sf,sn)] *)
+val eval_form : (StateSet.t * StateSet.t * StateSet.t) -> t -> bool
+(** [eval_form (s,sf,sn) F] evaluates the formula [F] on [(s,sf,sn)] *)
 
-val infer_form : (StateSet.t * StateSet.t) -> (StateSet.t * StateSet.t) -> t -> bool
-(** [eval_form S1 S2 F] infers S1; S2 |- F *)
+val infer_form : (StateSet.t * StateSet.t) -> (StateSet.t * StateSet.t) -> (StateSet.t * StateSet.t) -> t -> bool
+(** [eval_form S Sf Sn F] infers S; (S1,S2) |- F *)
 
 val print : Format.formatter -> t -> unit
 (** Pretty printer *)

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