(* 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 -> "" | _ -> " ") 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