automaton.ml

   1 (******************************************************************************)
   2 (*  SXSI : XPath evaluator                                                    *)
   3 (*  Kim Nguyen (Kim.Nguyen@nicta.com.au)                                      *)
   4 (*  Copyright NICTA 2008                                                      *)
   5 (*  Distributed under the terms of the LGPL (see LICENCE)                     *)
   6 (******************************************************************************)
   7 INCLUDE "debug.ml";;
   8
   9 module State =
  10 struct
  11   type t = int
  12   let mk = let i = ref ~-1 in fun () -> incr i;!i
  13   let compare p q = p - q
  14   let equal p q = p==q
  15   let hash p = p
  16   let print fmt p = Format.fprintf fmt "<%.6i>" p
  17 end
  18
  19 module ISet : Set.S with type elt = int=
  20 struct
  21   let max = Sys.word_size - 2
  22   type t = int
  23   type elt = int
  24
  25   let empty = 0
  26   let full = -1
  27   let is_empty x = x == 0
  28   let mem e s = ((1 lsl e) land s) != 0
  29   let add e s = (1 lsl e) lor s
  30   let singleton e = (1 lsl e)
  31   let union = (lor)
  32   let inter = (land)
  33   let diff a b = a land (lnot b)
  34   let remove e s = (lnot (1 lsl e) land s)
  35   let compare = (-)
  36   let equal = (==)
  37   let subset a b = a land (lnot b) == 0
  38   let cardinal s =
  39     let rec loop n s =
  40       if s == 0 then n else loop (succ n) (s - (s land (-s)))
  41     in
  42   loop 0 s
  43 (* inverse of bit i = 1 lsl i i.e. tib i = log_2(i) *)
  44 let log2 = Array.create 255 0
  45 let () = for i = 0 to 7 do log2.(1 lsl i) <- i done
  46
  47 (* assumption: x is a power of 2 *)
  48 let tib32 x =
  49   if x land 0xFFFF == 0 then
  50     let x = x lsr 16 in
  51     if x land 0xFF == 0 then 24 + log2.(x lsr 8) else 16 + log2.(x)
  52   else
  53     if x land 0xFF == 0 then 8 + log2.(x lsr 8) else log2.(x)
  54
  55 let ffffffff = (0xffff lsl 16) lor 0xffff
  56 let tib64 x =
  57   if x land ffffffff == 0 then 32 + tib32 (x lsr 32) else tib32 x
  58
  59 let tib =
  60   match Sys.word_size with 32 -> tib32 | 64 -> tib64 | _ -> assert false
  61
  62 let min_elt s =
  63   if s == 0 then raise Not_found;
  64   tib (s land (-s))
  65
  66 let choose = min_elt
  67
  68 (* TODO: improve? *)
  69 let max_elt s =
  70   if s == 0 then raise Not_found;
  71   let rec loop i =
  72     if s land i != 0 then tib i
  73     else if i = 1 then raise Not_found else loop (i lsr 1)
  74   in
  75   loop min_int
  76
  77 let rec elements s =
  78   if s == 0 then [] else let i = s land (-s) in tib i :: elements (s - i)
  79
  80 let rec iter f s =
  81   if s != 0 then let i = s land (-s) in f (tib i); iter f (s - i)
  82
  83 let rec fold f s acc =
  84   if s == 0 then acc else let i = s land (-s) in fold f (s - i) (f (tib i) acc)
  85
  86 let rec for_all p s =
  87   s == 0 || let i = s land (-s) in p (tib i) && for_all p (s - i)
  88
  89 let rec exists p s =
  90   s != 0 && let i = s land (-s) in p (tib i) || exists p (s - i)
  91
  92 let rec filter p s =
  93   if s == 0 then
  94     0
  95   else
  96     let i = s land (-s) in
  97     let s = filter p (s - i) in
  98     if p (tib i) then s + i else s
  99
 100 let rec partition p s =
 101    if s == 0 then
 102     0, 0
 103   else
 104     let i = s land (-s) in
 105     let st,sf = partition p (s - i) in
 106     if p (tib i) then st + i, sf else st, sf + i
 107
 108 let split i s =
 109   let bi = 1 lsl i in
 110   s land (bi - 1), s land bi != 0, s land (-1 lsl (i+1))
 111
 112
 113 end
 114 (* module SSet = Set.Make(State)*)
 115 module SSet = ISet
 116
 117 module Transition =
 118 struct
 119
 120   type t = Label of State.t * TagSet.Xml.t * State.t * State.t
 121            | External of State.t * (Tree.Binary.t -> bool)*State.t * State.t
 122
 123   let source = function Label(s,_,_,_) | External(s,_,_,_) -> s
 124   let dest1 = function Label(_,_,d,_) | External(_,_,d,_) -> d
 125   let dest2 = function Label(_,_,_,d) | External(_,_,_,d) -> d
 126
 127   let compatible t1 t2 =
 128     State.equal (source t1) (source t2)
 129     && State.equal (dest1 t1) (dest1 t2)
 130     && State.equal (dest2 t1) (dest2 t2)
 131
 132   let check t1 t2 =
 133     if not (compatible t1 t2)
 134     then failwith "Incompatible transitions"
 135
 136   let cup t1 t2 =
 137     check t1 t2;
 138     match (t1,t2) with
 139       | Label(s,ts,d1,d2), Label(_,ts',_,_) -> Label(s,TagSet.Xml.cup ts ts',d1,d2)
 140       | External(s,f,d1,d2), External(_,f',_,_) -> External(s,(fun x -> (f x)||(f' x)),d1,d2)
 141       | Label(s,ts,d1,d2), External(_,f,_,_)
 142       | External(_,f,_,_), Label(s,ts,d1,d2) ->  External(s,(fun x -> (TagSet.Xml.mem (Tree.Binary.tag x) ts)||f x),d1,d2)
 143
 144   let cap t1 t2 =
 145     check t1 t2;
 146     match (t1,t2) with
 147       | Label(s,ts,d1,d2), Label(_,ts',_,_) -> Label(s,TagSet.Xml.cap ts ts',d1,d2)
 148       | External(s,f,d1,d2), External(_,f',_,_) -> External(s,(fun x -> (f x)&&(f' x)),d1,d2)
 149       | Label(s,ts,d1,d2), External(_,f,_,_)
 150       | External(_,f,_,_), Label(s,ts,d1,d2) -> External(s,(fun x -> (TagSet.Xml.mem (Tree.Binary.tag x) ts)&& f x),d1,d2)
 151
 152   let neg = function
 153     | Label(s,ts,d1,d2) -> Label(s,TagSet.Xml.neg ts,d1,d2)
 154     | External(s,f,d1,d2) -> External(s,(fun x -> not(f x)), d1 ,d2)
 155
 156
 157   let can_take t = function
 158     | Label(_,ts,_,_)  -> TagSet.Xml.mem (Tree.Binary.tag t) ts
 159     | External(_,f,_,_) -> f t
 160
 161   (* Hashtbl indexed by source State *)
 162   module HT = Hashtbl.Make(State)
 163
 164
 165
 166   type hashtbl = { label : (TagSet.Xml.t*State.t*State.t) HT.t;
 167                    extern : ((Tree.Binary.t-> bool)*State.t*State.t) HT.t;
 168                  }
 169
 170
 171   let empty () = { label = HT.create 17;
 172                    extern = HT.create 17;
 173                  }
 174
 175   let clear h = HT.clear h.label; HT.clear h.extern
 176
 177   let add h = function
 178     | Label(s,t,d1,d2) -> HT.add h.label s (t,d1,d2)
 179     | External(s,f,d1,d2) -> HT.add h.extern s (f,d1,d2)
 180
 181   let find_all ?(accu=[]) ?(pred_label=fun _ _ _ _ -> true) ?(pred_extern= fun _ _ _ _ -> true) h q =
 182     List.fold_left
 183       (fun acc (t,d1,d2) ->
 184          if pred_label q t d1 d2
 185          then Label(q,t,d1,d2) :: acc
 186          else acc)
 187      (List.fold_left
 188          (fun acc (f,d1,d2) ->
 189             if pred_extern q f d1 d2
 190             then External(q,f,d1,d2) :: acc
 191             else acc)
 192          accu
 193          (HT.find_all h.extern q))
 194       (HT.find_all h.label q)
 195
 196   let find_all_dest q h =
 197     HT.fold (fun source (t,q1,q2) acc ->
 198                if  (State.equal q1 q || State.equal q2 q)
 199                then Label(source,t,q1,q2)::acc
 200                else acc) h.label
 201       (HT.fold (fun source (t,q1,q2) acc ->
 202                   if (State.equal q1 q || State.equal q2 q)
 203                   then External(source,t,q1,q2)::acc
 204                   else acc) h.extern [])
 205
 206
 207   let fold_state f_lab f_ext h q acc =
 208     List.fold_left
 209       (fun acc (t,d1,d2) ->
 210          f_lab acc q t d1 d2)
 211       (List.fold_left
 212          (fun acc (f,d1,d2) ->
 213             f_ext acc q f d1 d2)
 214          acc
 215          (HT.find_all h.extern q))
 216       (HT.find_all h.label q)
 217
 218
 219 end
 220 module BST = Set.Make(Tree.Binary)
 221
 222 type t = { initial : SSet.t;
 223            final : SSet.t;
 224            transitions : Transition.hashtbl;
 225            marking : SSet.t;
 226            ignore : SSet.t;
 227            mutable result : BST.t;
 228            (* Statistics *)
 229            mutable numbt : int;
 230            mutable max_states : int;
 231            }
 232
 233 let mk () = { initial = SSet.empty;
 234              final = SSet.empty;
 235              transitions = Transition.empty();
 236              marking = SSet.empty;
 237              ignore = SSet.empty;
 238              result = BST.empty;
 239              numbt = 0;
 240              max_states = 0
 241            };;
 242
 243   let print_tags fmt l =
 244     let l =
 245       if TagSet.Xml.is_finite l then l
 246       else (Format.fprintf fmt "* \\ "; TagSet.Xml.neg l )
 247     in
 248       Format.fprintf fmt "{ ";
 249       ignore(TagSet.Xml.fold (fun t first ->
 250                                 if not first
 251                                 then Format.fprintf fmt " ,";
 252                                 Tag.print fmt t; false) l true);
 253       Format.fprintf fmt "}"
 254
 255   let dump fmt auto =
 256     Format.fprintf fmt "----------------- Automaton dump -------------------\n";
 257     Format.fprintf fmt "Initial states: ";
 258     SSet.iter (fun s -> State.print fmt s;
 259                             Format.fprintf fmt " ") auto.initial;
 260     Format.fprintf fmt "\n";
 261     Format.fprintf fmt "Final states:   ";
 262     SSet.iter (fun s -> State.print fmt s;
 263                             Format.fprintf fmt " ") auto.final;
 264     Format.fprintf fmt "\n";
 265     Format.fprintf fmt "Marking states: ";
 266     SSet.iter (fun s -> State.print fmt s;
 267                             Format.fprintf fmt " ") auto.marking;
 268     Format.fprintf fmt "\n";
 269     Format.fprintf fmt "Ignore states:  ";
 270     SSet.iter (fun s -> State.print fmt s;
 271                             Format.fprintf fmt " ") auto.ignore;
 272     Format.fprintf fmt "\n";
 273     Format.fprintf fmt "Transitions:\n";
 274     Transition.HT.iter (fun source (l,dest1,dest2) ->
 275                           State.print fmt source;
 276                           Format.fprintf fmt "-> ";
 277                           print_tags fmt l;
 278                           Format.fprintf fmt "(";
 279                           State.print fmt dest1;
 280                           Format.fprintf fmt " ,";
 281                           State.print fmt dest2;
 282                           Format.fprintf fmt ")\n") auto.transitions.Transition.label;
 283     Format.fprintf fmt "----------------------------------------------------\n"
 284
 285
 286
 287 module BottomUp =
 288 struct
 289
 290
 291   exception Fail
 292
 293   let pr_states fmt st = SSet.iter (fun s -> State.print fmt s;
 294                                                  Format.fprintf fmt " ") st
 295
 296   let err = Format.err_formatter
 297   let filter_map_rev filt map l =
 298     let rec loop ((accuf,accum) as accu) = function
 299       | [] -> accu
 300       | t::r -> loop (if filt t  then (t::accuf,SSet.add (map t) accum)
 301                       else accu) r
 302     in
 303       loop ([],SSet.empty) l
 304
 305   let mem s x =  SSet.mem x s
 306   let rec accepting_among auto t r =
 307     if SSet.is_empty r then r else
 308
 309     let to_ignore = SSet.inter auto.ignore r in
 310     let r = SSet.diff r to_ignore
 311     in
 312     let res =
 313       match Tree.Binary.descr t with
 314         | Tree.Binary.Nil | Tree.Binary.String _ ->
 315             let i = SSet.inter r auto.final in i
 316
 317         | Tree.Binary.Node(_) ->
 318             let t1 = Tree.Binary.left t
 319             and t2 = Tree.Binary.right t
 320             in
 321             let transitions =
 322               SSet.fold
 323               ( fun q accu ->
 324                  Transition.fold_state
 325                    (fun acc q t d1 d2 -> Transition.Label(q,t,d1,d2) :: acc)
 326                    (fun acc q t d1 d2 -> Transition.External(q,t,d1,d2) :: acc)
 327                    auto.transitions q accu) r []
 328             in
 329             let transitions,r1 =
 330               filter_map_rev
 331                 (Transition.can_take t)
 332                 Transition.dest1 transitions
 333             in
 334             let s1 = accepting_among auto t1 r1
 335             in
 336             let transitions,r2 =
 337               filter_map_rev
 338                 (fun x->SSet.mem (Transition.dest1 x) s1)
 339                 Transition.dest2 transitions
 340             in
 341             let s2 = accepting_among auto t2 r2
 342             in
 343             let _,s = filter_map_rev
 344               (fun x -> SSet.mem (Transition.dest2 x) s2)
 345               (Transition.source) transitions
 346             in
 347               if SSet.is_empty s then s
 348               else
 349                 (if SSet.exists (mem auto.marking) s1 || SSet.exists (mem auto.marking) s2
 350                  then auto.result <- BST.add t auto.result;s)
 351     in SSet.union to_ignore res
 352
 353
 354   let accept auto t =
 355     auto.result <- BST.empty;
 356     if SSet.is_empty (accepting_among auto t auto.initial)
 357     then false
 358     else true
 359 end
 360 module TopDown = struct
 361
 362
 363   let rec accept_at auto t q =
 364     if SSet.mem q auto.ignore then true
 365     else
 366       match Tree.Binary.descr t with
 367         | Tree.Binary.Nil | Tree.Binary.String _ -> SSet.mem q auto.final
 368         | Tree.Binary.Node(_) ->
 369             let tag = Tree.Binary.tag t
 370             and t1 = Tree.Binary.left t
 371             and t2 = Tree.Binary.right t
 372             in
 373             let transitions =
 374               Transition.find_all
 375                 ~pred_label:(fun _ ts _ _ -> TagSet.Xml.mem tag ts)
 376                 ~pred_extern:(fun _ f _ _ -> f t)
 377                 auto.transitions q
 378             in
 379             let rec iter_trans res = function
 380                 [] -> res
 381               | (Transition.Label(_,_,q1,q2) | Transition.External (_,_,q1,q2))::r ->
 382                   let _ = auto.numbt <- succ auto.numbt in
 383                   if (accept_at auto  t1 q1) && (accept_at auto t2 q2)
 384                   then
 385                     begin
 386                       if (SSet.mem q1 auto.marking)||(SSet.mem q2 auto.marking)
 387                       then auto.result <- BST.add t auto.result;
 388                       iter_trans true r
 389                     end
 390                   else
 391                     iter_trans res r
 392             in iter_trans false transitions
 393
 394
 395
 396
 397   let accept auto t =
 398     auto.numbt <- -1;
 399     SSet.exists (fun q ->
 400                    P(auto.numbt <- succ auto.numbt);
 401                    auto.result <- BST.empty;
 402                    accept_at auto t q)  auto.initial
 403
 404
 405   let rec run_in auto t states =
 406     if SSet.is_empty states then ()
 407     else
 408     match Tree.Binary.descr t with
 409       | Tree.Binary.Nil | Tree.Binary.String _ -> ()
 410       | Tree.Binary.Node(_) ->
 411           let tag = Tree.Binary.tag t
 412           and t1 = Tree.Binary.left t
 413           and t2 = Tree.Binary.right t
 414           in
 415           P(let i = SSet.cardinal states in
 416               if i > auto.max_states then auto.max_states <- i);
 417           let s1,s2 =
 418             SSet.fold
 419               (fun q acc ->
 420                  if SSet.mem q auto.ignore then acc
 421                  else
 422                    Transition.fold_state
 423                      (fun (ss1,ss2) _ ts d1 d2 ->
 424                         if TagSet.Xml.mem tag ts
 425                         then
 426                           (SSet.add d1 ss1,
 427                            SSet.add d2 ss2)
 428                         else (ss1,ss2))
 429                      (fun (ss1,ss2) _ f d1 d2 ->
 430                         if f t
 431                         then
 432                           (SSet.add d1 ss1,
 433                            SSet.add d2 ss2)
 434                           else (ss1,ss2)) auto.transitions q acc ) states (SSet.empty,SSet.empty)
 435           in
 436             if SSet.is_empty (SSet.inter auto.marking (SSet.union s1 s2))
 437             then ()
 438             else auto.result <- BST.add t auto.result;
 439             run_in auto t1 s1;
 440             run_in auto t2 s2
 441
 442
 443   let run auto t =
 444     auto.result <- BST.empty;
 445     P(auto.numbt <- 0);
 446
 447       run_in auto t auto.initial
 448
 449 end