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       333333333333333210
  52       3333 -> kind
  53       2 -> has_right
  54       1 -> has_left
  55       0 -> is_left/is_right
  56     *)
  57      let is_left (s : t) : bool =
  58        s land 1 == 1
  59
  60      let is_right (s : t) : bool =
  61        s land 1 == 0
  62
  63      let has_left (s : t) : bool =
  64        (s lsr 1) land 1 == 1
  65
  66      let has_right (s : t) : bool =
  67        (s lsr 2) land 1 == 1
  68
  69      let kind (s : t) : Tree.NodeKind.t =
  70        Obj.magic (s lsr 3)
  71
  72      let make is_left has_left has_right kind =
  73        (int_of_bool is_left) lor
  74          ((int_of_bool has_left) lsl 1) lor
  75          ((int_of_bool has_right) lsl 2) lor
  76          ((Obj.magic kind) lsl 3)
  77    end
  78
  79    type node_status = {
  80      rank : int;
  81      sat : StateSet.t;  (* States that are satisfied at the current node *)
  82      todo : StateSet.t; (* States that remain to be proven *)
  83      (* For every node_status and automaton a,
  84         a.states - (sat U todo) = unsat *)
  85      summary : NodeSummary.t; (* Summary of the shape of the node *)
  86    }
  87 (* Describe what is kept at each node for a run *)
  88
  89    module NodeStatus =
  90      struct
  91        include Hcons.Make(struct
  92          type t = node_status
  93          let equal c d =
  94            c == d ||
  95              c.rank == d.rank &&
  96              c.sat == d.sat &&
  97              c.todo == d.todo &&
  98              c.summary == d.summary
  99
 100          let hash c =
 101            HASHINT4(c.rank,
 102                     (c.sat.StateSet.id :> int),
 103                     (c.todo.StateSet.id :> int),
 104                     c.summary)
 105        end
 106        )
 107        let print ppf s =
 108          fprintf ppf
 109            "{ rank: %i; sat: %a; todo: %a; summary: _ }"
 110            s.node.rank
 111            StateSet.print s.node.sat
 112            StateSet.print s.node.todo
 113      end
 114
 115    let dummy_status =
 116      NodeStatus.make {
 117        rank = -1;
 118        sat = StateSet.empty;
 119        todo = StateSet.empty;
 120        summary = NodeSummary.dummy;
 121      }
 122
 123
 124    type run = {
 125      tree : T.t ;
 126      (* The argument of the run *)
 127      auto : Ata.t;
 128      (* The automaton to be run *)
 129      status : NodeStatus.t array;
 130      (* A mapping from node preorders to NodeStatus *)
 131      mutable pass : int;
 132      mutable fetch_trans_cache : Ata.Formula.t Cache.N2.t;
 133      (* A cache from states * label to list of transitions *)
 134      mutable td_cache : NodeStatus.t Cache.N5.t;
 135      mutable bu_cache : NodeStatus.t Cache.N5.t;
 136    }
 137
 138
 139
 140    let dummy_form = Ata.Formula.stay State.dummy
 141
 142    let make auto tree =
 143      let len = T.size tree in
 144      {
 145        tree = tree;
 146        auto = auto;
 147        status = Array.create len dummy_status;
 148        pass = 0;
 149        fetch_trans_cache = Cache.N2.create dummy_form;
 150        td_cache = Cache.N5.create dummy_status;
 151        bu_cache = Cache.N5.create dummy_status;
 152      }
 153
 154    let get_status a i =
 155      if i < 0 then dummy_status else Array.get a i
 156
 157    let unsafe_get_status a i =
 158      if i < 0 then dummy_status else Array.unsafe_get a i
 159
 160 IFDEF HTMLTRACE
 161   THEN
 162 DEFINE IFTRACE(e) = (e)
 163   ELSE
 164 DEFINE IFTRACE(e) = ()
 165 END
 166
 167    let html tree node i config msg =
 168      let config = config.NodeStatus.node in
 169      Html.trace ~msg:msg
 170        (T.preorder tree node) i
 171        config.todo
 172        config.sat
 173
 174
 175
 176    let debug msg tree node i config =
 177      let config = config.NodeStatus.node in
 178      eprintf
 179        "DEBUG:%s node: %i\nsat: %a\ntodo: %a\nround: %i\n"
 180        msg
 181        (T.preorder tree node)
 182        StateSet.print config.sat
 183        StateSet.print config.todo
 184        i
 185
 186    let get_form fetch_trans_cache auto tag q =
 187      let phi =
 188        incr fetch_trans_cache_access;
 189        Cache.N2.find fetch_trans_cache (tag.QName.id :> int) (q :> int)
 190      in
 191      if phi == dummy_form then
 192        let phi = Ata.get_form auto tag q in
 193        let () =
 194          Cache.N2.add
 195            fetch_trans_cache
 196            (tag.QName.id :> int)
 197            (q :> int) phi
 198        in phi
 199      else begin
 200        incr fetch_trans_cache_hit;
 201        phi
 202      end
 203
 204    type trivalent = False | True | Unknown
 205    let of_bool = function false -> False | true -> True
 206    let or_ t1 t2 =
 207      match t1 with
 208        False -> t2
 209      | True -> True
 210      | Unknown -> if t2 == True then True else Unknown
 211
 212    let and_ t1 t2 =
 213      match t1 with
 214        False -> False
 215      | True -> t2
 216      | Unknown -> if t2 == False then False else Unknown
 217
 218  (* Define as macros to get lazyness *)
 219 DEFINE OR_(t1,t2) =
 220      match t1 with
 221        False -> (t2)
 222      | True -> True
 223      | Unknown -> if (t2) == True then True else Unknown
 224
 225 DEFINE AND_(t1,t2) =
 226      match t1 with
 227        False -> False
 228      | True -> (t2)
 229      | Unknown -> if (t2) == False then False else Unknown
 230
 231
 232    let eval_form phi fcs nss ps ss summary =
 233      let open Ata in
 234          let rec loop phi =
 235            begin match Formula.expr phi with
 236            | Boolean.False -> False
 237            | Boolean.True -> True
 238            | Boolean.Atom (a, b) ->
 239                begin
 240                  let open NodeSummary in
 241                      match a.Atom.node with
 242                      | Move (m, q) ->
 243                          let down, ({ NodeStatus.node = n_sum; _ } as sum) =
 244                            match m with
 245                              `First_child -> true, fcs
 246                            | `Next_sibling -> true, nss
 247                            | `Parent | `Previous_sibling -> false, ps
 248                            | `Stay -> false, ss
 249                          in
 250                          if sum == dummy_status
 251                            || (down && n_sum.rank < ss.NodeStatus.node.rank)
 252                            || StateSet.mem q n_sum.todo then
 253                            Unknown
 254                          else
 255                            of_bool (b == StateSet.mem q n_sum.sat)
 256                      | Is_first_child -> of_bool (b == is_left summary)
 257                      | Is_next_sibling -> of_bool (b == is_right summary)
 258                      | Is k -> of_bool (b == (k == kind summary))
 259                      | Has_first_child -> of_bool (b == has_left summary)
 260                      | Has_next_sibling -> of_bool (b == has_right summary)
 261                end
 262            | Boolean.And(phi1, phi2) -> AND_ (loop phi1, loop phi2)
 263            | Boolean.Or (phi1, phi2) -> OR_ (loop phi1, loop phi2)
 264            end
 265          in
 266          loop phi
 267
 268
 269    let eval_trans_aux auto fetch_trans_cache tag fcs nss ps old_status =
 270      let { sat = old_sat;
 271            todo = old_todo;
 272            summary = old_summary } as os_node = old_status.NodeStatus.node
 273      in
 274      let sat, todo =
 275        StateSet.fold (fun q ((a_sat, a_todo) as acc) ->
 276          let phi =
 277            get_form fetch_trans_cache auto tag q
 278          in
 279
 280          let v = eval_form phi fcs nss ps old_status old_summary in
 281          match v with
 282            True -> StateSet.add q a_sat, a_todo
 283          | False -> acc
 284          | Unknown -> a_sat, StateSet.add q a_todo
 285        ) old_todo (old_sat, StateSet.empty)
 286      in
 287      if old_sat != sat || old_todo != todo then
 288        NodeStatus.make { os_node with sat; todo }
 289      else old_status
 290
 291
 292    let rec eval_trans_fix auto fetch_trans_cache tag fcs nss ps old_status =
 293      let new_status =
 294        eval_trans_aux auto fetch_trans_cache tag fcs nss ps old_status
 295      in
 296      if new_status == old_status then old_status else
 297        eval_trans_fix auto fetch_trans_cache tag fcs nss ps new_status
 298
 299
 300    let eval_trans auto fetch_trans_cache td_cache tag fcs nss ps ss =
 301      let fcsid = (fcs.NodeStatus.id :> int) in
 302      let nssid = (nss.NodeStatus.id :> int) in
 303      let psid = (ps.NodeStatus.id :> int) in
 304      let ssid = (ss.NodeStatus.id :> int) in
 305      let tagid = (tag.QName.id :> int) in
 306      let res = Cache.N5.find td_cache tagid ssid fcsid nssid psid in
 307      incr eval_trans_cache_access;
 308      if res != dummy_status then begin incr eval_trans_cache_hit; res end
 309      else let new_status = eval_trans_fix auto fetch_trans_cache tag fcs nss ps ss in
 310           Cache.N5.add td_cache tagid ssid fcsid nssid psid new_status;
 311           new_status
 312
 313   let top_down run =
 314     let i = run.pass in
 315     let tree = run.tree in
 316     let auto = run.auto in
 317     let status = run.status in
 318     let fetch_trans_cache = run.fetch_trans_cache in
 319     let td_cache = run.td_cache in
 320     let bu_cache = run.bu_cache in
 321     let states_by_rank = Ata.get_states_by_rank auto in
 322     let td_todo = states_by_rank.(i) in
 323     let bu_todo = if i + 1 = Array.length states_by_rank then StateSet.empty
 324       else
 325         states_by_rank.(i+1)
 326     in
 327     let rec loop_td_and_bu node =
 328       if node == T.nil then () else begin
 329         let node_id = T.preorder tree node in
 330         let parent = T.parent tree node in
 331         let fc = T.first_child tree node in
 332         let fc_id = T.preorder tree fc in
 333         let ns = T.next_sibling tree node in
 334         let ns_id = T.preorder tree ns in
 335         let tag = T.tag tree node in
 336         (* We enter the node from its parent *)
 337         let status0 =
 338           let c = unsafe_get_status status node_id in
 339           if c.NodeStatus.node.rank < i then
 340             (* first time we visit the node during this run *)
 341             NodeStatus.make
 342               { rank = i;
 343                 sat = c.NodeStatus.node.sat;
 344                 todo = td_todo;
 345                 summary =
 346                   let summary = c.NodeStatus.node.summary in
 347                   if summary != NodeSummary.dummy then summary
 348                   else
 349                     NodeSummary.make
 350                       (node != T.next_sibling tree parent)
 351                       (fc != T.nil) (* has_left *)
 352                       (ns != T.nil) (* has_right *)
 353                       (T.kind tree node) (* kind *)
 354               }
 355           else c
 356         in
 357         (* get the node_statuses for the first child, next sibling and parent *)
 358         let ps = unsafe_get_status status (T.preorder tree parent) in
 359         let fcs = unsafe_get_status status fc_id in
 360         let nss = unsafe_get_status status ns_id in
 361         (* evaluate the transitions with all this statuses *)
 362         let status1 =
 363           if status0.NodeStatus.node.todo == StateSet.empty then status0
 364           else begin
 365             let status1 = eval_trans auto fetch_trans_cache td_cache tag fcs nss ps status0 in
 366           (* update the cache if the status of the node changed *)
 367             if status1 != status0 then status.(node_id) <- status1;
 368             status1
 369           end
 370         in
 371         (* recursively traverse the first child *)
 372         let () = loop_td_and_bu fc in
 373         (* here we re-enter the node from its first child,
 374            get the new status of the first child *)
 375         let fcs1 = unsafe_get_status status fc_id in
 376         (* update the status *)
 377         let status1 = if status1.NodeStatus.node.rank < i then
 378             NodeStatus.make { status1.NodeStatus.node with
 379               rank = i;
 380               todo = bu_todo }
 381           else
 382             status1
 383         in
 384         let status2 =
 385           if status1.NodeStatus.node.todo == StateSet.empty then status1
 386           else begin
 387             let status2 = eval_trans auto fetch_trans_cache bu_cache tag fcs1 nss ps status1 in
 388             if status2 != status1 then status.(node_id) <- status2;
 389             status2
 390           end
 391         in
 392         let () = loop_td_and_bu ns in
 393         let nss1 = unsafe_get_status status ns_id in
 394         if status2.NodeStatus.node.todo != StateSet.empty then
 395           let status3 = eval_trans auto fetch_trans_cache bu_cache tag fcs1 nss1 ps status2 in
 396           if status3 != status2 then status.(node_id) <- status3
 397       end
 398     and loop_td_only node =
 399       if node == T.nil then () else begin
 400         let node_id = T.preorder tree node in
 401         let parent = T.parent tree node in
 402         let fc = T.first_child tree node in
 403         let fc_id = T.preorder tree fc in
 404         let ns = T.next_sibling tree node in
 405         let ns_id = T.preorder tree ns in
 406         let tag = T.tag tree node in
 407         (* We enter the node from its parent *)
 408         let status0 =
 409           let c = unsafe_get_status status node_id in
 410           if c.NodeStatus.node.rank < i then
 411             (* first time we visit the node during this run *)
 412             NodeStatus.make
 413               { rank = i;
 414                 sat = c.NodeStatus.node.sat;
 415                 todo = td_todo;
 416                 summary =
 417                   let summary = c.NodeStatus.node.summary in
 418                   if summary != NodeSummary.dummy then summary
 419                   else
 420                     NodeSummary.make
 421                       (node != T.next_sibling tree parent)
 422                       (fc != T.nil) (* has_left *)
 423                       (ns != T.nil) (* has_right *)
 424                       (T.kind tree node) (* kind *)
 425               }
 426           else c
 427         in
 428         (* get the node_statuses for the first child, next sibling and parent *)
 429         let ps = unsafe_get_status status (T.preorder tree parent) in
 430         let fcs = unsafe_get_status status fc_id in
 431         let nss = unsafe_get_status status ns_id in
 432         (* evaluate the transitions with all this statuses *)
 433         if status0.NodeStatus.node.todo != StateSet.empty then begin
 434           let status1 = eval_trans auto fetch_trans_cache td_cache tag fcs nss ps status0 in
 435           (* update the cache if the status of the node changed *)
 436           if status1 != status0 then status.(node_id) <- status1;
 437         end;
 438         (* recursively traverse the first child *)
 439         loop_td_only fc;
 440         loop_td_only ns
 441       end
 442     in
 443     if bu_todo == StateSet.empty then loop_td_only (T.root tree)
 444     else loop_td_and_bu (T.root tree)
 445
 446
 447   let get_results run =
 448     let cache = run.status in
 449     let auto = run.auto in
 450     let tree = run.tree in
 451     let sel_states = Ata.get_selecting_states auto in
 452     let rec loop node acc =
 453       if node == T.nil then acc
 454       else
 455         let acc0 = loop (T.next_sibling tree node) acc in
 456         let acc1 = loop (T.first_child tree node) acc0 in
 457
 458         if StateSet.intersect
 459           cache.(T.preorder tree node).NodeStatus.node.sat
 460           sel_states then node::acc1
 461         else acc1
 462     in
 463     loop (T.root tree) []
 464
 465
 466   let get_full_results run =
 467     let cache = run.status in
 468     let auto = run.auto in
 469     let tree = run.tree in
 470     let res_mapper = Hashtbl.create MED_H_SIZE in
 471     let () =
 472       StateSet.iter
 473         (fun q -> Hashtbl.add res_mapper q [])
 474         (Ata.get_selecting_states auto)
 475     in
 476     let dummy = [ T.nil ] in
 477     let res_mapper = Cache.N1.create dummy in
 478     let () =
 479       StateSet.iter
 480         (fun q -> Cache.N1.add res_mapper (q :> int) [])
 481         (Ata.get_selecting_states auto)
 482     in
 483     let rec loop node =
 484       if node != T.nil then
 485         let () = loop (T.next_sibling tree node) in
 486         let () = loop (T.first_child tree node) in
 487         StateSet.iter
 488           (fun q ->
 489             let res = Cache.N1.find res_mapper (q :> int) in
 490             if res != dummy then
 491               Cache.N1.add res_mapper (q :> int) (node::res)
 492           )
 493           cache.(T.preorder tree node).NodeStatus.node.sat
 494     in
 495     loop (T.root tree);
 496     (StateSet.fold_right
 497        (fun q acc -> (q, Cache.N1.find res_mapper (q :> int))::acc)
 498        (Ata.get_selecting_states auto) [])
 499
 500
 501   let prepare_run run list =
 502     let tree = run.tree in
 503     let auto = run.auto in
 504     let status = run.status in
 505     List.iter (fun node ->
 506       let parent = T.parent tree node in
 507       let fc = T.first_child tree node in
 508       let ns = T.next_sibling tree node in
 509       let status0 =
 510         NodeStatus.make
 511           { rank = 0;
 512             sat = Ata.get_starting_states auto;
 513             todo =
 514               StateSet.diff (Ata.get_states auto) (Ata.get_starting_states auto);
 515             summary = NodeSummary.make
 516               (node != T.next_sibling tree parent) (* is_left *)
 517               (fc != T.nil) (* has_left *)
 518               (ns != T.nil) (* has_right *)
 519               (T.kind tree node) (* kind *)
 520           }
 521       in
 522       let node_id = T.preorder tree node in
 523       status.(node_id) <- status0) list
 524
 525   let tree_size = ref 0
 526   let pass = ref 0
 527   let compute_run auto tree nodes =
 528     pass := 0;
 529     tree_size := T.size tree;
 530     let run = make auto tree in
 531     prepare_run run nodes;
 532     for i = 0 to Ata.get_max_rank auto do
 533       top_down run;
 534       run.pass <- run.pass + 1;
 535       run.td_cache <- Cache.N5.create dummy_status;
 536       run.bu_cache <- Cache.N5.create dummy_status;
 537     done;
 538     pass := Ata.get_max_rank auto + 1;
 539     IFTRACE(Html.gen_trace auto (module T : Tree.S with type t = T.t) tree);
 540
 541     run
 542
 543   let full_eval auto tree nodes =
 544     let r = compute_run auto tree nodes in
 545     get_full_results r
 546
 547   let eval auto tree nodes =
 548     let r = compute_run auto tree nodes in
 549     get_results r
 550
 551   let stats () = {
 552     tree_size = !tree_size;
 553     run = !pass;
 554     fetch_trans_cache_access = !fetch_trans_cache_access;
 555     fetch_trans_cache_hit = !fetch_trans_cache_hit;
 556     eval_trans_cache_access = !eval_trans_cache_access;
 557     eval_trans_cache_hit = !eval_trans_cache_hit;
 558   }
 559
 560 end