src/ata.ml

   1 INCLUDE "debug.ml"
   2 INCLUDE "utils.ml"
   3
   4 open Format
   5
   6 type t =
   7     { id : int;
   8       states : StateSet.t;
   9       init : StateSet.t;
  10       last : State.t;
  11
  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) :
  23 States %a
  24 Initial states: %a
  25 Marking states: %a
  26 Topdown marking states: %a
  27 Bottom states: %a
  28 True states: %a
  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 ->
  40          List.fold_left (fun acc (_, tr) -> tr::acc) acc t) a.trans []
  41   in
  42   let sorted_trs = List.stable_sort Transition.compare trs in
  43   let strings = Transition.format_list sorted_trs in
  44     match strings with
  45       [] -> ()
  46     | line::_ ->
  47       let sline = Pretty.line (Pretty.length line) in
  48       fprintf ppf "%s\n%!" sline;
  49       List.iter (fun s -> fprintf ppf "%s\n%!" s) strings;
  50       fprintf ppf "%s\n%!" sline
  51
  52
  53 type jump_kind =
  54     NIL
  55   | NODE
  56   | STAR
  57   | JUMP_ONE of Ptset.Int.t
  58   | JUMP_MANY of Ptset.Int.t
  59   | CAPTURE_MANY of Ptset.Int.t
  60
  61
  62 let print_kind fmt k =
  63   begin
  64     match k with
  65     | NIL -> fprintf fmt "NIL"
  66     | STAR -> fprintf fmt "STAR"
  67     | NODE -> fprintf fmt "NODE"
  68
  69     | JUMP_ONE(t) ->
  70       let t = TagSet.inj_positive t in
  71       fprintf fmt "JUMP_ONE(%a)" TagSet.print t
  72
  73     | JUMP_MANY(t) ->
  74       let t = TagSet.inj_positive t in
  75       fprintf fmt "JUMP_MANY(%a)" TagSet.print t
  76
  77     | CAPTURE_MANY(t) ->
  78       let t = TagSet.inj_positive t in
  79       fprintf fmt "JUMP_MANY(%a)" TagSet.print t
  80   end;
  81   fprintf fmt "%!"
  82
  83
  84 let compute_jump auto tree states l marking =
  85   let rel_trans, skip_trans =
  86     List.fold_left
  87       (fun (acc_rel, acc_skip) ((ts, (l,r,marking)) as tr) ->
  88         if not marking &&
  89           ((l == states && r == states)
  90            || (l == StateSet.empty && states == r)
  91            || (l == states && r = StateSet.empty)
  92            || (l == StateSet.empty && r = StateSet.empty))
  93         then (acc_rel, tr::acc_skip)
  94         else (tr::acc_rel, acc_skip))
  95       ([],[]) l
  96   in
  97   let rel_labels = List.fold_left
  98     (fun acc (ts, _ ) ->
  99       Ptset.Int.union (TagSet.positive ts) acc)
 100     Ptset.Int.empty
 101     rel_trans
 102   in
 103   if Ptset.Int.is_empty rel_labels then NIL
 104   else
 105     match skip_trans with
 106       [ (_, (l, r, _) ) ] when l == r && l == states ->
 107         begin
 108           match rel_trans with
 109           | [ (_, (l, r, m) ) ]
 110               when (rel_labels == (Tree.element_tags tree) ||
 111                       Ptset.Int.is_singleton rel_labels)
 112                 && (StateSet.diff l auto.true_states) == states && m
 113                 -> CAPTURE_MANY(rel_labels)
 114           | _ ->
 115             JUMP_MANY(rel_labels)
 116         end
 117
 118     | [ (_, (l, r, _) ) ] when l == StateSet.empty -> JUMP_ONE(rel_labels)
 119
 120     | _ ->
 121       if Ptset.Int.mem Tag.pcdata rel_labels then
 122         let () =
 123           D_TRACE_(Format.eprintf ">>> Computed rel_labels: %a\n%!"
 124                      TagSet.print (TagSet.inj_positive rel_labels))
 125         in NODE
 126       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     D_TRACE_(
 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       eprintf "Top-down approximation (%b, %b):\n%!"
 225         (is_pairwise_disjoint td_approx)
 226         (is_complete td_approx);
 227       List.iter (fun (ts,(l,r, m)) ->
 228         let ts = if TagSet.cardinal ts >10
 229           then TagSet.diff TagSet.any
 230             (TagSet.diff
 231                (TagSet.inj_positive (Tree.node_tags tree))
 232                ts)
 233           else ts
 234         in
 235         eprintf "%a, %a, %b -> %a, %a\n%!"
 236           StateSet.print states
 237           TagSet.print ts
 238           m
 239           StateSet.print l
 240           StateSet.print r
 241       ) td_approx;
 242       eprintf "\n%!"
 243
 244     );
 245     let jump =
 246       compute_jump
 247         auto tree states td_approx
 248         (List.exists (fun (_,(_,_,b)) -> b) td_approx)
 249     in
 250     Cache.add cache states jump; jump
 251