X-Git-Url: http://git.nguyen.vg/gitweb/?p=tatoo.git;a=blobdiff_plain;f=src%2Fata.ml;h=939586f34ab31d691bc399cf563a9dad43860aec;hp=565dfc8bf1595a7c2a75315a239f5dde8cebdce7;hb=3b9dbcd9318dba41999dc6cc43093edbe5bc4c5d;hpb=5f1d396f4a04c9a0c6bb3da4176fd47a4473d35d

diff --git a/src/ata.ml b/src/ata.ml
index 565dfc8..939586f 100644
--- a/src/ata.ml
+++ b/src/ata.ml
@@ -23,66 +23,66 @@ type move = [ `First_child
             | `Stay ]
 
 module Move =
-  struct
-    type t = move
-    type 'a table = 'a array
-    let idx = function
-      | `First_child -> 0
-      | `Next_sibling -> 1
-      | `Parent -> 2
-      | `Previous_sibling -> 3
-      | `Stay -> 4
-    let ridx = function
-      | 0 -> `First_child
-      | 1 -> `Next_sibling
-      | 2 -> `Parent
-      | 3 -> `Previous_sibling
-      | 4 -> `Stay
-      | _ -> assert false
-
-    let create_table a = Array.make 5 a
-    let get m k = m.(idx k)
-    let set m k v = m.(idx k) <- v
-    let iter f m = Array.iteri (fun i v -> f (ridx i) v) m
-    let fold f m acc =
-      let acc = ref acc in
-      iter (fun i v -> acc := f i v !acc) m;
-      !acc
-    let for_all p m =
-      try
-        iter (fun i v -> if not (p i v) then raise Exit) m;
-        true
-      with
-        Exit -> false
-    let for_all2 p m1 m2 =
-      try
-        for i = 0 to 4 do
-          let v1 = m1.(i)
-          and v2 = m2.(i) in
-          if not (p (ridx i) v1 v2) then raise Exit
-        done;
-        true
-      with
-        Exit -> false
-
-    let exists p m =
-      try
-        iter (fun i v -> if p i v then raise Exit) m;
-        false
-      with
-        Exit -> true
-    let print ppf m =
-      match m with
-        `First_child -> fprintf ppf "%s" Pretty.down_arrow
-      | `Next_sibling -> fprintf ppf "%s" Pretty.right_arrow
-      | `Parent -> fprintf ppf "%s" Pretty.up_arrow
-      | `Previous_sibling -> fprintf ppf "%s" Pretty.left_arrow
-      | `Stay -> fprintf ppf "%s" Pretty.bullet
-
-    let print_table pr_e ppf m =
-      iter (fun i v -> fprintf ppf "%a: %a" print i pr_e v;
-        if (idx i) < 4 then fprintf ppf ", ") m
-  end
+struct
+  type t = move
+  type 'a table = 'a array
+  let idx = function
+    | `First_child -> 0
+    | `Next_sibling -> 1
+    | `Parent -> 2
+    | `Previous_sibling -> 3
+    | `Stay -> 4
+  let ridx = function
+    | 0 -> `First_child
+    | 1 -> `Next_sibling
+    | 2 -> `Parent
+    | 3 -> `Previous_sibling
+    | 4 -> `Stay
+    | _ -> assert false
+
+  let create_table a = Array.make 5 a
+  let get m k = m.(idx k)
+  let set m k v = m.(idx k) <- v
+  let iter f m = Array.iteri (fun i v -> f (ridx i) v) m
+  let fold f m acc =
+    let acc = ref acc in
+    iter (fun i v -> acc := f i v !acc) m;
+    !acc
+  let for_all p m =
+    try
+      iter (fun i v -> if not (p i v) then raise Exit) m;
+      true
+    with
+      Exit -> false
+  let for_all2 p m1 m2 =
+    try
+      for i = 0 to 4 do
+        let v1 = m1.(i)
+        and v2 = m2.(i) in
+        if not (p (ridx i) v1 v2) then raise Exit
+      done;
+      true
+    with
+      Exit -> false
+
+  let exists p m =
+    try
+      iter (fun i v -> if p i v then raise Exit) m;
+      false
+    with
+      Exit -> true
+  let print ppf m =
+    match m with
+      `First_child -> fprintf ppf "%s" Pretty.down_arrow
+    | `Next_sibling -> fprintf ppf "%s" Pretty.right_arrow
+    | `Parent -> fprintf ppf "%s" Pretty.up_arrow
+    | `Previous_sibling -> fprintf ppf "%s" Pretty.left_arrow
+    | `Stay -> fprintf ppf "%s" Pretty.bullet
+
+  let print_table pr_e ppf m =
+    iter (fun i v -> fprintf ppf "%a: %a" print i pr_e v;
+      if (idx i) < 4 then fprintf ppf ", ") m
+end
 
 type predicate = Move of move * State.t
                  | Is_first_child
