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 open Format
  20 open Misc
  21
  22 type stats = { run : int;
  23                tree_size : int;
  24                fetch_trans_cache_access : int;
  25                fetch_trans_cache_hit : int;
  26                eval_trans_cache_access : int;
  27                eval_trans_cache_hit : int;
  28              }
  29
  30 let fetch_trans_cache_hit = ref 0
  31 let fetch_trans_cache_access = ref 0
  32 let eval_trans_cache_hit = ref 0
  33 let eval_trans_cache_access = ref 0
  34 let reset_stat_counters () =
  35   fetch_trans_cache_hit := 0;
  36   fetch_trans_cache_access := 0;
  37   eval_trans_cache_hit := 0;
  38   eval_trans_cache_access := 0
  39
  40
  41 module Make (T : Tree.S) =
  42  struct
  43
  44    module NodeSummary =
  45    struct
  46      (* Pack into an integer the result of the is_* and has_ predicates
  47         for a given node *)
  48      type t = int
  49      let dummy = -1
  50     (*
  51       ...44443210
  52       ...4444 -> kind
  53       3 -> has_right
  54       2 -> has_left
  55       1 -> is_right
  56       0 -> is_left
  57     *)
  58      let is_left (s : t) : bool =
  59        s land 1 != 0
  60
  61      let is_right (s : t) : bool =
  62        s land 0b10 != 0
  63
  64      let has_left (s : t) : bool =
  65        s land 0b100 != 0
  66
  67      let has_right (s : t) : bool =
  68        s land 0b1000 != 0
  69
  70      let kind (s : t) : Tree.NodeKind.t =
  71        Obj.magic (s lsr 4)
  72
  73      let make is_left is_right has_left has_right kind =
  74        (int_of_bool is_left) lor
  75          ((int_of_bool is_right) lsl 1) lor
  76          ((int_of_bool has_left) lsl 2) lor
  77          ((int_of_bool has_right) lsl 3) lor
  78          ((Obj.magic kind) lsl 4)
  79    end
  80
  81    let dummy_set = StateSet.singleton State.dummy
  82    open Bigarray
  83    type run = {
  84      tree : T.t ;
  85      (* The argument of the run *)
  86      auto : Ata.t;
  87      (* The automaton to be run *)
  88      sat: StateSet.t array;
  89      (* A mapping from node preorders to states satisfied at that node *)
  90      mutable pass : int;
  91      (* Number of run we have performed *)
  92      mutable fetch_trans_cache : Ata.Formula.t Cache.N2.t;
  93      (* A cache from states * label to list of transitions *)
  94      mutable td_cache : StateSet.t Cache.N6.t;
  95      mutable bu_cache : StateSet.t Cache.N6.t;
  96      (* Two 6-way caches used during the top-down and bottom-up phase
  97         label * self-set * fc-set * ns-set * parent-set * node-shape -> self-set
  98      *)
  99      node_summaries: (int, int16_unsigned_elt, c_layout) Array1.t;
 100    }
 101
 102
 103    let dummy_form = Ata.Formula.stay State.dummy
 104
 105    let make auto tree =
 106      let len = T.size tree in
 107      {
 108        tree = tree;
 109        auto = auto;
 110        sat = Array.create len StateSet.empty;
 111        pass = 0;
 112        fetch_trans_cache = Cache.N2.create dummy_form;
 113        td_cache = Cache.N6.create dummy_set;
 114        bu_cache = Cache.N6.create dummy_set;
 115        node_summaries = let ba = Array1.create int16_unsigned c_layout len in
 116                         Array1.fill ba 0; ba
 117      }
 118
 119    let get_form fetch_trans_cache auto tag q =
 120      let phi =
 121        incr fetch_trans_cache_access;
 122        Cache.N2.find fetch_trans_cache (tag.QName.id :> int) (q :> int)
 123      in
 124      if phi == dummy_form then
 125        let phi = Ata.get_form auto tag q in
 126        let () =
 127          Cache.N2.add
 128            fetch_trans_cache
 129            (tag.QName.id :> int)
 130            (q :> int) phi
 131        in phi
 132      else begin
 133        incr fetch_trans_cache_hit;
 134        phi
 135      end
 136
 137
 138    let eval_form phi fcs nss ps ss summary =
 139      let open Ata in
 140          let rec loop phi =
 141            begin match Formula.expr phi with
 142            | Boolean.False -> false
 143            | Boolean.True -> true
 144            | Boolean.Atom (a, b) ->
 145                begin
 146                  let open NodeSummary in
 147                      match a.Atom.node with
 148                      | Move (m, q) ->
 149                        b && StateSet.mem q (
 150                            match m with
 151                              `First_child -> fcs
 152                            | `Next_sibling -> nss
 153                            | `Parent | `Previous_sibling ->  ps
 154                            | `Stay ->  ss
 155                        )
 156                      | Is_first_child -> b == is_left summary
 157                      | Is_next_sibling -> b == is_right summary
 158                      | Is k -> b == (k == kind summary)
 159                      | Has_first_child -> b == has_left summary
 160                      | Has_next_sibling -> b == has_right summary
 161                end
 162            | Boolean.And(phi1, phi2) -> loop phi1 && loop phi2
 163            | Boolean.Or (phi1, phi2) -> loop phi1 || loop phi2
 164            end
 165          in
 166          loop phi
 167
 168
 169    let eval_trans_aux auto fetch_trans_cache tag fcs nss ps sat todo summary =
 170      StateSet.fold (fun q (a_sat) ->
 171        let phi =
 172          get_form fetch_trans_cache auto tag q
 173        in
 174        if eval_form phi fcs nss ps a_sat summary then
 175          StateSet.add q a_sat
 176        else a_sat
 177      ) todo sat
 178
 179
 180    let rec eval_trans_fix auto fetch_trans_cache tag fcs nss ps sat todo summary =
 181      let new_sat =
 182        eval_trans_aux auto fetch_trans_cache tag fcs nss ps sat todo summary
 183      in
 184      if new_sat == sat then sat else
 185        eval_trans_fix auto fetch_trans_cache tag fcs nss ps new_sat todo summary
 186
 187
 188    let eval_trans auto fetch_trans_cache eval_cache tag fcs nss ps ss todo summary =
 189      let fcsid = (fcs.StateSet.id :> int) in
 190      let nssid = (nss.StateSet.id :> int) in
 191      let psid = (ps.StateSet.id :> int) in
 192      let ssid = (ss.StateSet.id :> int) in
 193      let tagid = (tag.QName.id :> int) in
 194      let res = Cache.N6.find eval_cache tagid summary ssid fcsid nssid psid in
 195      incr eval_trans_cache_access;
 196      if res != dummy_set then begin incr eval_trans_cache_hit; res end
 197      else let new_sat =
 198             eval_trans_fix auto fetch_trans_cache tag fcs  nss ps ss todo summary
 199           in
 200           Cache.N6.add eval_cache tagid summary ssid fcsid nssid psid new_sat;
 201           new_sat
 202
 203
 204    let unsafe_get a i = if i < 0 then StateSet.empty else Array.unsafe_get a i
 205
 206    let top_down run =
 207     let i = run.pass in
 208     let tree = run.tree in
 209     let auto = run.auto in
 210     let states_by_rank = Ata.get_states_by_rank auto in
 211     let td_todo = states_by_rank.(i) in
 212     let bu_todo = if i + 1 = Array.length states_by_rank then StateSet.empty
 213       else
 214         states_by_rank.(i+1)
 215     in
 216     let rec loop_td_and_bu node parent parent_sat =
 217       if node == T.nil then StateSet.empty else begin
 218         let node_id = T.preorder tree node in
 219         let fc = T.first_child tree node in
 220         let ns = T.next_sibling tree node in
 221         let tag = T.tag tree node in
 222         (* We enter the node from its parent *)
 223         let summary =
 224           let s = Array1.unsafe_get run.node_summaries node_id in
 225           if  s != 0 then s else
 226             let s =
 227               NodeSummary.make
 228                 (node == T.first_child tree parent) (*is_left *)
 229                 (node == T.next_sibling tree parent)(*is_right *)
 230                 (fc != T.nil) (* has_left *)
 231                 (ns != T.nil) (* has_right *)
 232                 (T.kind tree node) (* kind *)
 233             in
 234             run.node_summaries.{node_id} <- s; s
 235         in
 236         let status0 = unsafe_get run.sat node_id in
 237         (* get the node_statuses for the first child, next sibling and parent *)
 238         let fcs = unsafe_get run.sat (T.preorder tree fc) in
 239         let nss = unsafe_get run.sat (T.preorder tree ns) in
 240         (* evaluate the transitions with all this statuses *)
 241         let status1 =
 242           eval_trans auto run.fetch_trans_cache run.td_cache tag fcs nss
 243             parent_sat
 244             status0 td_todo summary
 245         in
 246         (* update the cache if the status of the node changed *)
 247         if status1 != status0 then run.sat.(node_id) <- status1;
 248         let fcs1 = loop_td_and_bu fc node status1 in
 249         if bu_todo == StateSet.empty then
 250           loop_td_and_bu ns node status1 (* tail call *)
 251         else
 252           let nss1 = loop_td_and_bu ns node status1 in
 253           let status2 =
 254             eval_trans auto run.fetch_trans_cache run.bu_cache tag fcs1 nss1
 255               parent_sat
 256               status1 bu_todo summary
 257           in
 258           if status2 != status1 then run.sat.(node_id) <- status2;
 259           status2
 260       end
 261     in
 262     let _ = loop_td_and_bu (T.root tree) T.nil StateSet.empty in
 263     run.pass <- run.pass + 2
 264
 265
 266   let get_results run =
 267     let cache = run.sat in
 268     let auto = run.auto in
 269     let tree = run.tree in
 270     let sel_states = Ata.get_selecting_states auto in
 271     let rec loop node acc =
 272       if node == T.nil then acc
 273       else
 274         let acc0 = loop (T.next_sibling tree node) acc in
 275         let acc1 = loop (T.first_child tree node) acc0 in
 276
 277         if StateSet.intersect
 278           cache.(T.preorder tree node)(* NodeStatus.node.sat *)
 279           sel_states then node::acc1
 280         else acc1
 281     in
 282     loop (T.root tree) []
 283
 284
 285   let get_full_results run =
 286     let cache = run.sat(*tatus*) in
 287     let auto = run.auto in
 288     let tree = run.tree in
 289     let res_mapper = Hashtbl.create MED_H_SIZE in
 290     let () =
 291       StateSet.iter
 292         (fun q -> Hashtbl.add res_mapper q [])
 293         (Ata.get_selecting_states auto)
 294     in
 295     let dummy = [ T.nil ] in
 296     let res_mapper = Cache.N1.create dummy in
 297     let () =
 298       StateSet.iter
 299         (fun q -> Cache.N1.add res_mapper (q :> int) [])
 300         (Ata.get_selecting_states auto)
 301     in
 302     let rec loop node =
 303       if node != T.nil then
 304         let () = loop (T.next_sibling tree node) in
 305         let () = loop (T.first_child tree node) in
 306         StateSet.iter
 307           (fun q ->
 308             let res = Cache.N1.find res_mapper (q :> int) in
 309             if res != dummy then
 310               Cache.N1.add res_mapper (q :> int) (node::res)
 311           )
 312           cache.(T.preorder tree node)(* NodeStatus.node.sat *)
 313     in
 314     loop (T.root tree);
 315     (StateSet.fold_right
 316        (fun q acc -> (q, Cache.N1.find res_mapper (q :> int))::acc)
 317        (Ata.get_selecting_states auto) [])
 318
 319
 320   let prepare_run run list =
 321     let tree = run.tree in
 322     let auto = run.auto in
 323     let sat0 = Ata.get_starting_states auto in
 324     List.iter (fun node ->
 325       let node_id = T.preorder tree node in
 326       run.sat.(node_id) <- sat0) list
 327
 328   let tree_size = ref 0
 329   let pass = ref 0
 330   let compute_run auto tree nodes =
 331     pass := 0;
 332     tree_size := T.size tree;
 333     let run = make auto tree in
 334     prepare_run run nodes;
 335     let rank = Ata.get_max_rank auto in
 336     while run.pass <= rank do
 337       top_down run;
 338       run.td_cache <- Cache.N6.create dummy_set;
 339       run.bu_cache <- Cache.N6.create dummy_set;
 340     done;
 341     pass := Ata.get_max_rank auto + 1;
 342
 343     run
 344
 345   let full_eval auto tree nodes =
 346     let r = compute_run auto tree nodes in
 347     get_full_results r
 348
 349   let eval auto tree nodes =
 350     let r = compute_run auto tree nodes in
 351     get_results r
 352
 353   let stats () = {
 354     tree_size = !tree_size;
 355     run = !pass;
 356     fetch_trans_cache_access = !fetch_trans_cache_access;
 357     fetch_trans_cache_hit = !fetch_trans_cache_hit;
 358     eval_trans_cache_access = !eval_trans_cache_access;
 359     eval_trans_cache_hit = !eval_trans_cache_hit;
 360   }
 361
 362 end