Have scc_map keep track of APs that are occurring in a SCC.

* src/tgbaalgos/scc.hh (scc_map::scc): Add a supp member to hold APs.
* src/tgbaalgos/scc.cc (scc_map::build_map): Update supp.
(scc_map::ap_set_of): New function.
(dump_scc_dot): Show the output of ap_set_of().

ChangeLog

@@ -1,3 +1,12 @@
+2009-09-17  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
+
+	Have scc_map keep track of APs that are occurring in a SCC.
+
+	* src/tgbaalgos/scc.hh (scc_map::scc): Add a supp member to hold APs.
+	* src/tgbaalgos/scc.cc (scc_map::build_map): Update supp.
+	(scc_map::ap_set_of): New function.
+	(dump_scc_dot): Show the output of ap_set_of().
+
 2009-09-07  Damien Lefortier <dam@lrde.epita.fr>
 
 	Fix some memory leaks.

src/tgbaalgos/scc.cc

@@ -233,6 +233,7 @@ namespace spot
 	succ_type succs;
 	cond_set conds;
 	conds.insert(cond);
+	bdd supp = bdd_support(cond);
 	while (threshold > root_.front().index)
 	  {
 	    assert(!root_.empty());
@@ -246,6 +247,7 @@ namespace spot
 	    conds.insert(arc_cond_.top());
 	    conds.insert(root_.front().conds.begin(),
 			 root_.front().conds.end());
+	    supp &= root_.front().supp;
 	    root_.pop_front();
 	    arc_acc_.pop();
 	    arc_cond_.pop();
@@ -262,6 +264,7 @@ namespace spot
 	root_.front().states.splice(root_.front().states.end(), states);
 	root_.front().succ.insert(succs.begin(), succs.end());
 	root_.front().conds.insert(conds.begin(), conds.end());
+	root_.front().supp &= supp;
       }
   }
 
@@ -278,6 +281,13 @@ namespace spot
     return scc_map_[n].conds;
   }
 
+  bdd scc_map::ap_set_of(unsigned n) const
+  {
+    assert(scc_map_.size() > n);
+    return scc_map_[n].supp;
+  }
+
+
   bdd scc_map::acc_set_of(unsigned n) const
   {
     assert(scc_map_.size() > n);
@@ -423,7 +433,9 @@ namespace spot
 		  ostr << ", ";
 		bdd_print_formula(ostr, m.get_aut()->get_dict(), *i);
 	      }
-	    ostr << "]";
+	    ostr << "]\\n APs=[";
+	    bdd_print_sat(ostr, m.get_aut()->get_dict(),
+			  m.ap_set_of(state)) << "]";
 	  }
 
 	std::cout << "  " << state << " [shape=box,"

src/tgbaalgos/scc.hh

@@ -105,6 +105,14 @@ namespace spot
     /// \pre This should only be called once build_map() has run.
     const cond_set& cond_set_of(unsigned n) const;
 
+    /// \brief Return the set of atomic properties occurring in an SCC.
+    ///
+    /// \return a BDD that is a conjuction of all atomic properties
+    /// occurring on the transitions in the SCC n.
+    ///
+    /// \pre This should only be called once build_map() has run.
+    bdd ap_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.
@@ -133,7 +141,7 @@ namespace spot
     struct scc
     {
     public:
-      scc(int index) : index(index), acc(bddfalse) {};
+      scc(int index) : index(index), acc(bddfalse), supp(bddtrue) {};
       /// Index of the SCC.
       int index;
       /// The union of all acceptance conditions of transitions which
@@ -143,6 +151,8 @@ namespace spot
       std::list<const state*> states;
       /// Set of conditions used in the SCC.
       cond_set conds;
+      /// Conjunction of atomic propositions used in the SCC.
+      bdd supp;
       /// Successor SCC.
       succ_type succ;
     };