+(* [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