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
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. *)
(* 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;
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;
(* 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)
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 +| `Self *+ q'
| x -> print_axis pr_er x; raise Not_core_XPath
in
INCLUDE "utils.ml"
open Format
-type move = [ `Left | `Right ]
+type move = [ `Left | `Right | `Self ]
type 'hcons expr =
| False | True
| Or of 'hcons * 'hcons
| 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
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;
let ss = match d with
| `Left -> si, StateSet.empty
| `Right -> StateSet.empty, si
+ | `Self -> StateSet.empty, 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
(** Implementation of hashconsed Boolean formulae *)
-type move = [ `Left |`Right ]
+type move = [ `Left |`Right | `Self ]
(** Direction for automata predicates *)
type 'hcons expr =
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 *)
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
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 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
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 *)
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
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 (set_node,set_nr) as self = 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 comp_acc_self set flag = function
+ | [] -> set,flag
+ | (q,form) :: tl ->
+ if Formula.infer_form set qf qn form
+ then if StateSet.mem q set
+ then comp_acc_self set 0 tl
+ else comp_acc_self (StateSet.add q set) 1 tl
+ else comp_acc_self set 0 tl
+ and rec fix_point selfq_i =
+ let setq,flag = comp_acc_self selfq_i 0 list_tr in
+ if flag = 1 then set
+ else fix_point setq qf qn 0 in
+ NodeHash.replace run node (fix_point set_node, set_nr);
+
let rec result = function
| [] -> []
| (q,form) :: tl ->
- if (Formula.infer_form (qfq,qnq) (qfr,qnr) form) &&
- (StateSet.mem q set_node) (* infers & trans. can start here *)
+ if (StateSet.mem q set_node) && (* infers & trans. can start here *)
+ (Formula.infer_form self qf qn form)
then form :: (result tl)
else result tl in
let list_form = result list_tr in (* tran. candidates *)
if tnnode == Tree.nil
then ()
else NodeHash.replace run nnode (StateSet.inter qnq qr,qnr);
+ (* indeed we delete all states from self transitions! *)
tp_max asta run tree tfnode;
tp_max asta run tree tnnode;
end;
projects / tatoo.git / commitdiff