+let cleanup_states a =
+ let memo = ref StateSet.empty in
+ let rec loop q =
+ if not (StateSet.mem q !memo) then begin
+ memo := StateSet.add q !memo;
+ let trs = try Hashtbl.find a.transitions q with Not_found -> [] in
+ List.iter (fun (_, phi) ->
+ StateSet.iter loop (SFormula.get_states phi)) trs
+ end
+ in
+ StateSet.iter loop a.selection_states;
+ let unused = StateSet.diff a.states !memo in
+ eprintf "Unused states %a\n%!" StateSet.print unused;
+ StateSet.iter (fun q -> Hashtbl.remove a.transitions q) unused;
+ a.states <- !memo