src/ata.ml

   1 INCLUDE "debug.ml"
   2 INCLUDE "utils.ml"
   3 open Format
   4
   5 type t = {
   6     id : int;
   7     states : StateSet.t;
   8     init : StateSet.t;
   9     last : State.t;
  10     (* Transitions of the Alternating automaton *)
  11     trans : (State.t, (TagSet.t * Transition.t) list) Hashtbl.t;
  12     marking_states : StateSet.t;
  13     topdown_marking_states : StateSet.t;
  14     bottom_states : StateSet.t;
  15     true_states : StateSet.t;
  16 }
  17
  18
  19 let print ppf a =
  20   fprintf ppf
  21 "Automaton (%i) :
  22 States %a
  23 Initial states: %a
  24 Marking states: %a
  25 Topdown marking states: %a
  26 Bottom states: %a
  27 True states: %a
  28 Alternating transitions\n"
  29     a.id
  30     StateSet.print a.states
  31     StateSet.print a.init
  32     StateSet.print a.marking_states
  33     StateSet.print a.topdown_marking_states
  34     StateSet.print a.bottom_states
  35     StateSet.print a.true_states;
  36   let trs =
  37     Hashtbl.fold
  38       (fun _ t acc ->
  39          List.fold_left (fun acc (_, tr) -> tr::acc) acc t) a.trans []
  40   in
  41   let sorted_trs = List.stable_sort Transition.compare trs in
  42   let strings = Transition.format_list sorted_trs in
  43     match strings with
  44         [] -> ()
  45       | line::_ ->
  46           let sline = Pretty.line (Pretty.length line) in
  47             fprintf ppf "%s\n%!" sline;
  48             List.iter (fun s -> fprintf ppf "%s\n%!" s) strings;
  49             fprintf ppf "%s\n%!" sline
  50
  51 type jump_kind = NIL
  52             | NODE
  53             | STAR
  54             | JUMP_ONE of Ptset.Int.t
  55             | JUMP_MANY of Ptset.Int.t
  56             | CAPTURE_MANY of Ptset.Int.t
  57
  58 let print_kind fmt k =
  59   let () =
  60     match k with
  61       | NIL -> fprintf fmt "NIL"
  62       | STAR -> fprintf fmt "STAR"
  63       | NODE -> fprintf fmt "NODE"
  64       | JUMP_ONE(t) -> let t = TagSet.inj_positive t in
  65           fprintf fmt "JUMP_ONE(%a)" TagSet.print t
  66       | JUMP_MANY(t) -> let t = TagSet.inj_positive t in
  67          fprintf fmt "JUMP_MANY(%a)" TagSet.print t
  68       | CAPTURE_MANY(t) ->
  69           let t = TagSet.inj_positive t in
  70             fprintf fmt "JUMP_MANY(%a)" TagSet.print t
  71
  72   in fprintf fmt "%!"
  73 let compute_jump auto tree states l marking =
  74   let rel_trans, skip_trans =
  75     List.fold_left
  76       (fun (acc_rel, acc_skip) ((ts, (l,r,m)) as tr) ->
  77          if not m &&
  78            ((l == states && r == states)
  79             || (l == StateSet.empty && states == r)
  80             || (l == states && r = StateSet.empty)
  81             || (l == StateSet.empty && r = StateSet.empty))
  82          then (acc_rel, tr::acc_skip)
  83          else (tr::acc_rel, acc_skip))
  84       ([],[]) l
  85   in
  86   let rel_labels = List.fold_left
  87     (fun acc (ts, _ ) ->
  88        Ptset.Int.union (TagSet.positive ts) acc)
  89     Ptset.Int.empty
  90     rel_trans
  91   in
  92     if Ptset.Int.is_empty rel_labels then NIL
  93     else
  94       match skip_trans with
  95           [ (_, (l, r, _) ) ] when l == r && l == states ->
  96             begin
  97               match rel_trans with
  98                 | [ (_, (l, r, m) ) ]
  99                     when (rel_labels == (Tree.element_tags tree) ||
 100                             Ptset.Int.is_singleton rel_labels)
 101                       && (StateSet.diff l auto.true_states) == states && m
 102                             -> CAPTURE_MANY(rel_labels)
 103                 | _ ->
 104                     JUMP_MANY(rel_labels)
 105             end
 106         | [ (_, (l, r, _) ) ] when l == StateSet.empty -> JUMP_ONE(rel_labels)
 107         | _ -> if Ptset.Int.mem Tag.pcdata rel_labels then
 108             let () = D_TRACE_(Format.eprintf ">>> Computed rel_labels: %a\n%!" TagSet.print (TagSet.inj_positive rel_labels)) in NODE else STAR
 109
 110 module Cache = Hashtbl.Make(StateSet)
 111 let cache = Cache.create 1023
 112 let init () = Cache.clear cache
 113
 114 let by_labels (tags1,(_,_,m1)) (tags2,(_,_,m2)) =
 115   let r = TagSet.compare tags1 tags2 in r
 116 (*
 117     if r == 0 then compare m1 m2 else r
 118 *)
 119 let by_states (_,(l1,r1, m1)) (_, (l2,r2,m2)) =
 120   let r = StateSet.compare l1 l2 in
 121     if r == 0 then
 122       let r' = StateSet.compare r1 r2 in
 123         if r' == 0 then compare m1 m2
 124         else r'
 125     else r
 126
 127 let merge_states (tags1, (l1, r1, m1)) (tags2, (l2, r2, m2)) =
 128   if tags1 == tags2 then (tags1,(StateSet.union l1 l2, StateSet.union r1 r2, m1 || m2))
 129   else assert false
 130
 131 let merge_labels (tags1, (l1, r1, m1)) (tags2, (l2, r2, m2)) =
 132   if (l1 == l2) && (r1 == r2) && (m1 == m2) then (TagSet.cup tags1 tags2),(l1,r1,m1)
 133   else assert false
 134
 135 let rec merge_trans comp f l =
 136   match l with
 137     | [] |[ _ ] -> l
 138     | tr1::tr2::ll ->
 139         if comp tr1 tr2 == 0 then merge_trans comp f ((f tr1 tr2)::ll)
 140         else tr1 :: (merge_trans comp f (tr2::ll))
 141
 142
 143 let top_down_approx auto states tree =
 144   try
 145     Cache.find cache states
 146   with
 147       Not_found ->
 148         let jump =
 149           begin
 150             let trs =
 151               StateSet.fold
 152                 (fun q acc -> List.fold_left
 153                    (fun acc_tr (ts, tr) ->
 154                        let pos =
 155                          if ts == TagSet.star
 156                          then Tree.element_tags tree
 157                          else if ts == TagSet.any then Tree.node_tags tree
 158                          else TagSet.positive ts
 159                        in
 160                        let _, _, m, f = Transition.node tr in
 161                        let (_, _, ls), (_, _, rs) = Formula.st f in
 162                          if Ptset.Int.is_empty pos then acc_tr else
 163                          (TagSet.inj_positive pos,(ls, rs, m))::acc_tr
 164                    )
 165                    acc
 166                    (Hashtbl.find auto.trans q)
 167                 )
 168                 states
 169                 []
 170             in
 171               (* all labels in the tree compute what transition would be taken *)
 172             let all_trs =
 173               Ptset.Int.fold (fun tag acc ->
 174                                 List.fold_left (fun acc' (ts, lhs) ->
 175                                                   if TagSet.mem tag ts then
 176                                                     (TagSet.singleton tag, lhs)::acc'
 177                                                   else acc') acc trs)
 178                 (Tree.node_tags tree) []
 179             in
 180               (* now merge together states that have common labels *)
 181             let uniq_states_trs =
 182               merge_trans by_labels merge_states (List.sort by_labels all_trs)
 183             in
 184               (* now merge together labels that have common states *)
 185             let td_approx =
 186               merge_trans by_states merge_labels (List.sort by_states uniq_states_trs)
 187             in
 188               D_TRACE_(
 189                 let is_pairwise_disjoint l =
 190                   List.for_all (fun ((ts, _) as tr) ->
 191                                   List.for_all (fun ((ts', _) as tr') ->
 192                                                   (ts == ts' && (by_states tr tr' == 0)) ||
 193                                                     TagSet.is_empty (TagSet.cap ts ts')) l) l
 194                 in
 195                 let is_complete l = TagSet.positive
 196                   (List.fold_left (fun acc (ts, _) -> TagSet.cup acc ts) TagSet.empty l)
 197                   ==
 198                   (Tree.node_tags tree)
 199                 in
 200                   eprintf "Top-down approximation (%b, %b):\n%!"
 201                     (is_pairwise_disjoint td_approx)
 202                     (is_complete td_approx);
 203                   List.iter (fun (ts,(l,r, m)) ->
 204                                let ts = if TagSet.cardinal ts >10
 205                                then TagSet.diff TagSet.any
 206                                  (TagSet.diff
 207                                     (TagSet.inj_positive (Tree.node_tags tree))
 208                                     ts)
 209                                else ts
 210                                in
 211                                eprintf "%a, %a, %b -> %a, %a\n%!"
 212                                  StateSet.print states
 213                                  TagSet.print ts
 214                                  m
 215                                  StateSet.print l
 216                                  StateSet.print r
 217                             ) td_approx;
 218                   eprintf "\n%!"
 219
 220               );
 221     let jump =
 222       compute_jump auto tree states td_approx (List.exists (fun (_,(_,_,b)) -> b) td_approx)
 223     in
 224       jump
 225           end
 226         in
 227           Cache.add cache states jump; jump