+ let _ = _flush_str_fmt () in
+ let strs_strings, max_pre, max_all = List.fold_left (fun (accl, accp, acca) (q, s, f) ->
+ let s1 = State.print _str_fmt q; _flush_str_fmt () in
+ let s2 = QNameSet.print _str_fmt s; _flush_str_fmt () in
+ let s3 = SFormula.print _str_fmt f; _flush_str_fmt () in
+ let pre = Pretty.length s1 + Pretty.length s2 in
+ let all = Pretty.length s3 in
+ ( (q, s1, s2, s3) :: accl, max accp pre, max acca all)
+ ) ([], 0, 0) sorted_trs
+ in
+ let line = Pretty.line (max_all + max_pre + 6) in
+ let prev_q = ref State.dummy in
+ List.iter (fun (q, s1, s2, s3) ->
+ if !prev_q != q && !prev_q != State.dummy then fprintf fmt " %s\n%!" line;
+ prev_q := q;
+ fprintf fmt " %s, %s" s1 s2;
+ fprintf fmt "%s" (Pretty.padding (max_pre - Pretty.length s1 - Pretty.length s2));
+ fprintf fmt " %s %s@\n%!" Pretty.right_arrow s3;
+ ) strs_strings;
+ fprintf fmt " %s\n%!" line
+
+(*
+ [complete transitions a] ensures that for each state q
+ and each symbols s in the alphabet, a transition q, s exists.
+ (adding q, s -> F when necessary).
+*)
+
+let complete_transitions a =
+ StateSet.iter (fun q ->
+ let qtrans = Hashtbl.find a.transitions q in
+ let rem =
+ List.fold_left (fun rem (labels, _) ->
+ QNameSet.diff rem labels) QNameSet.any qtrans
+ in
+ let nqtrans =
+ if QNameSet.is_empty rem then qtrans
+ else
+ (rem, SFormula.false_) :: qtrans
+ in
+ Hashtbl.replace a.transitions q nqtrans
+ ) a.states
+
+(* [normalize_negations a] removes negative atoms in the formula
+ complementing the sub-automaton in the negative states.
+ [TODO check the meaning of negative upward arrows]
+*)
+let normalize_negations a =
+ let memo_state = Hashtbl.create 17 in
+ let todo = Queue.create () in
+ let rec flip b f =
+ match SFormula.expr f with
+ Formula.True | Formula.False -> if b then f else SFormula.not_ f
+ | Formula.Or(f1, f2) -> (if b then SFormula.or_ else SFormula.and_)(flip b f1) (flip b f2)
+ | Formula.And(f1, f2) -> (if b then SFormula.and_ else SFormula.or_)(flip b f1) (flip b f2)
+ | Formula.Atom(a) -> begin
+ let l, b', q = Move.node a in
+ if b == b' then begin
+ (* a appears positively, either no negation or double negation *)
+ if not (Hashtbl.mem memo_state (q,b)) then Queue.add (q,true) todo;
+ SFormula.atom_ (Move.make (l, true, q))
+ end else begin
+ (* need to reverse the atom
+ either we have a positive state deep below a negation
+ or we have a negative state in a positive formula
+ b' = sign of the state
+ b = sign of the containing formula
+ *)
+ let not_q =
+ try
+ (* does the inverted state of q exist ? *)
+ Hashtbl.find memo_state (q, false)
+ with
+ Not_found ->
+ (* create a new state and add it to the todo queue *)
+ let nq = State.make () in
+ Hashtbl.add memo_state (q, false) nq;
+ Queue.add (q, false) todo; nq
+ in
+ SFormula.atom_ (Move.make (l, true, not_q))
+ end
+ end