ata.ml

   1 (* Todo refactor and remove this alias *)
   2 INCLUDE "debug.ml"
   3 module Tree = Tree.Binary
   4
   5 let gen_id() = Oo.id (object end)
   6 module State = struct
   7
   8   type t = int
   9   let mk = gen_id
  10
  11 end
  12 let mk_state = State.mk
  13
  14 type state = State.t
  15
  16 type predicate = Ptset.t*Ptset.t -> Tree.t -> [ `True | `False | `Maybe ]
  17
  18 type formula_expr =
  19   | False | True
  20     | Or of formula * formula
  21     | And of formula * formula
  22     | Atom of ([ `Left | `Right ]*bool*state*predicate option)
  23 and formula = { fid: int;
  24                   pos : formula_expr;
  25                   neg : formula;
  26                   st : Ptset.t*Ptset.t;
  27               }
  28
  29
  30 module FormNode =
  31 struct
  32   type t = formula
  33   let hash = function
  34     | False -> 0
  35     | True -> 1
  36     | And(f1,f2) -> 2+17*f1.fid + 37*f2.fid
  37     | Or(f1,f2) -> 3+101*f1.fid + 253*f2.fid
  38     | Atom(d,b,s,_) -> 5+(if d=`Left then 11 else 19)*(if b then 23 else 31)*s
  39
  40   let hash t = (hash t.pos) land max_int
  41
  42   let equal f1 f2 =
  43     match f1.pos,f2.pos with
  44       | False,False | True,True -> true
  45       | Atom(d1,b1,s1,_), Atom(d2,b2,s2,_) when (d1 = d2) && (b1=b2) &&(s1=s2) -> true
  46       | Or(g1,g2),Or(h1,h2)
  47       | And(g1,g2),And(h1,h2)  -> g1.fid == h1.fid && g2.fid == h2.fid
  48       | _ -> false
  49 end
  50 module WH = Weak.Make(FormNode)
  51
  52 let f_pool = WH.create 107
  53
  54 let true_,false_ =
  55   let rec t = { fid = 1; pos = True; neg = f ; st = Ptset.empty,Ptset.empty}
  56   and f = { fid = 0; pos = False; neg = t; st = Ptset.empty,Ptset.empty }
  57   in
  58     WH.add f_pool f;
  59     WH.add f_pool t;
  60     t,f
  61
  62 let is_true f = f.fid == 1
  63 let is_false f = f.fid == 0
  64
  65
  66 let cons pos neg s1 s2 =
  67   let rec pnode =
  68     { fid = gen_id ();
  69       pos = pos;
  70       neg = nnode;
  71       st = s1; }
  72   and nnode = {
  73     fid = gen_id ();
  74     pos = neg;
  75     neg = pnode;
  76     st = s2;
  77   }
  78   in
  79     (WH.merge f_pool pnode),(WH.merge f_pool nnode)
  80
  81 let atom_ ?(pred=None) d p s =
  82   let si = Ptset.singleton s in
  83   let ss = match d with
  84     | `Left -> si,Ptset.empty
  85     | `Right -> Ptset.empty,si
  86   in fst (cons (Atom(d,p,s,pred)) (Atom(d,not p,s,pred)) ss ss )
  87
  88 let merge_states f1 f2 =
  89   let sp =
  90     Ptset.union (fst f1.st) (fst f2.st),
  91     Ptset.union (snd f1.st) (snd f2.st)
  92   and sn =
  93     Ptset.union (fst f1.neg.st) (fst f2.neg.st),
  94     Ptset.union (snd f1.neg.st) (snd f2.neg.st)
  95   in
  96     sp,sn
  97
  98 let or_ f1 f2 =
  99   if is_true f1 || is_true f2 then true_
 100   else if is_false f1 && is_false f2 then false_
 101   else if is_false f1 then f2
 102   else if is_false f2 then f1
 103   else
 104     let sp,sn = merge_states f1 f2 in
 105       fst (cons (Or(f1,f2)) (And(f1.neg,f2.neg)) sp sn)
 106
 107
 108
 109 let and_ f1 f2 =
 110   if is_true f1 && is_true f2 then true_
 111   else if is_false f1 || is_false f2 then false_
 112   else if is_true f1 then f2
 113   else if is_true f2 then f1
 114   else
 115     let sp,sn = merge_states f1 f2 in
 116       fst (cons (And(f1,f2)) (Or(f1.neg,f2.neg)) sp sn)
 117
 118
 119 let not_ f = f.neg
 120
 121 type property = [ `None | `Existential  ]
 122 let get_prop h s =
 123   try
 124     Hashtbl.find h s
 125   with
 126       Not_found -> `None
 127
 128 type t = {
 129     id : int;
 130     states : Ptset.t;
 131     init : Ptset.t;
 132     final : Ptset.t;
 133     universal : Ptset.t;
 134     (* Transitions of the Alternating automaton *)
 135     (* (tags,q) -> (marking,formula) *)
 136     phi : ((TagSet.t*state),(bool*formula)) Hashtbl.t;
 137     delta : (TagSet.t,(Ptset.t*bool*Ptset.t*Ptset.t)) Hashtbl.t;
 138     properties : (state,property) Hashtbl.t;
 139   }
 140
 141   module Pair (X : Set.OrderedType) (Y : Set.OrderedType) =
 142   struct
 143     type t = X.t*Y.t
 144     let compare (x1,y1) (x2,y2) =
 145       let r = X.compare x1 x2 in
 146         if r == 0 then Y.compare y1 y2
 147         else r
 148   end
 149
 150   module PL = Set.Make (Pair (Ptset) (Ptset))
 151
 152
 153       let pr_st ppf l = Format.fprintf ppf "{";
 154     begin
 155       match l with
 156         |       [] -> ()
 157         | [s] -> Format.fprintf ppf " %i" s
 158         | p::r -> Format.fprintf ppf " %i" p;
 159             List.iter (fun i -> Format.fprintf ppf "; %i" i) r
 160     end;
 161     Format.fprintf ppf " }"
 162   let rec pr_frm ppf f = match f.pos with
 163     | True -> Format.fprintf ppf "⊤"
 164     | False -> Format.fprintf ppf "⊤"
 165     | And(f1,f2) ->
 166         Format.fprintf ppf "(";
 167         (pr_frm ppf f1);
 168         Format.fprintf ppf ") ∧ (";
 169         (pr_frm ppf f2);
 170         Format.fprintf ppf ")"
 171     | Or(f1,f2) ->
 172         (pr_frm ppf f1);
 173         Format.fprintf ppf " ∨ ";
 174         (pr_frm ppf f2);
 175     | Atom(dir,b,s,p) -> Format.fprintf ppf "%s%s[%i]%s"
 176         (if b then "" else "¬")
 177         (if dir = `Left then "↓₁" else "↓₂")s
 178           (match p with None -> "" | _ -> " <hint>")
 179
 180   let dnf_hash = Hashtbl.create 17
 181
 182   let rec dnf_aux f = match f.pos with
 183     | False -> PL.empty
 184     | True -> PL.singleton (Ptset.empty,Ptset.empty)
 185     | Atom(`Left,_,s,_) -> PL.singleton (Ptset.singleton s,Ptset.empty)
 186     | Atom(`Right,_,s,_) -> PL.singleton (Ptset.empty,Ptset.singleton s)
 187     | Or(f1,f2) -> PL.union (dnf f1) (dnf f2)
 188     | And(f1,f2) ->
 189           let pl1 = dnf f1
 190           and pl2 = dnf f2
 191           in
 192             PL.fold (fun (s1,s2) acc ->
 193                        PL.fold ( fun (s1', s2') acc' ->
 194                                    (PL.add
 195                                       ((Ptset.union s1 s1'),
 196                                        (Ptset.union s2 s2')) acc') )
 197                           pl2 acc )
 198               pl1 PL.empty
 199
 200
 201   and dnf f =
 202     try
 203       Hashtbl.find dnf_hash f.fid
 204     with
 205         Not_found ->
 206           let d = dnf_aux f in
 207             Hashtbl.add dnf_hash f.fid d;d
 208
 209
 210   let equal_form f1 f2 =
 211     (f1.fid == f2.fid) || (FormNode.equal f1 f2) || (PL.equal (dnf f1) (dnf f2))
 212
 213   let alt_trans_to_nfa ?(accu=[]) ts s mark f =
 214     (* todo memoize *)
 215     let f' = dnf f in
 216       PL.fold (fun (s1,s2) acc -> (ts,s,mark,s1,s2)::acc) f' accu
 217
 218
 219   let possible_trans ?(accu=[]) a q tag =
 220     (* todo change the data structure to avoid creating (,) *)
 221     let ata_trans =
 222       Hashtbl.fold (fun (ts,s) (m,f) acc ->
 223                       if (q==s) && (TagSet.mem tag ts)
 224                       then (ts,s,m,f)::acc
 225                       else acc) a.phi []
 226     in
 227       if ata_trans != []
 228       then begin
 229         List.iter (fun (ts,s,m,f) ->
 230                      (* The following builds too many transitions in the nfa
 231                      let ts' = TagSet.remove tag ts
 232                      in
 233                        Hashtbl.remove a.phi (ts,s);
 234                        if not (TagSet.is_empty ts')
 235                        then Hashtbl.add a.phi (ts',s) (m,f)
 236                      *)
 237                      Hashtbl.remove a.phi (ts,s)
 238                   ) ata_trans;
 239         (* let tstag = TagSet.tag tag in *)
 240         let nfa_trs = List.fold_left (fun acc (ts,s,m,f) ->
 241                                         alt_trans_to_nfa ~accu:acc ts s m f) [] ata_trans
 242         in
 243           List.iter (fun (ts,s,m,s1,s2) ->
 244                        Hashtbl.add a.delta ts ((Ptset.singleton s),m,s1,s2)) nfa_trs
 245       end;
 246       Hashtbl.fold (fun ts (s,m,s1,s2) acc ->
 247                       if (Ptset.mem q s) && (TagSet.mem tag ts)
 248                       then  (m,s1,s2)::acc else acc) a.delta accu
 249
 250   let dump ppf a =
 251     Format.fprintf ppf "Automaton (%i) :\n" a.id;
 252     Format.fprintf ppf "States : "; pr_st ppf (Ptset.elements a.states);
 253     Format.fprintf ppf "\nInitial states : "; pr_st ppf (Ptset.elements a.init);
 254     Format.fprintf ppf "\nFinal states : "; pr_st ppf (Ptset.elements a.final);
 255     Format.fprintf ppf "\nUniversal states : "; pr_st ppf (Ptset.elements a.universal);
 256     Format.fprintf ppf "\nAlternating transitions :\n------------------------------\n";
 257     let l = Hashtbl.fold (fun k t acc -> (k,t)::acc) a.phi [] in
 258     let l = List.sort (fun ((tsx,x),_) ((tsy,y),_) -> if x-y == 0 then TagSet.compare tsx tsy else x-y) l in
 259     List.iter (fun ((ts,q),(b,f)) ->
 260
 261                     let s =
 262                       try
 263                         Tag.to_string (TagSet.choose ts)
 264                       with
 265                         | _ -> "*"
 266                     in
 267                       Format.fprintf ppf "(%s,%i) %s " s q (if b then "=>" else "->");
 268                       pr_frm ppf f;
 269                       Format.fprintf ppf "\n")l;
 270
 271     Format.fprintf ppf "NFA transitions :\n------------------------------\n";
 272     Hashtbl.iter (fun (ts) (q,b,s1,s2) ->
 273
 274                     let s =
 275                       try
 276                         Tag.to_string (TagSet.choose ts)
 277                       with
 278                         | _ -> "*"
 279                     in
 280                       pr_st ppf (Ptset.elements q);
 281                       Format.fprintf ppf ",%s  %s " s (if b then "=>" else "->");
 282                       Format.fprintf ppf "(";
 283                       pr_st ppf (Ptset.elements s1);
 284                       Format.fprintf ppf ",";
 285                       pr_st ppf (Ptset.elements s2);
 286                       Format.fprintf ppf ")\n" ) a.delta;
 287     Format.fprintf ppf "=======================================\n"
 288
 289   module Transitions = struct
 290     type t =  state*TagSet.t*bool*formula
 291     let ( ?< ) x = x
 292     let ( >< ) state label = state,label
 293     let ( >=> ) (state,(label,mark)) form = (state,label,mark,form)
 294     let ( +| ) f1 f2 = or_ f1 f2
 295     let ( *& ) f1 f2 = and_ f1 f2
 296     let ( ** ) d s = atom_ d true s
 297
 298
 299   end
 300   type transition = Transitions.t
 301
 302   let equal_trans (q1,t1,m1,f1) (q2,t2,m2,f2) =
 303     (q1 == q2) && (TagSet.equal t1 t2) && (m1 == m2) && (equal_form f1 f2)
 304
 305   module TS : Set.S with type elt = Tree.t = Set.Make(Tree)
 306   let res =  ref TS.empty
 307
 308
 309   module BottomUpNew = struct
 310
 311 IFDEF DEBUG
 312 THEN
 313     type trace =
 314       | TNil of Ptset.t*Ptset.t
 315       | TNode of Ptset.t*Ptset.t*bool* (int*bool*formula) list
 316
 317     let traces = Hashtbl.create 17
 318     let dump_trace t =
 319       let out = open_out "debug_trace.dot"
 320       in
 321       let outf = Format.formatter_of_out_channel out in
 322
 323       let rec aux t num =
 324         if Tree.is_node t
 325         then
 326           match (try Hashtbl.find traces (Tree.id t) with Not_found -> TNil(Ptset.empty,Ptset.empty)) with
 327             | TNode(r,s,mark,trs) ->
 328                 let numl = aux (Tree.left t) num in
 329                 let numr = aux (Tree.right t) (numl+1) in
 330                 let mynum = numr + 1 in
 331                   Format.fprintf outf "n%i [ label=\"<%s>\\nr=" mynum (Tag.to_string (Tree.tag t));
 332                   pr_st outf (Ptset.elements r);
 333                   Format.fprintf outf "\\ns=";
 334                   pr_st outf (Ptset.elements s);
 335                   List.iter (fun (q,m,f) ->
 336                                Format.fprintf outf "\\n%i %s" q (if m then "⇨" else "→");
 337                                pr_frm outf f ) trs;
 338                   Format.fprintf outf "\", %s shape=box ];\n"
 339                     (if mark then "color=cyan1, style=filled," else "");
 340                   let _ = Format.fprintf outf "n%i -> n%i;\n" mynum numl in
 341                   let _ = Format.fprintf outf "n%i -> n%i;\n" mynum numr in
 342                   mynum
 343             | TNil(r,s) -> Format.fprintf outf "n%i [ shape=box, label=\"Nil\\nr=" num;
 344                 pr_st outf (Ptset.elements r);
 345                 Format.fprintf outf "\\ns=";
 346                 pr_st outf (Ptset.elements s);
 347                 Format.fprintf outf "\"];\n";num
 348         else
 349           match Hashtbl.find traces (-10) with
 350             | TNil(r,s) ->
 351                 Format.fprintf outf "n%i [ shape=box, label=\"Nil\\nr=" num;
 352                 pr_st outf (Ptset.elements r);
 353                 Format.fprintf outf "\\ns=";
 354                 pr_st outf (Ptset.elements s);
 355                 Format.fprintf outf "\"];\n";
 356                 num
 357             | _ -> assert false
 358
 359       in
 360         Format.fprintf outf "digraph G {\n";
 361         ignore(aux t 0);
 362         Format.fprintf outf "}\n%!";
 363         close_out out;
 364         ignore(Sys.command "dot -Tsvg debug_trace.dot > debug_trace.svg")
 365 END
 366
 367
 368
 369     let hfeval = Hashtbl.create 17
 370     let miss = ref 0
 371     let call = ref 0
 372     let rec findlist s1 s2 = function
 373       | [] -> raise Not_found
 374       | ((ss1,ss2),r)::_ when
 375           (not (Ptset.is_empty s1)) && (Ptset.subset s1 ss1) &&
 376             (not (Ptset.is_empty s2)) && (Ptset.subset s2 ss2) -> r
 377       | _::r -> findlist s1 s2 r
 378
 379     let eval_form f s1 s2 res1 res2 =
 380
 381       let rec eval_aux f = match f.pos with
 382         | Atom(`Left,b,q,_) -> if b == (Ptset.mem q s1) then (true,res1) else false,TS.empty
 383         | Atom(`Right,b,q,_) -> if b == (Ptset.mem q s2) then (true,res2) else false,TS.empty
 384         | True -> true,(TS.union res1 res2)
 385         | False -> false,TS.empty
 386         | Or(f1,f2) ->
 387             let b1,r1 = eval_aux f1
 388             and b2,r2 = eval_aux f2
 389             in
 390             let r1 = if b1 then r1 else TS.empty
 391             and r2 = if b2 then r2 else TS.empty
 392             in (b1 || b2, TS.union r1 r2)
 393
 394         | And(f1,f2) ->
 395             let b1,r1 = eval_aux f1
 396             and b2,r2 = eval_aux f2
 397             in
 398               if b1 && b2 then (true, TS.union r1 r2)
 399               else (false,TS.empty)
 400
 401       in incr call;eval_aux f
 402
 403
 404     (* If true, then the formule may evaluate to true in the future,
 405        if false it will always return false, i.e. necessary conditions are not
 406        satisfied
 407     *)
 408
 409     let val3 = function true -> `True
 410       | false -> `False
 411
 412     let or3 a b = match a,b with
 413       | `True,_ | _,`True -> `True
 414       | `False,`False -> `False
 415       | _ -> `Maybe
 416
 417     let and3 a b = match a,b with
 418       | `True,`True -> `True
 419       | `False,_ | _,`False -> `False
 420       | _ -> `Maybe
 421     let not3 = function
 422       | `True -> `False
 423       | `False -> `True
 424       | `Maybe -> `Maybe
 425
 426     let true3 = function true -> `Maybe
 427       | false -> `False
 428
 429     let may_eval (s1,s2) f t =
 430       let rec aux f = match f.pos with
 431         | True -> `True
 432         | False -> `False
 433         | Or(f1,f2) -> or3 (aux f1) (aux f2)
 434         | And(f1,f2) -> and3 (aux f1) (aux f2)
 435         | Atom(dir,b,q,predo) ->
 436             and3 (true3 ((Ptset.mem q (match dir with
 437                                         | `Left -> s1
 438                                         | `Right -> s2)) == b))
 439               (match predo with
 440                  | Some pred -> (pred (s1,s2) t)
 441                  | None -> `True)
 442
 443       in aux f
 444
 445     let rec accepting_among a t r =
 446       let r = Ptset.diff r a.final in
 447       let rest = Ptset.inter a.final r in
 448         if Ptset.is_empty r then r,TS.empty else
 449           if (not (Tree.is_node t))
 450           then
 451             let _ = D(Hashtbl.add traces (-10) (TNil(r,Ptset.inter a.final r)))
 452             in
 453               Ptset.inter a.final r,TS.empty
 454           else
 455             let tag = Tree.tag t
 456             and t1 = Tree.first_child t
 457             and t2 = Tree.next_sibling t
 458             in
 459             let r1,r2,trs =
 460               Hashtbl.fold (fun (ts,q) ((m,f)as tr) ((ar1,ar2,lt)as acc) ->
 461                               if (TagSet.mem tag ts) && Ptset.mem q r
 462                               then begin
 463                                 (* Format.fprintf Format.err_formatter "Tree with tag %s qualifies for transition : (%s,%i)%s"
 464                                    (Tag.to_string tag)
 465                                    (try
 466                                    Tag.to_string (TagSet.choose ts)
 467                                    with
 468                                   | _ -> "*" )
 469                                    q
 470                                    (if m then "=>" else "->");
 471                                    pr_frm Format.err_formatter f;
 472                                    Format.fprintf Format.err_formatter "\n"; *)
 473                                 let ls,rs = f.st in
 474                               Ptset.union ls ar1,Ptset.union rs ar2,(q,tr)::lt
 475                               end
 476                               else acc
 477                            ) a.phi (Ptset.empty,Ptset.empty,[])
 478             in
 479             let rtrue,rfalse,rmay,trs,selnodes =
 480               List.fold_left (fun (at,af,am,atrs,selnodes) (q,(m,f)) ->
 481                                 let ppf = Format.err_formatter in
 482                                   match (*may_eval (r1,r2) f t *) `Maybe with
 483                               | `True ->
 484                                   (* Format.fprintf ppf "Will skip (%i) %s " q (if m then "=>" else "->");
 485                                   pr_frm ppf f;
 486                                   Format.fprintf ppf ", always true \n"; *)
 487                                   (Ptset.add q at),af,am,atrs,TS.add t selnodes
 488                               | `False ->
 489                                   (*Format.fprintf ppf "Will skip (%i) %s " q (if m then "=>" else "->");
 490                                   pr_frm ppf f;
 491                                   Format.fprintf ppf ", always false \n"; *)
 492                                   at,(Ptset.add q af),am,atrs,selnodes
 493
 494                               | `Maybe ->
 495 (*                                Format.fprintf ppf "Must take (%i) %s " q (if m then "=>" else "->");
 496                                   pr_frm ppf f;
 497                                   Format.fprintf ppf "\n"; *)
 498                                   at,af,(Ptset.add q am),(q,(m,f))::atrs,selnodes)
 499             (Ptset.empty,Ptset.empty,Ptset.empty,[],TS.empty) trs
 500         in
 501         let rr1,rr2,trs =
 502           List.fold_left (fun ((ar1,ar2,trs)as acc) ((q,(_,f)as tr)) ->
 503                             if Ptset.mem q rmay
 504                             then let ls,rs = f.st in
 505                               Ptset.union ls ar1,Ptset.union rs ar2,tr::trs
 506                             else acc) (Ptset.empty,Ptset.empty,[]) trs
 507         in
 508         let s1,res1 = accepting_among a t1 rr1
 509         and s2,res2 = accepting_among a t2 rr2
 510         in
 511         let res,set,mark,trs =  List.fold_left (fun  ((sel_nodes,res,amark,acctr) as acc) (q,(mark,f)) ->
 512                             let b,resnodes = eval_form f s1 s2 res1 res2 in
 513                               (*     if b then begin
 514                                      pr_st Format.err_formatter (Ptset.elements s1);
 515                                      Format.fprintf Format.err_formatter ",";
 516                                      pr_st Format.err_formatter (Ptset.elements s2);
 517                                      Format.fprintf Format.err_formatter "  satisfies ";
 518                                      pr_frm Format.err_formatter f;
 519                                      Format.fprintf Format.err_formatter " for input tree %s\n" (Tag.to_string tag);
 520                                      end; *)
 521                               if b
 522                               then
 523                                 (TS.union
 524                                    (if mark then TS.add t resnodes else resnodes)
 525                                    sel_nodes)
 526                                   ,Ptset.add q res,amark||mark,(q,mark,f)::acctr
 527                               else acc
 528                          ) (TS.empty,rtrue,false,[]) trs
 529         in
 530
 531         let set = Ptset.union a.final set in
 532         let _ = D(Hashtbl.add traces (Tree.id t) (TNode(r,set,mark,trs))) in
 533           set,res
 534
 535
 536     let run a t =
 537       let st,res = accepting_among a t a.init in
 538       let b = Ptset.is_empty (st) in
 539       let _ = D(dump_trace t) in
 540         if b then []
 541         else (TS.elements res)
 542
 543   end