let table = get_states_by_move phi in
Move.fold (fun _ s acc -> StateSet.union s acc) table StateSet.empty
+ let rec rename_state phi qfrom qto =
+ let open Boolean in
+ match expr phi with
+ False | True -> phi
+ | Or (phi1, phi2) -> or_ (rename_state phi1 qfrom qto) (rename_state phi2 qfrom qto)
+ | And (phi1, phi2) -> and_ (rename_state phi1 qfrom qto) (rename_state phi2 qfrom qto)
+ | Atom ({ Atom.node = Move(m, q); }, b) when q == qfrom ->
+ let atm = mk_move m qto in if b then atm else not_ atm
+ | Atom _ -> phi
end
module Transition =
done;
cleanup_states auto
+exception Found of State.t * State.t
+
+let simplify_epsilon auto =
+ let rec loop old_states =
+ if old_states != auto.states then begin
+ let old_states = auto.states in
+ try
+ Hashtbl.iter
+ (fun qfrom v -> match v with
+ [ (labels, phi) ] ->
+ if labels == QNameSet.any then begin
+ match (Formula.expr phi) with
+ Boolean.Atom ( {Atom.node = Move(`Stay, qto); _ }, true) -> raise (Found (qfrom, qto))
+ | _ -> ()
+ end
+ | _ -> ()
+ ) auto.transitions
+ with Found (qfrom, qto) ->
+ Hashtbl.remove auto.transitions qfrom;
+ let new_trans = Hashtbl.fold (fun q tr_lst acc ->
+ let new_tr_lst =
+ List.map (fun (lab, phi) ->
+ (lab, Formula.rename_state phi qfrom qto))
+ tr_lst
+ in
+ (q, new_tr_lst) :: acc) auto.transitions []
+ in
+ Hashtbl.reset auto.transitions;
+ List.iter (fun (q, l) -> Hashtbl.add auto.transitions q l) new_trans;
+ auto.states <- StateSet.remove qfrom auto.states;
+ if (StateSet.mem qfrom auto.starting_states) then
+ auto.starting_states <- StateSet.add qto (StateSet.remove qfrom auto.starting_states);
+ if (StateSet.mem qfrom auto.selecting_states) then
+ auto.selecting_states <- StateSet.add qto (StateSet.remove qfrom auto.selecting_states);
+ loop old_states
+ end
+ in
+ loop StateSet.empty
+
+
+
(* [compute_dependencies auto] returns a hash table storing for each
states [q] a Move.table containing the set of states on which [q]
depends (loosely). [q] depends on [q'] if there is a transition
done;
let by_rank = Hashtbl.create 17 in
List.iter (fun (r,s) ->
- let set = try Hashtbl.find by_rank r with Not_found -> StateSet.empty in
- Hashtbl.replace by_rank r (StateSet.union s set)) !rank_list;
+ let set = try Hashtbl.find by_rank r with Not_found -> StateSet.empty in
+ Hashtbl.replace by_rank r (StateSet.union s set)) !rank_list;
auto.ranked_states <-
Array.init (Hashtbl.length by_rank) (fun i -> Hashtbl.find by_rank i)
in
Hashtbl.replace a.transitions q ntrs
+
+
let finalize a =
complete_transitions a;
normalize_negations a;
+ simplify_epsilon a;
compute_rank a;
a
end