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
 125           (TagSet.inj_positive rel_labels));
 126         NODE
 127       end else STAR
 128
 129 module Cache = Hashtbl.Make(StateSet)
 130 let cache = Cache.create 1023
 131 let init () = Cache.clear cache
 132
 133 let by_labels (tags1, _) (tags2, _) = TagSet.compare tags1 tags2
 134
 135 let by_states x1 x2 =
 136   let l1, r1, (m1 : bool) = snd x1
 137   and l2, r2, (m2 : bool) = snd x2 in
 138   (* force m1/m2 to be of type bool for efficient compare *)
 139   let r = StateSet.compare l1 l2 in
 140   if r != 0 then r
 141   else
 142     let r' = StateSet.compare r1 r2 in
 143     if r' != 0 then r'
 144     else compare m1 m2
 145
 146 let merge_states (tags1, (l1, r1, m1)) (tags2, (l2, r2, m2)) =
 147   if tags1 == tags2 then
 148     tags1, (StateSet.union l1 l2, StateSet.union r1 r2, m1 || m2)
 149   else assert false
 150
 151 let merge_labels (tags1, (l1, r1, m1)) (tags2, (l2, r2, m2)) =
 152   if l1 == l2 && r1 == r2 && m1 == m2 then
 153     (TagSet.cup tags1 tags2), (l1, r1, m1)
 154   else assert false
 155
 156 let rec merge_trans comp f l =
 157   match l with
 158   | [] |[ _ ] -> l
 159   | tr1::tr2::ll ->
 160     if comp tr1 tr2 == 0 then merge_trans comp f ((f tr1 tr2)::ll)
 161     else tr1 :: (merge_trans comp f (tr2::ll))
 162
 163 let fold_trans_of_states auto f states acc =
 164   StateSet.fold
 165     (fun q tr_acc ->
 166       List.fold_left f tr_acc (Hashtbl.find auto.trans q))
 167     states
 168     acc
 169
 170 let top_down_approx auto states tree =
 171   try Cache.find cache states with
 172   | Not_found ->
 173     let trs =
 174       (* Collect all (ts, (l, r, m)) where
 175          ts is a tagset, l and r are left and right set of states
 176          m is marking flag
 177       *)
 178       fold_trans_of_states auto
 179         (fun acc_tr (ts, tr) ->
 180           let pos =
 181             if ts == TagSet.star then Tree.element_tags tree
 182             else if ts == TagSet.any then Tree.node_tags tree
 183             else TagSet.positive ts
 184           in
 185           let _, _, m, f = Transition.node tr in
 186           let ls, rs = Formula.st f in
 187           if Ptset.Int.is_empty pos then acc_tr
 188           else
 189             (TagSet.inj_positive pos, (ls, rs, m))::acc_tr
 190         )
 191         states
 192         []
 193     in
 194     (* for all labels in the tree compute which transition is taken *)
 195     let all_trs =
 196       Ptset.Int.fold (fun tag acc ->
 197         List.fold_left (fun acc' (ts, rhs) ->
 198           if TagSet.mem tag ts then
 199             (TagSet.singleton tag, rhs)::acc'
 200           else acc') acc trs)
 201         (Tree.node_tags tree) []
 202     in
 203     (* merge together states that have common labels *)
 204     let uniq_states_trs =
 205       merge_trans by_labels merge_states (List.sort by_labels all_trs)
 206     in
 207     (* merge together labels that have common states *)
 208     let td_approx =
 209       merge_trans by_states merge_labels
 210         (List.sort by_states uniq_states_trs)
 211     in
 212     LOG(
 213       "top-down-approx", 2,
 214          let is_pairwise_disjoint l =
 215            List.for_all (fun ((ts, _) as tr) ->
 216              List.for_all (fun ((ts', _) as tr') ->
 217                (ts == ts' && (by_states tr tr' == 0)) ||
 218                  TagSet.is_empty (TagSet.cap ts ts')) l) l
 219          in
 220          let is_complete l = TagSet.positive
 221            (List.fold_left (fun acc (ts, _) -> TagSet.cup acc ts)
 222               TagSet.empty l)
 223            ==
 224            (Tree.node_tags tree)
 225          in
 226          let pr_td_approx fmt 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              fprintf fmt "\t%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            fprintf fmt "\n%!"
 243          in
 244          __ " pairwise-disjoint:%b, complete:%b:\n%a"
 245            (is_pairwise_disjoint td_approx)
 246            (is_complete td_approx)
 247            pr_td_approx td_approx
 248     );
 249     let jump =
 250       compute_jump
 251         auto tree states td_approx
 252         (List.exists (fun (_,(_,_,b)) -> b) td_approx)
 253     in
 254     Cache.add cache states jump; jump
 255
 256
 257
 258 let get_trans ?(attributes=TagSet.empty) auto states tag =
 259   StateSet.fold (fun q acc ->
 260     List.fold_left (fun ((tr_acc, l_acc, r_acc) as acc) (ts, tr) ->
 261       let ts = if ts == TagSet.star then TagSet.diff ts attributes else ts
 262       in
 263       let b = TagSet.mem tag ts in
 264       let () = LOG("transition", 3, __ "Transition: %a, tag=%s, %s\n%!"
 265         Transition.print
 266         tr
 267         (Tag.to_string tag)
 268         (if b then "selected" else "not selected"))
 269       in
 270       if b then
 271         let _, _, _, f = Transition.node tr in
 272         let l, r = Formula.st f in
 273         (Translist.cons tr tr_acc,
 274          StateSet.union l l_acc,
 275          StateSet.union r r_acc)
 276       else acc) acc (Hashtbl.find auto.trans q))
 277     states
 278     (Translist.nil, StateSet.empty, StateSet.empty)
 279