diff --git a/ChangeLog b/ChangeLog index cb3bc0511..9aa20b2d0 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,12 @@ +2009-09-17 Alexandre Duret-Lutz + + 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 Fix some memory leaks. diff --git a/src/tgbaalgos/scc.cc b/src/tgbaalgos/scc.cc index 21969d38e..0918d5497 100644 --- a/src/tgbaalgos/scc.cc +++ b/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," diff --git a/src/tgbaalgos/scc.hh b/src/tgbaalgos/scc.hh index 9eb85071d..bcd50d7f3 100644 --- a/src/tgbaalgos/scc.hh +++ b/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 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; };