+(* [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 =
+ let trans = Hashtbl.find auto.transitions q in
+ List.fold_left (fun acc (_, phi) ->
+ let m_phi = Formula.get_states_by_move phi in
+ let prereq = Move.get m_phi dir in
+ StateSet.union prereq acc)
+ StateSet.empty trans
+
+
+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
+ in
+ let satisfied = loop StateSet.empty in
+ StateSet.iter (fun q ->
+ Hashtbl.remove dependencies q) satisfied;
+ satisfied
+ in
+ let current_states = ref StateSet.empty in
+ let rank_list = ref [] in
+ let rank = ref 0 in
+ let current_dir = ref upward in
+ let detect_cycle = ref 0 in
+ while Hashtbl.length dependencies != 0 do
+ let new_sat = update_dependencies !current_dir !current_states in
+ if StateSet.is_empty new_sat then incr detect_cycle;
+ if !detect_cycle > 2 then assert false;
+ rank_list := (!rank, new_sat) :: !rank_list;
+ rank := !rank + 1;
+ current_dir := swap !current_dir;
+ current_states := StateSet.union new_sat !current_states;
+ 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 rank = Hashtbl.length by_rank in
+ if rank mod 2 == 1 then Hashtbl.replace by_rank rank StateSet.empty;
+ let rank = Hashtbl.length by_rank in
+ assert (rank mod 2 == 0);
+ let rank_array =
+ Array.init (rank / 2)
+ (fun i ->
+ let td_set = Hashtbl.find by_rank (2 * i) in
+ let bu_set = Hashtbl.find by_rank (2 * i + 1) in
+ { td = td_set; bu = bu_set ; exit = StateSet.empty }
+ )
+ in
+ let max_rank = Array.length rank_array - 1 in
+ for i = 0 to max_rank do
+ let this_rank = rank_array.(i) in
+ let exit = if i == max_rank then auto.selecting_states else
+ let next = rank_array.(i+1) in
+ let res =
+ StateSet.fold (fun q acc ->
+ List.fold_left (fun acc m ->
+ StateSet.union acc (state_prerequisites m auto q ))
+ acc [`First_child; `Next_sibling; `Parent; `Previous_sibling; `Stay]
+ ) (StateSet.union next.td next.bu) StateSet.empty
+ in
+
+ StateSet.(
+ union auto.selecting_states ( inter res (union this_rank.td this_rank.bu)))
+
+ in
+ rank_array.(i) <- {this_rank with exit = exit };
+ done;
+ auto.ranked_states <- rank_array
+