From a2b6bef003d4e1fa847737c5e3428c483a1a0118 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 2 Jun 2009 15:47:01 +0200 Subject: [PATCH] * src/tgbatest/scc.test: New file. * src/tgbatest/Makefile.am: Adjust. * src/tgbaalgos/scc.hh: More documentation. * src/tgbaalgos/scc.cc (scc_recurse): Fix computation of acc_paths and dead_paths. Prevent recursions in states that have already been visited. --- ChangeLog | 9 ++++++++ src/tgbaalgos/scc.cc | 28 ++++++++++++++--------- src/tgbaalgos/scc.hh | 46 ++++++++++++++++++++++++++++++++++--- src/tgbatest/Makefile.am | 3 ++- src/tgbatest/scc.test | 49 ++++++++++++++++++++++++++++++++++++++++ 5 files changed, 120 insertions(+), 15 deletions(-) create mode 100755 src/tgbatest/scc.test diff --git a/ChangeLog b/ChangeLog index 2b83fb1b1..e48051558 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,12 @@ +2009-06-02 Alexandre Duret-Lutz + + * src/tgbatest/scc.test: New file. + * src/tgbatest/Makefile.am: Adjust. + * src/tgbaalgos/scc.hh: More documentation. + * src/tgbaalgos/scc.cc (scc_recurse): Fix computation of + acc_paths and dead_paths. Prevent recursions in states that + have already been visited. + 2009-05-31 Alexandre Duret-Lutz Lift the SCC computation off future_condition_collectors, into diff --git a/src/tgbaalgos/scc.cc b/src/tgbaalgos/scc.cc index 23ef562f5..5af363198 100644 --- a/src/tgbaalgos/scc.cc +++ b/src/tgbaalgos/scc.cc @@ -297,44 +297,50 @@ namespace spot struct scc_recurse_data { scc_recurse_data() : acc_scc(0), dead_scc(0) {}; - typedef std::map graph_counter; + typedef std::map graph_counter; graph_counter acc_paths; graph_counter dead_paths; unsigned acc_scc; unsigned dead_scc; }; - bool scc_recurse(const scc_map& m, int state, scc_recurse_data& data) + bool scc_recurse(const scc_map& m, unsigned state, scc_recurse_data& data) { + // Don't recurse on previously visited states. + scc_recurse_data::graph_counter::const_iterator i = + data.acc_paths.find(state); + if (i != data.acc_paths.end()) + return i->second > 0; + const scc_map::succ_type& succ = m.succ(state); bool accepting = m.accepting(state); scc_map::succ_type::const_iterator it; - int acc_paths = 0; - int dead_paths = 0; + unsigned acc_paths = 0; + unsigned dead_paths = 0; bool paths_accepting = false; for (it = succ.begin(); it != succ.end(); ++it) { - int dest = it->first; + unsigned dest = it->first; bool path_accepting = scc_recurse(m, dest, data); paths_accepting |= path_accepting; - if (path_accepting) - acc_paths += data.acc_paths[dest]; - else - dead_paths += data.dead_paths[dest]; + acc_paths += data.acc_paths[dest]; + dead_paths += data.dead_paths[dest]; } if (accepting) { ++data.acc_scc; - if (!paths_accepting) + if (acc_paths == 0) acc_paths = 1; } else if (!paths_accepting) { ++data.dead_scc; + if (dead_paths == 0) + dead_paths = 1; } data.acc_paths[state] = acc_paths; @@ -351,7 +357,7 @@ namespace spot res.scc_total = m.scc_count(); scc_recurse_data d; - int init = m.initial(); + unsigned init = m.initial(); scc_recurse(m, init, d); res.acc_scc = d.acc_scc; diff --git a/src/tgbaalgos/scc.hh b/src/tgbaalgos/scc.hh index b4ed08e02..38098b79a 100644 --- a/src/tgbaalgos/scc.hh +++ b/src/tgbaalgos/scc.hh @@ -44,10 +44,11 @@ namespace spot /// Note that an SCC can be neither dead nor accepting. unsigned dead_scc; - /// Number of path to a terminal accepting SCC. + /// Number of maximal accepting paths. /// - /// A terminal accepting SCC is an accepting SCC that has - /// only dead successors (or no successors at all). + /// An path is maximal and accepting if it ends in an accepting + /// SCC that is only dead (i.e. non accepting) successors, or no + /// successors at all. unsigned acc_paths; /// Number of paths to a terminal dead SCC. /// @@ -57,29 +58,68 @@ namespace spot std::ostream& dump(std::ostream& out) const; }; + /// Build a map of Strongly Connected components in in a TGBA. class scc_map { public: typedef std::map succ_type; typedef std::set cond_set; + /// \brief Constructor. + /// + /// This will note compute the map initially. You should call + /// build_map() to do so. scc_map(const tgba* aut); + ~scc_map(); + /// Actually compute the graph of strongly connected components. void build_map(); + /// Get the automaton for which the map has been constructed. const tgba* get_aut() const; + /// \brief Get the number of SCC in the automaton. + /// + /// \pre This should only be called once build_map() has run. unsigned scc_count() const; + /// \brief Get number of the SCC containing the initial state. + /// + /// \pre This should only be called once build_map() has run. unsigned initial() const; + /// \brief Successor SCCs of a SCC. + /// + /// \pre This should only be called once build_map() has run. const succ_type& succ(unsigned n) const; + + /// \brief Return whether an SCC is accepting. + /// + /// \pre This should only be called once build_map() has run. bool accepting(unsigned n) const; + + /// \brief Return the set of conditions occurring in an SCC. + /// + /// \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 acceptance conditions occurring in an SCC. + /// + /// \pre This should only be called once build_map() has run. bdd acc_set_of(unsigned n) const; + + /// \brief Return the set of states of an SCC. + /// + /// The states in the returned list are still owned by the scc_map + /// instance. They should NOT be deleted by the client code. + /// + /// \pre This should only be called once build_map() has run. const std::list& states_of(unsigned n) const; + /// \brief Return the number of the SCC a state belongs too. + /// + /// \pre This should only be called once build_map() has run. unsigned scc_of_state(const state* s) const; protected: diff --git a/src/tgbatest/Makefile.am b/src/tgbatest/Makefile.am index a413e6d79..a2646a9f0 100644 --- a/src/tgbatest/Makefile.am +++ b/src/tgbatest/Makefile.am @@ -1,4 +1,4 @@ -## Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de +## Copyright (C) 2003, 2004, 2005, 2006, 2009 Laboratoire d'Informatique de ## Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), ## Université Pierre et Marie Curie. ## @@ -83,6 +83,7 @@ TESTS = \ dupexp.test \ reduccmp.test \ reductgba.test \ + scc.test \ emptchk.test \ emptchke.test \ dfs.test \ diff --git a/src/tgbatest/scc.test b/src/tgbatest/scc.test new file mode 100755 index 000000000..6b7c69a75 --- /dev/null +++ b/src/tgbatest/scc.test @@ -0,0 +1,49 @@ +#!/bin/sh +# Copyright (C) 2009 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. + +. ./defs + +set -e + + +run 0 ./ltl2tgba -f -k '(a U c) U b & (b U c)' >out +cat >expected <out +cat >expected <