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 module Node  =
  17 struct
  18   type t = int
  19   let hash n = n
  20   let compare = (-)
  21   let equal = (=)
  22 end
  23
  24 module NodeHash = Hashtbl.Make (Node)
  25
  26 type t = (StateSet.t*StateSet.t) NodeHash.t
  27 (** Map from nodes to query and recognizing states *)
  28 (* Note that we do not consider nil nodes *)
  29
  30 exception Oracle_fail
  31 exception Over_max_fail
  32 exception Max_fail
  33
  34 (* Mapped sets for leaves *)
  35 let map_leaf asta = (Asta.bot_states_s asta, StateSet.empty)
  36
  37 (* Build the Oracle *)
  38 let rec bu_oracle asta run tree tnode =
  39   let node = Tree.preorder tree tnode in
  40   if Tree.is_leaf tree tnode
  41   then
  42     if tnode == Tree.nil
  43     then ()
  44     else NodeHash.add run node (map_leaf asta)
  45   else
  46     let tfnode = Tree.first_child_x tree tnode
  47     and tnnode = Tree.next_sibling tree tnode in
  48     let fnode,nnode =                            (* their preorders *)
  49       (Tree.preorder tree tfnode, Tree.preorder tree tnnode) in
  50     begin
  51       bu_oracle asta run tree tfnode;
  52       bu_oracle asta run tree tnnode;
  53       let q_rec n =                     (* compute the set for child/sibling *)
  54         try NodeHash.find run n
  55         with Not_found -> map_leaf asta in
  56       let (_,qfr),(_,qnr) = q_rec fnode,q_rec nnode (* computed in rec call *)
  57       and lab = Tree.tag tree tnode in
  58       let _,list_tr = Asta.transitions_lab asta lab in (* only reco. tran.*)
  59       let rec result set flag = function (* add states which satisfy a transition *)
  60         | [] -> set,flag
  61         | (q,form) :: tl ->
  62           if Formula.eval_form (set,qfr,qnr) form (* evaluates the formula*)
  63           then
  64             if StateSet.mem q set
  65             then result set 0 tl
  66             else result (StateSet.add q set) 1 tl
  67           else result set 0 tl in
  68       let rec fix_point set_i =  (* compute the fixed point of states of node *)
  69         let set,flag = result set_i 0 list_tr in
  70         if flag = 0 then set
  71         else fix_point set in
  72       NodeHash.add run node (StateSet.empty, fix_point StateSet.empty)
  73     end
  74
  75 (* Build the over-approx. of the maximal run *)
  76 let rec bu_over_max asta run tree tnode =
  77   if (Tree.is_leaf tree tnode)      (* BU_oracle has already created the map *)
  78   then
  79     ()
  80   else
  81     let tfnode = Tree.first_child_x tree tnode
  82     and tnnode = Tree.next_sibling tree tnode in
  83     begin
  84       bu_over_max asta run tree tfnode;
  85       bu_over_max asta run tree tnnode;
  86       let (fnode,nnode) =
  87         (Tree.preorder tree tfnode, Tree.preorder tree tnnode)
  88       and node = Tree.preorder tree tnode in
  89       let q_rec n =
  90         try NodeHash.find run n
  91         with Not_found -> map_leaf asta in
  92       let qf,qn = q_rec fnode,q_rec nnode in
  93       let lab = Tree.tag tree tnode in
  94       let list_tr,_ = Asta.transitions_lab asta lab (* only take query st. *)
  95       and _,resultr = try NodeHash.find run node
  96         with _ -> raise Over_max_fail in
  97       let rec result set flag = function
  98         | [] -> set,flag
  99         | (q,form) :: tl ->
 100           if Formula.infer_form (set,resultr) qf qn form (* infers the formula*)
 101           then if StateSet.mem q set
 102             then result set 0 tl
 103             else result (StateSet.add q set) 1 tl
 104           else result set 0 tl in
 105       let rec fix_point set_i =
 106         let set,flag = result set_i 0 list_tr in
 107         if flag = 0
 108         then set
 109         else fix_point set in
 110       let result_set = fix_point StateSet.empty in
 111       (* we keep the old recognizing states set *)
 112       NodeHash.replace run node (result_set, resultr)
 113     end
 114
 115
 116 (* Build the maximal run *)
 117 let rec tp_max asta run tree tnode =
 118   if (Tree.is_leaf tree tnode)      (* BU_oracle has already created the map *)
 119   then
 120     ()
 121   else
 122     let node = Tree.preorder tree tnode
 123     and tfnode = Tree.first_child_x tree tnode
 124     and tnnode = Tree.next_sibling tree tnode in
 125     let (fnode,nnode) =
 126       (Tree.preorder tree tfnode, Tree.preorder tree tnnode) in
 127     begin
 128       if tnode == Tree.root tree        (* we must intersect with top states *)
 129       then let setq,_  = try NodeHash.find run node
 130         with _ -> raise Max_fail in
 131            NodeHash.replace run node
 132              ((StateSet.inter (Asta.top_states_s asta) setq),StateSet.empty)
 133       else ();
 134       let q_rec n =
 135         try NodeHash.find run n
 136         with Not_found -> map_leaf asta in
 137       let qf,qn = q_rec fnode,q_rec nnode in
 138       let lab = Tree.tag tree tnode in
 139       let list_tr,_ = Asta.transitions_lab asta lab in (* only take query. *)
 140       let (set_node,set_nr) as self = try NodeHash.find run node
 141         with Not_found -> raise Max_fail in
 142       (* We must compute again accepting states from self transitions since
 143          previous calls of tp_max may remove them *)
 144       let rec comp_acc_self set flag =
 145        () (* given a current set of states we add
 146              states from self transitions which satisfy the two conditions *)
 147       (* With result (below) we have all valid transitions at step 0
 148       we compute the self states which occur in it and which are not in cthe current state.
 149       For each of these states we compute the transitions with the correct label and state
 150       we infer each of these transitions: true -> add self states occuring in it
 151          to the acc and to the current set + add left and right states as result do *)
 152       (* ----> With a FIFO *)
 153       and fix_point selfq_i =
 154         () in
 155       NodeHash.replace run node (set_node, set_nr);
 156
 157       let rec result = function
 158         | [] -> []
 159         | (q,form) :: tl ->
 160           if (StateSet.mem q set_node) &&  (* infers & trans. can start here *)
 161             (Formula.infer_form self qf qn form)
 162           then form :: (result tl)
 163           else result tl in
 164       let list_form = result list_tr in (* tran. candidates *)
 165       (* compute states occuring in transition candidates *)
 166       let rec add_st (ql,qr) = function
 167         | [] -> ql,qr
 168         | f :: tl -> let sqs,sql,sqr = Formula.st f in
 169                      let ql' = StateSet.union sql ql
 170                      and qr' = StateSet.union sqr qr in
 171                      add_st (ql',qr') tl in
 172       let ql,qr = add_st (StateSet.empty, StateSet.empty) list_form in
 173       let qfq,qfr = try NodeHash.find run fnode
 174         with | _ -> map_leaf asta
 175       and qnq,qnr = try NodeHash.find run nnode
 176         with | _ -> map_leaf asta in
 177       begin
 178         if tfnode == Tree.nil || Tree.is_attribute tree tnode
 179         then ()
 180         else NodeHash.replace run fnode (StateSet.inter qfq ql,qfr);
 181         if tnnode == Tree.nil || Tree.is_attribute tree tnode
 182         then ()
 183         else NodeHash.replace run nnode (StateSet.inter qnq qr,qnr);
 184         (* indeed we delete all states from self transitions!  *)
 185         tp_max asta run tree tfnode;
 186         tp_max asta run tree tnnode;
 187       end;
 188     end
 189
 190 let compute tree asta =
 191   let flag = 2 in                       (* debug  *)
 192   let size_tree = 10000 in              (* todo (Tree.size ?) *)
 193   let map = NodeHash.create size_tree in
 194   bu_oracle asta map tree (Tree.root tree);
 195   if flag > 0 then begin
 196     bu_over_max asta map tree (Tree.root tree);
 197     if flag = 2
 198     then
 199       tp_max asta map tree (Tree.root tree)
 200     else ()
 201   end
 202   else ();
 203   map
 204
 205 let selected_nodes tree asta =
 206   let run = compute tree asta in
 207   NodeHash.fold
 208     (fun key set acc ->
 209       if not(StateSet.is_empty
 210                (StateSet.inter (fst set) (Asta.selec_states asta)))
 211       then key :: acc
 212       else acc)
 213     run []
 214
 215 let print fmt run =
 216   let print_d_set fmt (s_1,s_2) =
 217     Format.fprintf fmt "(%a,%a)"
 218       StateSet.print s_1 StateSet.print s_2 in
 219   let print_map fmt run =
 220     let pp = Format.fprintf fmt in
 221     if NodeHash.length run = 0
 222     then Format.fprintf fmt "ø"
 223     else
 224       NodeHash.iter (fun cle set -> pp "|  %i->%a  @ " cle print_d_set set)
 225         run in
 226   let print_box fmt run =
 227     let pp = Format.fprintf fmt in
 228     pp "@[<hov 0>@.  # Mapping:@.   @[<hov 0>%a@]@]"
 229       print_map run
 230   in
 231   Format.fprintf fmt "@[<hov 0>##### RUN #####@, %a@]@." print_box run