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