From c1b43e1dcdb3d0960dbc50db9f226d68ad30c16e Mon Sep 17 00:00:00 2001 From: Lucca Hirschi Date: Wed, 4 Jul 2012 17:38:21 +0200 Subject: [PATCH] Full implem BU Oracle + eval_form in Formula (impossible in Asta) + transitions_lab (transitions matching a specific tag) --- .gitignore | 2 +- src/asta.ml | 12 +++++++-- src/asta.mli | 6 ++++- src/formula.ml | 11 ++++++++ src/formula.mli | 3 +++ src/run.ml | 31 +++++++++++++++++++--- src/stateSet.ml | 2 +- src/test.ml | 1 + tests/results/my.result | 58 ----------------------------------------- 9 files changed, 60 insertions(+), 66 deletions(-) delete mode 100644 tests/results/my.result diff --git a/.gitignore b/.gitignore index f22646a..8709b08 100644 --- a/.gitignore +++ b/.gitignore @@ -4,4 +4,4 @@ _build doc/*.ps doc/*.out doc/html/* -tests/results/* \ No newline at end of file +tests/results/my.result \ No newline at end of file diff --git a/src/asta.ml b/src/asta.ml index 19fe29f..bbbba49 100644 --- a/src/asta.ml +++ b/src/asta.ml @@ -74,12 +74,20 @@ let transition asta st lab = let transitions asta st = let filter (s,l,f) = State.compare s st = 0 in - let rec remove_states l = match l with + let rec remove_states = function | [] -> [] - | (a,s,l) :: tl -> (s,l) :: (remove_states tl) in + | (s,l,f) :: tl -> (l,f) :: (remove_states tl) in (remove_states (SetT.elements (SetT.filter filter asta.trans_q)), (remove_states (SetT.elements (SetT.filter filter asta.trans_r)))) +let transitions_lab asta lab = + let filter (s,l,f) = QNameSet.mem lab l in + let rec remove_lab = function + | [] -> [] + | (s,l,f) :: tl -> (s,f) :: (remove_lab tl) in + (remove_lab (SetT.elements (SetT.filter filter asta.trans_q)), + (remove_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 14c2562..190f979 100644 --- a/src/asta.mli +++ b/src/asta.mli @@ -34,10 +34,14 @@ type t val transition : t -> state -> label -> formula (** Give the formula which must hold for a current state and label *) -val transitions : t -> state -> ((label*formula) list)*((label*formula) list) +val transitions : t -> state -> (label*formula) list * (label*formula) list (** Give the list of labels and formulae from queries and recognizing transitions for a given state *) +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 empty : t (** The empty automaton *) diff --git a/src/formula.ml b/src/formula.ml index f7eae85..03618c2 100644 --- a/src/formula.ml +++ b/src/formula.ml @@ -71,6 +71,17 @@ let prio f = | Atom _ -> 8 | And _ -> 6 | 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 + StateSet.mem s set +(* End *) let rec print ?(parent=false) ppf f = if parent then fprintf ppf "("; diff --git a/src/formula.mli b/src/formula.mli index 46cbe65..e108758 100644 --- a/src/formula.mli +++ b/src/formula.mli @@ -52,6 +52,9 @@ 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 s_1,s_2 F] evaluates the formula [F] on [(s_1,s_2)] *) + val print : Format.formatter -> t -> unit (** Pretty printer *) diff --git a/src/run.ml b/src/run.ml index d6ca22d..d88352b 100644 --- a/src/run.ml +++ b/src/run.ml @@ -27,6 +27,10 @@ type t = (StateSet.t*StateSet.t) NodeHash.t (** Map from node to query and recognizing states *) (* Note that we do not consider the nil nodes *) +exception Oracle_fail +exception Over_max_fail +exception Max_fail + (* Build the Oracle *) let rec bu_oracle asta run tree tnode = let init_set node = @@ -40,10 +44,31 @@ let rec bu_oracle asta run tree tnode = init_set node else () else + let tfnode = Tree.first_child tree tnode + and tnnode = Tree.next_sibling tree tnode in begin - bu_oracle asta run tree (Tree.first_child tree tnode); - bu_oracle asta run tree (Tree.next_sibling tree tnode); - (); + bu_oracle asta run tree tfnode; + bu_oracle asta run tree tnnode; + let (fnode,nnode) = + (Tree.preorder tree tfnode, Tree.preorder tree tnnode) in + let q_rec n = + try NodeHash.find run n + with Not_found -> (StateSet.empty,StateSet.empty) 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 reco. *) + let result_set = ref StateSet.empty in + let rec result = function + | [] -> () + | (q,form) :: tl -> + if Formula.eval_form (qf,qn) form + then begin + result_set := (StateSet.add q (!result_set)); + result tl; end + else result tl in + result list_tr; + NodeHash.add run node (StateSet.empty, !result_set) + (* Do not remove elt in Hahs (the old one would appear) *) end (* Build the over-approx. of the maximal run *) diff --git a/src/stateSet.ml b/src/stateSet.ml index 082ac8e..b97be4e 100644 --- a/src/stateSet.ml +++ b/src/stateSet.ml @@ -22,6 +22,6 @@ let print ppf s = if is_empty s then fprintf ppf "ø" else - (Pretty.print_list ~sep:" " (State.print)) ppf (elements s) in + (Pretty.print_list ~sep:"," (State.print)) ppf (elements s) in fprintf ppf "{ %a }" p_set s diff --git a/src/test.ml b/src/test.ml index 00f75f0..e9000c3 100644 --- a/src/test.ml +++ b/src/test.ml @@ -65,4 +65,5 @@ let () = Run.print err_formatter run; output_string stderr "\n # Doc: \n"; Tree.print_xml_preorder stderr doc (Tree.root doc); + output_string stderr "\n"; exit 0 diff --git a/tests/results/my.result b/tests/results/my.result deleted file mode 100644 index 53567dc..0000000 --- a/tests/results/my.result +++ /dev/null @@ -1,58 +0,0 @@ -Parse Tree OK ! Parse query OK ! Compil OK ! Run OK ! -##### Query ##### - /descendant::a[descendant::c[child::e and not descendant::f[not descendant::e]/descendant::g]]/descendant::b[child::g] - -##### Doc ##### -<#document> - - - - - - - - - - -##### ASTA ##### - # Query states: { q₁ q₂ q₈ q₉ } - # Recognizing states: { q₀ q₃ q₄ q₅ q₆ q₇ } - # Selecting states: { q₁ } - # Bottom states: { q₂ q₈ q₉ } - # Top states: { q₉ } - # Queries transitions: - | q₁ ----F(b)---> ↓₁q₀ - | q₂ ----Cof(ø)---> ↓₁q₂ ∨ ↓₂q₂ ∨ ↓₁q₁ ∨ ↓₂q₁ - | q₈ ----F(a)---> (↓₁q₂ ∨ ↓₁q₁) ∧ ↓₁q₇ - | q₈ ----Cof(ø)---> ↓₁q₈ ∨ ↓₂q₈ - | q₉ ----Cof(ø)---> ↓₁q₈ - # Recognizing transitions: - | q₀ ----F(g)---> ⊤ | q₀ ----Cof(ø)---> ↓₂q₀ - | q₃ ----F(g)---> ⊤ - | q₃ ----Cof(ø)---> ↓₁q₃ ∨ ↓₂q₃ - | q₄ ----F(e)---> ⊤ - | q₄ ----Cof(ø)---> ↓₁q₄ ∨ ↓₂q₄ - | q₅ ----F(f)---> ̅↓̅₁̅q̅₄ ∧ ↓₁q₃ - | q₅ ----Cof(ø)---> ↓₁q₅ ∨ ↓₂q₅ - | q₆ ----F(e)---> ⊤ | q₆ ----Cof(ø)---> ↓₂q₆ - | q₇ ----F(c)---> ↓₁q₆ ∧ ̅↓̅₁̅q̅₅ - | q₇ ----Cof(ø)---> ↓₁q₇ ∨ ↓₂q₇ - -##### RUN ##### - # Mapping: - | 14-->({ ø }, { ø }) | 16-->({ ø }, { ø }) - | 21-->({ ø }, { ø }) | 24-->({ ø }, { ø }) - | 25-->({ ø }, { ø }) | 34-->({ ø }, { ø }) - | 35-->({ ø }, { ø }) - - # Doc: -<#document '0> - '2 - '4 - '6 - '8 - '10 '17 '19 '21 - '22 '24 - '25 - '26 '28 '30 '32 '34 -'35 \ No newline at end of file -- 2.17.1