src/run.ml

   1 (***********************************************************************)
   2 (*                                                                     *)
   3 (*                               TAToo                                 *)
   4 (*                                                                     *)
   5 (*                     Kim Nguyen, LRI UMR8623                         *)
   6 (*                   Université Paris-Sud & CNRS                       *)
   7 (*                                                                     *)
   8 (*  Copyright 2010-2013 Université Paris-Sud and Centre National de la *)
   9 (*  Recherche Scientifique. All rights reserved.  This file is         *)
  10 (*  distributed under the terms of the GNU Lesser General Public       *)
  11 (*  License, with the special exception on linking described in file   *)
  12 (*  ../LICENSE.                                                        *)
  13 (*                                                                     *)
  14 (***********************************************************************)
  15
  16 INCLUDE "utils.ml"
  17 INCLUDE "debug.ml"
  18
  19
  20 module Make (T : Tree.S) =
  21 struct
  22
  23   let int (x : bool) : int = Obj.magic x
  24   let kint (x : Tree.NodeKind.t) : int = Obj.magic x
  25   let summary tree node is_first is_next fc ns =
  26     (int (ns != T.nil)) lor
  27       ((int (fc != T.nil)) lsl 1) lor
  28       ((int is_next) lsl 2) lor
  29       ((int is_first) lsl 3) lor
  30       ((kint (T.kind tree node)) lsl 4)
  31
  32   let has_next_sibling summary : bool = Obj.magic (summary land 1)
  33   let has_first_child summary : bool = Obj.magic ((summary lsr 1) land 1)
  34   let is_next_sibling summary : bool = Obj.magic ((summary lsr 2) land 1)
  35   let is_first_child summary : bool = Obj.magic ((summary lsr 3) land 1)
  36   let kind summary : Tree.NodeKind.t  = Obj.magic (summary lsr 4)
  37
  38   let dummy_set = StateSet.singleton State.dummy
  39   let dummy_trans_list =
  40     Ata.(TransList.cons
  41       (Transition.make (State.dummy, QNameSet.empty, Formula.false_))
  42       TransList.nil)
  43
  44   module Run =
  45     struct
  46       open Bigarray
  47       type t = {
  48         mutable pass : int;
  49         auto : Ata.t;
  50         trans_cache : Ata.TransList.t Cache.N2.t;
  51         td_cache : StateSet.t Cache.N6.t;
  52         bu_cache : StateSet.t Cache.N6.t;
  53         mark_cache : (StateSet.t*StateSet.t*StateSet.t) Cache.N4.t;
  54       }
  55
  56       let create a =
  57         {
  58           pass = 0;
  59           auto = a;
  60           trans_cache = Cache.N2.create dummy_trans_list;
  61           td_cache = Cache.N6.create dummy_set;
  62           bu_cache = Cache.N6.create dummy_set;
  63           mark_cache = Cache.N4.create (dummy_set,dummy_set,dummy_set);
  64         }
  65     end
  66
  67
  68   let eval_form phi node_summary f_set n_set p_set s_set =
  69     let rec loop phi =
  70       let open Boolean in
  71       match Ata.Formula.expr phi with
  72         False -> false
  73       | True -> true
  74       | Or (phi1, phi2) -> loop phi1 || loop phi2
  75       | And (phi1, phi2) -> loop phi1 && loop phi2
  76       | Atom (a, b) -> b == Ata.(
  77         match Atom.node a with
  78           Is_first_child -> is_first_child node_summary
  79         | Is_next_sibling -> is_next_sibling node_summary
  80         | Is k -> k == kind node_summary
  81         | Has_first_child -> has_first_child node_summary
  82         | Has_next_sibling -> has_next_sibling node_summary
  83         | Move (m, q) ->
  84           let set =
  85             match m with
  86               `First_child -> f_set
  87             | `Next_sibling -> n_set
  88             | `Parent
  89             | `Previous_sibling -> p_set
  90             | `Stay -> s_set
  91           in
  92           StateSet.mem q set
  93       )
  94     in
  95     loop phi
  96
  97
  98   let eval_trans_aux trans_list node_summary f_set n_set p_set s_set =
  99     let open Ata in
 100     TransList.fold (fun trs acc ->
 101       let q, _ , phi = Transition.node trs in
 102       if eval_form phi node_summary f_set n_set p_set s_set then
 103         StateSet.add q acc
 104       else
 105         acc) trans_list s_set
 106
 107   let eval_trans trans_list node_summary f_set n_set p_set s_set =
 108     let rec loop old_s =
 109
 110       let new_s =
 111         eval_trans_aux trans_list node_summary f_set n_set p_set old_s
 112       in
 113       if new_s == old_s then old_s else loop new_s
 114     in
 115     loop s_set
 116
 117   let get_trans run tag set =
 118     let i = (tag.QName.id :> int) in
 119     let j = (set.StateSet.id :> int) in
 120     let res = Cache.N2.find run.Run.trans_cache i j in
 121     if res == dummy_trans_list then begin
 122       let res = Ata.get_trans run.Run.auto tag set in
 123       Cache.N2.add run.Run.trans_cache i j res;
 124       res
 125     end
 126     else
 127       res
 128
 129   let eval_trans run cache set tag node_summary f_set n_set p_set s_set =
 130     let i = node_summary in
 131     let j = (tag.QName.id :> int) in
 132     let k = (f_set.StateSet.id :> int) in
 133     let l = (n_set.StateSet.id :> int) in
 134     let m = (p_set.StateSet.id :> int) in
 135     let n = (s_set.StateSet.id :> int) in
 136     let res = Cache.N6.find cache i j k l m n in
 137     if res == dummy_set then begin
 138       let trans_list = get_trans run tag set in
 139       let res = eval_trans trans_list node_summary f_set n_set p_set s_set in
 140       Cache.N6.add cache i j k l m n res;
 141       res
 142     end
 143     else res
 144
 145   let auto_run run tree prev_nodes td_states bu_states exit_states _i =
 146     let exit_id = (exit_states.StateSet.id :> int) in
 147     let empty_sets = StateSet.(empty,empty,empty) in
 148
 149     let mark_node front res node set f_set n_set =
 150       let i = (set.StateSet.id :> int) in
 151       let j = (f_set.StateSet.id :> int) in
 152       let k = (n_set.StateSet.id :> int) in
 153       let (mstates, _, _) as block =
 154         Cache.N4.find run.Run.mark_cache exit_id i j k
 155       in
 156
 157       let mstates, ll, rr =
 158         if mstates == dummy_set then begin
 159         let r1 = StateSet.inter set exit_states in
 160         let r2 = StateSet.inter f_set exit_states in
 161         let r3 = StateSet.inter n_set exit_states in
 162         let r = r1,r2,r3 in
 163         Cache.N4.add run.Run.mark_cache exit_id i j k r;
 164         r
 165         end
 166         else block
 167       in
 168       if mstates != StateSet.empty then
 169         let block = mstates, ll, rr, node in
 170         if front then Sequence.push_front block res
 171         else Sequence.push_back block res
 172     in
 173     let rec loop res node is_first is_next parent_set =
 174       if node == T.nil then StateSet.empty else begin
 175         let set,lset,rset =
 176         if Sequence.is_empty prev_nodes then
 177           empty_sets
 178         else
 179           let set,lset,rset, node' = Sequence.peek prev_nodes in
 180           if node == node' then begin
 181             ignore (Sequence.pop prev_nodes);
 182             set,lset,rset
 183           end
 184           else
 185             empty_sets
 186         in
 187         let tag = T.tag tree node in
 188         let first_child = T.first_child tree node in
 189         let next_sibling = T.next_sibling tree node in
 190         let node_summary =
 191           summary tree node is_first is_next first_child next_sibling
 192         in
 193         let status1 =
 194           eval_trans run run.Run.td_cache td_states tag node_summary lset rset parent_set set
 195         in
 196         let fcs = loop res first_child true false status1 in
 197         let rres = Sequence.create () in
 198         let nss = loop rres next_sibling false true status1 in
 199         if bu_states == StateSet.empty then (* tail call *) begin
 200           mark_node true res node status1 fcs StateSet.empty;
 201           Sequence.append res rres;
 202           status1
 203         end else begin
 204
 205           let status2 =
 206             eval_trans run run.Run.bu_cache bu_states tag node_summary fcs nss parent_set status1
 207           in
 208           if status2 != StateSet.empty then
 209             mark_node true res node status2 fcs nss;
 210           Sequence.append res rres;
 211           status2
 212         end;
 213       end
 214     in
 215     let res = Sequence.create () in
 216     ignore (loop res (T.root tree) false false StateSet.empty);
 217     res
 218
 219
 220
 221   let prepare_run auto l =
 222     let res = Sequence.create () in
 223     let start = Ata.get_starting_states auto in
 224     Sequence.iter (fun n -> Sequence.push_back (start, StateSet.empty, StateSet.empty, n) res) l;
 225     res
 226
 227 let time f arg msg =
 228   let t1 = Unix.gettimeofday () in
 229   let r = f arg in
 230   let t2 = Unix.gettimeofday () in
 231   let time = (t2 -. t1) *. 1000. in
 232   Logger.msg `STATS "%s: %fms" msg time;
 233   r
 234
 235
 236   let main_eval auto tree nodes =
 237     let s_nodes = prepare_run auto nodes in
 238     let ranked_states = Ata.get_states_by_rank auto in
 239     let acc = ref s_nodes in
 240     let max_rank = Ata.get_max_rank auto in
 241     let run = Run.create auto in
 242     for i = 0 to max_rank do
 243       let open Ata in
 244       let { td; bu; exit } = ranked_states.(i) in
 245       run.Run.pass <- i;
 246       acc := auto_run run tree !acc td bu exit i;
 247     done;
 248     !acc
 249
 250
 251   let eval auto tree nodes =
 252     let res = main_eval auto tree nodes in
 253     let r = Sequence.create () in
 254     Sequence.iter (fun (_,_,_, n) -> Sequence.push_back n r) res;
 255     r
 256
 257
 258   let full_eval auto tree nodes =
 259     let res = main_eval auto tree nodes in
 260     let dummy = Sequence.create () in
 261     let cache = Cache.N1.create dummy in
 262     Sequence.iter (fun (set, _, _, n) ->
 263       StateSet.iter (fun q ->
 264         let qres = Cache.N1.find cache q in
 265         let qres =
 266           if qres == dummy then begin
 267             let s = Sequence.create () in
 268             Cache.N1.add cache q s;
 269             s
 270           end
 271           else qres
 272         in
 273         Sequence.push_back n qres) set )
 274       res;
 275     let l = StateSet.fold (fun q acc ->
 276       let res = Cache.N1.find cache q in
 277       (q, res) :: acc) (Ata.get_selecting_states auto) []
 278     in
 279     List.rev l
 280
 281 end