@@ -146,19 +146,19 @@ struct
       has_first_child
 
   let next_sibling q =
-  and_
-    (mk_move `Next_sibling q)
-    has_next_sibling
+    and_
+      (mk_move `Next_sibling q)
+      has_next_sibling
 
   let parent q =
-  and_
-    (mk_move `Parent  q)
-    is_first_child
+    and_
+      (mk_move `Parent  q)
+      is_first_child
 
   let previous_sibling q =
-  and_
-    (mk_move `Previous_sibling q)
-    is_next_sibling
+    and_
+      (mk_move `Previous_sibling q)
+      is_next_sibling
 
   let stay q = mk_move `Stay q
 
@@ -179,39 +179,42 @@ struct
 end
 
 module Transition =
-  struct
-    include Hcons.Make (struct
-  type t = State.t * QNameSet.t * Formula.t
-  let equal (a, b, c) (d, e, f) =
-    a == d && b == e && c == f
-  let hash (a, b, c) =
-    HASHINT4 (PRIME1, a, ((QNameSet.uid b) :> int), ((Formula.uid c) :> int))
-end)
-    let print ppf t =
-      let q, l, f = t.node in
-      fprintf ppf "%a, %a %s %a"
-        State.print q
-        QNameSet.print l
-        Pretty.double_right_arrow
-        Formula.print f
-  end
+struct
+  include Hcons.Make (struct
+    type t = State.t * QNameSet.t * Formula.t
+    let equal (a, b, c) (d, e, f) =
+      a == d && b == e && c == f
+    let hash (a, b, c) =
+      HASHINT4 (PRIME1, a, ((QNameSet.uid b) :> int), ((Formula.uid c) :> int))
+  end)
+  let print ppf t =
+    let q, l, f = t.node in
+    fprintf ppf "%a, %a %s %a"
+      State.print q
+      QNameSet.print l
+      Pretty.double_right_arrow
+      Formula.print f
+end
 
 
 module TransList : sig
   include Hlist.S with type elt = Transition.t
   val print : Format.formatter -> ?sep:string -> t -> unit
 end =
-  struct
-    include Hlist.Make(Transition)
-    let print ppf ?(sep="\n") l =
-      iter (fun t ->
-        let q, lab, f = Transition.node t in
-        fprintf ppf "%a, %a → %a%s"
-          State.print q
-          QNameSet.print lab
-          Formula.print f sep) l
-  end
+struct
+  include Hlist.Make(Transition)
+  let print ppf ?(sep="\n") l =
+    iter (fun t ->
+      let q, lab, f = Transition.node t in
+      fprintf ppf "%a, %a → %a%s"
+        State.print q
+        QNameSet.print lab
+        Formula.print f sep) l
+end
 
+type rank = { td : StateSet.t;
+              bu : StateSet.t;
+              exit : StateSet.t }
 
 
 type t = {
@@ -220,7 +223,7 @@ type t = {
   mutable starting_states : StateSet.t;
   mutable selecting_states: StateSet.t;
   transitions: (State.t, (QNameSet.t*Formula.t) list) Hashtbl.t;
-  mutable ranked_states : StateSet.t array
+  mutable ranked_states : rank array
 }
 
 let uid t = t.id
@@ -253,7 +256,9 @@ let print fmt a =
     StateSet.print a.starting_states
     StateSet.print a.selecting_states
     (let r = ref 0 in Pretty.print_array ~sep:", " (fun ppf s ->
-      fprintf ppf "%i:%a" !r StateSet.print s; incr r)) a.ranked_states;
+      fprintf ppf "(%i:{td=%a,bu=%a,exit=%a)" !r
+        StateSet.print s.td StateSet.print s.bu StateSet.print s.exit;
+      incr r)) a.ranked_states;
   let trs =
     Hashtbl.fold
       (fun q t acc -> List.fold_left (fun acc (s , f) -> (q,s,f)::acc) acc t)
@@ -369,31 +374,31 @@ let normalize_negations auto =
     | Boolean.Atom(a, b') -> begin
       match a.Atom.node with
       | Move (m,  q) ->
-          if b == b' then begin
-          (* a appears positively, either no negation or double negation *)
-            if not (Hashtbl.mem memo_state (q,b)) then Queue.add (q,true) todo;
-            Formula.mk_atom (Move(m, q))
-          end else begin
-        (* need to reverse the atom
-           either we have a positive state deep below a negation
-           or we have a negative state in a positive formula
-           b' = sign of the state
-           b = sign of the enclosing formula
-        *)
-            let not_q =
-              try
-            (* does the inverted state of q exist ? *)
-                Hashtbl.find memo_state (q, false)
-              with
-                Not_found ->
-              (* create a new state and add it to the todo queue *)
-                  let nq = State.make () in
-                  auto.states <- StateSet.add nq auto.states;
-                  Hashtbl.add memo_state (q, false) nq;
-                  Queue.add (q, false) todo; nq
-            in
-            Formula.mk_atom (Move (m,not_q))
-          end
+        if b == b' then begin
+            (* a appears positively, either no negation or double negation *)
+          if not (Hashtbl.mem memo_state (q,b)) then Queue.add (q,true) todo;
+          Formula.mk_atom (Move(m, q))
+        end else begin
+            (* need to reverse the atom
+               either we have a positive state deep below a negation
+               or we have a negative state in a positive formula
+               b' = sign of the state
+               b = sign of the enclosing formula
+            *)
+          let not_q =
+            try
+                (* does the inverted state of q exist ? *)
+              Hashtbl.find memo_state (q, false)
+            with
+              Not_found ->
+                  (* create a new state and add it to the todo queue *)
+                let nq = State.make () in
+                auto.states <- StateSet.add nq auto.states;
+                Hashtbl.add memo_state (q, false) nq;
+                Queue.add (q, false) todo; nq
+          in
+          Formula.mk_atom (Move (m,not_q))
+        end
       | _ -> if b then f else Formula.not_ f
     end
   in
@@ -445,14 +450,25 @@ let compute_dependencies auto =
 
   edges
 
+let state_prerequisites dir auto q =
+  let trans = Hashtbl.find auto.transitions q in
+  List.fold_left (fun acc (_, phi) ->
+    let m_phi = Formula.get_states_by_move phi in
+    let prereq = Move.get m_phi dir in
+    StateSet.union prereq acc)
+    StateSet.empty trans
+
 
 let compute_rank auto =
   let dependencies = compute_dependencies auto in
   let upward = [ `Stay ; `Parent ; `Previous_sibling ] in
   let downward = [ `Stay; `First_child; `Next_sibling ] in
   let swap dir = if dir == upward then downward else upward in
-  let is_satisfied q t =
-    Move.for_all (fun _ set -> StateSet.(is_empty (remove q set))) t
+  let is_satisfied dir q t =
+    Move.for_all (fun d set ->
+      if List.mem d dir then
+        StateSet.(is_empty (remove q set))
+      else StateSet.is_empty set) t
   in
   let update_dependencies dir initacc =
     let rec loop acc =
@@ -464,7 +480,7 @@ let compute_rank auto =
               Move.set deps m (StateSet.diff (Move.get deps m) to_remove)
             )
             dir;
-          if is_satisfied q deps then StateSet.add q acc else acc
+          if is_satisfied dir q deps then StateSet.add q acc else acc
         ) dependencies acc
       in
       if acc == new_acc then new_acc else loop new_acc
@@ -492,64 +508,94 @@ let compute_rank auto =
   List.iter (fun (r,s) ->
     let set = try Hashtbl.find by_rank r with Not_found -> StateSet.empty in
     Hashtbl.replace by_rank r (StateSet.union s set)) !rank_list;
-  auto.ranked_states <-
-    Array.init (Hashtbl.length by_rank) (fun i -> Hashtbl.find by_rank i)
-
+  let rank = Hashtbl.length by_rank in
+  if rank mod 2 == 1 then Hashtbl.replace by_rank rank StateSet.empty;
+  let rank = Hashtbl.length by_rank in
+  assert (rank mod 2 == 0);
+  let rank_array =
+    Array.init (rank / 2)
+      (fun i ->
+        let td_set = Hashtbl.find by_rank (2 * i) in
+        let bu_set = Hashtbl.find by_rank (2 * i + 1) in
+        { td = td_set; bu = bu_set ; exit = StateSet.empty }
+      )
+  in
+  let max_rank = Array.length rank_array - 1 in
+  for i = 0 to max_rank do
+    let this_rank = rank_array.(i) in
+    let exit = if i == max_rank then auto.selecting_states else
+        let next = rank_array.(i+1) in
+        let res =
+          StateSet.fold (fun q acc ->
+            List.fold_left (fun acc m ->
+              StateSet.union acc (state_prerequisites m auto q ))
+              acc [`First_child; `Next_sibling; `Parent; `Previous_sibling; `Stay]
+          ) (StateSet.union next.td next.bu) StateSet.empty
+        in
+
+        StateSet.(
+          union  auto.selecting_states ( inter res (union this_rank.td this_rank.bu)))
 
