src/run.ml

   1 (***********************************************************************)
   2 (*                                                                     *)
   3 (*                               TAToo                                 *)
   4 (*                                                                     *)
   5 (*                   Lucca Hirschi, LRI UMR8623                        *)
   6 (*                   Université Paris-Sud & CNRS                       *)
   7 (*                                                                     *)
   8 (*  Copyright 2010-2012 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
  18 module Node  =
  19 struct
  20   type t = int
  21   let hash n = n
  22   let compare = (-)
  23   let equal = (=)
  24 end
  25
  26 module NodeHash = Hashtbl.Make (Node)
  27
  28 type t = (StateSet.t*StateSet.t) NodeHash.t
  29 (** Map from nodes to query and recognizing states *)
  30 (* Note that we do not consider nil nodes *)
  31
  32 exception Oracle_fail
  33 exception Over_max_fail
  34 exception Max_fail
  35
  36
  37 (* Hash Consign modules *)
  38 open Hconsed_run
  39 module HashOracle = Hashtbl.Make(Oracle_fixpoint)
  40 module HashRun = Hashtbl.Make(Run_fixpoint)
  41
  42 (* Mapped sets for leaves *)
  43 let map_leaf asta = (Asta.bot_states_s asta, StateSet.empty)
  44
  45 let num_call_oracle_fixpoint = ref 0
  46 let num_miss_oracle_fixpoint = ref 0
  47 let () = at_exit(fun () -> Format.fprintf Format.err_formatter
  48   "Num: call %d, Num Miss: %d\n%!" (!num_call_oracle_fixpoint)
  49   (!num_miss_oracle_fixpoint))
  50
  51 (* Build the Oracle *)
  52 let rec bu_oracle asta run tree tnode hashOracle hashEval =
  53   let node = Tree.preorder tree tnode in
  54   if Tree.is_leaf tree tnode
  55   then
  56     if tnode == Tree.nil
  57     then ()
  58     else NodeHash.add run node (map_leaf asta)
  59   else
  60     let tfnode = Tree.first_child_x tree tnode
  61     and tnnode = Tree.next_sibling tree tnode in
  62     let fnode,nnode =                            (* their preorders *)
  63       (Tree.preorder tree tfnode, Tree.preorder tree tnnode) in
  64     begin
  65       bu_oracle asta run tree tfnode hashOracle hashEval;
  66       bu_oracle asta run tree tnnode hashOracle hashEval;
  67       (* add states which satisfy a transition *)
  68       let rec result set qfr qnr flag = function
  69         | [] -> set,flag
  70         | (q,form) :: tl ->
  71           if Formula.eval_form (set,qfr,qnr) form hashEval
  72           then
  73             if StateSet.mem q set
  74             then result set qfr qnr 0 tl
  75             else result (StateSet.add q set) qfr qnr 1 tl
  76           else result set qfr qnr 0 tl in
  77       (* compute the fixed point of states of node *)
  78       let rec fix_point set_i qfr qnr list_tr t =
  79         incr num_call_oracle_fixpoint;
  80         try HashOracle.find hashOracle (set_i, qfr, qnr, list_tr, t)
  81         with _ ->
  82           incr num_miss_oracle_fixpoint;
  83           let set,flag = result set_i qfr qnr 0 list_tr in
  84           HashOracle.add hashOracle (set_i,qfr,qnr,list_tr,t) (set); (* todo: Think about this position *)
  85           if flag = 0
  86           then set
  87           else fix_point set qfr qnr list_tr t in
  88       let q_rec n =                     (* compute the set for child/sibling *)
  89         try NodeHash.find run n
  90         with Not_found -> map_leaf asta in
  91       let (_,qfr),(_,qnr) = q_rec fnode,q_rec nnode (* computed in rec call *)
  92       and lab = Tree.tag tree tnode in
  93       let _,list_tr = Asta.transitions_lab asta lab in (*only reco. tran.*)
  94      NodeHash.add run node (StateSet.empty,
  95                             fix_point StateSet.empty qfr qnr list_tr lab)
  96     end
  97
  98 let num_call_over_max_fixpoint = ref 0
  99 let num_miss_over_max_fixpoint = ref 0
 100 let () = at_exit(fun () -> Format.fprintf Format.err_formatter
 101   "Num: call %d, Num Miss: %d\n%!" (!num_call_over_max_fixpoint)
 102   (!num_miss_over_max_fixpoint))
 103
 104
 105 (* Build the over-approx. of the maximal run *)
 106 let rec bu_over_max asta run tree tnode hashOver hashInfer =
 107   if (Tree.is_leaf tree tnode)      (* BU_oracle has already created the map *)
 108   then
 109     ()
 110   else
 111     let tfnode = Tree.first_child_x tree tnode
 112     and tnnode = Tree.next_sibling tree tnode in
 113     begin
 114       bu_over_max asta run tree tfnode hashOver hashInfer;
 115       bu_over_max asta run tree tnnode hashOver hashInfer;
 116       let (fnode,nnode) =
 117         (Tree.preorder tree tfnode, Tree.preorder tree tnnode)
 118       and node = Tree.preorder tree tnode in
 119       let q_rec n =
 120         try NodeHash.find run n
 121         with Not_found -> map_leaf asta in
 122       let qf,qn = q_rec fnode,q_rec nnode in
 123       let lab = Tree.tag tree tnode in
 124       let list_tr,_ = Asta.transitions_lab asta lab (* only take query st. *)
 125       and _,resultr = try NodeHash.find run node
 126         with _ -> raise Over_max_fail in
 127       let rec result set qf qn flag list_tr = function
 128         | [] -> if flag = 0 then set else result set qf qn 0 list_tr list_tr
 129         | (q,form) :: tl ->
 130           if StateSet.mem q set
 131           then result set qf qn 0 list_tr tl
 132           else if Formula.infer_form (set,resultr) qf qn form hashInfer
 133           then result (StateSet.add q set) qf qn 1 list_tr tl
 134           else result set qf qn 0 list_tr tl in
 135       let result_set () =
 136         incr num_call_over_max_fixpoint;
 137         try HashRun.find hashOver ((StateSet.empty,resultr),qf,qn,list_tr,lab)
 138         with _ ->
 139           incr num_miss_over_max_fixpoint;
 140           let res = result StateSet.empty qf qn 0 list_tr list_tr in
 141                   HashRun.add hashOver
 142                     ((StateSet.empty,resultr), qf,qn,list_tr,lab) res;
 143                   res in
 144       (* we keep the old recognizing states set *)
 145       NodeHash.replace run node (result_set(), resultr)
 146     end
 147
 148 let num_call_tp_max_fixpoint = ref 0
 149 let num_miss_tp_max_fixpoint = ref 0
 150 let () = at_exit(fun () -> Format.fprintf Format.err_formatter
 151   "Num: call %d, Num Miss: %d\n%!" (!num_call_tp_max_fixpoint)
 152   (!num_miss_tp_max_fixpoint))
 153
 154
 155 (* Build the maximal run *)
 156 let rec tp_max asta run tree tnode hashMax hashInfer =
 157   if (Tree.is_leaf tree tnode)      (* BU_oracle has already created the map *)
 158   then
 159     ()
 160   else
 161     let node = Tree.preorder tree tnode
 162     and tfnode = Tree.first_child_x tree tnode
 163     and tnnode = Tree.next_sibling tree tnode in
 164     let (fnode,nnode) =
 165       (Tree.preorder tree tfnode, Tree.preorder tree tnnode) in
 166     begin
 167       if tnode == Tree.root tree        (* we must intersect with top states *)
 168       then let setq,_  = try NodeHash.find run node
 169         with _ -> raise Max_fail in
 170            NodeHash.replace run node
 171              ((StateSet.inter (Asta.top_states_s asta) setq),StateSet.empty)
 172       else ();
 173       let q_rec n =
 174         try NodeHash.find run n
 175         with Not_found -> map_leaf asta in
 176       let qf,qn = q_rec fnode,q_rec nnode in
 177       let lab = Tree.tag tree tnode in
 178       let list_tr,_ = Asta.transitions_lab asta lab in (* only take query. *)
 179       let (self_q,self_r) = try NodeHash.find run node
 180         with Not_found -> raise Max_fail in
 181
 182       (* We must compute again accepting states from self transitions since
 183          previous calls of tp_max may remove them *)
 184       let rec result_q self_q queue = function (* for initializing the queue *)
 185         | [] -> self_q,queue
 186         | (q,form) :: tl ->
 187           if (StateSet.mem q self_q)
 188           then begin
 189             let q_cand,_,_ = Formula.st form in
 190             StateSet.iter (fun x -> Queue.push x queue) q_cand;
 191             result_q (StateSet.add q self_q) queue tl;
 192           end
 193           else result_q self_q queue tl
 194       and result_st_q self_q queue flag = function (*for computing the fixed p*)
 195         | [] -> flag,queue
 196         | form :: tl ->
 197           if Formula.infer_form (self_q,self_r) qf qn form hashInfer
 198           then begin
 199             let q_cand,_,_ = Formula.st form in
 200             StateSet.iter (fun x -> Queue.push x queue) q_cand;
 201             result_st_q self_q queue 1 tl;
 202           end
 203           else result_st_q self_q queue flag tl in
 204       let rec comp_acc_self self_q_i queue = (* compute the fixed point *)
 205         if Queue.is_empty queue              (* todo: to be hconsigned? *)
 206         then self_q_i
 207         else
 208           let q = Queue.pop queue in
 209           let list_q,_ = Asta.transitions_st_lab asta q lab in
 210           let flag,queue = result_st_q self_q_i queue 0 list_q in
 211           let self_q = if flag = 1 then StateSet.add q self_q_i else self_q_i in
 212           comp_acc_self self_q queue in
 213
 214       let self,queue_init = result_q self_q (Queue.create()) list_tr in
 215       let self_q = comp_acc_self self_q queue_init in
 216       NodeHash.replace run node (self_q,self_r);
 217       (* From now, the correct set of states is mapped to (self) node! *)
 218       let rec result self qf qn = function
 219         | [] -> []
 220         | (q,form) :: tl ->
 221           if (StateSet.mem q (fst self)) && (* infers & trans. can start here *)
 222             (Formula.infer_form self qf qn form hashInfer)
 223           then form :: (result self qf qn tl)
 224           else result self qf qn tl in
 225       let list_form =
 226         incr num_call_tp_max_fixpoint;
 227         try HashRun.find hashMax ((self_q,self_r),qf,qn,list_tr,lab)
 228         with _ ->
 229           incr num_miss_tp_max_fixpoint;
 230           let res = result (self_q,self_r) qf qn list_tr in
 231           HashRun.add hashMax ((self_q,self_r),qf,qn,list_tr,lab) res;
 232           res in
 233       (* compute states occuring in transition candidates *)
 234       let rec add_st (ql,qr) = function
 235         | [] -> ql,qr
 236         | f :: tl -> let sqs,sql,sqr = Formula.st f in
 237                      let ql' = StateSet.union sql ql
 238                      and qr' = StateSet.union sqr qr in
 239                      add_st (ql',qr') tl in
 240       let ql,qr = add_st (StateSet.empty, StateSet.empty) list_form in
 241       let qfq,qfr = try NodeHash.find run fnode
 242         with | _ -> map_leaf asta
 243       and qnq,qnr = try NodeHash.find run nnode
 244         with | _ -> map_leaf asta in
 245       begin
 246         if tfnode == Tree.nil || Tree.is_attribute tree tnode
 247         then ()
 248         else NodeHash.replace run fnode (StateSet.inter qfq ql,qfr);
 249         if tnnode == Tree.nil || Tree.is_attribute tree tnode
 250         then ()
 251         else NodeHash.replace run nnode (StateSet.inter qnq qr,qnr);
 252         (* indeed we delete all states from self transitions!  *)
 253         tp_max asta run tree tfnode hashMax hashInfer;
 254         tp_max asta run tree tnnode hashMax hashInfer;
 255       end;
 256     end
 257
 258 let compute tree asta =
 259   let flag = 2 in                       (* debug  *)
 260   let size_tree = 10000 in              (* todo (Tree.size ?) *)
 261   let size_hcons_O = 1000 in            (* todo size Hashtbl *)
 262   let size_hcons_M = 1000 in            (* todo size Hashtbl *)
 263   let size_hcons_F = 1000 in            (* todo size Hashtbl *)
 264   let map = NodeHash.create size_tree in
 265   let hashOracle = HashOracle.create(size_hcons_O) in
 266   let hashEval = Formula.HashEval.create(size_hcons_F) in
 267   let hashInfer = Formula.HashInfer.create(size_hcons_F) in
 268   bu_oracle asta map tree (Tree.root tree) hashOracle hashEval;
 269   HashOracle.clear hashOracle;
 270   Formula.HashEval.clear hashEval;
 271   if flag > 0 then begin
 272     let hashOver = HashRun.create(size_hcons_M) in
 273     let hashMax = HashRun.create(size_hcons_M) in
 274     bu_over_max asta map tree (Tree.root tree) hashOver hashInfer;
 275     if flag = 2
 276     then
 277       tp_max asta map tree (Tree.root tree) hashMax hashInfer
 278     else ();
 279     HashRun.clear hashOver;
 280     HashRun.clear hashMax;
 281   end
 282   else ();
 283   map
 284
 285 let selected_nodes tree asta =
 286   let run = compute tree asta in
 287   NodeHash.fold
 288     (fun key set acc ->
 289       if not(StateSet.is_empty
 290                (StateSet.inter (fst set) (Asta.selec_states asta)))
 291       then key :: acc
 292       else acc)
 293     run []
 294
 295 let print fmt run =
 296   let print_d_set fmt (s_1,s_2) =
 297     Format.fprintf fmt "(%a,%a)"
 298       StateSet.print s_1 StateSet.print s_2 in
 299   let print_map fmt run =
 300     let pp = Format.fprintf fmt in
 301     if NodeHash.length run = 0
 302     then Format.fprintf fmt "ø"
 303     else
 304       NodeHash.iter (fun cle set -> pp "|  %i->%a  @ " cle print_d_set set)
 305         run in
 306   let print_box fmt run =
 307     let pp = Format.fprintf fmt in
 308     pp "@[<hov 0>@.  # Mapping:@.   @[<hov 0>%a@]@]"
 309       print_map run
 310   in
 311   Format.fprintf fmt "@[<hov 0>##### RUN #####@, %a@]@." print_box run