alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

stats: rename structures and attribute for concistency

Browse source 
* src/taalgos/stats.cc, src/taalgos/stats.hh
(tgba_statistics::transitions, tgba_sub_statistics::sub_transitions):
Rename ...
(twa_statistics::edges, twa_sub_statistics::transitions): ... to
these.
* NEWS: Mention it.
* src/bin/common_aoutput.hh, src/bin/ltlcross.cc,
src/tests/checkta.cc, src/tests/complementation.cc,
src/tests/ikwiad.cc, src/tests/ltl2tgba.test,
src/tests/neverclaimread.test, src/tests/randtgba.cc,
src/tests/renault.test, src/tests/wdba2.test, src/twaalgos/dtbasat.cc,
src/twaalgos/dtgbasat.cc, src/twaalgos/stats.cc,
src/twaalgos/stats.hh, wrap/python/ajax/spotcgi.in: Adjust.
This commit is contained in:
Alexandre Duret-Lutz 2015-10-24 17:03:56 +02:00
parent f7c4ca816b
commit 4a91fccc33
18 changed files with 96 additions and 97 deletions
Download patch file Download diff file Expand all files Collapse all files

5
NEWS
View file

@ -48,7 +48,10 @@ New in spot 1.99.4a (not yet released)
"trust_hoa": when true (the default) supported properties declared
in HOA files are trusted even if they cannot be easily be verified.
* ltl_simplifier renamed to tl_simplifier.
* renamings:
ltl_simplifier -> tl_simplifier
tgba_statistics::transitions -> twa_statistics::edges
tgba_sub_statistics::sub_transitions -> twa_sub_statistics::transitions
Python:

10
src/bin/common_aoutput.hh
View file

