Commentaries

diff --git a/src/compil.ml b/src/compil.ml
index 1ac98e2..574485e 100644 (file)
--- a/src/compil.ml
+++ b/src/compil.ml
@@ -30,12 +30,12 @@ let trans query =
     | [s] -> trans_last s
     | s :: tl ->  trans tl; trans_step s
     | [] -> ()
     | [s] -> trans_last s
     | s :: tl ->  trans tl; trans_step s
     | [] -> ()

-      
+ 

   (* Add THE top most state for top-level query (done in the end) *)
   and trans_init () =
     let top_st = Asta.new_state () in
     let or_top = 
   (* Add THE top most state for top-level query (done in the end) *)
   and trans_init () =
     let top_st = Asta.new_state () in
     let or_top = 

-      List.fold_left (fun acc x -> ((`Left *+ x) +| acc))
+ List.fold_left (fun acc x -> ((`Left *+ x) +| acc))

        (Formula.false_) (Asta.top_states asta)
     in
     Asta.add_quer asta top_st;
        (Formula.false_) (Asta.top_states asta)
     in
     Asta.add_quer asta top_st;


@@ -43,7 +43,7 @@ let trans query =
     Asta.add_top asta top_st;
     Asta.add_bot asta top_st;  (* for trees which are leaves *)
     Asta.add_tr asta (top_st, Asta.any_label, or_top) true
     Asta.add_top asta top_st;
     Asta.add_bot asta top_st;  (* for trees which are leaves *)
     Asta.add_tr asta (top_st, Asta.any_label, or_top) true

-      
+

   (* A selecting state is needed *)
   and trans_last (ax,test,pred) =
     let fo_p = trans_pr pred in
   (* A selecting state is needed *)
   and trans_last (ax,test,pred) =
     let fo_p = trans_pr pred in


@@ -59,7 +59,7 @@ let trans query =
     and tr_q = (q, Asta.any_label, form_propa_selec q q' ax) in
     Asta.add_tr asta tr_selec true;
     Asta.add_tr asta tr_q true
     and tr_q = (q, Asta.any_label, form_propa_selec q q' ax) in
     Asta.add_tr asta tr_selec true;
     Asta.add_tr asta tr_q true

-    
+ 

   (* Add a new state and its transitions for the step *)
   and trans_step (ax,test,pred) =
     let fo_p = trans_pr pred
   (* Add a new state and its transitions for the step *)
   and trans_step (ax,test,pred) =
     let fo_p = trans_pr pred


@@ -67,7 +67,7 @@ let trans query =
     let Simple label = test
     and form_next = (fo_p) *&                    (* (\/ top_next) /\ predicat *)
       (List.fold_left (fun acc x -> (`Left *+ x ) +| acc)
     let Simple label = test
     and form_next = (fo_p) *&                    (* (\/ top_next) /\ predicat *)
       (List.fold_left (fun acc x -> (`Left *+ x ) +| acc)

-        Formula.false_ (Asta.top_states asta)) in
+         Formula.false_ (Asta.top_states asta)) in

     let tr_next = (q, label, form_next)
     and tr_propa = (q, Asta.any_label, form_propa q ax) in
     Asta.add_quer asta q;
     let tr_next = (q, label, form_next)
     and tr_propa = (q, Asta.any_label, form_propa q ax) in
     Asta.add_quer asta q;


@@ -77,7 +77,7 @@ let trans query =
     Asta.add_tr asta tr_propa true;
     Asta.init_top asta;
     Asta.add_top asta q
     Asta.add_tr asta tr_propa true;
     Asta.init_top asta;
     Asta.add_top asta q

-      
+

   (* Translating of predicates. Either we apply De Morgan rules
      in xPath.parse or here *)
   and trans_pr  = function
   (* Translating of predicates. Either we apply De Morgan rules
      in xPath.parse or here *)
   and trans_pr  = function


@@ -88,7 +88,7 @@ let trans query =
     | Not (Expr Path q) -> (trans_pr_path false q)
     | Expr Path q -> (trans_pr_path true q)
     | x -> print_predicate pr_er x; raise Not_core_XPath
     | Not (Expr Path q) -> (trans_pr_path false q)
     | Expr Path q -> (trans_pr_path true q)
     | x -> print_predicate pr_er x; raise Not_core_XPath

-     
+

   (* Builds asta for predicate and gives the formula which must be satsified *)
   and trans_pr_path posi = function
     | Relative [] -> if posi then Formula.true_ else Formula.false_
   (* Builds asta for predicate and gives the formula which must be satsified *)
   and trans_pr_path posi = function
     | Relative [] -> if posi then Formula.true_ else Formula.false_


@@ -97,7 +97,7 @@ let trans query =
       Formula.false_ (trans_pr_step_l steps)
     | AbsoluteDoS steps as x -> print pr_er x; raise Not_core_XPath
     | Absolute steps as x -> print pr_er x; raise Not_core_XPath
       Formula.false_ (trans_pr_step_l steps)
     | AbsoluteDoS steps as x -> print pr_er x; raise Not_core_XPath
     | Absolute steps as x -> print pr_er x; raise Not_core_XPath

-      
+

   (* Builds asta for a predicate query and give the formula *)
   and trans_pr_step_l = function
     | [step] -> trans_pr_step [] step
   (* Builds asta for a predicate query and give the formula *)
   and trans_pr_step_l = function
     | [step] -> trans_pr_step [] step

diff --git a/src/formula.mli b/src/formula.mli
index 6c54386..69bdb78 100644 (file)
--- a/src/formula.mli
+++ b/src/formula.mli
@@ -53,7 +53,7 @@ val size : t -> int
 (** Syntactic size of the formula *)
 
 val eval_form : (StateSet.t * StateSet.t) -> t -> bool
 (** 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)] *)
+(** [eval_form (sf,sn) F] evaluates the formula [F] on [(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) -> t -> bool
 (** [eval_form S1 S2 F] infers S1; S2 |- F *)

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)
 
 (* 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 =
 
 (* 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 *)
   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;
       (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
         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 ->
       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
           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 ->
       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
           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)
       NodeHash.replace run node (result_set, resultr)

-    (* Never remove elt in Hash (the old one would appear) *)

     end
 
 
     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
     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
       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) &&
         | [] -> []
         | (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
           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
       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 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
   let map = NodeHash.create size_tree in
   bu_oracle asta map tree (Tree.root tree);
   if flag > 0 then begin