From 9903ae2fa836cc352874b1e1028280656b462c2a Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 28 Apr 2014 21:03:31 +0200 Subject: [PATCH] Implement an scc_info class that should eventually replace scc_map. * src/graph/graph.hh (trans_iterator): Add operator->() and operator bool(). * src/tgbaalgos/sccinfo.cc, src/tgbaalgos/sccinfo.hh: New files. * src/tgbaalgos/Makefile.am: Add them. * src/tgbatest/ltl2tgba.cc: Use the new dump_scc_info_dot() function. --- src/graph/graph.hh | 15 ++ src/tgbaalgos/Makefile.am | 6 +- src/tgbaalgos/sccinfo.cc | 287 ++++++++++++++++++++++++++++++++++++++ src/tgbaalgos/sccinfo.hh | 137 ++++++++++++++++++ src/tgbatest/ltl2tgba.cc | 19 ++- 5 files changed, 460 insertions(+), 4 deletions(-) create mode 100644 src/tgbaalgos/sccinfo.cc create mode 100644 src/tgbaalgos/sccinfo.hh diff --git a/src/graph/graph.hh b/src/graph/graph.hh index df41d77fd..7147413af 100644 --- a/src/graph/graph.hh +++ b/src/graph/graph.hh @@ -215,6 +215,12 @@ namespace spot return g_->trans_storage(t_); } + typename super::pointer + operator->() + { + return &g_->trans_storage(t_); + } + trans_iterator operator++() { t_ = operator*().next_succ; @@ -228,6 +234,11 @@ namespace spot return ti; } + operator bool() const + { + return t_; + } + protected: Graph* g_; transition t_; @@ -278,7 +289,11 @@ namespace spot { friend class internal::trans_iterator; friend class internal::trans_iterator; + public: + typedef internal::trans_iterator iterator; + typedef internal::trans_iterator const_iterator; + static constexpr bool alternating() { return Alternating; diff --git a/src/tgbaalgos/Makefile.am b/src/tgbaalgos/Makefile.am index cb710ffc3..a2db955f5 100644 --- a/src/tgbaalgos/Makefile.am +++ b/src/tgbaalgos/Makefile.am @@ -1,6 +1,6 @@ ## -*- coding: utf-8 -*- -## Copyright (C) 2008, 2009, 2010, 2011, 2012, 2013 Laboratoire de -## Recherche et Développement de l'Epita (LRDE). +## Copyright (C) 2008, 2009, 2010, 2011, 2012, 2013, 2014 Laboratoire +## de Recherche et Développement de l'Epita (LRDE). ## Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris ## 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), ## Université Pierre et Marie Curie. @@ -66,6 +66,7 @@ tgbaalgos_HEADERS = \ save.hh \ sccfilter.hh \ scc.hh \ + sccinfo.hh \ se05.hh \ simulation.hh \ stats.hh \ @@ -114,6 +115,7 @@ libtgbaalgos_la_SOURCES = \ safety.cc \ save.cc \ scc.cc \ + sccinfo.cc \ sccfilter.cc \ se05.cc \ simulation.cc \ diff --git a/src/tgbaalgos/sccinfo.cc b/src/tgbaalgos/sccinfo.cc new file mode 100644 index 000000000..f7a09ae15 --- /dev/null +++ b/src/tgbaalgos/sccinfo.cc @@ -0,0 +1,287 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2014 Laboratoire de Recherche et Développement 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 3 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 this program. If not, see . + +#include "sccinfo.hh" +#include +#include +#include +#include "tgba/bddprint.hh" +#include "misc/escape.hh" + +namespace spot +{ + + namespace + { + struct scc + { + public: + scc(int index, bdd in_cond, bdd in_acc): + index(index), in_cond(in_cond), in_acc(in_acc) + { + } + + int index; // Index of the SCC + bdd in_cond; // Condition on incoming transition + bdd in_acc; // Acceptance sets on the incoming transition + scc_info::scc_node node; + }; + } + + scc_info::scc_info(const tgba_digraph* aut) + { + unsigned n = aut->num_states(); + sccof_.resize(n, -1U); + bdd all_acc = aut->all_acceptance_conditions(); + + 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. + std::vector h_(n, 0); + // Map of visited states. Values > 0 designate maximal SCC. + // Values < 0 number states that are part of incomplete SCCs being + // completed. 0 denotes non-visited states. + + int num_; // Number of visited nodes, negated. + + typedef tgba_digraph::graph_t::const_iterator iterator; + 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. + + + // Setup depth-first search from the initial state. + { + unsigned init = aut->get_init_state_number(); + num_ = -1; + h_[init] = num_; + root_.emplace_front(num_, bddfalse, bddfalse); + todo_.emplace(init, aut->get_graph().out(init).begin()); + } + + while (!todo_.empty()) + { + // We are looking at the next successor in SUCC. + iterator succ = todo_.top().second; + + // If there is no more successor, backtrack. + if (!succ) + { + // We have explored all successors of state CURR. + unsigned curr = todo_.top().first; + + // Backtrack TODO_. + todo_.pop(); + + // Fill STATES with any state removed, so that + // remove_component() does not have to traverse the SCC + // again. + root_.front().node.states.push_front(curr); + + // 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 == h_[curr]) + { + int num = node_.size(); + for (auto s: root_.front().node.states) + { + sccof_[s] = num; + h_[s] = num + 1; + } + bdd cond = root_.front().in_cond; + bdd acc = root_.front().node.acc; + bool triv = root_.front().node.trivial; + node_.emplace_back(acc, triv); + std::swap(node_.back().succ, root_.front().node.succ); + std::swap(node_.back().states, root_.front().node.states); + node_.back().accepting = acc == all_acc; + root_.pop_front(); + // Record the transition between the SCC being popped + // and the previous SCC. + if (!root_.empty()) + root_.front().node.succ.emplace_back(cond, num); + } + continue; + } + + // We have a successor to look at. + // Fetch the values we are interested in... + unsigned dest = succ->dst; + bdd acc = succ->acc; + bdd cond = succ->cond; + ++todo_.top().second; + + // We do not need SUCC from now on. + + // Are we going to a new state? + int spi = h_[dest]; + if (spi == 0) + { + // Yes. Number it, stack it, and register its successors + // for later processing. + h_[dest] = --num_; + root_.emplace_front(num_, cond, acc); + todo_.emplace(dest, aut->get_graph().out(dest).begin()); + continue; + } + + // We already know the state. + + // Have we reached a maximal SCC? + if (spi > 0) + { + --spi; + // Record that there is a transition from this SCC to the + // dest SCC labelled with cond. + auto& succ = root_.front().node.succ; + scc_succs::iterator i = std::find_if(succ.begin(), succ.end(), + [spi](const scc_trans& x) { + return (x.dst == + (unsigned) spi); + }); + if (i == succ.end()) + succ.emplace_back(cond, spi); + else + i->cond |= 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 descending: we just have to merge all SCCs from the + // top of ROOT that have an index lesser than the one of + // the SCC of S2 (called the "threshold"). + int threshold = spi; + std::list states; + scc_succs succs; + while (threshold > root_.front().index) + { + assert(!root_.empty()); + acc |= root_.front().node.acc | root_.front().in_acc; + states.splice(states.end(), root_.front().node.states); + + succs.insert(succs.end(), + root_.front().node.succ.begin(), + root_.front().node.succ.end()); + root_.pop_front(); + } + + // 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 higher SCC. + + // Accumulate all acceptance conditions, states, SCC + // successors, and conditions into the merged SCC. + root_.front().node.acc |= acc; + root_.front().node.states.splice(root_.front().node.states.end(), + states); + root_.front().node.succ.insert(root_.front().node.succ.end(), + succs.begin(), succs.end()); + // This SCC is no longer trivial. + root_.front().node.trivial = false; + } + + // An SCC is useful if it is accepting or it has a successor SCC + // that is useful. + unsigned scccount = scc_count(); + for (unsigned i = 0; i < scccount; i++) + { + bool useful = node_[i].accepting; + for (auto j: node_[i].succ) + useful |= node_[j.dst].useful; + node_[i].useful = useful; + } + } + + std::ostream& + dump_scc_info_dot(std::ostream& out, + const tgba_digraph* aut, scc_info* sccinfo) + { + scc_info* m = sccinfo ? sccinfo : new scc_info(aut); + + bdd all_acc = aut->all_acceptance_conditions(); + + out << "digraph G {\n i [label=\"\", style=invis, height=0]\n"; + int start = m->scc_of(aut->get_init_state_number()); + out << " i -> " << start << std::endl; + + std::vector seen(m->scc_count()); + seen[start] = true; + + std::queue q; + q.push(start); + while (!q.empty()) + { + int state = q.front(); + q.pop(); + + out << " " << state << " [shape=box," + << (m->acc(state) == all_acc ? "style=bold," : "") + << "label=\"" << state; + { + size_t n = m->states_of(state).size(); + out << " (" << n << " state"; + if (n > 1) + out << 's'; + out << ')'; + } + out << "\"]\n"; + + for (auto& i: m->succ(state)) + { + int dest = i.dst; + bdd label = i.cond; + + out << " " << state << " -> " << dest + << " [label=\""; + escape_str(out, bdd_format_formula(aut->get_dict(), label)); + out << "\"]\n"; + + if (seen[dest]) + continue; + + seen[dest] = true; + q.push(dest); + } + } + + out << "}\n"; + if (!sccinfo) + delete m; + return out; + } + + +} diff --git a/src/tgbaalgos/sccinfo.hh b/src/tgbaalgos/sccinfo.hh new file mode 100644 index 000000000..f03a42d16 --- /dev/null +++ b/src/tgbaalgos/sccinfo.hh @@ -0,0 +1,137 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2014 Laboratoire de Recherche et Développement 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 3 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 this program. If not, see . + +#ifndef SPOT_TGBAALGOS_SCCINFO_HH +# define SPOT_TGBAALGOS_SCCINFO_HH + +#include +#include "bdd.h" +#include "tgba/tgbagraph.hh" + +namespace spot +{ + + class SPOT_API scc_info + { + public: + struct scc_trans + { + scc_trans(bdd cond, unsigned dst) + : cond(cond), dst(dst) + { + } + bdd cond; + unsigned dst; + }; + + typedef std::vector scc_succs; + + struct scc_node + { + scc_node(): + acc(bddfalse), trivial(true) + { + } + + scc_node(bdd acc, bool trivial): + acc(acc), trivial(trivial) + { + } + + scc_succs succ; + bdd acc; + std::list states; // States of the component + bool trivial:1; + bool accepting:1; + bool useful:1; + }; + + protected: + + std::vector sccof_; + std::vector node_; + + const scc_node& node(unsigned scc) + { + assert(scc < node_.size()); + return node_[scc]; + } + + public: + scc_info(const tgba_digraph* aut); + + unsigned scc_count() + { + return node_.size(); + } + + unsigned scc_of(unsigned st) + { + assert(st < sccof_.size()); + return sccof_[st]; + } + + const std::list& states_of(unsigned scc) + { + return node(scc).states; + } + + const scc_succs& succ(unsigned scc) + { + return node(scc).succ; + } + + bool is_trivial(unsigned scc) + { + return node(scc).trivial; + } + + bdd acc(unsigned scc) + { + return node(scc).acc; + } + + bool is_accepting_scc(unsigned scc) + { + return node(scc).accepting; + } + + bool is_useful_scc(unsigned scc) + { + return node(scc).useful; + } + + bool is_useful_state(unsigned st) + { + return node(scc_of(st)).useful; + } + + }; + + + /// \brief Dump the SCC graph of \a aut on \a out. + /// + /// If \a sccinfo is not given, it will be computed. + SPOT_API std::ostream& + dump_scc_info_dot(std::ostream& out, + const tgba_digraph* aut, scc_info* sccinfo = nullptr); + +} + +#endif // SPOT_TGBAALGOS_SCCINFO_HH diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index 2ed34f5f9..a2a2fed39 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -62,6 +62,7 @@ #include "tgbaalgos/scc.hh" #include "tgbaalgos/emptiness_stats.hh" #include "tgbaalgos/scc.hh" +#include "tgbaalgos/sccinfo.hh" #include "tgbaalgos/isdet.hh" #include "tgbaalgos/cycles.hh" #include "tgbaalgos/isweakscc.hh" @@ -1802,10 +1803,24 @@ main(int argc, char** argv) build_scc_stats(a).dump(std::cout); break; case 10: - dump_scc_dot(a, std::cout, false); + { + const spot::tgba_digraph* g = + dynamic_cast(a); + if (!g) + dump_scc_dot(a, std::cout, false); + else + dump_scc_info_dot(std::cout, g); + } break; case 11: - dump_scc_dot(a, std::cout, true); + { + //const spot::tgba_digraph* g = + // dynamic_cast(a); + //if (!g) + dump_scc_dot(a, std::cout, true); + //else + // dump_scc_info_dot(std::cout, g); + } break; case 12: stats_reachable(a).dump(std::cout);