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 open Bigarray
  22
  23 type stats = { mutable pass : int;
  24                tree_size : int;
  25                mutable fetch_trans_cache_access : int;
  26                mutable fetch_trans_cache_miss : int;
  27                mutable eval_trans_cache_access : int;
  28                mutable eval_trans_cache_miss : int;
  29                mutable nodes_per_run : int list;
  30              }
  31
  32 module NodeSummary =
  33 struct
  34   (* Pack into an integer the result of the is_* and has_ predicates
  35      for a given node *)
  36   type t = int
  37   let dummy = -1
  38   (*
  39     ...44443210
  40     ...4444 -> kind
  41     3 -> has_right
  42     2 -> has_left
  43     1 -> is_right
  44     0 -> is_left
  45   *)
  46   let is_left (s : t) : bool =
  47     s land 1 != 0
  48
  49   let is_right (s : t) : bool =
  50     s land 0b10 != 0
  51
  52   let has_left (s : t) : bool =
  53     s land 0b100 != 0
  54
  55   let has_right (s : t) : bool =
  56     s land 0b1000 != 0
  57
  58   let kind (s : t) : Tree.NodeKind.t =
  59     Obj.magic (s lsr 4)
  60
  61   let make is_left is_right has_left has_right kind =
  62     (int_of_bool is_left) lor
  63       ((int_of_bool is_right) lsl 1) lor
  64       ((int_of_bool has_left) lsl 2) lor
  65       ((int_of_bool has_right) lsl 3) lor
  66       ((Obj.magic kind) lsl 4)
  67 end
  68
  69 let dummy_set = StateSet.singleton State.dummy_state
  70
  71
  72
  73   IFDEF HTMLTRACE
  74   THEN
  75 type sat_array = StateSet.t array list
  76   DEFINE IFHTML(a,b) = (a)
  77   ELSE
  78 type sat_array = StateSet.t array
  79   DEFINE IFHTML(a,b) = (b)
  80   END
  81
  82 let unsafe_get a i =
  83   if i < 0 then StateSet.empty else
  84     Array.unsafe_get (IFHTML(List.hd a, a)) i
  85
  86 let unsafe_set a i v old_v =
  87   if v != old_v then
  88     Array.unsafe_set (IFHTML(List.hd a, a)) i v
  89
  90 type 'a run = {
  91   tree : 'a ;
  92      (* The argument of the run *)
  93   auto : Ata.t;
  94      (* The automaton to be run *)
  95   mutable sat: sat_array;
  96      (* A mapping from node preorders to states satisfied at that node *)
  97   mutable pass : int;
  98      (* Number of run we have performed *)
  99   mutable fetch_trans_cache : Ata.Formula.t Cache.N2.t;
 100      (* A cache from states * label to list of transitions *)
 101   mutable td_cache : StateSet.t Cache.N6.t;
 102   mutable bu_cache : StateSet.t Cache.N6.t;
 103      (* Two 6-way caches used during the top-down and bottom-up phase
 104         label * self-set * fc-set * ns-set * parent-set * node-shape -> self-set
 105      *)
 106   (*node_summaries: (int, int16_unsigned_elt, c_layout) Array1.t; *)
 107   node_summaries: Bytes.t;
 108   stats : stats;
 109 }
 110
 111 let dummy_form = Ata.Formula.stay State.dummy_state
 112
 113 let get_form run tag (q : State.t) =
 114   let auto = run.auto in
 115   let fetch_trans_cache = run.fetch_trans_cache in
 116   let stats = run.stats in
 117   let phi =
 118     stats.fetch_trans_cache_access <- stats.fetch_trans_cache_access + 1;
 119     Cache.N2.find fetch_trans_cache (tag.QName.id :> int) (q :> int)
 120   in
 121   if phi == dummy_form then
 122     let phi = Ata.get_form auto tag q in
 123     let () =
 124       stats.fetch_trans_cache_miss <- stats.fetch_trans_cache_miss + 1;
 125       Cache.N2.add
 126         fetch_trans_cache
 127         (tag.QName.id :> int)
 128         (q :> int) phi
 129     in phi
 130   else
 131     phi
 132
 133
 134
 135 let eval_form phi fcs nss ps ss summary =
 136   let open Ata in
 137   let rec loop phi =
 138     begin match Formula.expr phi with
 139     | Boolean.False -> false
 140     | Boolean.True -> true
 141     | Boolean.Atom (a, b) ->
 142       begin
 143         let open NodeSummary in
 144         match a.Atom.node with
 145         | Move (m, q) ->
 146           b && StateSet.mem q (
 147             match m with
 148               `First_child -> fcs
 149             | `Next_sibling -> nss
 150             | `Parent | `Previous_sibling -> ps
 151             | `Stay -> ss
 152           )
 153         | Is_first_child -> b == is_left summary
 154         | Is_next_sibling -> b == is_right summary
 155         | Is k -> b == (k == kind summary)
 156         | Has_first_child -> b == has_left summary
 157         | Has_next_sibling -> b == has_right summary
 158       end
 159     | Boolean.And(phi1, phi2) -> loop phi1 && loop phi2
 160     | Boolean.Or (phi1, phi2) -> loop phi1 || loop phi2
 161     end
 162   in
 163   loop phi
 164
 165
 166 let eval_trans_aux run tag summary fcs nss ps sat todo  =
 167   StateSet.fold (fun q (a_sat) ->
 168     let phi =
 169       get_form run tag q
 170     in
 171     if eval_form phi fcs nss ps a_sat summary then
 172       StateSet.add q a_sat
 173     else a_sat
 174   ) todo sat
 175
 176
 177 let rec eval_trans_fix run tag summary fcs nss ps sat todo  =
 178   let new_sat =
 179     eval_trans_aux run tag summary fcs nss ps sat todo
 180   in
 181   if new_sat == sat then sat else
 182     eval_trans_fix run tag summary fcs nss ps new_sat todo
 183
 184
 185 let eval_trans run trans_cache tag summary fcs nss ps ss todo =
 186   let stats = run.stats in
 187   let fcsid = (fcs.StateSet.id :> int) in
 188   let nssid = (nss.StateSet.id :> int) in
 189   let psid = (ps.StateSet.id :> int) in
 190   let ssid = (ss.StateSet.id :> int) in
 191   let tagid = (tag.QName.id :> int) in
 192
 193   let res = Cache.N6.find trans_cache tagid summary ssid fcsid nssid psid in
 194   stats.eval_trans_cache_access <- 1 + stats.eval_trans_cache_access;
 195   if res != dummy_set then
 196     res
 197   else let new_sat = if todo == StateSet.empty then ss else
 198              eval_trans_fix run tag summary fcs nss ps ss todo
 199     in
 200     stats.eval_trans_cache_miss <- 1 + stats.eval_trans_cache_miss;
 201     Cache.N6.add trans_cache tagid summary ssid fcsid nssid psid new_sat;
 202     new_sat
 203
 204
 205 module Make (T : Tree.S)  =
 206 struct
 207   module Tree : Tree.S with type node = T.node = T
 208   module ResultSet : Deque.S with type elem = Tree.node =
 209     Deque.Make (struct type t = Tree.node end)
 210
 211
 212   let make auto tree =
 213     let len = Tree.size tree in
 214     (* let ba = Array1.create int16_unsigned c_layout len in
 215        Array1.fill ba 0; *)
 216     let ba = Bytes.make len '\000' in
 217     {
 218       tree = tree;
 219       auto = auto;
 220       sat = (let a = Array.make len StateSet.empty in
 221              IFHTML([a], a));
 222       pass = 0;
 223       fetch_trans_cache = Cache.N2.create dummy_form;
 224       td_cache = Cache.N6.create dummy_set;
 225       bu_cache = Cache.N6.create dummy_set;
 226       node_summaries = ba;
 227       stats = {
 228         pass = 0;
 229         tree_size = len;
 230         fetch_trans_cache_access = 0;
 231         fetch_trans_cache_miss = 0;
 232         eval_trans_cache_access = 0;
 233         eval_trans_cache_miss = 0;
 234         nodes_per_run = [];
 235       }
 236     }
 237
 238
 239   let top_down2 run update_res =
 240     let num_visited = ref 0 in
 241     let i = run.pass in
 242     let tree = run.tree in
 243     let auto = run.auto in
 244     let states_by_rank = Ata.get_states_by_rank auto in
 245     let td_todo = states_by_rank.(i) in
 246     let bu_todo =
 247       if i == Array.length states_by_rank - 1 then StateSet.empty
 248       else
 249         states_by_rank.(i+1)
 250     in
 251     let run_sat = run.sat in
 252     let last_run = i >= Array.length states_by_rank - 2 in
 253     let rec common node parent parent_sat kont =
 254       if node == Tree.nil then StateSet.empty
 255       else begin
 256         incr num_visited;
 257         let tag = Tree.tag tree node in
 258         let node_id = Tree.preorder tree node in
 259         let fc = Tree.first_child tree node in
 260         let ns = Tree.next_sibling tree node in
 261         (* We enter the node from its parent *)
 262         let summary =
 263           let s = Char.code (Bytes.unsafe_get run.node_summaries node_id) in
 264           if  s != 0 then s else
 265             let s =
 266               NodeSummary.make
 267                 (node == (Tree.first_child tree parent)) (*is_left *)
 268                 (node == (Tree.next_sibling tree parent)) (*is_right *)
 269                 (fc != Tree.nil) (* has_left *)
 270                 (ns != Tree.nil) (* has_right *)
 271                 (Tree.kind tree node) (* kind *)
 272             in
 273             Bytes.unsafe_set run.node_summaries node_id (Char.chr s); s
 274         in
 275         let status0 = unsafe_get run_sat node_id in
 276         (* get the node_statuses for the first child, next sibling and parent *)
 277         (* evaluate the transitions with all this statuses *)
 278         let status1 =
 279           eval_trans run
 280             run.td_cache tag
 281             summary
 282             (unsafe_get run_sat (Tree.preorder tree fc))
 283             (unsafe_get run_sat (Tree.preorder tree ns))
 284             parent_sat
 285             status0 td_todo
 286         in
 287         kont summary tag parent_sat status0 status1 fc ns node node_id
 288       end
 289
 290     and kont_pure_td summary tag parent_sat status0 status1 fc ns node node_id =
 291       unsafe_set run_sat node_id status1 status0; (* write the td_states *)
 292       update_res false status1 node;
 293       if fc != Tree.nil then ignore (loop_td fc node status1);
 294       if ns == Tree.nil then StateSet.empty else loop_td ns node status1 (* tail call *)
 295     and kont_td_and_bu summary tag parent_sat status0 status1 fc ns node node_id =
 296       let fcs1 = if fc == Tree.nil then StateSet.empty else loop_td_and_bu fc node status1 in
 297       let nss1 = if ns == Tree.nil then StateSet.empty else loop_td_and_bu ns node status1 in
 298       let status2 =
 299         eval_trans run run.bu_cache tag
 300           summary fcs1
 301           nss1
 302           parent_sat
 303           status1 bu_todo
 304       in
 305       unsafe_set run_sat node_id status2 status0;
 306       status2
 307     and kont_td_and_bu_last summary tag parent_sat status0 status1 fc ns node node_id =
 308       let nss1 = if ns == Tree.nil then StateSet.empty else loop_td_and_bu_last ns node status1 in
 309       let fcs1 = if fc == Tree.nil then StateSet.empty else loop_td_and_bu_last fc node status1 in
 310       let status2 =
 311         eval_trans run run.bu_cache tag
 312           summary fcs1
 313           nss1
 314           parent_sat
 315           status1 bu_todo
 316       in
 317       unsafe_set run_sat node_id status2 status0;
 318       if status2 != StateSet.empty then update_res true status2 node;
 319       status2
 320     and loop_td node parent parent_sat =
 321       common node parent parent_sat kont_pure_td
 322     and loop_td_and_bu node parent parent_sat =
 323       common node parent parent_sat kont_td_and_bu
 324     and loop_td_and_bu_last node parent parent_sat =
 325       common node parent parent_sat kont_td_and_bu_last
 326     in
 327
 328     let _ =
 329       if bu_todo == StateSet.empty then
 330         loop_td (Tree.root tree) Tree.nil dummy_set
 331       else if last_run then
 332         loop_td_and_bu_last (Tree.root tree) Tree.nil dummy_set
 333       else
 334         loop_td_and_bu (Tree.root tree) Tree.nil dummy_set
 335     in
 336     run.pass <- run.pass + 2;
 337     run.stats.pass <- run.stats.pass + 1;
 338     run.stats.nodes_per_run <- !num_visited :: run.stats.nodes_per_run
 339
 340
 341   type res_op = Dummy | Prepend | Append | Nothing
 342
 343   let mk_update_result auto =
 344     let sel_states = Ata.get_selecting_states auto in
 345     let res = ResultSet.create () in
 346     let cache = Cache.N2.create Dummy in
 347     (fun prepend sat node ->
 348        let sat_id = (sat.StateSet.id :> int) in
 349        let prep_id : int = Obj.magic prepend in
 350        let op = Cache.N2.find cache prep_id sat_id in
 351        let op =
 352          if op == Dummy then
 353            let op =
 354              if StateSet.intersect sel_states sat then
 355                if prepend then
 356                  Prepend
 357                else Append
 358              else Nothing
 359            in
 360            let () = Cache.N2.add cache prep_id sat_id op in
 361            op
 362          else op
 363        in
 364        match op with
 365          Dummy | Nothing -> ()
 366        | Prepend -> ResultSet.push_front node res
 367        | Append -> ResultSet.push_back node res
 368                      (*
 369       if StateSet.intersect sel_states sat then begin
 370         if prepend then L.push_front node res else
 371           L.push_back node res
 372       end*)),
 373     (fun () -> res)
 374
 375
 376   let mk_update_full_result auto =
 377     let dummy = ResultSet.create () in
 378     let res_mapper = Cache.N1.create dummy in
 379     let () =
 380       StateSet.iter
 381         (fun q -> Cache.N1.add res_mapper (q :> int) (ResultSet.create()))
 382         (Ata.get_selecting_states auto)
 383     in
 384     (fun prepend sat node ->
 385       StateSet.iter
 386         (fun q ->
 387           let res = Cache.N1.find res_mapper (q :> int) in
 388           if res != dummy then begin
 389             if prepend then ResultSet.push_front node res
 390             else ResultSet.push_back node res
 391           end
 392         ) sat),
 393     (fun () ->
 394       StateSet.fold_right
 395         (fun q acc -> (q, Cache.N1.find res_mapper (q :> int))::acc)
 396         (Ata.get_selecting_states auto) [])
 397
 398   let prepare_run run list =
 399     let tree = run.tree in
 400     let auto = run.auto in
 401     let sat = IFHTML((List.hd run.sat), run.sat) in
 402     let sat0 = Ata.get_starting_states auto in
 403    ResultSet.iter (fun node ->
 404       let node_id = Tree.preorder tree node in
 405       sat.(node_id) <- sat0) list
 406
 407
 408   let compute_run auto tree nodes update_res =
 409     let run = make auto tree in
 410     prepare_run run nodes;
 411     let rank = Ata.get_max_rank auto in
 412     while run.pass <= rank do
 413       top_down2 run update_res;
 414       IFHTML((run.sat <- (Array.copy (List.hd run.sat)) :: run.sat), ());
 415       run.td_cache <- Cache.N6.create dummy_set;
 416       run.bu_cache <- Cache.N6.create dummy_set;
 417     done;
 418     IFHTML((run.sat <- List.tl run.sat), ());
 419     IFHTML(Html_trace.gen_trace auto run.sat (module T : Tree.S with type t = Tree.t) tree ,());
 420     run
 421
 422
 423   let last_stats = ref None
 424
 425   let full_eval auto tree nodes =
 426     let update_full,get_full = mk_update_full_result auto in
 427     let run = compute_run auto tree nodes update_full in
 428     last_stats := Some run.stats;
 429     get_full ()
 430
 431   let eval auto tree nodes =
 432     let update_res,get_res = mk_update_result auto in
 433     let run = compute_run auto tree nodes update_res in
 434     last_stats := Some run.stats;
 435     get_res ()
 436
 437   let stats () = match !last_stats with
 438       Some s -> s.nodes_per_run <- List.rev s.nodes_per_run;s
 439     | None -> failwith "Missing stats"
 440
 441 end