X-Git-Url: http://git.nguyen.vg/gitweb/?p=tatoo.git;a=blobdiff_plain;f=src%2Fata.ml;fp=src%2Fata.ml;h=190c4c72443ec18c6d76186eda0c96f326d37bd3;hp=8a13705c5d5e056c4cec98123f0ab281b015ce80;hb=6844beef9142975d1bf4a2b3fb72b93dfa3402dc;hpb=836d6ea0aebf1f947faa74db1d78168afb882930

diff --git a/src/ata.ml b/src/ata.ml
index 8a13705..190c4c7 100644
--- a/src/ata.ml
+++ b/src/ata.ml
@@ -445,6 +445,13 @@ let compute_dependencies auto =
 
   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