@ -128,16 +128,16 @@ public:
if (has('T'))
{
spot::tgba_sub_statistics s = sub_stats_reachable(haut->aut);
spot::twa_sub_statistics s = sub_stats_reachable(haut->aut);
haut_states_ = s.states;
haut_edges_ = s.transitions;
haut_trans_ = s.sub_transitions;
haut_edges_ = s.edges;
haut_trans_ = s.transitions;
}
else if (has('E'))
{
spot::tgba_sub_statistics s = sub_stats_reachable(haut->aut);
spot::twa_sub_statistics s = sub_stats_reachable(haut->aut);
haut_states_ = s.states;
haut_edges_ = s.transitions;
haut_edges_ = s.edges;
}
if (has('M'))
{

10
src/bin/ltlcross.cc
View file

@ -601,10 +601,10 @@ namespace
if (verbose)
std::cerr << "info: getting statistics\n";
st->ok = true;
spot::tgba_sub_statistics s = sub_stats_reachable(res);
spot::twa_sub_statistics s = sub_stats_reachable(res);
st->states = s.states;
st->edges = s.transitions;
st->transitions = s.sub_transitions;
st->edges = s.edges;
st->transitions = s.transitions;
st->acc = res->acc().num_sets();
spot::scc_info m(res);
unsigned c = m.scc_count();
@ -927,9 +927,9 @@ namespace
if (sm)
{
(*stats)[i].product_scc.push_back(sm->scc_count());
spot::tgba_statistics s = spot::stats_reachable(sm->get_aut());
spot::twa_statistics s = spot::stats_reachable(sm->get_aut());
(*stats)[i].product_states.push_back(s.states);
(*stats)[i].product_transitions.push_back(s.transitions);
(*stats)[i].product_transitions.push_back(s.edges);
}
else
{

8
src/taalgos/stats.cc
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2008, 2014 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
// Copyright (C) 2008, 2014, 2015 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie.
@ -49,7 +49,7 @@ namespace spot
void
process_link(int, int, const ta_succ_iterator*)
{
++s_.transitions;
++s_.edges;
}
private:
@ -61,7 +61,7 @@ namespace spot
std::ostream&
ta_statistics::dump(std::ostream& out) const
{
out << "transitions: " << transitions << std::endl;
out << "edges: " << edges << std::endl;
out << "states: " << states << std::endl;
return out;
}

6
src/taalgos/stats.hh
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2011, 2013, 2014 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
// Copyright (C) 2011, 2013, 2014, 2015 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
//
@ -30,7 +30,7 @@ namespace spot
struct SPOT_API ta_statistics
{
unsigned transitions;
unsigned edges;
unsigned states;
unsigned acceptance_states;

4
src/tests/checkta.cc
View file

@ -47,7 +47,7 @@ stats(std::string title, const spot::ta_ptr& ta)
std::cout << std::left << std::setw(20) << title << " | "
<< std::right << std::setw(6) << s.states << " | "
<< std::setw(6) << s.transitions << " | "
<< std::setw(6) << s.edges << " | "
<< std::setw(6) << s.acceptance_states << '\n';
}
@ -58,7 +58,7 @@ stats(std::string title, const spot::twa_ptr& tg)
std::cout << std::left << std::setw(20) << title << " | "
<< std::right << std::setw(6) << s.states << " | "
<< std::setw(6) << s.transitions << " | "
<< std::setw(6) << s.edges << " | "
<< std::setw(6) << "XXX" << '\n';
}

16
src/tests/complementation.cc
View file

@ -186,10 +186,10 @@ int main(int argc, char* argv[])
auto safra_complement = spot::make_safra_complement(a);
spot::tgba_statistics a_size = spot::stats_reachable(a);
spot::twa_statistics a_size = spot::stats_reachable(a);
std::cout << "Original: "
<< a_size.states << ", "
<< a_size.transitions << ", "
<< a_size.edges << ", "
<< a->acc().num_sets()
<< std::endl;
@ -200,20 +200,20 @@ int main(int argc, char* argv[])
<< buchi->acc().num_sets()
<< std::endl;
spot::tgba_statistics b_size = spot::stats_reachable(safra_complement);
spot::twa_statistics b_size = spot::stats_reachable(safra_complement);
std::cout << "Safra Complement: "
<< b_size.states << ", "
<< b_size.transitions << ", "
<< b_size.edges << ", "
<< safra_complement->acc().num_sets()
<< std::endl;
if (formula)
{
auto a2 = spot::ltl_to_tgba_fm(spot::formula::Not(f1), dict);
spot::tgba_statistics a_size = spot::stats_reachable(a2);
spot::twa_statistics a_size = spot::stats_reachable(a2);
std::cout << "Not Formula: "
<< a_size.states << ", "
<< a_size.transitions << ", "
<< a_size.edges << ", "
<< a2->acc().num_sets()
<< std::endl;
}
@ -233,11 +233,11 @@ int main(int argc, char* argv[])
auto nAnf = spot::make_safra_complement(Anf);
auto ec = spot::couvreur99(spot::otf_product(nAf, nAnf));
auto res = ec->check();
spot::tgba_statistics a_size = spot::stats_reachable(ec->automaton());
spot::twa_statistics a_size = spot::stats_reachable(ec->automaton());
std::cout << "States: "
<< a_size.states << std::endl
<< "Transitions: "
<< a_size.transitions << std::endl
<< a_size.edges << std::endl
<< "Acc Cond: "
<< ec->automaton()->acc().num_sets()
<< std::endl;

4
src/tests/ikwiad.cc
View file

@ -1516,12 +1516,12 @@ checked_main(int argc, char** argv)
std::ios::fmtflags old = std::cout.flags();
std::cout << std::left << std::setw(25)
<< echeck_algo << ", ";
spot::tgba_statistics a_size =
spot::twa_statistics a_size =
spot::stats_reachable(ec->automaton());
std::cout << std::right << std::setw(10)
<< a_size.states << ", "
<< std::right << std::setw(10)
<< a_size.transitions << ", ";
<< a_size.edges << ", ";
std::cout << ec->automaton()->acc().num_sets()
<< ", ";
auto ecs = ec->emptiness_check_statistics();

26
src/tests/ltl2tgba.test
View file

@ -109,7 +109,7 @@ run 0 ../ikwiad -e -R3 '(G!{(b;1)*;a} && ({1;1[*3]*}[]->{(b&!a)[*2];!b&!a}))'
# before and after degeneralization.
for opt in '' -DT -DS; do
../ikwiad -ks -f -R3 $opt 'a U (b U c)' > stdout
grep 'transitions: 6$' stdout
grep 'edges: 6$' stdout
grep 'states: 3$' stdout
done
@ -117,8 +117,8 @@ done
# before and after degeneralization.
for opt in '' -DT -DS; do
../ikwiad -kt -f -R3 $opt '!(Ga U b)' > stdout
grep 'sub trans.: 11$' stdout
grep 'transitions: 6$' stdout
grep 'transitions: 11$' stdout
grep 'edges: 6$' stdout
grep 'states: 3$' stdout
done
@ -126,8 +126,8 @@ done
# before and after degeneralization.
for opt in '' -DT -DS; do
../ikwiad -kt -f -R3 $opt 'Ga U b' > stdout
grep 'sub trans.: 12$' stdout
grep 'transitions: 6$' stdout
grep 'transitions: 12$' stdout
grep 'edges: 6$' stdout
grep 'states: 4$' stdout
done
@ -136,10 +136,10 @@ done
f='(G (p -> F q)) && ((X (p) U q) || ! X (p U (p && q)))'
for opt in '' -DT -DS; do
../ikwiad -ks -f -R3 $opt "$f" > stdout
grep 'transitions: 15$' stdout
grep 'edges: 15$' stdout
grep 'states: 6$' stdout
../ikwiad -ks -f -R3f $opt "$f" > stdout
grep 'transitions: 15$' stdout
grep 'edges: 15$' stdout
grep 'states: 6$' stdout
done
@ -147,16 +147,16 @@ done
# has 7 states and 34 transitions after degeneralization.
f='GFa & GFb & GFc & GFd & GFe & GFg'
../ikwiad -ks -DS -x -f "$f" > stdout
grep 'transitions: 34$' stdout
grep 'edges: 34$' stdout
grep 'states: 7$' stdout
# Make sure 'Ga & XXXX!a' is minimized to one state.
f='Ga & XXXX!a'
../ikwiad -ks -f "$f" > stdout
grep 'transitions: 4$' stdout
grep 'edges: 4$' stdout
grep 'states: 5$' stdout
../ikwiad -ks -Rm -f "$f" > stdout
grep 'transitions: 0$' stdout
grep 'edges: 0$' stdout
grep 'states: 1$' stdout
# Make sure a monitor for F(a & F(b)) accepts everything.
@ -169,12 +169,12 @@ cmp stdout expected
# This formula caused a segfault with Spot 0.7.
run 0 ../ikwiad -Rm -ks -f "Gq|Gr|(G(q|FGp)&G(r|FG!p))" >stdout
grep 'transitions: 5$' stdout
grep 'edges: 5$' stdout
grep 'states: 3$' stdout
# Adding -R3 used to make it work...
run 0 ../ikwiad -R3 -Rm -ks -f "Gq|Gr|(G(q|FGp)&G(r|FG!p))" >stdout
grep 'transitions: 5$' stdout
grep 'edges: 5$' stdout
grep 'states: 3$' stdout
# Make sure FGa|GFb has the same number of states/transitions when
@ -189,7 +189,7 @@ cmp count.never count.hoa
# The following automaton should have only 4 states.
run 0 ../ikwiad -R3 -ks -f '(p&XF!p)|(!p&XFp)|X(Fp&F!p)' >stdout
grep 'transitions: 7$' stdout
grep 'edges: 7$' stdout
grep 'states: 4$' stdout
# A bug in the translation of !{xxx} when xxx reduces to false caused

2
src/tests/neverclaimread.test
View file

@ -205,7 +205,7 @@ accept_T3:
}
EOF
cat >expected<<EOF
transitions: 6
edges: 6
states: 4
EOF

