From 07ead6134e52e78a336c27f134cae6be632b75c6 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 28 May 2009 13:08:20 +0200 Subject: [PATCH] Keep track of conditions in SCC, and add a more verbose dump. * src/tgbaalgos/scc.hh (scc_map::scc_of_state, scc_map::cond_set_of, scc_map::acc_set_of, scc_map::states_of): New functions. (scc_map::scc::conds): New attribute. (dump_scc_dot): Take an optional VERBOSE argument. * src/tgbaalgos/scc.cc (scc_map::scc_of_state, scc_map::cond_set_of, scc_map::acc_set_of, scc_map::states_of): Implement these new functions. (dump_scc_dot): Display number of states, conditions and acceptance conditions, with VERBOSE is set. (build_map): Fill the new scc_map::scc::cond field. --- ChangeLog | 16 ++++++++ src/tgbaalgos/scc.cc | 85 +++++++++++++++++++++++++++++++++------- src/tgbaalgos/scc.hh | 18 +++++++-- src/tgbatest/ltl2tgba.cc | 14 +++++-- 4 files changed, 112 insertions(+), 21 deletions(-) diff --git a/ChangeLog b/ChangeLog index cb105824d..cb8a4baaa 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,19 @@ +2009-05-28 Alexandre Duret-Lutz + + Keep track of conditions in SCC, and add a more verbose dump. + + * src/tgbaalgos/scc.hh (scc_map::scc_of_state, + scc_map::cond_set_of, scc_map::acc_set_of, scc_map::states_of): + New functions. + (scc_map::scc::conds): New attribute. + (dump_scc_dot): Take an optional VERBOSE argument. + * src/tgbaalgos/scc.cc (scc_map::scc_of_state, + scc_map::cond_set_of, scc_map::acc_set_of, scc_map::states_of): + Implement these new functions. + (dump_scc_dot): Display number of states, conditions and + acceptance conditions, with VERBOSE is set. + (build_map): Fill the new scc_map::scc::cond field. + 2009-05-28 Alexandre Duret-Lutz * src/tgbaalgos/scc.cc (scc_map::relabel_component): Make sure diff --git a/src/tgbaalgos/scc.cc b/src/tgbaalgos/scc.cc index 21d4d27a3..941883846 100644 --- a/src/tgbaalgos/scc.cc +++ b/src/tgbaalgos/scc.cc @@ -21,6 +21,7 @@ #include #include #include +#include #include "scc.hh" #include "tgba/bddprint.hh" @@ -160,8 +161,7 @@ namespace spot } // We have a successor to look at. - // Fetch the values (destination state, acceptance conditions - // of the arc) we are interested in... + // Fetch the values we are interested in... const state* dest = succ->current_state(); bdd acc = succ->current_acceptance_conditions(); bdd cond = succ->current_condition(); @@ -186,7 +186,7 @@ namespace spot continue; } - // Have we reached maximal SCC? + // Have we reached a maximal SCC? if (spi->second < 0) { int dest = spi->second; @@ -215,6 +215,8 @@ namespace spot int threshold = spi->second; std::list states; succ_type succs; + cond_set conds; + conds.insert(cond); while (threshold < root_.front().index) { assert(!root_.empty()); @@ -225,23 +227,53 @@ namespace spot states.splice(states.end(), root_.front().states); succs.insert(root_.front().succ.begin(), root_.front().succ.end()); + conds.insert(arc_cond_.top()); + conds.insert(root_.front().conds.begin(), + root_.front().conds.end()); root_.pop_front(); arc_acc_.pop(); arc_cond_.pop(); } + // Note that we do not always have // threshold == root_.front().index // after this loop, the SCC whose index is threshold might have // been merged with a lower SCC. - // Accumulate all acceptance conditions into the merged SCC. + // Accumulate all acceptance conditions, states, SCC + // successors, and conditions into the merged SCC. root_.front().acc |= acc; root_.front().states.splice(root_.front().states.end(), states); - // Likewise with SCC successors. root_.front().succ.insert(succs.begin(), succs.end()); + root_.front().conds.insert(conds.begin(), conds.end()); } } + int scc_map::scc_of_state(const state* s) const + { + hash_type::const_iterator i = h_.find(s); + assert(i != h_.end()); + return i->second; + } + + const scc_map::cond_set& scc_map::cond_set_of(int n) const + { + scc_map_type::const_iterator i = scc_map_.find(n); + return i->second.conds; + } + + bdd scc_map::acc_set_of(int n) const + { + scc_map_type::const_iterator i = scc_map_.find(n); + return i->second.acc; + } + + const std::list& scc_map::states_of(int n) const + { + scc_map_type::const_iterator i = scc_map_.find(n); + return i->second.states; + } + int scc_map::scc_count() const { return -scc_num_; @@ -326,7 +358,7 @@ namespace spot } std::ostream& - dump_scc_dot(const scc_map& m, std::ostream& out) + dump_scc_dot(const scc_map& m, std::ostream& out, bool verbose) { out << "digraph G {\n 0 [label=\"\", style=invis, height=0]" << std::endl; int start = m.initial(); @@ -343,10 +375,33 @@ namespace spot int state = q.front(); q.pop(); - if (m.accepting(state)) - std::cout << " " << -state << " [shape=doublecircle]" << std::endl; - else - std::cout << " " << -state << " [shape=circle]" << std::endl; + const scc_map::cond_set& cs = m.cond_set_of(state); + + std::ostringstream ostr; + ostr << -state; + if (verbose) + { + size_t n = m.states_of(state).size(); + ostr << " (" << n << " state"; + if (n > 1) + ostr << "s"; + ostr << ")\\naccs="; + bdd_print_accset(ostr, m.get_aut()->get_dict(), + m.acc_set_of(state)); + ostr << "\\nconds=["; + for (scc_map::cond_set::const_iterator i = cs.begin(); + i != cs.end(); ++i) + { + if (i != cs.begin()) + ostr << ", "; + bdd_print_formula(ostr, m.get_aut()->get_dict(), *i); + } + ostr << "]"; + } + + std::cout << " " << -state << " [shape=box," + << (m.accepting(state) ? "style=bold," : "") + << "label=\"" << ostr.str() << "\"]" << std::endl; const scc_map::succ_type& succ = m.succ(state); @@ -357,9 +412,9 @@ namespace spot bdd label = it->second; out << " " << -state << " -> " << -dest - << " [label=\"" - << bdd_format_formula(m.get_aut()->get_dict(), label) - << "\"]" << std::endl; + << " [label=\""; + bdd_print_formula(out, m.get_aut()->get_dict(), label); + out << "\"]" << std::endl; seen_map::const_iterator it = seen.find(dest); if (it != seen.end()) @@ -376,11 +431,11 @@ namespace spot } std::ostream& - dump_scc_dot(const tgba* a, std::ostream& out) + dump_scc_dot(const tgba* a, std::ostream& out, bool verbose) { scc_map m(a); m.build_map(); - return dump_scc_dot(m, out); + return dump_scc_dot(m, out, verbose); } } diff --git a/src/tgbaalgos/scc.hh b/src/tgbaalgos/scc.hh index bba2156a1..02ff0d9d1 100644 --- a/src/tgbaalgos/scc.hh +++ b/src/tgbaalgos/scc.hh @@ -26,6 +26,7 @@ #include "tgba/tgba.hh" #include #include "misc/hash.hh" +#include "misc/bddlt.hh" namespace spot { @@ -59,12 +60,18 @@ namespace spot { public: typedef std::map succ_type; + typedef std::set cond_set; scc_map(const tgba* aut); void build_map(); void relabel_component(int n); + int scc_of_state(const state* s) const; + const cond_set& cond_set_of(int n) const; + bdd acc_set_of(int n) const; + const std::list& states_of(int n) const; + const tgba* get_aut() const; int scc_count() const; @@ -86,6 +93,8 @@ namespace spot bdd acc; /// States of the component. std::list states; + /// Set of conditions used in the SCC. + cond_set conds; /// Successor SCC. succ_type succ; }; @@ -113,14 +122,17 @@ namespace spot // but STATE should not because // it is used as a key in H. - std::map scc_map_; // Map of constructed maximal SCC. + typedef std::map scc_map_type; + scc_map_type scc_map_; // Map of constructed maximal SCC. }; scc_stats build_scc_stats(const tgba* a); scc_stats build_scc_stats(const scc_map& m); - std::ostream& dump_scc_dot(const tgba* a, std::ostream& out); - std::ostream& dump_scc_dot(const scc_map& m, std::ostream& out); + std::ostream& dump_scc_dot(const tgba* a, std::ostream& out, + bool verbose = false); + std::ostream& dump_scc_dot(const scc_map& m, std::ostream& out, + bool verbose = false); } #endif // SPOT_TGBAALGOS_SCC_HH diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index 82f7b511c..445fa40b4 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2003, 2004, 2005, 2006, 2007, 2008 Laboratoire +// Copyright (C) 2003, 2004, 2005, 2006, 2007, 2008, 2009 Laboratoire // d'Informatique de Paris 6 (LIP6), département Systèmes Répartis // Coopératifs (SRC), Université Pierre et Marie Curie. // @@ -93,7 +93,8 @@ syntax(char* prog) << " (requires -e)" << std::endl << " -k display statistics on the TGBA instead of dumping it" << std::endl - << " -K dump the graph of SCCs in dot" + << " -K dump the graph of SCCs in dot format" << std::endl + << " -KV verbosely dump the graph of SCCs in dot format" << std::endl << " -L fair-loop approximation (implies -f)" << std::endl << " -m try to reduce accepting runs, in a second pass" @@ -332,6 +333,10 @@ main(int argc, char** argv) { output = 10; } + else if (!strcmp(argv[formula_index], "-KV")) + { + output = 11; + } else if (!strcmp(argv[formula_index], "-L")) { fair_loop_approx = true; @@ -742,7 +747,10 @@ main(int argc, char** argv) build_scc_stats(a).dump(std::cout); break; case 10: - dump_scc_dot(a, std::cout); + dump_scc_dot(a, std::cout, false); + break; + case 11: + dump_scc_dot(a, std::cout, true); break; default: assert(!"unknown output option");