+(* Todo refactor and remove this alias *)
+INCLUDE "debug.ml"
+module Tree = Tree.Binary
+
+let gen_id() = Oo.id (object end)
+module State = struct
+
+ type t = int
+ let mk = gen_id
+
+end
+let mk_state = State.mk
+
+type state = State.t
+
+type predicate = Ptset.t*Ptset.t -> Tree.t -> [ `True | `False | `Maybe ]
+
+type formula_expr =
+ | False | True
+ | Or of formula * formula
+ | And of formula * formula
+ | Atom of ([ `Left | `Right ]*bool*state*predicate option)
+and formula = { fid: int;
+ pos : formula_expr;
+ neg : formula;
+ st : Ptset.t*Ptset.t;
+ }
+
+
+module FormNode =
+struct
+ type t = formula
+ let hash = function
+ | False -> 0
+ | True -> 1
+ | And(f1,f2) -> 2+17*f1.fid + 37*f2.fid
+ | Or(f1,f2) -> 3+101*f1.fid + 253*f2.fid
+ | Atom(d,b,s,_) -> 5+(if d=`Left then 11 else 19)*(if b then 23 else 31)*s
+
+ let hash t = (hash t.pos) land max_int
+
+ let equal f1 f2 =
+ match f1.pos,f2.pos with
+ | False,False | True,True -> true
+ | Atom(d1,b1,s1,_), Atom(d2,b2,s2,_) when (d1 = d2) && (b1=b2) &&(s1=s2) -> true
+ | Or(g1,g2),Or(h1,h2)
+ | And(g1,g2),And(h1,h2) -> g1.fid == h1.fid && g2.fid == h2.fid
+ | _ -> false
+end
+module WH = Weak.Make(FormNode)
+
+let f_pool = WH.create 107
+
+let true_,false_ =
+ let rec t = { fid = 1; pos = True; neg = f ; st = Ptset.empty,Ptset.empty}
+ and f = { fid = 0; pos = False; neg = t; st = Ptset.empty,Ptset.empty }
+ in
+ WH.add f_pool f;
+ WH.add f_pool t;
+ t,f
+
+let is_true f = f.fid == 1
+let is_false f = f.fid == 0
+
+
+let cons pos neg s1 s2 =
+ let rec pnode =
+ { fid = gen_id ();
+ pos = pos;
+ neg = nnode;
+ st = s1; }
+ and nnode = {
+ fid = gen_id ();
+ pos = neg;
+ neg = pnode;
+ st = s2;
+ }
+ in
+ (WH.merge f_pool pnode),(WH.merge f_pool nnode)
+
+let atom_ ?(pred=None) d p s =
+ let si = Ptset.singleton s in
+ let ss = match d with
+ | `Left -> si,Ptset.empty
+ | `Right -> Ptset.empty,si
+ in fst (cons (Atom(d,p,s,pred)) (Atom(d,not p,s,pred)) ss ss )
+
+let merge_states f1 f2 =
+ let sp =
+ Ptset.union (fst f1.st) (fst f2.st),
+ Ptset.union (snd f1.st) (snd f2.st)
+ and sn =
+ Ptset.union (fst f1.neg.st) (fst f2.neg.st),
+ Ptset.union (snd f1.neg.st) (snd f2.neg.st)
+ in
+ sp,sn
+
+let or_ f1 f2 =
+ if is_true f1 || is_true f2 then true_
+ else if is_false f1 && is_false f2 then false_
+ else if is_false f1 then f2
+ else if is_false f2 then f1
+ else
+ let sp,sn = merge_states f1 f2 in
+ fst (cons (Or(f1,f2)) (And(f1.neg,f2.neg)) sp sn)
+
+
+
+let and_ f1 f2 =
+ if is_true f1 && is_true f2 then true_
+ else if is_false f1 || is_false f2 then false_
+ else if is_true f1 then f2
+ else if is_true f2 then f1
+ else
+ let sp,sn = merge_states f1 f2 in
+ fst (cons (And(f1,f2)) (Or(f1.neg,f2.neg)) sp sn)
+
+
+let not_ f = f.neg
+
+type property = [ `None | `Existential ]
+let get_prop h s =
+ try
+ Hashtbl.find h s
+ with
+ Not_found -> `None
+
+type t = {
+ id : int;
+ states : Ptset.t;
+ init : Ptset.t;
+ final : Ptset.t;
+ universal : Ptset.t;
+ (* Transitions of the Alternating automaton *)
+ (* (tags,q) -> (marking,formula) *)
+ phi : ((TagSet.t*state),(bool*formula)) Hashtbl.t;
+ delta : (TagSet.t,(Ptset.t*bool*Ptset.t*Ptset.t)) Hashtbl.t;
+ properties : (state,property) Hashtbl.t;
+ }
+
+ module Pair (X : Set.OrderedType) (Y : Set.OrderedType) =
+ struct
+ type t = X.t*Y.t
+ let compare (x1,y1) (x2,y2) =
+ let r = X.compare x1 x2 in
+ if r == 0 then Y.compare y1 y2
+ else r
+ end
+
+ module PL = Set.Make (Pair (Ptset) (Ptset))
+
+
+ let pr_st ppf l = Format.fprintf ppf "{";
+ begin
+ match l with
+ | [] -> ()
+ | [s] -> Format.fprintf ppf " %i" s
+ | p::r -> Format.fprintf ppf " %i" p;
+ List.iter (fun i -> Format.fprintf ppf "; %i" i) r
+ end;
+ Format.fprintf ppf " }"
+ let rec pr_frm ppf f = match f.pos with
+ | True -> Format.fprintf ppf "⊤"
+ | False -> Format.fprintf ppf "⊤"
+ | And(f1,f2) ->
+ Format.fprintf ppf "(";
+ (pr_frm ppf f1);
+ Format.fprintf ppf ") ∧ (";
+ (pr_frm ppf f2);
+ Format.fprintf ppf ")"
+ | Or(f1,f2) ->
+ (pr_frm ppf f1);
+ Format.fprintf ppf " ∨ ";
+ (pr_frm ppf f2);
+ | Atom(dir,b,s,p) -> Format.fprintf ppf "%s%s[%i]%s"
+ (if b then "" else "¬")
+ (if dir = `Left then "↓₁" else "↓₂")s
+ (match p with None -> "" | _ -> " <hint>")
+
+ let dnf_hash = Hashtbl.create 17
+
+ let rec dnf_aux f = match f.pos with
+ | False -> PL.empty
+ | True -> PL.singleton (Ptset.empty,Ptset.empty)
+ | Atom(`Left,_,s,_) -> PL.singleton (Ptset.singleton s,Ptset.empty)
+ | Atom(`Right,_,s,_) -> PL.singleton (Ptset.empty,Ptset.singleton s)
+ | Or(f1,f2) -> PL.union (dnf f1) (dnf f2)
+ | And(f1,f2) ->
+ let pl1 = dnf f1
+ and pl2 = dnf f2
+ in
+ PL.fold (fun (s1,s2) acc ->
+ PL.fold ( fun (s1', s2') acc' ->
+ (PL.add
+ ((Ptset.union s1 s1'),
+ (Ptset.union s2 s2')) acc') )
+ pl2 acc )
+ pl1 PL.empty
+
+
+ and dnf f =
+ try
+ Hashtbl.find dnf_hash f.fid
+ with
+ Not_found ->
+ let d = dnf_aux f in
+ Hashtbl.add dnf_hash f.fid d;d
+
+
+ let equal_form f1 f2 =
+ (f1.fid == f2.fid) || (FormNode.equal f1 f2) || (PL.equal (dnf f1) (dnf f2))
+
+ let alt_trans_to_nfa ?(accu=[]) ts s mark f =
+ (* todo memoize *)
+ let f' = dnf f in
+ PL.fold (fun (s1,s2) acc -> (ts,s,mark,s1,s2)::acc) f' accu
+
+
+ let possible_trans ?(accu=[]) a q tag =
+ (* todo change the data structure to avoid creating (,) *)
+ let ata_trans =
+ Hashtbl.fold (fun (ts,s) (m,f) acc ->
+ if (q==s) && (TagSet.mem tag ts)
+ then (ts,s,m,f)::acc
+ else acc) a.phi []
+ in
+ if ata_trans != []
+ then begin
+ List.iter (fun (ts,s,m,f) ->
+ (* The following builds too many transitions in the nfa
+ let ts' = TagSet.remove tag ts
+ in
+ Hashtbl.remove a.phi (ts,s);
+ if not (TagSet.is_empty ts')
+ then Hashtbl.add a.phi (ts',s) (m,f)
+ *)
+ Hashtbl.remove a.phi (ts,s)
+ ) ata_trans;
+ (* let tstag = TagSet.tag tag in *)
+ let nfa_trs = List.fold_left (fun acc (ts,s,m,f) ->
+ alt_trans_to_nfa ~accu:acc ts s m f) [] ata_trans
+ in
+ List.iter (fun (ts,s,m,s1,s2) ->
+ Hashtbl.add a.delta ts ((Ptset.singleton s),m,s1,s2)) nfa_trs
+ end;
+ Hashtbl.fold (fun ts (s,m,s1,s2) acc ->
+ if (Ptset.mem q s) && (TagSet.mem tag ts)
+ then (m,s1,s2)::acc else acc) a.delta accu
+
+ let dump ppf a =
+ Format.fprintf ppf "Automaton (%i) :\n" a.id;
+ Format.fprintf ppf "States : "; pr_st ppf (Ptset.elements a.states);
+ Format.fprintf ppf "\nInitial states : "; pr_st ppf (Ptset.elements a.init);
+ Format.fprintf ppf "\nFinal states : "; pr_st ppf (Ptset.elements a.final);
+ Format.fprintf ppf "\nUniversal states : "; pr_st ppf (Ptset.elements a.universal);
+ Format.fprintf ppf "\nAlternating transitions :\n------------------------------\n";
+ let l = Hashtbl.fold (fun k t acc -> (k,t)::acc) a.phi [] in
+ let l = List.sort (fun ((tsx,x),_) ((tsy,y),_) -> if x-y == 0 then TagSet.compare tsx tsy else x-y) l in
+ List.iter (fun ((ts,q),(b,f)) ->
+
+ let s =
+ try
+ Tag.to_string (TagSet.choose ts)
+ with
+ | _ -> "*"
+ in
+ Format.fprintf ppf "(%s,%i) %s " s q (if b then "=>" else "->");
+ pr_frm ppf f;
+ Format.fprintf ppf "\n")l;
+
+ Format.fprintf ppf "NFA transitions :\n------------------------------\n";
+ Hashtbl.iter (fun (ts) (q,b,s1,s2) ->
+
+ let s =
+ try
+ Tag.to_string (TagSet.choose ts)
+ with
+ | _ -> "*"
+ in
+ pr_st ppf (Ptset.elements q);
+ Format.fprintf ppf ",%s %s " s (if b then "=>" else "->");
+ Format.fprintf ppf "(";
+ pr_st ppf (Ptset.elements s1);
+ Format.fprintf ppf ",";
+ pr_st ppf (Ptset.elements s2);
+ Format.fprintf ppf ")\n" ) a.delta;
+ Format.fprintf ppf "=======================================\n"
+
+ module Transitions = struct
+ type t = state*TagSet.t*bool*formula
+ let ( ?< ) x = x
+ let ( >< ) state label = state,label
+ let ( >=> ) (state,(label,mark)) form = (state,label,mark,form)
+ let ( +| ) f1 f2 = or_ f1 f2
+ let ( *& ) f1 f2 = and_ f1 f2
+ let ( ** ) d s = atom_ d true s
+
+
+ end
+ type transition = Transitions.t
+
+ let equal_trans (q1,t1,m1,f1) (q2,t2,m2,f2) =
+ (q1 == q2) && (TagSet.equal t1 t2) && (m1 == m2) && (equal_form f1 f2)
+
+ module TS : Set.S with type elt = Tree.t = Set.Make(Tree)
+ let res = ref TS.empty
+
+
+ module BottomUpNew = struct
+
+IFDEF DEBUG
+THEN
+ type trace =
+ | TNil of Ptset.t*Ptset.t
+ | TNode of Ptset.t*Ptset.t*bool* (int*bool*formula) list
+
+ let traces = Hashtbl.create 17
+ let dump_trace t =
+ let out = open_out "debug_trace.dot"
+ in
+ let outf = Format.formatter_of_out_channel out in
+
+ let rec aux t num =
+ if Tree.is_node t
+ then
+ match (try Hashtbl.find traces (Tree.id t) with Not_found -> TNil(Ptset.empty,Ptset.empty)) with
+ | TNode(r,s,mark,trs) ->
+ let numl = aux (Tree.left t) num in
+ let numr = aux (Tree.right t) (numl+1) in
+ let mynum = numr + 1 in
+ Format.fprintf outf "n%i [ label=\"<%s>\\nr=" mynum (Tag.to_string (Tree.tag t));
+ pr_st outf (Ptset.elements r);
+ Format.fprintf outf "\\ns=";
+ pr_st outf (Ptset.elements s);
+ List.iter (fun (q,m,f) ->
+ Format.fprintf outf "\\n%i %s" q (if m then "⇨" else "→");
+ pr_frm outf f ) trs;
+ Format.fprintf outf "\", %s shape=box ];\n"
+ (if mark then "color=cyan1, style=filled," else "");
+ let _ = Format.fprintf outf "n%i -> n%i;\n" mynum numl in
+ let _ = Format.fprintf outf "n%i -> n%i;\n" mynum numr in
+ mynum
+ | TNil(r,s) -> Format.fprintf outf "n%i [ shape=box, label=\"Nil\\nr=" num;
+ pr_st outf (Ptset.elements r);
+ Format.fprintf outf "\\ns=";
+ pr_st outf (Ptset.elements s);
+ Format.fprintf outf "\"];\n";num
+ else
+ match Hashtbl.find traces (-10) with
+ | TNil(r,s) ->
+ Format.fprintf outf "n%i [ shape=box, label=\"Nil\\nr=" num;
+ pr_st outf (Ptset.elements r);
+ Format.fprintf outf "\\ns=";
+ pr_st outf (Ptset.elements s);
+ Format.fprintf outf "\"];\n";
+ num
+ | _ -> assert false
+
+ in
+ Format.fprintf outf "digraph G {\n";
+ ignore(aux t 0);
+ Format.fprintf outf "}\n%!";
+ close_out out;
+ ignore(Sys.command "dot -Tsvg debug_trace.dot > debug_trace.svg")
+END
+
+
+
+ let hfeval = Hashtbl.create 17
+ let miss = ref 0
+ let call = ref 0
+ let rec findlist s1 s2 = function
+ | [] -> raise Not_found
+ | ((ss1,ss2),r)::_ when
+ (not (Ptset.is_empty s1)) && (Ptset.subset s1 ss1) &&
+ (not (Ptset.is_empty s2)) && (Ptset.subset s2 ss2) -> r
+ | _::r -> findlist s1 s2 r
+
+ let eval_form f s1 s2 res1 res2 =
+
+ let rec eval_aux f = match f.pos with
+ | Atom(`Left,b,q,_) -> if b == (Ptset.mem q s1) then (true,res1) else false,TS.empty
+ | Atom(`Right,b,q,_) -> if b == (Ptset.mem q s2) then (true,res2) else false,TS.empty
+ | True -> true,(TS.union res1 res2)
+ | False -> false,TS.empty
+ | Or(f1,f2) ->
+ let b1,r1 = eval_aux f1
+ and b2,r2 = eval_aux f2
+ in
+ let r1 = if b1 then r1 else TS.empty
+ and r2 = if b2 then r2 else TS.empty
+ in (b1 || b2, TS.union r1 r2)
+
+ | And(f1,f2) ->
+ let b1,r1 = eval_aux f1
+ and b2,r2 = eval_aux f2
+ in
+ if b1 && b2 then (true, TS.union r1 r2)
+ else (false,TS.empty)
+
+ in incr call;eval_aux f
+
+
+ (* If true, then the formule may evaluate to true in the future,
+ if false it will always return false, i.e. necessary conditions are not
+ satisfied
+ *)
+
+ let val3 = function true -> `True
+ | false -> `False
+
+ let or3 a b = match a,b with
+ | `True,_ | _,`True -> `True
+ | `False,`False -> `False
+ | _ -> `Maybe
+
+ let and3 a b = match a,b with
+ | `True,`True -> `True
+ | `False,_ | _,`False -> `False
+ | _ -> `Maybe
+ let not3 = function
+ | `True -> `False
+ | `False -> `True
+ | `Maybe -> `Maybe
+
+ let true3 = function true -> `Maybe
+ | false -> `False
+
+ let may_eval (s1,s2) f t =
+ let rec aux f = match f.pos with
+ | True -> `True
+ | False -> `False
+ | Or(f1,f2) -> or3 (aux f1) (aux f2)
+ | And(f1,f2) -> and3 (aux f1) (aux f2)
+ | Atom(dir,b,q,predo) ->
+ and3 (true3 ((Ptset.mem q (match dir with
+ | `Left -> s1
+ | `Right -> s2)) == b))
+ (match predo with
+ | Some pred -> (pred (s1,s2) t)
+ | None -> `True)
+
+ in aux f
+
+ let rec accepting_among a t r =
+ let r = Ptset.diff r a.final in
+ let rest = Ptset.inter a.final r in
+ if Ptset.is_empty r then r,TS.empty else
+ if (not (Tree.is_node t))
+ then
+ let _ = D(Hashtbl.add traces (-10) (TNil(r,Ptset.inter a.final r)))
+ in
+ Ptset.inter a.final r,TS.empty
+ else
+ let tag = Tree.tag t
+ and t1 = Tree.first_child t
+ and t2 = Tree.next_sibling t
+ in
+ let r1,r2,trs =
+ Hashtbl.fold (fun (ts,q) ((m,f)as tr) ((ar1,ar2,lt)as acc) ->
+ if (TagSet.mem tag ts) && Ptset.mem q r
+ then begin
+ (* Format.fprintf Format.err_formatter "Tree with tag %s qualifies for transition : (%s,%i)%s"
+ (Tag.to_string tag)
+ (try
+ Tag.to_string (TagSet.choose ts)
+ with
+ | _ -> "*" )
+ q
+ (if m then "=>" else "->");
+ pr_frm Format.err_formatter f;
+ Format.fprintf Format.err_formatter "\n"; *)
+ let ls,rs = f.st in
+ Ptset.union ls ar1,Ptset.union rs ar2,(q,tr)::lt
+ end
+ else acc
+ ) a.phi (Ptset.empty,Ptset.empty,[])
+ in
+ let rtrue,rfalse,rmay,trs,selnodes =
+ List.fold_left (fun (at,af,am,atrs,selnodes) (q,(m,f)) ->
+ let ppf = Format.err_formatter in
+ match (*may_eval (r1,r2) f t *) `Maybe with
+ | `True ->
+ (* Format.fprintf ppf "Will skip (%i) %s " q (if m then "=>" else "->");
+ pr_frm ppf f;
+ Format.fprintf ppf ", always true \n"; *)
+ (Ptset.add q at),af,am,atrs,TS.add t selnodes
+ | `False ->
+ (*Format.fprintf ppf "Will skip (%i) %s " q (if m then "=>" else "->");
+ pr_frm ppf f;
+ Format.fprintf ppf ", always false \n"; *)
+ at,(Ptset.add q af),am,atrs,selnodes
+
+ | `Maybe ->
+(* Format.fprintf ppf "Must take (%i) %s " q (if m then "=>" else "->");
+ pr_frm ppf f;
+ Format.fprintf ppf "\n"; *)
+ at,af,(Ptset.add q am),(q,(m,f))::atrs,selnodes)
+ (Ptset.empty,Ptset.empty,Ptset.empty,[],TS.empty) trs
+ in
+ let rr1,rr2,trs =
+ List.fold_left (fun ((ar1,ar2,trs)as acc) ((q,(_,f)as tr)) ->
+ if Ptset.mem q rmay
+ then let ls,rs = f.st in
+ Ptset.union ls ar1,Ptset.union rs ar2,tr::trs
+ else acc) (Ptset.empty,Ptset.empty,[]) trs
+ in
+ let s1,res1 = accepting_among a t1 rr1
+ and s2,res2 = accepting_among a t2 rr2
+ in
+ let res,set,mark,trs = List.fold_left (fun ((sel_nodes,res,amark,acctr) as acc) (q,(mark,f)) ->
+ let b,resnodes = eval_form f s1 s2 res1 res2 in
+ (* if b then begin
+ pr_st Format.err_formatter (Ptset.elements s1);
+ Format.fprintf Format.err_formatter ",";
+ pr_st Format.err_formatter (Ptset.elements s2);
+ Format.fprintf Format.err_formatter " satisfies ";
+ pr_frm Format.err_formatter f;
+ Format.fprintf Format.err_formatter " for input tree %s\n" (Tag.to_string tag);
+ end; *)
+ if b
+ then
+ (TS.union
+ (if mark then TS.add t resnodes else resnodes)
+ sel_nodes)
+ ,Ptset.add q res,amark||mark,(q,mark,f)::acctr
+ else acc
+ ) (TS.empty,rtrue,false,[]) trs
+ in
+
+ let set = Ptset.union a.final set in
+ let _ = D(Hashtbl.add traces (Tree.id t) (TNode(r,set,mark,trs))) in
+ set,res
+
+
+ let run a t =
+ let st,res = accepting_among a t a.init in
+ let b = Ptset.is_empty (st) in
+ let _ = D(dump_trace t) in
+ if b then []
+ else (TS.elements res)
+
+ end