src/ata.ml

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