From: Lucca Hirschi <lucca.hirschi@gmail.com>
Date: Tue, 17 Jul 2012 12:56:44 +0000 (+0200)
Subject: Merge branch 'lucca-tests-bench' into lucca-optim
X-Git-Tag: Core+Extentions+Optim-hconsed_V1
X-Git-Url: http://git.nguyen.vg/gitweb/?p=tatoo.git;a=commitdiff_plain;h=5e7268fb95cdc7e56fe24f324a710550ade3d851;hp=9e29715d08094dfad88ddb0316080ec383071536

Merge branch 'lucca-tests-bench' into lucca-optim
---

diff --git a/correct_test b/correct_test
index d28ee73..ec62b8a 100755
--- a/correct_test
+++ b/correct_test
@@ -1 +1 @@
-./solve.native ./tests/docs/XPath-FT.xml -f ./tests/queries/XPath-FT.queries
\ No newline at end of file
+./solve.native ./tests/docs/XPath-FT.xml -f ./tests/queries/XPath-FT.queries 1
\ No newline at end of file
diff --git a/run_tests b/run_tests
index 4a26469..6ee6c55 100755
--- a/run_tests
+++ b/run_tests
@@ -6,4 +6,5 @@ echo "__________________________________________________________________________
 echo "________________________________________________________________________________"
 ./test.native ./tests/docs/my.xml -f ./tests/queries/my.queries.old
 echo "Expected answer: 43 (the b from the second big sub-tree)."
-./test.native ./tests/docs/my.xml -f ./tests/queries/my.queries.old 2> tests/results/my.result
\ No newline at end of file
+./test.native ./tests/docs/my.xml -f ./tests/queries/my.queries.old 2> tests/results/my.result
+./test.native ./tests/docs/my.xml '/descendant::b/self::b'
\ No newline at end of file
diff --git a/src/asta.ml b/src/asta.ml
index d866005..f96cd42 100644
--- a/src/asta.ml
+++ b/src/asta.ml
@@ -39,6 +39,7 @@ struct
       State.print st
       (QNameSet.to_string la)
       Formula.print f
+
 end
 
 module  SetT = 
@@ -88,6 +89,14 @@ let transitions_lab asta lab =
     (remove_lab (SetT.elements (SetT.filter filter asta.trans_q)),
      (remove_lab (SetT.elements (SetT.filter filter asta.trans_r))))
 
+let transitions_st_lab asta q lab = 
+  let filter (s,l,f) = q = s && QNameSet.mem lab l in
+    let rec remove_st_lab = function
+      | [] -> []
+      | (s,l,f) :: tl -> f :: (remove_st_lab tl) in
+    (remove_st_lab (SetT.elements (SetT.filter filter asta.trans_q)),
+     (remove_st_lab (SetT.elements (SetT.filter filter asta.trans_r))))
+
 let empty = {
   quer = StateSet.empty;
   reco = StateSet.empty;
diff --git a/src/asta.mli b/src/asta.mli
index 7bbf13d..3fd9886 100644
--- a/src/asta.mli
+++ b/src/asta.mli
@@ -42,6 +42,10 @@ val transitions_lab : t -> QName.t -> (state*formula) list *(state*formula) list
 (** Give the list of states and formulae from queries and recognizing
     transitions for a given tag *)
 
+val transitions_st_lab : t -> state -> QName.t -> formula list * formula list
+(** Give the list of formulae from queries and recognizing transitions for a
+    given state and tag *)
+
 val empty : t
 (** The empty automaton *)
 
diff --git a/src/compil.ml b/src/compil.ml
index 574485e..b15b069 100644
--- a/src/compil.ml
+++ b/src/compil.ml
@@ -21,6 +21,8 @@ exception Not_core_XPath
 
 let pr_er = Format.err_formatter
 
+let ax_ (a,b,c) = a
+
 let trans query =
   (* Buidling of the ASTA step by step with a special case for the last
      step. Then add a top most state. Each function modifies asta. *)
@@ -28,16 +30,15 @@ let trans query =
   (* builds asta from the bottom of the query *)
   let rec trans = function
     | [s] -> trans_last s
-    | s :: tl ->  trans tl; trans_step s
+    | s :: tl -> trans tl; trans_step s (ax_(List.hd tl))
     | [] -> ()
  
   (* 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))
