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         let () = Logger.msg `STATS "Run %i, Node %a, %a@\n"
 358           i QName.print tag NodeStatus.print status0
 359         in
 360         (* get the node_statuses for the first child, next sibling and parent *)
 361         let ps = unsafe_get_status status (T.preorder tree parent) in
 362         let fcs = unsafe_get_status status fc_id in
 363         let nss = unsafe_get_status status ns_id in
 364         (* evaluate the transitions with all this statuses *)
 365         let status1 =
 366           if status0.NodeStatus.node.todo == StateSet.empty then status0
 367           else begin
 368             let status1 = eval_trans auto fetch_trans_cache td_cache tag fcs nss ps status0 in
 369           (* update the cache if the status of the node changed *)
 370             if status1 != status0 then status.(node_id) <- status1;
 371             status1
 372           end
 373         in
 374         let () = Logger.msg `STATS "Run %i, Node %a, %a@\n"
 375           i QName.print tag NodeStatus.print status1
 376         in
 377         (* recursively traverse the first child *)
 378         let () = loop_td_and_bu fc in
 379         (* here we re-enter the node from its first child,
 380            get the new status of the first child *)
 381         let fcs1 = unsafe_get_status status fc_id in
 382         (* update the status *)
 383         let status1 = if status1.NodeStatus.node.rank < i+1 then
 384             NodeStatus.make { status1.NodeStatus.node with
 385               rank = i+1;
 386               todo = bu_todo }
 387           else
 388             status1
 389         in
 390         let status2 =
 391           if status1.NodeStatus.node.todo == StateSet.empty then status1
 392           else begin
 393             let status2 = eval_trans auto fetch_trans_cache bu_cache tag fcs1 nss ps status1 in
 394             if status2 != status1 then status.(node_id) <- status2;
 395             status2
 396           end
 397         in
 398         let () = Logger.msg `STATS "Run %i, Node %a, %a@\n"
 399           (i+1) QName.print tag NodeStatus.print status2
 400         in
 401         let () = loop_td_and_bu ns in
 402         let nss1 = unsafe_get_status status ns_id in
 403         if status2.NodeStatus.node.todo != StateSet.empty then
 404           let status3 = eval_trans auto fetch_trans_cache bu_cache tag fcs1 nss1 ps status2 in
 405           let () = Logger.msg `STATS "Run %i, Node %a, %a@\n"
 406             (i+1) QName.print tag NodeStatus.print status3
 407           in
 408
 409           if status3 != status2 then status.(node_id) <- status3
 410       end
 411     and loop_td_only node =
 412       if node == T.nil then () else begin
 413         let node_id = T.preorder tree node in
 414         let parent = T.parent tree node in
 415         let fc = T.first_child tree node in
 416         let fc_id = T.preorder tree fc in
 417         let ns = T.next_sibling tree node in
 418         let ns_id = T.preorder tree ns in
 419         let tag = T.tag tree node in
 420         (* We enter the node from its parent *)
 421         let status0 =
 422           let c = unsafe_get_status status node_id in
 423           if c.NodeStatus.node.rank < i then
 424             (* first time we visit the node during this run *)
 425             NodeStatus.make
 426               { rank = i;
 427                 sat = c.NodeStatus.node.sat;
 428                 todo = td_todo;
 429                 summary =
 430                   let summary = c.NodeStatus.node.summary in
 431                   if summary != NodeSummary.dummy then summary
 432                   else
 433                     NodeSummary.make
 434                       (node != T.next_sibling tree parent)
 435                       (fc != T.nil) (* has_left *)
 436                       (ns != T.nil) (* has_right *)
 437                       (T.kind tree node) (* kind *)
 438               }
 439           else c
 440         in
 441         let () = Logger.msg `STATS "Run %i, Node %a, %a@\n"
 442           (i) QName.print tag NodeStatus.print status0
 443         in
 444
 445         (* get the node_statuses for the first child, next sibling and parent *)
 446         let ps = unsafe_get_status status (T.preorder tree parent) in
 447         let fcs = unsafe_get_status status fc_id in
 448         let nss = unsafe_get_status status ns_id in
 449         (* evaluate the transitions with all this statuses *)
 450         if status0.NodeStatus.node.todo != StateSet.empty then begin
 451           let status1 = eval_trans auto fetch_trans_cache td_cache tag fcs nss ps status0 in
 452           (* update the cache if the status of the node changed *)
 453           let () = Logger.msg `STATS "Run %i, Node %a, %a@\n"
 454             (i) QName.print tag NodeStatus.print status1
 455           in
 456
 457           if status1 != status0 then status.(node_id) <- status1;
 458         end;
 459         (* recursively traverse the first child *)
 460         loop_td_only fc;
 461         loop_td_only ns
 462       end
 463     in
 464     if bu_todo == StateSet.empty then
 465       let () = loop_td_only (T.root tree) in
 466       run.pass <- run.pass + 1
 467     else
 468       let () = loop_td_and_bu (T.root tree) in
 469       run.pass <- run.pass + 2
 470
 471
 472   let get_results run =
 473     let cache = run.status in
 474     let auto = run.auto in
 475     let tree = run.tree in
 476     let sel_states = Ata.get_selecting_states auto in
 477     let rec loop node acc =
 478       if node == T.nil then acc
 479       else
 480         let acc0 = loop (T.next_sibling tree node) acc in
 481         let acc1 = loop (T.first_child tree node) acc0 in
 482
 483         if StateSet.intersect
 484           cache.(T.preorder tree node).NodeStatus.node.sat
 485           sel_states then node::acc1
 486         else acc1
 487     in
 488     loop (T.root tree) []
 489
 490
 491   let get_full_results run =
 492     let cache = run.status in
 493     let auto = run.auto in
 494     let tree = run.tree in
 495     let res_mapper = Hashtbl.create MED_H_SIZE in
 496     let () =
 497       StateSet.iter
 498         (fun q -> Hashtbl.add res_mapper q [])
 499         (Ata.get_selecting_states auto)
 500     in
 501     let dummy = [ T.nil ] in
 502     let res_mapper = Cache.N1.create dummy in
 503     let () =
 504       StateSet.iter
 505         (fun q -> Cache.N1.add res_mapper (q :> int) [])
 506         (Ata.get_selecting_states auto)
 507     in
 508     let rec loop node =
 509       if node != T.nil then
 510         let () = loop (T.next_sibling tree node) in
 511         let () = loop (T.first_child tree node) in
 512         StateSet.iter
 513           (fun q ->
 514             let res = Cache.N1.find res_mapper (q :> int) in
 515             if res != dummy then
 516               Cache.N1.add res_mapper (q :> int) (node::res)
 517           )
 518           cache.(T.preorder tree node).NodeStatus.node.sat
 519     in
 520     loop (T.root tree);
 521     (StateSet.fold_right
 522        (fun q acc -> (q, Cache.N1.find res_mapper (q :> int))::acc)
 523        (Ata.get_selecting_states auto) [])
 524
 525
 526   let prepare_run run list =
 527     let tree = run.tree in
 528     let auto = run.auto in
 529     let status = run.status in
 530     List.iter (fun node ->
 531       let parent = T.parent tree node in
 532       let fc = T.first_child tree node in
 533       let ns = T.next_sibling tree node in
 534       let status0 =
 535         NodeStatus.make
 536           { rank = 0;
 537             sat = Ata.get_starting_states auto;
 538             todo =
 539               StateSet.diff (Ata.get_states auto) (Ata.get_starting_states auto);
 540             summary = NodeSummary.make
 541               (node != T.next_sibling tree parent) (* is_left *)
 542               (fc != T.nil) (* has_left *)
 543               (ns != T.nil) (* has_right *)
 544               (T.kind tree node) (* kind *)
 545           }
 546       in
 547       let node_id = T.preorder tree node in
 548       status.(node_id) <- status0) list
 549
 550   let tree_size = ref 0
 551   let pass = ref 0
 552   let compute_run auto tree nodes =
 553     pass := 0;
 554     tree_size := T.size tree;
 555     let run = make auto tree in
 556     prepare_run run nodes;
 557     let rank = Ata.get_max_rank auto in
 558     while run.pass <= rank do
 559       top_down run;
 560       run.td_cache <- Cache.N5.create dummy_status;
 561       run.bu_cache <- Cache.N5.create dummy_status;
 562     done;
 563     pass := Ata.get_max_rank auto + 1;
 564     IFTRACE(Html.gen_trace auto (module T : Tree.S with type t = T.t) tree);
 565
 566     run
 567
 568   let full_eval auto tree nodes =
 569     let r = compute_run auto tree nodes in
 570     get_full_results r
 571
 572   let eval auto tree nodes =
 573     let r = compute_run auto tree nodes in
 574     get_results r
 575
 576   let stats () = {
 577     tree_size = !tree_size;
 578     run = !pass;
 579     fetch_trans_cache_access = !fetch_trans_cache_access;
 580     fetch_trans_cache_hit = !fetch_trans_cache_hit;
 581     eval_trans_cache_access = !eval_trans_cache_access;
 582     eval_trans_cache_hit = !eval_trans_cache_hit;
 583   }
 584
 585 end