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