-	(Formula.false_) (Asta.top_states asta)
-    in
+      List.fold_left (fun acc x -> ((`Left *+ x) +| acc))
+	(Formula.false_) (Asta.top_states asta) in
     Asta.add_quer asta top_st;
     Asta.init_top asta;
     Asta.add_top asta top_st;
@@ -46,7 +47,7 @@ let trans query =
 
   (* A selecting state is needed *)
   and trans_last (ax,test,pred) =
-    let fo_p = trans_pr pred in
+    let fo_p = trans_pr pred in         (* TODO (if ax=Self, only q *)
     let q,q' = Asta.new_state(), Asta.new_state() in
     Asta.add_selec asta q';
     Asta.add_quer asta q;
@@ -60,14 +61,24 @@ let trans query =
     Asta.add_tr asta tr_selec true;
     Asta.add_tr asta tr_q true
  
+  and form_next_step ax_next top_states_next form_pred =
+    match ax_next with
+      | Self -> (form_pred) *&                (* (\/ top_next) /\ predicate *)
+        (List.fold_left (fun acc x -> (`Self *+ x ) +| acc)
+           Formula.false_ top_states_next)
+      | FollowingSibling -> (form_pred) *&    (* (\/ top_next) /\ predicate *)
+        (List.fold_left (fun acc x -> (`Right *+ x ) +| acc)
+           Formula.false_ top_states_next)
+      | _ -> (form_pred) *&                   (* (\/ top_next) /\ predicate *)
+        (List.fold_left (fun acc x -> (`Left *+ x ) +| acc)
+           Formula.false_ top_states_next)
+        
   (* Add a new state and its transitions for the step *)
-  and trans_step (ax,test,pred) =
+  and trans_step (ax,test,pred) ax_next =
     let fo_p = trans_pr pred
     and q = Asta.new_state() in
     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
+    and form_next = form_next_step ax_next (Asta.top_states asta) fo_p 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;
@@ -92,27 +103,30 @@ let trans query =
   (* 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_
-    | Relative steps -> List.fold_left
-      (fun acc x -> if posi then (`Left *+ x) +| acc else (`Left *- x) +| acc)
-      Formula.false_ (trans_pr_step_l steps)
+    | Relative steps ->
+      let dir = match ax_ (List.hd steps) with
+        | Self -> `Self
+        | FollowingSibling -> `Right
+        | _ -> `Left in
+      List.fold_left
+        (fun acc x -> if posi then (dir *+ x) +| acc else (dir *- x) +| acc)
+        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
+    | [step] -> trans_pr_step [] step (Self) (* Self doesn't matter since [] *)
     | step :: tl -> let list_top = trans_pr_step_l tl in
-		    trans_pr_step list_top step
+                    trans_pr_step list_top step (ax_ (List.hd tl))
     | [] -> failwith "Can not happened! 1"
 
   (* Add a step on the top of a list of states in a predicate *)
-  and trans_pr_step list (ax,test,pred) =
+  and trans_pr_step list (ax,test,pred) ax_next =
     let form_next =
       if list = []
       then trans_pr pred
-      else (trans_pr pred) *&
-	(List.fold_left (fun acc x -> (`Left *+ x) +| acc)
-	   Formula.false_ list)
+      else form_next_step ax_next list (trans_pr pred)
     and q = Asta.new_state() 
     and Simple label = test in
     let tr_next = (q,label, form_next)
@@ -126,12 +140,16 @@ let trans query =
   and form_propa q = function
     | Child -> `Right *+ q
     | Descendant -> (`Left *+ q +| `Right *+ q)
+    | Self -> `Self *+ q
+    | FollowingSibling -> `Right *+ q
     | x -> print_axis pr_er x; raise Not_core_XPath 
 
   (* The same with a selecting state *)
   and form_propa_selec q q' = function
     | Child -> `Right *+ q +| `Right *+ q'
     | Descendant -> (`Left *+ q +| `Right *+ q) +| (`Left *+ q' +| `Right *+ q')
