From 731561cdac32f34ad87b95af6ebc59d804943145 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sun, 18 Jan 2015 21:24:11 +0100 Subject: [PATCH] scc: get rid of scc_stats * src/tgbaalgos/scc.cc, src/tgbaalgos/scc.hh: Here. * src/tgbatest/ltl2tgba.cc: Remove option -k. * src/tgbatest/sccsimpl.test: Move the only -k test... * src/tgbatest/scc.test:... here. --- src/tgbaalgos/scc.cc | 111 +------------------------------------ src/tgbaalgos/scc.hh | 44 +-------------- src/tgbatest/ltl2tgba.cc | 10 ---- src/tgbatest/scc.test | 1 + src/tgbatest/sccsimpl.test | 15 ----- 5 files changed, 5 insertions(+), 176 deletions(-) diff --git a/src/tgbaalgos/scc.cc b/src/tgbaalgos/scc.cc index d6c847109..83d40005e 100644 --- a/src/tgbaalgos/scc.cc +++ b/src/tgbaalgos/scc.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2008, 2009, 2011, 2012, 2013, 2014 Laboratoire de -// Recherche et Développement de l'Epita. +// Copyright (C) 2008, 2009, 2011, 2012, 2013, 2014, 2015 Laboratoire +// de Recherche et Développement de l'Epita. // // This file is part of Spot, a model checking library. // @@ -27,18 +27,6 @@ namespace spot { - std::ostream& - scc_stats::dump(std::ostream& out) const - { - out << "total SCCs: " << scc_total << std::endl; - out << "accepting SCCs: " << acc_scc << std::endl; - out << "dead SCCs: " << dead_scc << std::endl; - out << "accepting paths: " << acc_paths << std::endl; - out << "dead paths: " << dead_paths << std::endl; - return out; - } - - scc_map::scc_map(const const_tgba_ptr& aut) : aut_(aut) { @@ -373,101 +361,6 @@ namespace spot return scc_map_[n].useful_acc; } - namespace - { - struct scc_recurse_data - { - scc_recurse_data() : acc_scc(0), dead_scc(0) {}; - 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, 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; - unsigned acc_paths = 0; - unsigned dead_paths = 0; - - bool paths_accepting = false; - for (it = succ.begin(); it != succ.end(); ++it) - { - unsigned dest = it->first; - bool path_accepting = scc_recurse(m, dest, data); - paths_accepting |= path_accepting; - - acc_paths += data.acc_paths[dest]; - dead_paths += data.dead_paths[dest]; - } - - if (accepting) - { - ++data.acc_scc; - 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; - data.dead_paths[state] = dead_paths; - - return accepting | paths_accepting; - } - - } - - scc_stats build_scc_stats(const scc_map& m) - { - scc_stats res; - res.self_loops = m.self_loops(); - res.scc_total = m.scc_count(); - - scc_recurse_data d; - unsigned init = m.initial(); - scc_recurse(m, init, d); - - res.acc_scc = d.acc_scc; - res.dead_scc = d.dead_scc; - res.acc_paths = d.acc_paths[init]; - res.dead_paths = d.dead_paths[init]; - - res.useless_scc_map.reserve(res.scc_total); - for (unsigned n = 0; n < res.scc_total; ++n) - { - res.useless_scc_map[n] = !d.acc_paths[n]; - if (m.accepting(n)) - { - auto& c = m.useful_acc_of(n); - res.useful_acc.insert(c.begin(), c.end()); - } - } - return res; - } - - scc_stats - build_scc_stats(const const_tgba_ptr& 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, bool verbose) { diff --git a/src/tgbaalgos/scc.hh b/src/tgbaalgos/scc.hh index 7488fbf33..0e9615101 100644 --- a/src/tgbaalgos/scc.hh +++ b/src/tgbaalgos/scc.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2008, 2009, 2010, 2011, 2012, 2013, 2014 Laboratoire de -// Recherche et Développement de l'Epita. +// Copyright (C) 2008, 2009, 2010, 2011, 2012, 2013, 2014, 2015 +// Laboratoire de Recherche et Développement de l'Epita. // // This file is part of Spot, a model checking library. // @@ -31,41 +31,6 @@ namespace spot { - struct SPOT_API scc_stats - { - /// Total number of SCCs. - unsigned scc_total; - /// Total number of accepting SCC. - unsigned acc_scc; - /// Total number of dead SCC. - /// - /// An SCC is dead if no accepting SCC is reachable from it. - /// Note that an SCC can be neither dead nor accepting. - unsigned dead_scc; - - /// Number of maximal accepting paths. - /// - /// A path is maximal and accepting if it ends in an accepting - /// SCC that has only dead (i.e. non accepting) successors, or no - /// successors at all. - unsigned acc_paths; - /// Number of paths to a terminal dead SCC. - /// - /// A terminal dead SCC is a dead SCC without successors. - unsigned dead_paths; - unsigned self_loops; - - /// A map of the useless SCCs. - std::vector useless_scc_map; - - /// The set of useful acceptance conditions (i.e. acceptance - /// conditions that are not always implied by other acceptance - /// conditions). - std::set useful_acc; - - std::ostream& dump(std::ostream& out) const; - }; - /// Build a map of Strongly Connected components in in a TGBA. class SPOT_API scc_map { @@ -238,11 +203,6 @@ namespace spot unsigned self_loops_; // Self loops count. }; - SPOT_API scc_stats - build_scc_stats(const const_tgba_ptr& a); - SPOT_API scc_stats - build_scc_stats(const scc_map& m); - SPOT_API std::ostream& dump_scc_dot(const const_tgba_ptr& a, std::ostream& out, bool verbose = false); diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index 6b5c65512..988aa2760 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -273,8 +273,6 @@ syntax(char* prog) << "Output options (if no emptiness check):" << std::endl << " -b output the automaton in the format of spot" << std::endl - << " -k display statistics on the automaton (size and SCCs)" - << std::endl << " -ks display statistics on the automaton (size only)" << std::endl << " -kt display statistics on the automaton (size + " @@ -553,10 +551,6 @@ checked_main(int argc, char** argv) output = 17; hoa_opt = argv[formula_index] + 2; } - else if (!strcmp(argv[formula_index], "-k")) - { - output = 9; - } else if (!strcmp(argv[formula_index], "-ks")) { output = 12; @@ -1608,10 +1602,6 @@ checked_main(int argc, char** argv) } break; } - case 9: - stats_reachable(a).dump(std::cout); - build_scc_stats(a).dump(std::cout); - break; case 10: { auto aa = diff --git a/src/tgbatest/scc.test b/src/tgbatest/scc.test index 3b0b42d9e..4bbf8bf81 100755 --- a/src/tgbatest/scc.test +++ b/src/tgbatest/scc.test @@ -27,6 +27,7 @@ cat >formulas<out diff --git a/src/tgbatest/sccsimpl.test b/src/tgbatest/sccsimpl.test index cf1730ab0..4313dc1ef 100755 --- a/src/tgbatest/sccsimpl.test +++ b/src/tgbatest/sccsimpl.test @@ -171,18 +171,3 @@ test `grep '^acc' out8.txt | wc -w` = 4 run 0 ../ltl2tgba -R3 -s -RDS -ks \ '(G(!((b) R (a)))) R (((c) R (!(d))) U (G((a) | (!(G(e))))))' > out9.txt grep 'states: 6$' out9.txt - - -# From Spot 1.1 to 1.1.2, this failed with a BDD error because of -# a bug in scc_filter(). -run 0 ../ltl2tgba -R3 -k '(a) <-> F(Ga <-> F!(b -> a))' >stdout -cat >expected <