diff --git a/NEWS b/NEWS index 844734f21..ad4324de0 100644 --- a/NEWS +++ b/NEWS @@ -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: diff --git a/src/bin/common_aoutput.hh b/src/bin/common_aoutput.hh index ee11b71e7..8b68618bd 100644 --- a/src/bin/common_aoutput.hh +++ b/src/bin/common_aoutput.hh @@ -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')) { diff --git a/src/bin/ltlcross.cc b/src/bin/ltlcross.cc index 71f80e4a1..db48a3f0b 100644 --- a/src/bin/ltlcross.cc +++ b/src/bin/ltlcross.cc @@ -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 { diff --git a/src/taalgos/stats.cc b/src/taalgos/stats.cc index 7e963154d..9742cc190 100644 --- a/src/taalgos/stats.cc +++ b/src/taalgos/stats.cc @@ -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; } diff --git a/src/taalgos/stats.hh b/src/taalgos/stats.hh index a26d7469b..0853dae03 100644 --- a/src/taalgos/stats.hh +++ b/src/taalgos/stats.hh @@ -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; diff --git a/src/tests/checkta.cc b/src/tests/checkta.cc index b973756e2..eec5d5062 100644 --- a/src/tests/checkta.cc +++ b/src/tests/checkta.cc @@ -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'; } diff --git a/src/tests/complementation.cc b/src/tests/complementation.cc index 09568f917..aba54c06c 100644 --- a/src/tests/complementation.cc +++ b/src/tests/complementation.cc @@ -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; diff --git a/src/tests/ikwiad.cc b/src/tests/ikwiad.cc index 4c5b8b6a5..a76861bd7 100644 --- a/src/tests/ikwiad.cc +++ b/src/tests/ikwiad.cc @@ -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(); diff --git a/src/tests/ltl2tgba.test b/src/tests/ltl2tgba.test index 08fe5caca..fa81056f2 100755 --- a/src/tests/ltl2tgba.test +++ b/src/tests/ltl2tgba.test @@ -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 diff --git a/src/tests/neverclaimread.test b/src/tests/neverclaimread.test index 87f607474..158c72597 100755 --- a/src/tests/neverclaimread.test +++ b/src/tests/neverclaimread.test @@ -205,7 +205,7 @@ accept_T3: } EOF cat >expected<(x); } -spot::tgba_statistics prod_stats; +spot::twa_statistics prod_stats; static float prod_conv(const char* name, unsigned x) { float y = static_cast(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) diff --git a/src/tests/renault.test b/src/tests/renault.test index 3fa907173..b43755290 100755 --- a/src/tests/renault.test +++ b/src/tests/renault.test @@ -65,7 +65,7 @@ State: 9 EOF cat >outexp <expected <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')) diff --git a/src/twaalgos/stats.hh b/src/twaalgos/stats.hh index b625454ff..5c75fff48 100644 --- a/src/twaalgos/stats.hh +++ b/src/twaalgos/stats.hh @@ -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 diff --git a/wrap/python/ajax/spotcgi.in b/wrap/python/ajax/spotcgi.in index cc5560705..696c72176 100755 --- a/wrap/python/ajax/spotcgi.in +++ b/wrap/python/ajax/spotcgi.in @@ -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'):