- let eval_form_bool f s1 s2 =
- let rec eval f = match f.pos with
- | Atom((`Left|`LLeft),b,q) -> if b == (Ptset.mem q s1) then (true,true,false) else false,false,false
- | Atom((`Right|`RRight),b,q) -> if b == (Ptset.mem q s2) then (true,false,true) else false,false,false
- (* test some inlining *)
- | True -> true,true,true
- | False -> false,false,false
- | _ ->
- try
- HFEval.find hfeval (f.fid,s1,s2)
- with
- | Not_found -> let r =
- match f.pos with
- | Or(f1,f2) ->
- let b1,rl1,rr1 = eval f1
- in
- if b1 && rl1 && rr1 then (true,true,true)
- else
- let b2,rl2,rr2 = eval f2
- in
- let rl1,rr1 = if b1 then rl1,rr1 else false,false
- and rl2,rr2 = if b2 then rl2,rr2 else false,false
- in (b1 || b2, rl1||rl2,rr1||rr2)
- | And(f1,f2) ->
- let b1,rl1,rr1 = eval f1 in
- if b1 && rl1 && rr1 then (true,true,true)
- else if b1
- then let b2,rl2,rr2 = eval f2 in
- if b2 then (true,rl1||rl2,rr1||rr2)
- else (false,false,false)
- else (false,false,false)
- | _ -> assert false
- in
- HFEval.add hfeval (f.fid,s1,s2) r;
- r
- in eval f
-
-
- let fstate_pool = Hashtbl.create 11
-
- let merge_pred a b = match a,b with
- | Some(f1), Some(f2) -> Some(fun x -> f1 x || f2 x)
- | None,None -> None
- | None,Some(_) -> b
- | Some(_),None -> a
-
- let acc_pred p l1 l2 = match p with
- | `Left _ -> p::l1,l2
- | `Right _ -> l1,p::l2
- | _ -> l1,l2
-
-
- let merge_trans t a tag q acc =
- List.fold_left (fun (accf,accm,acchtrue) (ts,(m,f,pred)) ->
- if TagSet.mem tag ts
- then
- let tmpf,hastrue =
- if is_true f then
- let newfinal =
- try Hashtbl.find fstate_pool f.fid with
- | Not_found -> let s = mk_state() in
- a.states <- Ptset.add s a.states;
- a.final <- Ptset.add s a.final;
- Hashtbl.add fstate_pool f.fid s;s
- in
- (atom_ `Left true newfinal),true
- else f,false in
- (or_ tmpf accf,accm||m,acchtrue||hastrue)
- else (accf,accm,acchtrue)
- ) acc (try Hashtbl.find a.phi q with Not_found -> [])
-
- let get_trans t a tag r =
- try
- let mark,f,predl,has_true =
- HTagSet.find a.sigma (r,tag)
- in f.st,f,mark,has_true,r
- with
- Not_found ->
- let f,mark,has_true,accq =
- Ptset.fold (fun q (accf,accm,acchtrue,accq) ->
- let naccf,naccm,nacctrue =
- merge_trans t a tag q (accf,accm,acchtrue )
- in
- if is_false naccf then (naccf,naccm,nacctrue,accq)
- else (naccf,naccm,nacctrue,Ptset.add q accq)
- )
- r (false_,false,false,Ptset.empty)
- in
- HTagSet.add a.sigma (accq,tag) (mark,f,([],[]),has_true);
- f.st,f,mark,has_true,accq
-
- let h_union = Hashtbl.create 4097
-
- let pt_cup s1 s2 =
- let h = (Ptset.hash s1,Ptset.hash s2) in
- try
- Hashtbl.find h_union h
- with
- | Not_found -> let s = Ptset.union s1 s2
- in
- Hashtbl.add h_union h s;s
+
+let dump ppf a =
+ Format.fprintf ppf "Automaton (%i) :\n" a.id;
+ Format.fprintf ppf "States : "; StateSet.print ppf a.states;
+ Format.fprintf ppf "\nInitial states : "; StateSet.print ppf a.init;
+ Format.fprintf ppf "\nAlternating transitions :\n";
+ let l = Hashtbl.fold (fun k t acc ->
+ (List.map (fun (ts,tr) -> (ts,k),Transition.node tr) t) @ acc) a.trans [] in
+ let l = List.sort (fun ((tsx,x),_) ((tsy,y),_) ->
+ if y-x == 0 then TagSet.compare tsy tsx else y-x) l in
+ let maxh,maxt,l_print =
+ List.fold_left (
+ fun (maxh,maxt,l) ((ts,q),(_,b,f,_)) ->
+ let s =
+ if TagSet.is_finite ts
+ then "{" ^ (TagSet.fold (fun t a -> a ^ " '" ^ (Tag.to_string t)^"'") ts "") ^" }"
+ else let cts = TagSet.neg ts in
+ if TagSet.is_empty cts then "*" else
+ (TagSet.fold (fun t a -> a ^ " " ^ (Tag.to_string t)) cts "*\\{"
+ )^ "}"
+ in
+ let s = Printf.sprintf "(%s,%i)" s q in
+ let s_frm =
+ Formula.print Format.str_formatter f;
+ Format.flush_str_formatter()
+ in
+ (max (String.length s) maxh, max (String.length s_frm) maxt,
+ (s,(if b then "⇒" else "→"),s_frm)::l)) (0,0,[]) l
+ in
+ Format.fprintf ppf "%s\n%!" (String.make (maxt+maxh+3) '_');
+ List.iter (fun (s,m,f) -> let s = s ^ (String.make (maxh-(String.length s)) ' ') in
+ Format.fprintf ppf "%s %s %s\n" s m f) l_print;
+ Format.fprintf ppf "%s\n%!" (String.make (maxt+maxh+3) '_')
+