Full implem BU Oracle + eval_form in Formula (impossible in Asta) + transitions_lab...

diff --git a/.gitignore b/.gitignore
index f22646a..8709b08 100644 (file)
--- 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 (file)
--- 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 (file)
--- 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 (file)
--- 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 (file)
--- 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 (file)
--- 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 (file)
--- 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 (file)
--- 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 (file)
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><a>
-  <b/>
-  <c/>
-  <d/>
-  <e>
-    <f id="1" value="2"> <g/> <h/> </f>
-    <i> </i>
-  </e>
-  <j> <k/> <l/> <m/> </j>
-</a></#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><a '1>
-  '2<b '3/>
-  '4<c '5/>
-  '6<d '7/>
-  '8<e '9>
-    '10<f '11 id="1" value="2"> '17<g '18/> '19<h '20/> '21</f>
-    '22<i '23> '24</i>
-  '25</e>
-  '26<j '27> '28<k '29/> '30<l '31/> '32<m '33/> '34</j>
-'35</a></#document>
\ No newline at end of file