* 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.
This commit is contained in:
Alexandre Duret-Lutz
parent
642c2b1a71
commit
a2b6bef003
5 changed files with 120 additions and 15 deletions
|
|
@ -1,3 +1,12 @@
|
|||
2009-06-02 Alexandre Duret-Lutz <adl@lrde.epita.fr>
|
||||
|
||||
* 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 <adl@lrde.epita.fr>
|
||||
|
||||
Lift the SCC computation off future_condition_collectors, into
|
||||
|
|
|
|||
|
|
@ -297,44 +297,50 @@ namespace spot
|
|||
struct scc_recurse_data
|
||||
{
|
||||
scc_recurse_data() : acc_scc(0), dead_scc(0) {};
|
||||
typedef std::map<int, unsigned> graph_counter;
|
||||
typedef std::map<unsigned, unsigned> 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;
|
||||
|
|
|
|||
|
|
@ -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<unsigned, bdd> succ_type;
|
||||
typedef std::set<bdd, bdd_less_than> 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<const state*>& 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:
|
||||
|
|
|
|||
|
|
@ -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 \
|
||||
|
|
|
|||
49
src/tgbatest/scc.test
Executable file
49
src/tgbatest/scc.test
Executable file
|
|
@ -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 <<EOF
|
||||
transitions: 15
|
||||
states: 6
|
||||
total SCCs: 5
|
||||
accepting SCCs: 1
|
||||
dead SCCs: 0
|
||||
accepting paths: 4
|
||||
dead paths: 0
|
||||
EOF
|
||||
diff out expected
|
||||
|
||||
|
||||
run 0 ./ltl2tgba -f -k '(b U a) | (GFa & XG!a)' >out
|
||||
cat >expected <<EOF
|
||||
transitions: 7
|
||||
states: 4
|
||||
total SCCs: 4
|
||||
accepting SCCs: 1
|
||||
dead SCCs: 1
|
||||
accepting paths: 2
|
||||
dead paths: 1
|
||||
EOF
|
||||
Loading…
Add table
Add a link
Reference in a new issue