- 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) -> Format.fprintf ppf "%s%s[%i]"
- (if b then "" else "¬")
- (match dir with
- | `Left -> "↓₁"
- | `Right -> "↓₂"
- | `LLeft -> "⇓₁"
- | `RRight -> "⇓₂") s
-
- 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|`LLeft),_,s) -> PL.singleton (Ptset.singleton s,Ptset.empty)
- | Atom((`Right|`RRight),_,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 can_top_down f =
- let nf = dnf f in
- if (PL.cardinal nf > 3)then None
- else match PL.elements nf with
- | [(s1,s2); (t1,t2); (u1,u2)] when
- Ptset.is_empty s1 && Ptset.is_empty s2 && Ptset.is_empty t1 && Ptset.is_empty u2
- -> Some(true,t2,u1)
- | [(t1,t2); (u1,u2)] when Ptset.is_empty t1 && Ptset.is_empty u2
- -> Some(false,t2,u1)
- | _ -> None
-
-
- let equal_form f1 f2 =
- (f1.fid == f2.fid) || (FormNode.equal f1 f2) || (PL.equal (dnf f1) (dnf f2))
-
- 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 ->
- (List.map (fun (t,(m,f,p)) -> (t,k),(m,f,p)) 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 =
- 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
- 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";
-(* HTagSet.iter (fun (qs,t) (disp,b,_,flist,_,_) ->
- let (ls,lls,_),(rs,rrs,_) =
- List.fold_left (fun ((a1,b1,c1),(a2,b2,c2)) (_,f) ->
- let (x1,y1,z1),(x2,y2,z2) = f.st in
- ((Ptset.union x1 a1),(Ptset.union y1 b1),(Ptset.union c1 z1)),
- ((Ptset.union x2 a2),(Ptset.union y2 b2),(Ptset.union c2 z2)))
- ((Ptset.empty,Ptset.empty,Ptset.empty),
- (Ptset.empty,Ptset.empty,Ptset.empty))
- flist
- in
- pr_st ppf (Ptset.elements qs);
- Format.fprintf ppf ",%s %s " (Tag.to_string t) (if b then "=>" else "->");
- List.iter (fun (q,f) ->
- Format.fprintf ppf "\n%i," q;
- pr_frm ppf f) flist;
- Format.fprintf ppf "\nleft=";
- pr_st ppf (Ptset.elements ls);
- Format.fprintf ppf " , ";
- pr_st ppf (Ptset.elements lls);
- Format.fprintf ppf ", right=";
- pr_st ppf (Ptset.elements rs);
- Format.fprintf ppf ", ";
- pr_st ppf (Ptset.elements rrs);
- Format.fprintf ppf ", first=%s, next=%s\n\n" disp.flabel disp.nlabel;
- ) a.sigma; *)
- Format.fprintf ppf "=======================================\n%!"
+
+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) '_')