-module Builder =
-  struct
-    type auto = t
-    type t = auto
-    let next = Uid.make_maker ()
-
-    let make () =
-      let auto =
-        {
-          id = next ();
-          states = StateSet.empty;
-          starting_states = StateSet.empty;
-          selecting_states = StateSet.empty;
-          transitions = Hashtbl.create MED_H_SIZE;
-          ranked_states = [| |]
-        }
-      in
-      auto
+    in
+    rank_array.(i) <- {this_rank with exit = exit };
+  done;
+  auto.ranked_states <- rank_array
 
-    let add_state a ?(starting=false) ?(selecting=false) q =
-      a.states <- StateSet.add q a.states;
-      if starting then a.starting_states <- StateSet.add q a.starting_states;
-      if selecting then a.selecting_states <- StateSet.add q a.selecting_states
 
-    let add_trans a q s f =
-      if not (StateSet.mem q a.states) then add_state a q;
-      let trs = try Hashtbl.find a.transitions q with Not_found -> [] in
-      let cup, ntrs =
-        List.fold_left (fun (acup, atrs) (labs, phi) ->
-          let lab1 = QNameSet.inter labs s in
-          let lab2 = QNameSet.diff labs s in
-          let tr1 =
-            if QNameSet.is_empty lab1 then []
-            else [ (lab1, Formula.or_ phi f) ]
-          in
-          let tr2 =
-            if QNameSet.is_empty lab2 then []
-            else [ (lab2, Formula.or_ phi f) ]
-          in
-          (QNameSet.union acup labs, tr1@ tr2 @ atrs)
-        ) (QNameSet.empty, []) trs
-      in
-      let rem = QNameSet.diff s cup in
-      let ntrs = if QNameSet.is_empty rem then ntrs
-        else (rem, f) :: ntrs
-      in
-      Hashtbl.replace a.transitions q ntrs
+module Builder =
+struct
+  type auto = t
+  type t = auto
+  let next = Uid.make_maker ()
+
+  let make () =
+    let auto =
+      {
+        id = next ();
+        states = StateSet.empty;
+        starting_states = StateSet.empty;
+        selecting_states = StateSet.empty;
+        transitions = Hashtbl.create MED_H_SIZE;
+        ranked_states = [| |]
+      }
+    in
+    auto
+
+  let add_state a ?(starting=false) ?(selecting=false) q =
+    a.states <- StateSet.add q a.states;
+    if starting then a.starting_states <- StateSet.add q a.starting_states;
+    if selecting then a.selecting_states <- StateSet.add q a.selecting_states
+
+  let add_trans a q s f =
+    if not (StateSet.mem q a.states) then add_state a q;
+    let trs = try Hashtbl.find a.transitions q with Not_found -> [] in
+    let cup, ntrs =
+      List.fold_left (fun (acup, atrs) (labs, phi) ->
+        let lab1 = QNameSet.inter labs s in
+        let lab2 = QNameSet.diff labs s in
+        let tr1 =
+          if QNameSet.is_empty lab1 then []
+          else [ (lab1, Formula.or_ phi f) ]
+        in
+        let tr2 =
+          if QNameSet.is_empty lab2 then []
+          else [ (lab2, Formula.or_ phi f) ]
+        in
+        (QNameSet.union acup labs, tr1@ tr2 @ atrs)
+      ) (QNameSet.empty, []) trs
+    in
+    let rem = QNameSet.diff s cup in
+    let ntrs = if QNameSet.is_empty rem then ntrs
+      else (rem, f) :: ntrs
+    in
+    Hashtbl.replace a.transitions q ntrs
 