+    | Self -> `Self *+ q'
+    | FollowingSibling -> `Right *+ q +| `Right *+ q'
     | x -> print_axis pr_er x; raise Not_core_XPath 
       
   in
diff --git a/src/formula.ml b/src/formula.ml
index 8369571..6c98118 100644
--- 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
@@ -25,7 +25,7 @@ type 'hcons expr =
 type 'hcons node = {
   pos : 'hcons expr;
   mutable neg : 'hcons;
-  st : StateSet.t * StateSet.t;
+  st : StateSet.t * StateSet.t * StateSet.t;
   size: int; (* Todo check if this is needed *)
 }
 
@@ -73,30 +73,83 @@ let prio f =
     | Or _ -> 1
       
 (* Begin Lucca Hirschi *)
-let rec eval_form ss 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
-  | Atom(dir, b, s) -> 
-    let set = match dir with |`Left -> fst ss | `Right -> snd ss 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
-  | 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
-  | Atom(dir, b, s) -> 
-    let setq, setr = match dir with
-      |`Left -> fst ssq, fst ssr
-      | `Right -> snd ssq, snd ssr in
+module type HcEval =
+sig
+  type t = StateSet.t*StateSet.t*StateSet.t*Node.t
+  val equal : t -> t -> bool
+  val hash : t -> int
+end
+  
+type dStateS = StateSet.t*StateSet.t
+module type HcInfer =
+sig
+  type t = dStateS*dStateS*dStateS*Node.t
+  val equal : t -> t -> bool
+  val hash : t -> int
+end
+    
+module HcEval : HcEval = struct
+  type t =
+      StateSet.t*StateSet.t*StateSet.t*Node.t
+  let equal (s,l,r,f) (s',l',r',f') = StateSet.equal s s' &&
+    StateSet.equal l l' && StateSet.equal r r' && Node.equal f f'
+  let hash (s,l,r,f) =
+    HASHINT4(StateSet.hash s, StateSet.hash l, StateSet.hash r, Node.hash f)
+end
+  
+let dequal (x,y) (x',y') = StateSet.equal x x' && StateSet.equal y y'
+let dhash (x,y) = HASHINT2(StateSet.hash x, StateSet.hash y)
+module HcInfer : HcInfer = struct
+  type t = dStateS*dStateS*dStateS*Node.t
+  let equal (s,l,r,f) (s',l',r',f') = dequal s s' &&
+    dequal l l' && dequal r r' && Node.equal f f'
+  let hash (s,l,r,f) =
+    HASHINT4(dhash s, dhash l, dhash r, Node.hash f)
+end
+
+module HashEval = Hashtbl.Make(HcEval)
+module HashInfer = Hashtbl.Make(HcInfer)
+type hcEval = bool Hashtbl.Make(HcEval).t
+type hcInfer = bool Hashtbl.Make(HcInfer).t
+
+let rec eval_form (q,qf,qn) f hashEval =
+try HashEval.find hashEval (q,qf,qn,f)
+with _ ->
+  let res = match expr f with
+    | False -> false
+    | True -> true 
+    | And(f1,f2) -> eval_form (q,qf,qn) f1 hashEval &&
+      eval_form (q,qf,qn) f2 hashEval
+    | Or(f1,f2) -> eval_form (q,qf,qn) f1 hashEval ||
+      eval_form (q,qf,qn) f2 hashEval
+    | Atom(dir, b, s) -> 
+      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) in
+  HashEval.add hashEval (q,qf,qn,f) res;
+  res
+
+let rec infer_form sq sqf sqn f hashInfer =
+try HashInfer.find hashInfer (sq,sqf,sqn,f)
+with _ ->
+  let res = match expr f with
+    | False -> false
+    | True -> true
+    | And(f1,f2) -> infer_form sq sqf sqn f1 hashInfer &&
+      infer_form sq sqf sqn f2 hashInfer
+    | Or(f1,f2) -> infer_form sq sqf sqn f1 hashInfer ||
+      infer_form sq sqf sqn f2 hashInfer
+    | Atom(dir, b, s) -> 
+      let setq, setr = match dir with
+        | `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
+      let mem =  StateSet.mem s setq || StateSet.mem s setr in
+      if b then mem else not mem in
+  HashInfer.add hashInfer (sq,sqf,sqn,f) res;
+  res   
 (* End *)
-
+      
 let rec print ?(parent=false) ppf f =
   if parent then fprintf ppf "(";
   let _ = match expr f with
@@ -117,6 +170,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;
@@ -140,26 +194,28 @@ let cons pos neg s1 s2 size1 size2 =
     pnode,nnode
 
 
-let empty_pair = StateSet.empty, StateSet.empty
-let true_,false_ = cons True False empty_pair empty_pair 0 0
+let empty_triple = StateSet.empty, StateSet.empty, StateSet.empty
+let true_,false_ = cons True False empty_triple empty_triple 0 0
 let atom_ d p s =
   let si = StateSet.singleton s in
   let ss = match d with
