+ 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
+ [q, {...} -> phi], where [q'] occurs in [phi].
+*)
+let compute_dependencies auto =
+ let edges = Hashtbl.create 17 in
+ StateSet.iter
+ (fun q -> Hashtbl.add edges q (Move.create_table StateSet.empty))
+ auto.starting_states;
+ Hashtbl.iter (fun q trans ->
+ let moves = try Hashtbl.find edges q with Not_found ->
+ let m = Move.create_table StateSet.empty in
+ Hashtbl.add edges q m;
+ m
+ in
+ List.iter (fun (_, phi) ->
+ let m_phi = Formula.get_states_by_move phi in
+ Move.iter (fun m set ->
+ Move.set moves m (StateSet.union set (Move.get moves m)))
+ m_phi) trans) auto.transitions;
+
+ edges
+
+let state_prerequisites dir auto q =
+ Hashtbl.fold (fun q' trans acc ->
+ List.fold_left (fun acc (_, phi) ->
+ let m_phi = Formula.get_states_by_move phi in
+ if StateSet.mem q (Move.get m_phi dir)
+ then StateSet.add q' acc else acc)
+ acc trans) auto.transitions StateSet.empty
+
+let compute_rank auto =
+ let dependencies = compute_dependencies auto in
+ let upward = [ `Stay ; `Parent ; `Previous_sibling ] in
+ let downward = [ `Stay; `First_child; `Next_sibling ] in
+ let swap dir = if dir == upward then downward else upward in
+ let is_satisfied dir q t =
+ Move.for_all (fun d set ->
+ if List.mem d dir then
+ StateSet.(is_empty (remove q set))
+ else StateSet.is_empty set) t
+ in
+ let update_dependencies dir initacc =
+ let rec loop acc =
+ let new_acc =
+ Hashtbl.fold (fun q deps acc ->
+ let to_remove = StateSet.union acc initacc in
+ List.iter
+ (fun m ->
+ Move.set deps m (StateSet.diff (Move.get deps m) to_remove)
+ )
+ dir;
+ if is_satisfied dir q deps then StateSet.add q acc else acc
+ ) dependencies acc
+ in
+ if acc == new_acc then new_acc else loop new_acc