6
src/tests/randtgba.cc
View file

@ -248,14 +248,14 @@ id(const char*, unsigned x)
return static_cast<T>(x);
}
spot::tgba_statistics prod_stats;
spot::twa_statistics prod_stats;
static float
prod_conv(const char* name, unsigned x)
{
float y = static_cast<float>(x);
if (!strcmp(name, "transitions"))
return y / prod_stats.transitions * 100.0;
return y / prod_stats.edges * 100.0;
return y / prod_stats.states * 100.0;
}
@ -958,7 +958,7 @@ main(int argc, char** argv)
{
// To trigger a division by 0 if used erroneously.
prod_stats.states = 0;
prod_stats.transitions = 0;
prod_stats.edges = 0;
}
if (opt_z && ecs)

2
src/tests/renault.test
View file

@ -65,7 +65,7 @@ State: 9
EOF
cat >outexp <<EOF
transitions: 12
edges: 12
states: 6
EOF

4
src/tests/wdba2.test
View file

@ -23,8 +23,8 @@
set -e
cat >expected <<EOF
sub trans.: 16
transitions: 8
transitions: 16
edges: 8
states: 4
nondeterministic states: 0
EOF

5
src/twaalgos/dtbasat.cc
View file

@ -785,9 +785,8 @@ namespace spot
out << target_state_number << ',';
if (res)
{
tgba_sub_statistics st = sub_stats_reachable(res);
out << st.states << ',' << st.transitions
<< ',' << st.sub_transitions;
twa_sub_statistics st = sub_stats_reachable(res);
out << st.states << ',' << st.edges << ',' << st.transitions;
}
else
{

5
src/twaalgos/dtgbasat.cc
View file

@ -1170,9 +1170,8 @@ namespace spot
out << target_state_number << ',';
if (res)
{
tgba_sub_statistics st = sub_stats_reachable(res);
out << st.states << ',' << st.transitions
<< ',' << st.sub_transitions;
twa_sub_statistics st = sub_stats_reachable(res);
out << st.states << ',' << st.edges << ',' << st.transitions;
}
else
{

46
src/twaalgos/stats.cc
View file

@ -36,7 +36,7 @@ namespace spot
class stats_bfs: public tgba_reachable_iterator_breadth_first
{
public:
stats_bfs(const const_twa_ptr& a, tgba_statistics& s)
stats_bfs(const const_twa_ptr& a, twa_statistics& s)
: tgba_reachable_iterator_breadth_first(a), s_(s)
{
}
@ -51,17 +51,17 @@ namespace spot
process_link(const state*, int, const state*, int,
const twa_succ_iterator*)
{
++s_.transitions;
++s_.edges;
}
private:
tgba_statistics& s_;
twa_statistics& s_;
};
class sub_stats_bfs: public stats_bfs
{
public:
sub_stats_bfs(const const_twa_ptr& a, tgba_sub_statistics& s)
sub_stats_bfs(const const_twa_ptr& a, twa_sub_statistics& s)
: stats_bfs(a, s), s_(s), seen_(bddtrue)
{
}
@ -70,7 +70,7 @@ namespace spot
process_link(const state*, int, const state*, int,
const twa_succ_iterator* it)
{
++s_.transitions;
++s_.edges;
bdd cond = it->current_condition();
bdd newvars = bdd_exist(bdd_support(cond), seen_);
@ -87,49 +87,49 @@ namespace spot
// transitions we counted so far are actually double
// subtransitions. If we have two new variables, they where
// quadruple transitions, etc.
s_.sub_transitions <<= count;
s_.transitions <<= count;
}
while (cond != bddfalse)
{
cond -= bdd_satoneset(cond, seen_, bddtrue);
++s_.sub_transitions;
++s_.transitions;
}
}
private:
tgba_sub_statistics& s_;
twa_sub_statistics& s_;
bdd seen_;
};
} // anonymous
std::ostream& tgba_statistics::dump(std::ostream& out) const
std::ostream& twa_statistics::dump(std::ostream& out) const
{
out << "transitions: " << transitions << std::endl;
out << "states: " << states << std::endl;
out << "edges: " << edges << '\n';
out << "states: " << states << '\n';
return out;
}
std::ostream& tgba_sub_statistics::dump(std::ostream& out) const
std::ostream& twa_sub_statistics::dump(std::ostream& out) const
{
out << "sub trans.: " << sub_transitions << std::endl;
this->tgba_statistics::dump(out);
out << "transitions: " << transitions << '\n';
this->twa_statistics::dump(out);
return out;
}
tgba_statistics
twa_statistics
stats_reachable(const const_twa_ptr& g)
{
tgba_statistics s;
twa_statistics s;
stats_bfs d(g, s);
d.run();
return s;
}
tgba_sub_statistics
twa_sub_statistics
sub_stats_reachable(const const_twa_ptr& g)
{
tgba_sub_statistics s;
twa_sub_statistics s;
sub_stats_bfs d(g, s);
d.run();
return s;
@ -169,16 +169,16 @@ namespace spot
if (has('t'))
{
tgba_sub_statistics s = sub_stats_reachable(aut);
twa_sub_statistics s = sub_stats_reachable(aut);
states_ = s.states;
edges_ = s.transitions;
trans_ = s.sub_transitions;
edges_ = s.edges;
trans_ = s.transitions;
}
else if (has('s') || has('e'))
{
tgba_sub_statistics s = sub_stats_reachable(aut);
twa_sub_statistics s = sub_stats_reachable(aut);
states_ = s.states;
edges_ = s.transitions;
edges_ = s.edges;
}
if (has('a'))

16
src/twaalgos/stats.hh
View file

@ -32,27 +32,27 @@ namespace spot
/// \addtogroup twa_misc
/// @{
struct SPOT_API tgba_statistics
struct SPOT_API twa_statistics
{
unsigned transitions;
unsigned edges;
unsigned states;
tgba_statistics() { transitions = 0; states = 0; }
twa_statistics() { edges = 0; states = 0; }
std::ostream& dump(std::ostream& out) const;
};
struct SPOT_API tgba_sub_statistics: public tgba_statistics
struct SPOT_API twa_sub_statistics: public twa_statistics
{
unsigned sub_transitions;
unsigned transitions;
tgba_sub_statistics() { sub_transitions = 0; }
twa_sub_statistics() { transitions = 0; }
std::ostream& dump(std::ostream& out) const;
};
/// \brief Compute statistics for an automaton.
SPOT_API tgba_statistics stats_reachable(const const_twa_ptr& g);
SPOT_API twa_statistics stats_reachable(const const_twa_ptr& g);
/// \brief Compute sub statistics for an automaton.
SPOT_API tgba_sub_statistics sub_stats_reachable(const const_twa_ptr& g);
SPOT_API twa_sub_statistics sub_stats_reachable(const const_twa_ptr& g);
class SPOT_API printable_formula: public printable_value<formula>

18
wrap/python/ajax/spotcgi.in
View file

@ -349,16 +349,14 @@ def print_stats(automaton, detinfo = False, ta = False):
unbufprint(" (deterministic)")
else:
unbufprint(" (%d nondeterministic)" % nondet)
if not hasattr(stats, 'sub_transitions'):
unbufprint(", %d transition" % stats.transitions)
if stats.transitions > 1:
if not hasattr(stats, 'transitions'):
unbufprint(", %d edge" % stats.edges)
if stats.edges > 1:
unbufprint("s")
else:
unbufprint(", %d edge%s (%d transition%s)"
% (stats.transitions,
's' if stats.transitions > 1 else '',
stats.sub_transitions,
's' if stats.sub_transitions > 1 else ''))
% (stats.edges, 's' if stats.edges > 1 else '',
stats.transitions, 's' if stats.transitions > 1 else ''))
if hasattr(automaton, 'get_acceptance'):
acc = automaton.get_acceptance()
if (automaton.is_sba() and automaton.acc().is_buchi() and
@ -372,9 +370,9 @@ def print_stats(automaton, detinfo = False, ta = False):
# Decide whether we will render the automaton or not.
# (A webserver is not a computation center...)
if stats.states > 64:
return "Automaton has too much states"
if float(stats.transitions)/stats.states > 10:
return "Automaton has too much transitions per state"
return "Automaton has too many states"
if float(stats.edges)/stats.states > 10:
return "Automaton has too many edges per state"
return False
def format_formula(f, kind='div'):