-    | `Left -> si, StateSet.empty
-    | `Right -> StateSet.empty, si
+    | `Left -> StateSet.empty, si, StateSet.empty
+    | `Right -> StateSet.empty, StateSet.empty, si
+    | `Self -> si, StateSet.empty, StateSet.empty
   in fst (cons (Atom(d,p,s)) (Atom(d,not p,s)) ss ss 1 1)
 
 let not_ f = f.Node.node.neg
 
-let union_pair (l1,r1) (l2, r2) =
+let union_triple (s1,l1,r1) (s2,l2, r2) =
+  StateSet.union s1 s2,
   StateSet.union l1 l2,
   StateSet.union r1 r2
 
 let merge_states f1 f2 =
   let sp =
-    union_pair (st f1) (st f2)
+    union_triple (st f1) (st f2)
   and sn =
-    union_pair (st (not_ f1)) (st (not_ f2))
+    union_triple (st (not_ f1)) (st (not_ f2))
   in
     sp,sn
 
diff --git a/src/formula.mli b/src/formula.mli
index 69bdb78..14e0f80 100644
--- 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 =
@@ -43,8 +43,8 @@ val equal : t -> t -> bool
 val expr : t -> t expr
 (** Equality over formulae *)
 
-val st : t -> StateSet.t * StateSet.t
-(** states occuring left and right, positively or negatively *)
+val st : t -> StateSet.t * StateSet.t * StateSet.t
+(** States occuring self, left and right, positively or negatively *)
 
 val compare : t -> t -> int
 (** Comparison of formulae *)
@@ -52,11 +52,25 @@ 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 infer_form : (StateSet.t * StateSet.t) -> (StateSet.t * StateSet.t) -> t -> bool
-(** [eval_form S1 S2 F] infers S1; S2 |- F *)
+module HcEval : sig
+  include Sigs.HashedType
+end
+module HcInfer : sig
+  include Sigs.HashedType
+end
+module HashEval : Hashtbl.S
+module HashInfer : Hashtbl.S
+type hcEval = bool HashEval.t
+type hcInfer = bool HashInfer.t
+(** Optimization: hconsigned eval and infer *)
+
+val eval_form : (StateSet.t * StateSet.t * StateSet.t) -> t -> hcEval -> 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) ->
+  (StateSet.t * StateSet.t) -> t -> hcInfer -> bool
+(** [eval_form S Sf Sn F] infers S; (S1,S2) |- F *)
 
 val print : Format.formatter -> t -> unit
 (** Pretty printer *)
diff --git a/src/hconsed_run.ml b/src/hconsed_run.ml
new file mode 100644
index 0000000..2214028
--- /dev/null
+++ b/src/hconsed_run.ml
@@ -0,0 +1,51 @@
+(***********************************************************************)
+(*                                                                     *)
+(*                   Lucca Hirschi, LRI UMR8623                        *)
+(*                   Université Paris-Sud & CNRS                       *)
+(*                                                                     *)
+(*  Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
+(*  Recherche Scientifique. All rights reserved.  This file is         *)
+(*  distributed under the terms of the GNU Lesser General Public       *)
+(*  License, with the special exception on linking described in file   *)
+(*  ../LICENSE.                                                        *)
+(*                                                                     *)
+(***********************************************************************)
+
+INCLUDE "utils.ml"
+
+
+(* Hash Consign modules *)
+
+module type Oracle_fixpoint =
+sig
+  type t = StateSet.t*StateSet.t*StateSet.t*((StateSet.elt*Formula.t) list)*QName.t
+  val equal : t -> t -> bool
+  val hash : t -> int
+end
+
+type dStateS = StateSet.t*StateSet.t
+module type Run_fixpoint =
+sig
+  type t = dStateS*dStateS*dStateS*(State.t*Formula.t) list*QName.t
+  val equal : t -> t -> bool
+  val hash : t -> int
+end
+    
+module Oracle_fixpoint : Oracle_fixpoint = struct
+  type t =
+      StateSet.t*StateSet.t*StateSet.t*((StateSet.elt*Formula.t) list)*QName.t
+  let equal (s,l,r,list,t) (s',l',r',list',t') = StateSet.equal s s' &&
+    StateSet.equal l l' && StateSet.equal r r' && QName.equal t t'
+  let hash (s,l,r,list,t) =
+    HASHINT4(StateSet.hash s, StateSet.hash l, StateSet.hash r, QName.hash t)
+end
+  
+let dequal (x,y) (x',y') = StateSet.equal x x' && StateSet.equal y y'
+let dhash (x,y) = HASHINT2(StateSet.hash x, StateSet.hash y)
+module Run_fixpoint : Run_fixpoint = struct
+  type t = dStateS*dStateS*dStateS*(State.t*Formula.t) list*QName.t
+  let equal (s,l,r,list,t) (s',l',r',list',t') = dequal s s' &&
+    dequal l l' && dequal r r' && QName.equal t t'
+  let hash (s,l,r,list,t) =
+    HASHINT4(dhash s, dhash l, dhash r, QName.hash t)
+end
diff --git a/src/run.ml b/src/run.ml
index 482a749..39eec26 100644
--- a/src/run.ml
+++ b/src/run.ml
@@ -13,6 +13,8 @@
 (*                                                                     *)
 (***********************************************************************)
 
+INCLUDE "utils.ml"
+
 module Node  =
 struct
   type t = int
@@ -25,17 +27,23 @@ 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
 exception Max_fail
 
+
+(* Hash Consign modules *)
+open Hconsed_run
+module HashOracle = Hashtbl.Make(Oracle_fixpoint)
+module HashRun = Hashtbl.Make(Run_fixpoint)
+
 (* Mapped sets for leaves *)
 let map_leaf asta = (Asta.bot_states_s asta, StateSet.empty)
 
 (* Build the Oracle *)
-let rec bu_oracle asta run tree tnode =
+let rec bu_oracle asta run tree tnode hashOracle hashEval =
   let node = Tree.preorder tree tnode in
   if Tree.is_leaf tree tnode
   then
@@ -43,71 +51,91 @@ let rec bu_oracle asta run tree tnode =
     then ()
     else NodeHash.add run node (map_leaf asta)
   else
-    let tfnode = Tree.first_child tree tnode (* first child *)
-    and tnnode = Tree.next_sibling tree tnode in (* next-sibling *)
+    let tfnode = Tree.first_child_x tree tnode
+    and tnnode = Tree.next_sibling tree tnode in
     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;
+      bu_oracle asta run tree tfnode hashOracle hashEval;
+      bu_oracle asta run tree tnnode hashOracle hashEval;
+      (* add states which satisfy a transition *)
+      let rec result set qfr qnr flag = function
+        | [] -> set,flag
+        | (q,form) :: tl ->
+          if Formula.eval_form (set,qfr,qnr) form hashEval
+          then
+            if StateSet.mem q set
+            then result set qfr qnr 0 tl
+            else result (StateSet.add q set) qfr qnr 1 tl
+          else result set qfr qnr 0 tl in
+      (* compute the fixed point of states of node *)
+      let rec fix_point set_i qfr qnr list_tr t =
+        try HashOracle.find hashOracle (set_i, qfr, qnr, list_tr, t)
+        with _ -> 
+          let set,flag = result set_i qfr qnr 0 list_tr in
+          HashOracle.add hashOracle (set_i,qfr,qnr,list_tr,t) (set); (* todo: Think about this position *)
+          if flag = 0
+          then set
+          else fix_point set qfr qnr list_tr t in
       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 reco. tran.*)
-      let rec result set = function
-        | [] -> set
-        | (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)
+      let _,list_tr = Asta.transitions_lab asta lab in (*only reco. tran.*)     
+     NodeHash.add run node (StateSet.empty,
+                            fix_point StateSet.empty qfr qnr list_tr lab)
     end
 
 (* Build the over-approx. of the maximal run *)
-let rec bu_over_max asta run tree tnode =
+let rec bu_over_max asta run tree tnode hashOver hashInfer =
   if (Tree.is_leaf tree tnode)      (* BU_oracle has already created the map *)
   then
     ()
   else
-    let tfnode = Tree.first_child tree tnode
+    let tfnode = Tree.first_child_x tree tnode
     and tnnode = Tree.next_sibling tree tnode in
     begin
-      bu_over_max asta run tree tfnode;
-      bu_over_max asta run tree tnnode;
+      bu_over_max asta run tree tfnode hashOver hashInfer;
+      bu_over_max asta run tree tnnode hashOver hashInfer;
       let (fnode,nnode) =
         (Tree.preorder tree tfnode, Tree.preorder tree tnnode)
       and node = Tree.preorder tree tnode in          
       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 qf qn flag list_tr = function 
+        | [] -> if flag = 0 then set else result set qf qn 0 list_tr list_tr
+        | (q,form) :: tl ->
+          if StateSet.mem q set
+          then result set qf qn 0 list_tr tl
+          else if Formula.infer_form (set,resultr) qf qn form hashInfer
+          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 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 hashOver
+                    ((StateSet.empty,resultr), qf,qn,list_tr,lab) res;
+                  res in
       (* we keep the old recognizing states set *)
-      NodeHash.replace run node (result_set, resultr)
+      NodeHash.replace run node (result_set(), resultr)
     end
 
 
 (* Build the maximal run *)
-let rec tp_max asta run tree tnode =
+let rec tp_max asta run tree tnode hashMax hashInfer =
   if (Tree.is_leaf tree tnode)      (* BU_oracle has already created the map *)
   then
     ()
   else
     let node = Tree.preorder tree tnode
-    and tfnode = Tree.first_child tree tnode
+    and tfnode = Tree.first_child_x tree tnode
     and tnnode = Tree.next_sibling tree tnode in
     let (fnode,nnode) =
       (Tree.preorder tree tfnode, Tree.preorder tree tnnode) in
@@ -121,23 +149,64 @@ 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 rec result = function
+      let (self_q,self_r) = try NodeHash.find run node
+        with Not_found -> raise Max_fail in
+
+      (* We must compute again accepting states from self transitions since
+         previous calls of tp_max may remove them *)
+      let rec result_q self_q queue = function (* for initializing the queue *)
+        | [] -> self_q,queue
+        | (q,form) :: tl ->
+          if (StateSet.mem q self_q)
+          then begin 
+            let q_cand,_,_ = Formula.st form in
+            StateSet.iter (fun x -> Queue.push x queue) q_cand;
+            result_q (StateSet.add q self_q) queue tl;
+          end
+          else result_q self_q queue tl
+      and result_st_q self_q queue flag = function (*for computing the fixed p*)
+        | [] -> flag,queue
+        | form :: tl ->
+          if Formula.infer_form (self_q,self_r) qf qn form hashInfer
+          then begin 
+            let q_cand,_,_ = Formula.st form in
+            StateSet.iter (fun x -> Queue.push x queue) q_cand;
+            result_st_q self_q queue 1 tl;
+          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              (* todo: to be hconsigned? *)
+        then self_q_i
+        else
+          let q = Queue.pop queue in
+          let list_q,_ = Asta.transitions_st_lab asta q lab in
+          let flag,queue = result_st_q self_q_i queue 0 list_q in
+          let self_q = if flag = 1 then StateSet.add q self_q_i else self_q_i in
+          comp_acc_self self_q queue in
+      
+      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 (self) node! *)
+      let rec result self qf qn = function
         | [] -> []
         | (q,form) :: tl ->
-          if (Formula.infer_form (qfq,qnq) (qfr,qnr) form) &&
-            (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 (* tran. candidates *)
+          if (StateSet.mem q (fst self)) && (* infers & trans. can start here *)
+            (Formula.infer_form self qf qn form hashInfer)
+          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
-        | f :: tl -> let sql,sqr = Formula.st f in
+        | f :: tl -> let sqs,sql,sqr = Formula.st f in
                      let ql' = StateSet.union sql ql
                      and qr' = StateSet.union sqr qr in
                      add_st (ql',qr') tl in
@@ -147,28 +216,41 @@ let rec tp_max asta run tree tnode =
       and qnq,qnr = try NodeHash.find run nnode
         with | _ -> map_leaf asta in
       begin
-        if tfnode == Tree.nil
+        if tfnode == Tree.nil || Tree.is_attribute tree tnode
         then ()
         else NodeHash.replace run fnode (StateSet.inter qfq ql,qfr);
-        if tnnode == Tree.nil
+        if tnnode == Tree.nil || Tree.is_attribute tree tnode
         then ()
         else NodeHash.replace run nnode (StateSet.inter qnq qr,qnr);
-        tp_max asta run tree tfnode;
-        tp_max asta run tree tnnode;
+        (* indeed we delete all states from self transitions!  *)
+        tp_max asta run tree tfnode hashMax hashInfer;
+        tp_max asta run tree tnnode hashMax hashInfer;
       end;
     end
         
 let compute tree asta =
   let flag = 2 in                       (* debug  *)
   let size_tree = 10000 in              (* todo (Tree.size ?) *)
+  let size_hcons_O = 1000 in            (* todo size Hashtbl *)
+  let size_hcons_M = 1000 in            (* todo size Hashtbl *)
+  let size_hcons_F = 1000 in            (* todo size Hashtbl *)
   let map = NodeHash.create size_tree in
-  bu_oracle asta map tree (Tree.root tree);
+  let hashOracle = HashOracle.create(size_hcons_O) in
+  let hashEval = Formula.HashEval.create(size_hcons_F) in
+  let hashInfer = Formula.HashInfer.create(size_hcons_F) in
+  bu_oracle asta map tree (Tree.root tree) hashOracle hashEval;
+  HashOracle.clear hashOracle;
+  Formula.HashEval.clear hashEval;
   if flag > 0 then begin
-    bu_over_max asta map tree (Tree.root tree);
+    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 hashInfer;
     if flag = 2
     then
-      tp_max asta map tree (Tree.root tree)
-    else ()
+      tp_max asta map tree (Tree.root tree) hashMax hashInfer
+    else ();
+    HashRun.clear hashOver;
+    HashRun.clear hashMax;
   end
   else ();
   map
@@ -178,7 +260,7 @@ let selected_nodes tree asta =
   NodeHash.fold
     (fun key set acc ->
       if not(StateSet.is_empty
-               (StateSet.inter (fst set) (Asta.selec_states asta)))        
+               (StateSet.inter (fst set) (Asta.selec_states asta)))
       then key :: acc
       else acc)
     run []
diff --git a/src/solve.ml b/src/solve.ml
index 6e25db2..4ab1147 100644
--- a/src/solve.ml
+++ b/src/solve.ml
@@ -47,6 +47,10 @@ let compute_run doc query =
 
 let () =
   let flag  = Array.length Sys.argv = 5 in
+  let flag2 =
+    if flag
+    then int_of_string Sys.argv.(4) = 1
+    else false in
   Format.pp_set_margin err_formatter 80;
   let doc = doc () in
   let queries = query () in
@@ -65,8 +69,10 @@ let () =
         fprintf err_formatter "  ### Query: %a"
           XPath.Ast.print query
       else ();
-      fprintf err_formatter "@.  ### Selected nodes: {%a}@."
-        print_selec selected_nodes;
+      if flag2 then
+        fprintf err_formatter "@.  ### Selected nodes: {%a}@."
+          print_selec selected_nodes
+      else ();
       if flag
       then begin
         Asta.print err_formatter asta;
diff --git a/src/tree.ml b/src/tree.ml
index 2b0fa4e..434d195 100644
--- a/src/tree.ml
+++ b/src/tree.ml
@@ -261,10 +261,16 @@ let rec print_xml out tree_ node =
 
 let root t = t.root
 let first_child _ n = n.first_child
+let first_child_x _ n =
+  if n.first_child.tag == QName.attribute_map
+  then n.first_child.next_sibling
+  else n.first_child
 let next_sibling _ n = n.next_sibling
 let parent _ n = n.parent
 (* Begin Lucca Hirschi *)
-let is_leaf t n = (first_child t n == nil) && (next_sibling t n == nil)
+let is_leaf t n = (not (n.tag == QName.attribute_map)) &&
+  (first_child t n == nil) && (next_sibling t n == nil)
+let is_attribute t n = n.tag == QName.attribute_map
 (* End *)
 let tag _ n = n.tag
 let data _ n = n.data
@@ -287,7 +293,8 @@ let rec print_xml_preorder out tree_ node =
         let fchild =
           if node.first_child.tag == QName.attribute_map then
             let () =
-              print_attributes out tree_ node.first_child.first_child
+              let ffn = node.first_child.first_child in
+              print_attributes out tree_ ffn;
             in
             node.first_child.next_sibling
           else
@@ -303,3 +310,6 @@ let rec print_xml_preorder out tree_ node =
         end
     in
     print_xml_preorder out tree_ node.next_sibling
+
+let debug_node fmt t n = 
+  Parser.debug_node fmt n
diff --git a/src/tree.mli b/src/tree.mli
index c75fd26..b64b0ff 100644
--- a/src/tree.mli
+++ b/src/tree.mli
@@ -49,6 +49,12 @@ val first_child : t -> node -> node
     Returns [nil] if [n] is a leaf. Returns [nil] if [n == nil].
 *)
 
+val first_child_x : t -> node -> node
+(** [first_child t n] returns the first child which is not an attribute
+    of node [n] in tree [t].
+    Returns [nil] if [n] is a leaf. Returns [nil] if [n == nil].
+*)
+
 val next_sibling : t -> node -> node
 (** [next_sibling t n] returns the next_sibling of node [n] in tree [t].
     Returns [nil] if [n] is the last child of a node.
@@ -62,7 +68,10 @@ val parent : t -> node -> node
 *)
 
 val is_leaf : t -> node -> bool
-(** Return true if the node is a *)
+(** Return true if the node is a leaf or an attribute *)
+
+val is_attribute : t -> node -> bool
+(** Return true if the node is an attribute *)
 
 val tag : t -> node -> QName.t
 (** Returns the label of a given node *)
@@ -81,3 +90,6 @@ val preorder : t -> node -> int
 val print_xml_preorder : out_channel -> t -> node -> unit
 (** Outputs the tree with IDs for nodes as an XML document on the
     given output_channel *)
+
+val debug_node : Format.formatter -> t -> node -> unit
+(** DEBUG *)
diff --git a/tests/docs/XPath-FT.xml b/tests/docs/XPath-FT.xml
index 90aef04..bd46991 100644
--- a/tests/docs/XPath-FT.xml
+++ b/tests/docs/XPath-FT.xml
@@ -1 +1,40 @@
-<?xml version="1.0" encoding="UTF-8"?><!DOCTYPE A SYSTEM "alphabet.dtd"><A id="n1" pre="1" post="26" xml:lang="en"><B id="n2" pre="2" post="3"><C id="n3" pre="3" post="1">clergywoman</C><D id="n4" pre="4" post="2">decadent</D></B><E id="n5" pre="5" post="22"><F id="n6" pre="6" post="6"><G id="n7" pre="7" post="4">gentility</G><H id="n8" pre="8" post="5" idrefs="n17 n26">happy-go-lucky man</H></F><I id="n9" pre="9" post="9"><J id="n10" pre="10" post="7">jigsaw</J><K id="n11" pre="11" post="8">kerchief</K></I><L id="n12" pre="12" post="15"><!--L is the twelve-th letter of the English alphabet-->The letter L is followed by the letter:<M id="n13" pre="13" post="10"/>which is followed by the letter:<N id="n14" pre="14" post="13"><O id="n15" pre="15" post="11">ovenware</O><P id="n16" pre="16" post="12">plentiful</P></N><?myPI value="XPath is nice"?><Q id="n17" pre="17" post="14" idrefs="n8 n26">quarrelsome</Q></L><R id="n18" pre="18" post="18"><S id="n19" pre="19" post="16">sage</S><T id="n20" pre="20" post="17">tattered</T></R><U id="n21" pre="21" post="21"><V id="n22" pre="22" post="19">voluptuary</V><W id="n23" pre="23" post="20">wriggle</W></U></E><X id="n24" pre="24" post="25"><Y id="n25" pre="25" post="23">yawn</Y><Z id="n26" pre="26" post="24" idrefs="n8 n17" xml:lang="it">zuzzurellone</Z></X></A>
+<A id="n1" pre="1" post="26" xml:lang="en">
+<B id="n2" pre="2" post="3">
+<C id="n3" pre="3" post="1">clergywoman</C>
+<D id="n4" pre="4" post="2">decadent</D>
+</B>
+<E id="n5" pre="5" post="22">
+<F id="n6" pre="6" post="6">
+<G id="n7" pre="7" post="4">gentility</G>
+<H id="n8" pre="8" post="5" idrefs="n17 n26">happy-go-lucky man</H>
+</F>
+<I id="n9" pre="9" post="9">
+<J id="n10" pre="10" post="7">jigsaw</J>
+<K id="n11" pre="11" post="8">kerchief</K>
+</I>
+<L id="n12" pre="12" post="15">
+<!-- L is the twelve-th letter of the English alphabet -->
+The letter L is followed by the letter:
+<M id="n13" pre="13" post="10"/>
+which is followed by the letter:
+<N id="n14" pre="14" post="13">
+<O id="n15" pre="15" post="11">ovenware</O>
+<P id="n16" pre="16" post="12">plentiful</P>
+</N>
+<?myPI value="XPath is nice"?>
+<Q id="n17" pre="17" post="14" idrefs="n8 n26">quarrelsome</Q>
+</L>
+<R id="n18" pre="18" post="18">
+<S id="n19" pre="19" post="16">sage</S>
+<T id="n20" pre="20" post="17">tattered</T>
+</R>
+<U id="n21" pre="21" post="21">
+<V id="n22" pre="22" post="19">voluptuary</V>
+<W id="n23" pre="23" post="20">wriggle</W>
+</U>
+</E>
+<X id="n24" pre="24" post="25">
+<Y id="n25" pre="25" post="23">yawn</Y>
+<Z id="n26" pre="26" post="24" idrefs="n8 n17" xml:lang="it">zuzzurellone</Z>
+</X>
+</A>
diff --git a/tests/queries/XPath-FT.queries b/tests/queries/XPath-FT.queries
index bf29a0d..de956e9 100644
--- a/tests/queries/XPath-FT.queries
+++ b/tests/queries/XPath-FT.queries
@@ -1,4 +1,4 @@
-/descendant::L
+/descendant::L/child::*
 /descendant::L/descendant::* 
 /descendant::L/following-sibling::*
 /descendant::L/self::*