-    let finalize a =
-      complete_transitions a;
-      normalize_negations a;
-      compute_rank a;
-      a
-  end
+  let finalize a =
+    complete_transitions a;
+    normalize_negations a;
+    compute_rank a;
+    a
+end
 
 
 let map_set f s =
@@ -565,8 +611,8 @@ let rec map_form f phi =
   | Boolean.Or(phi1, phi2) -> Formula.or_ (map_form f phi1) (map_form f phi2)
   | Boolean.And(phi1, phi2) -> Formula.and_ (map_form f phi1) (map_form f phi2)
   | Boolean.Atom({ Atom.node = Move(m,q); _}, b) ->
-      let a = Formula.mk_atom (Move (m,f q)) in
-      if b then a else Formula.not_ a
+    let a = Formula.mk_atom (Move (m,f q)) in
+    if b then a else Formula.not_ a
   | _ -> phi
 
 let rename_states mapper a =
@@ -581,7 +627,11 @@ let rename_states mapper a =
         (fun l ->
           (List.map (fun (labels, form) -> (labels, map_form rename form)) l))
         a.transitions;
-    ranked_states = Array.map (map_set rename) a.ranked_states
+    ranked_states = Array.map (fun s ->
+      { td = map_set rename s.td;
+        bu = map_set rename s.bu;
+        exit = map_set rename s.exit;
+      }) a.ranked_states
   }
 
 let copy a =