From c44d6277f2c28cfde6cf3a2a3ba9de918875a9fd Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 5 Dec 2008 12:04:31 +0100 Subject: [PATCH] Introduce scc.cc to compute SCC stats and map. --- ChangeLog | 7 + src/tgbaalgos/Makefile.am | 4 +- src/tgbaalgos/scc.cc | 306 ++++++++++++++++++++++++++++++++++++++ src/tgbaalgos/scc.hh | 105 +++++++++++++ src/tgbatest/ltl2tgba.cc | 11 ++ 5 files changed, 432 insertions(+), 1 deletion(-) create mode 100644 src/tgbaalgos/scc.cc create mode 100644 src/tgbaalgos/scc.hh diff --git a/ChangeLog b/ChangeLog index acf19300c..f8c35710d 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,10 @@ +2008-12-10 Alexandre Duret-Lutz + + * src/tgbaalgos/scc.hh, src/tgbaalgos/scc.cc: New files. + * src/tgbaalgos/Makefile.am: Add them. + * src/tgbatest/ltl2tgba.cc (-k): Also call build_scc_stats(). + (-K): New option that dumps the SCCs for dot. + 2008-12-05 Alexandre Duret-Lutz * src/tgbatest/ltl2tgba.cc (-k): New option that calls diff --git a/src/tgbaalgos/Makefile.am b/src/tgbaalgos/Makefile.am index 88a9e891c..2acfba1e0 100644 --- a/src/tgbaalgos/Makefile.am +++ b/src/tgbaalgos/Makefile.am @@ -1,4 +1,4 @@ -## Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), +## Copyright (C) 2003, 2004, 2005, 2008 Laboratoire d'Informatique de Paris 6 (LIP6), ## département Systèmes Répartis Coopératifs (SRC), Université Pierre ## et Marie Curie. ## @@ -48,6 +48,7 @@ tgbaalgos_HEADERS = \ replayrun.hh \ rundotdec.hh \ save.hh \ + scc.hh \ se05.hh \ stats.hh \ tau03.hh \ @@ -78,6 +79,7 @@ libtgbaalgos_la_SOURCES = \ replayrun.cc \ rundotdec.cc \ save.cc \ + scc.cc \ se05.cc \ stats.cc \ tau03.cc \ diff --git a/src/tgbaalgos/scc.cc b/src/tgbaalgos/scc.cc new file mode 100644 index 000000000..b24b1bcf0 --- /dev/null +++ b/src/tgbaalgos/scc.cc @@ -0,0 +1,306 @@ +// Copyright (C) 2008 Laboratoire de Recherche et Developpement de +// l'Epita. +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + +#include +#include +#include +#include "scc.hh" +#include "tgba/bddprint.hh" + +namespace spot +{ + std::ostream& + scc_stats::dump(std::ostream& out) const + { + out << "total SCCs: " << scc_total << std::endl; + return out; + } + + + scc_map::scc_map(const tgba* aut) + : aut_(aut) + { + } + + int + scc_map::initial() const + { + state* in = aut_->get_init_state(); + hash_type::const_iterator i = h_.find(in); + assert(i != h_.end()); + int val = i->second; + delete in; + return val; + } + + const scc_map::succ_type& + scc_map::succ(int i) const + { + std::map::const_iterator j = scc_map_.find(i); + assert (j != scc_map_.end()); + return j->second.succ; + } + + bool + scc_map::accepting(int i) const + { + std::map::const_iterator j = scc_map_.find(i); + assert (j != scc_map_.end()); + return j->second.acc == aut_->all_acceptance_conditions(); + } + + const tgba* + scc_map::get_aut() const + { + return aut_; + } + + + void + scc_map::relabel_component(int n) + { + assert(!root_.front().states.empty()); + std::list::iterator i; + for (i = root_.front().states.begin(); i != root_.front().states.end(); ++i) + { + hash_type::iterator spi = h_.find(*i); + assert(spi != h_.end()); + assert(spi->first == *i); + assert(spi->second != -1); + spi->second = n; + } + scc_map_.insert(std::make_pair(n, root_.front())); + } + + void + scc_map::build_map() + { + // Setup depth-first search from the initial state. + { + state* init = aut_->get_init_state(); + num_ = 1; + scc_num_ = 0; + h_.insert(std::make_pair(init, 1)); + root_.push_front(scc(1)); + arc_.push(bddfalse); + tgba_succ_iterator* iter = aut_->succ_iter(init); + iter->first(); + todo_.push(pair_state_iter(init, iter)); + } + + while (!todo_.empty()) + { + assert(root_.size() == arc_.size()); + + // We are looking at the next successor in SUCC. + tgba_succ_iterator* succ = todo_.top().second; + + // If there is no more successor, backtrack. + if (succ->done()) + { + // We have explored all successors of state CURR. + const state* curr = todo_.top().first; + + // Backtrack TODO_. + todo_.pop(); + + // Fill rem with any component removed, so that + // remove_component() does not have to traverse the SCC + // again. + hash_type::const_iterator spi = h_.find(curr); + assert(spi != h_.end()); + root_.front().states.push_front(spi->first); + + // When backtracking the root of an SCC, we must also + // remove that SCC from the ARC/ROOT stacks. We must + // discard from H all reachable states from this SCC. + assert(!root_.empty()); + if (root_.front().index == spi->second) + { + assert(!arc_.empty()); + arc_.pop(); + relabel_component(--scc_num_); + root_.pop_front(); + } + + delete succ; + // Do not delete CURR: it is a key in H. + continue; + } + + // We have a successor to look at. + // Fetch the values (destination state, acceptance conditions + // of the arc) we are interested in... + const state* dest = succ->current_state(); + bdd acc = succ->current_acceptance_conditions(); + bdd cond = succ->current_condition(); + // ... and point the iterator to the next successor, for + // the next iteration. + succ->next(); + // We do not need SUCC from now on. + + // Are we going to a new state? + hash_type::const_iterator spi = h_.find(dest); + if (spi == h_.end()) + { + // Yes. Number it, stack it, and register its successors + // for later processing. + h_.insert(std::make_pair(dest, ++num_)); + root_.push_front(scc(num_)); + arc_.push(acc); + tgba_succ_iterator* iter = aut_->succ_iter(dest); + iter->first(); + todo_.push(pair_state_iter(dest, iter)); + continue; + } + + // Have we reached maximal SCC? + if (spi->second < 0) + { + int dest = spi->second; + // Record that there is a transition from this SCC to the + // dest SCC labelled with cond. + succ_type::iterator i = root_.front().succ.find(dest); + if (i == root_.front().succ.end()) + root_.front().succ.insert(std::make_pair(dest, cond)); + else + i->second |= cond; + + continue; + } + + // Now this is the most interesting case. We have reached a + // state S1 which is already part of a non-dead SCC. Any such + // non-dead SCC has necessarily been crossed by our path to + // this state: there is a state S2 in our path which belongs + // to this SCC too. We are going to merge all states between + // this S1 and S2 into this SCC. + // + // This merge is easy to do because the order of the SCC in + // ROOT is ascending: we just have to merge all SCCs from the + // top of ROOT that have an index greater to the one of + // the SCC of S2 (called the "threshold"). + int threshold = spi->second; + std::list states; + succ_type succs; + while (threshold < root_.front().index) + { + assert(!root_.empty()); + assert(!arc_.empty()); + acc |= root_.front().acc; + acc |= arc_.top(); + states.splice(states.end(), root_.front().states); + succs.insert(root_.front().succ.begin(), + root_.front().succ.end()); + root_.pop_front(); + arc_.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. + 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()); + } + } + + int scc_map::scc_count() const + { + return -scc_num_; + } + + scc_stats build_scc_stats(const scc_map& m) + { + scc_stats res; + res.scc_total = m.scc_count(); + return res; + } + + scc_stats + build_scc_stats(const tgba* a) + { + scc_map m(a); + m.build_map(); + return build_scc_stats(m); + } + + std::ostream& + dump_scc_dot(const scc_map& m, std::ostream& out) + { + out << "digraph G {\n 0 [label=\"\", style=invis, height=0]" << std::endl; + int start = m.initial(); + out << " 0 -> " << -start << std::endl; + + typedef std::set seen_map; + seen_map seen; + seen.insert(start); + + std::queue q; + q.push(start); + while (!q.empty()) + { + 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::succ_type& succ = m.succ(state); + + scc_map::succ_type::const_iterator it; + for (it = succ.begin(); it != succ.end(); ++it) + { + int dest = it->first; + bdd label = it->second; + + out << " " << -state << " -> " << -dest + << " [label=\"" + << bdd_format_formula(m.get_aut()->get_dict(), label) + << "\"]" << std::endl; + + seen_map::const_iterator it = seen.find(dest); + if (it != seen.end()) + continue; + + seen.insert(dest); + q.push(dest); + } + } + + out << "}" << std::endl; + + return out; + } + + std::ostream& + dump_scc_dot(const tgba* a, std::ostream& out) + { + scc_map m(a); + m.build_map(); + return dump_scc_dot(m, out); + } + +} diff --git a/src/tgbaalgos/scc.hh b/src/tgbaalgos/scc.hh new file mode 100644 index 000000000..5ad36a614 --- /dev/null +++ b/src/tgbaalgos/scc.hh @@ -0,0 +1,105 @@ +// Copyright (C) 2008 Laboratoire de Recherche et Developpement de +// l'Epita. +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + +#ifndef SPOT_TGBAALGOS_SCC_HH +# define SPOT_TGBAALGOS_SCC_HH + +#include +#include +#include "tgba/tgba.hh" +#include + +namespace spot +{ + + struct scc_stats + { + unsigned scc_total; + + std::ostream& dump(std::ostream& out) const; + }; + + class scc_map + { + public: + typedef std::map succ_type; + + scc_map(const tgba* aut); + + void build_map(); + void relabel_component(int n); + + const tgba* get_aut() const; + + int scc_count() const; + + int initial() const; + + const succ_type& succ(int i) const; + bool accepting(int i) const; + + protected: + struct scc + { + public: + scc(int index) : index(index), acc(bddfalse) {}; + /// Index of the SCC. + int index; + /// The union of all acceptance conditions of transitions which + /// connect the states of the connected component. + bdd acc; + /// States of the component. + std::list states; + /// Successor SCC. + succ_type succ; + }; + + const tgba* aut_; // Automata to decompose. + typedef std::list stack_type; + stack_type root_; // Stack of SCC roots. + std::stack arc_; // A stack of acceptance conditions + // between each of these SCC. + typedef Sgi::hash_map hash_type; + hash_type h_; // Map of visited states. + int num_; // Number of visited nodes. + int scc_num_; // Opposite of the number of + // maximal SCC constructed. + typedef std::pair pair_state_iter; + std::stack todo_; // DFS stack. Holds (STATE, + // ITERATOR) pairs where + // ITERATOR is an iterator over + // the successors of STATE. + // ITERATOR should always be + // freed when TODO is popped, + // but STATE should not because + // it is used as a key in H. + + std::map 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); +} + +#endif // SPOT_TGBAALGOS_SCC_HH diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index 937c588a4..78eaf7b17 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -47,6 +47,7 @@ #include "tgbaalgos/rundotdec.hh" #include "tgbaalgos/stats.hh" +#include "tgbaalgos/scc.hh" #include "tgbaalgos/emptiness_stats.hh" void @@ -91,6 +92,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" + << std::endl << " -L fair-loop approximation (implies -f)" << std::endl << " -m try to reduce accepting runs, in a second pass" << std::endl @@ -324,6 +327,10 @@ main(int argc, char** argv) { output = 9; } + else if (!strcmp(argv[formula_index], "-K")) + { + output = 10; + } else if (!strcmp(argv[formula_index], "-L")) { fair_loop_approx = true; @@ -731,6 +738,10 @@ main(int argc, char** argv) } case 9: stats_reachable(a).dump(std::cout); + build_scc_stats(a).dump(std::cout); + break; + case 10: + dump_scc_dot(a, std::cout); break; default: assert(!"unknown output option");