1 (* Todo refactor and remove this alias *)
3 module Tree = Tree.Binary
5 let gen_id() = Oo.id (object end)
12 let mk_state = State.mk
16 type predicate = Ptset.t*Ptset.t -> Tree.t -> [ `True | `False | `Maybe ]
20 | Or of formula * formula
21 | And of formula * formula
22 | Atom of ([ `Left | `Right ]*bool*state*predicate option)
23 and formula = { fid: int;
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
40 let hash t = (hash t.pos) land max_int
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
47 | And(g1,g2),And(h1,h2) -> g1.fid == h1.fid && g2.fid == h2.fid
50 module WH = Weak.Make(FormNode)
52 let f_pool = WH.create 107
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 }
62 let is_true f = f.fid == 1
63 let is_false f = f.fid == 0
66 let cons pos neg s1 s2 =
79 (WH.merge f_pool pnode),(WH.merge f_pool nnode)
81 let atom_ ?(pred=None) d p s =
82 let si = Ptset.singleton s in
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 )
88 let merge_states f1 f2 =
90 Ptset.union (fst f1.st) (fst f2.st),
91 Ptset.union (snd f1.st) (snd f2.st)
93 Ptset.union (fst f1.neg.st) (fst f2.neg.st),
94 Ptset.union (snd f1.neg.st) (snd f2.neg.st)
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
104 let sp,sn = merge_states f1 f2 in
105 fst (cons (Or(f1,f2)) (And(f1.neg,f2.neg)) sp sn)
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
115 let sp,sn = merge_states f1 f2 in
116 fst (cons (And(f1,f2)) (Or(f1.neg,f2.neg)) sp sn)
121 type property = [ `None | `Existential ]
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;
141 module Pair (X : Set.OrderedType) (Y : Set.OrderedType) =
144 let compare (x1,y1) (x2,y2) =
145 let r = X.compare x1 x2 in
146 if r == 0 then Y.compare y1 y2
150 module PL = Set.Make (Pair (Ptset) (Ptset))
153 let pr_st ppf l = Format.fprintf ppf "{";
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
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 "⊤"
166 Format.fprintf ppf "(";
168 Format.fprintf ppf ") ∧ (";
170 Format.fprintf ppf ")"
173 Format.fprintf ppf " ∨ ";
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>")
180 let dnf_hash = Hashtbl.create 17
182 let rec dnf_aux f = match f.pos with
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)
192 PL.fold (fun (s1,s2) acc ->
193 PL.fold ( fun (s1', s2') acc' ->
195 ((Ptset.union s1 s1'),
196 (Ptset.union s2 s2')) acc') )
203 Hashtbl.find dnf_hash f.fid
207 Hashtbl.add dnf_hash f.fid d;d
210 let equal_form f1 f2 =
211 (f1.fid == f2.fid) || (FormNode.equal f1 f2) || (PL.equal (dnf f1) (dnf f2))
213 let alt_trans_to_nfa ?(accu=[]) ts s mark f =
216 PL.fold (fun (s1,s2) acc -> (ts,s,mark,s1,s2)::acc) f' accu
219 let possible_trans ?(accu=[]) a q tag =
220 (* todo change the data structure to avoid creating (,) *)
222 Hashtbl.fold (fun (ts,s) (m,f) acc ->
223 if (q==s) && (TagSet.mem tag ts)
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
233 Hashtbl.remove a.phi (ts,s);
234 if not (TagSet.is_empty ts')
235 then Hashtbl.add a.phi (ts',s) (m,f)
237 Hashtbl.remove a.phi (ts,s)
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
243 List.iter (fun (ts,s,m,s1,s2) ->
244 Hashtbl.add a.delta ts ((Ptset.singleton s),m,s1,s2)) nfa_trs
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
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)) ->
263 Tag.to_string (TagSet.choose ts)
267 Format.fprintf ppf "(%s,%i) %s " s q (if b then "=>" else "->");
269 Format.fprintf ppf "\n")l;
271 Format.fprintf ppf "NFA transitions :\n------------------------------\n";
272 Hashtbl.iter (fun (ts) (q,b,s1,s2) ->
276 Tag.to_string (TagSet.choose ts)
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"
289 module Transitions = struct
290 type t = state*TagSet.t*bool*formula
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
300 type transition = Transitions.t
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)
305 module TS : Set.S with type elt = Tree.t = Set.Make(Tree)
306 let res = ref TS.empty
309 module BottomUpNew = struct
314 | TNil of Ptset.t*Ptset.t
315 | TNode of Ptset.t*Ptset.t*bool* (int*bool*formula) list
317 let traces = Hashtbl.create 17
319 let out = open_out "debug_trace.dot"
321 let outf = Format.formatter_of_out_channel out in
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 "→");
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
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
349 match Hashtbl.find traces (-10) with
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";
360 Format.fprintf outf "digraph G {\n";
362 Format.fprintf outf "}\n%!";
364 ignore(Sys.command "dot -Tsvg debug_trace.dot > debug_trace.svg")
369 let hfeval = Hashtbl.create 17
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
379 let eval_form f s1 s2 res1 res2 =
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
387 let b1,r1 = eval_aux f1
388 and b2,r2 = eval_aux f2
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)
395 let b1,r1 = eval_aux f1
396 and b2,r2 = eval_aux f2
398 if b1 && b2 then (true, TS.union r1 r2)
399 else (false,TS.empty)
401 in incr call;eval_aux f
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
409 let val3 = function true -> `True
412 let or3 a b = match a,b with
413 | `True,_ | _,`True -> `True
414 | `False,`False -> `False
417 let and3 a b = match a,b with
418 | `True,`True -> `True
419 | `False,_ | _,`False -> `False
426 let true3 = function true -> `Maybe
429 let may_eval (s1,s2) f t =
430 let rec aux f = match f.pos with
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
438 | `Right -> s2)) == b))
440 | Some pred -> (pred (s1,s2) t)
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))
451 let _ = D(Hashtbl.add traces (-10) (TNil(r,Ptset.inter a.final r)))
453 Ptset.inter a.final r,TS.empty
456 and t1 = Tree.first_child t
457 and t2 = Tree.next_sibling t
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
463 (* Format.fprintf Format.err_formatter "Tree with tag %s qualifies for transition : (%s,%i)%s"
466 Tag.to_string (TagSet.choose ts)
470 (if m then "=>" else "->");
471 pr_frm Format.err_formatter f;
472 Format.fprintf Format.err_formatter "\n"; *)
474 Ptset.union ls ar1,Ptset.union rs ar2,(q,tr)::lt
477 ) a.phi (Ptset.empty,Ptset.empty,[])
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
484 (* Format.fprintf ppf "Will skip (%i) %s " q (if m then "=>" else "->");
486 Format.fprintf ppf ", always true \n"; *)
487 (Ptset.add q at),af,am,atrs,TS.add t selnodes
489 (*Format.fprintf ppf "Will skip (%i) %s " q (if m then "=>" else "->");
491 Format.fprintf ppf ", always false \n"; *)
492 at,(Ptset.add q af),am,atrs,selnodes
495 (* Format.fprintf ppf "Must take (%i) %s " q (if m then "=>" else "->");
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
502 List.fold_left (fun ((ar1,ar2,trs)as acc) ((q,(_,f)as tr)) ->
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
508 let s1,res1 = accepting_among a t1 rr1
509 and s2,res2 = accepting_among a t2 rr2
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
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);
524 (if mark then TS.add t resnodes else resnodes)
526 ,Ptset.add q res,amark||mark,(q,mark,f)::acctr
528 ) (TS.empty,rtrue,false,[]) trs
531 let set = Ptset.union a.final set in
532 let _ = D(Hashtbl.add traces (Tree.id t) (TNode(r,set,mark,trs))) in
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
541 else (TS.elements res)