From fa8dd7f1609423f78383fbb1313fef6f171a6860 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Thu, 17 Sep 2009 17:56:35 +0200
Subject: [PATCH] Have scc_map keep track of APs that are reachable from a SCC.

* src/tgbaalgos/scc.hh (scc_map::scc): Add a supp_rec member to
hold reachable APs.
* src/tgbaalgos/scc.cc (scc_map::update_supp_rec): New function,
to update supp_rec.
(scc_map::build_map): Call it.
(scc_map::aprec_set_of): New function.
(dump_scc_dot): Show the output of aprec_set_of().
---
 ChangeLog            | 12 ++++++++++++
 src/tgbaalgos/scc.cc | 39 +++++++++++++++++++++++++++++++++++++--
 src/tgbaalgos/scc.hh | 17 ++++++++++++++---
 3 files changed, 63 insertions(+), 5 deletions(-)

diff --git a/ChangeLog b/ChangeLog
index 9aa20b2d0..0ccc521e2 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,3 +1,15 @@
+2009-09-17  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
+
+	Have scc_map keep track of APs that are reachable from a SCC.
+
+	* src/tgbaalgos/scc.hh (scc_map::scc): Add a supp_rec member to
+	hold reachable APs.
+	* src/tgbaalgos/scc.cc (scc_map::update_supp_rec): New function,
+	to update supp_rec.
+	(scc_map::build_map): Call it.
+	(scc_map::aprec_set_of): New function.
+	(dump_scc_dot): Show the output of aprec_set_of().
+
 2009-09-17  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
 
 	Have scc_map keep track of APs that are occurring in a SCC.
diff --git a/src/tgbaalgos/scc.cc b/src/tgbaalgos/scc.cc
index 0918d5497..04de57857 100644
--- a/src/tgbaalgos/scc.cc
+++ b/src/tgbaalgos/scc.cc
@@ -104,6 +104,28 @@ namespace spot
     return n;
   }
 
+  // recursively update supp rec
+  bdd
+  scc_map::update_supp_rec(unsigned state)
+  {
+    assert(scc_map_.size() > state);
+
+    bdd& res = scc_map_[state].supp_rec;
+
+    if (res == bddtrue)
+      {
+	const succ_type& s = succ(state);
+	succ_type::const_iterator it;
+
+	for (it = s.begin(); it != s.end(); ++it)
+	  res &= update_supp_rec(it->first);
+
+	res &= scc_map_[state].supp;
+      }
+
+    return res;
+  }
+
   void
   scc_map::build_map()
   {
@@ -266,6 +288,9 @@ namespace spot
 	root_.front().conds.insert(conds.begin(), conds.end());
 	root_.front().supp &= supp;
       }
+
+    // recursively update supp_rec
+    (void) update_supp_rec(initial());
   }
 
   unsigned scc_map::scc_of_state(const state* s) const
@@ -288,6 +313,13 @@ namespace spot
   }
 
 
+  bdd scc_map::aprec_set_of(unsigned n) const
+  {
+    assert(scc_map_.size() > n);
+    return scc_map_[n].supp_rec;
+  }
+
+
   bdd scc_map::acc_set_of(unsigned n) const
   {
     assert(scc_map_.size() > n);
@@ -433,9 +465,12 @@ namespace spot
 		  ostr << ", ";
 		bdd_print_formula(ostr, m.get_aut()->get_dict(), *i);
 	      }
-	    ostr << "]\\n APs=[";
+	    ostr << "]\\n AP=[";
 	    bdd_print_sat(ostr, m.get_aut()->get_dict(),
-			  m.ap_set_of(state)) << "]";
+			  m.ap_set_of(state));
+	    ostr << "]\\n APrec=[";
+	    bdd_print_sat(ostr, m.get_aut()->get_dict(),
+			  m.aprec_set_of(state)) << "]";
 	  }
 
 	std::cout << "  " << state << " [shape=box,"
diff --git a/src/tgbaalgos/scc.hh b/src/tgbaalgos/scc.hh
index bcd50d7f3..3c050d9fc 100644
--- a/src/tgbaalgos/scc.hh
+++ b/src/tgbaalgos/scc.hh
@@ -113,6 +113,14 @@ namespace spot
     /// \pre This should only be called once build_map() has run.
     bdd ap_set_of(unsigned n) const;
 
+    /// \brief Return the set of atomic properties reachable from this SCC.
+    ///
+    /// \return a BDD that is a conjuction of all atomic properties
+    /// occurring on the transitions reachable from this SCC n.
+    ///
+    /// \pre This should only be called once build_map() has run.
+    bdd aprec_set_of(unsigned n) const;
+
     /// \brief Return the set of acceptance conditions occurring in an SCC.
     ///
     /// \pre This should only be called once build_map() has run.
@@ -135,13 +143,14 @@ namespace spot
     unsigned self_loops() const;
 
   protected:
-
+    bdd update_supp_rec(unsigned state);
     int relabel_component();
 
     struct scc
     {
     public:
-      scc(int index) : index(index), acc(bddfalse), supp(bddtrue) {};
+      scc(int index) : index(index), acc(bddfalse),
+		       supp(bddtrue), supp_rec(bddtrue) {};
       /// Index of the SCC.
       int index;
       /// The union of all acceptance conditions of transitions which
@@ -153,6 +162,8 @@ namespace spot
       cond_set conds;
       /// Conjunction of atomic propositions used in the SCC.
       bdd supp;
+      /// Conjunction of atomic propositions used in the SCC.
+      bdd supp_rec;
       /// Successor SCC.
       succ_type succ;
     };
@@ -186,7 +197,7 @@ namespace spot
 			   // SCC number "n" in H_ corresponds to entry
                            // "n" in SCC_MAP_.
     unsigned self_loops_; // Self loops count.
-  };
+ };
 
   scc_stats build_scc_stats(const tgba* a);
   scc_stats build_scc_stats(const scc_map& m);