+
+(*
+ [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
+ in
+ StateSet.iter (fun q -> Queue.add (q, true) todo) a.top_states;
+ while not (Queue.is_empty todo) do
+ let (q, b) as key = Queue.pop todo in
+ let q' =
+ try
+ Hashtbl.find memo_state key
+ with
+ Not_found ->
+ let nq = if b then q else State.make () in
+ Hashtbl.add memo_state key nq; nq
+ in
+ let trans = Hashtbl.find a.transitions q in
+ let trans' = List.map (fun (lab, f) -> lab, flip b f) trans in
+ Hashtbl.replace a.transitions q' trans'
+ done;
+ Hashtbl.iter (fun (q, b) q' ->
+ if not (b || StateSet.mem q a.bottom_states) then
+ a.bottom_states <- StateSet.add q' a.bottom_states
+ ) memo_state
+