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.
This commit is contained in:
Alexandre Duret-Lutz
parent
5b74160abb
commit
731561cdac
5 changed files with 5 additions and 176 deletions
|
|
@ -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<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, 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)
|
||||
{
|
||||
|
|
|
|||
|
|
@ -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<bool> useless_scc_map;
|
||||
|
||||
/// The set of useful acceptance conditions (i.e. acceptance
|
||||
/// conditions that are not always implied by other acceptance
|
||||
/// conditions).
|
||||
std::set<acc_cond::mark_t> 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);
|
||||
|
|
|
|||
|
|
@ -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 =
|
||||
|
|
|
|||
|
|
@ -27,6 +27,7 @@ cat >formulas<<EOF
|
|||
b U a,3,2,2
|
||||
0,0,1,1
|
||||
(Gb | F!a) W GFc,22,6,5
|
||||
(!a & G(Ga | F(!a & b))) | (a & F(F!a & G(a | !b))),16,7,6
|
||||
EOF
|
||||
|
||||
run 0 ../../bin/ltl2tgba --low --any --stats='%f,%e,%s,%c' -F formulas/1 >out
|
||||
|
|
|
|||
|
|
@ -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 <<EOF
|
||||
transitions: 21
|
||||
states: 8
|
||||
total SCCs: 6
|
||||
accepting SCCs: 3
|
||||
dead SCCs: 0
|
||||
accepting paths: 4
|
||||
dead paths: 0
|
||||
EOF
|
||||
diff stdout expected
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue