diff --git a/NEWS b/NEWS index d8fd0ab70..bf9e1079e 100644 --- a/NEWS +++ b/NEWS @@ -1,5 +1,12 @@ New in spot 2.11.1.dev (not yet released) + Command-line tools: + + - The --stats specifications %s, %e, %t for printing the number of + (reachable) states, edges, and transitions, learned to support + options [r], [u], [a] to indicate if only reachable, unreachable, + or all elements should be counted. + Library: - spot::reduce_parity() now has a "layered" option to force all diff --git a/bin/common_aoutput.cc b/bin/common_aoutput.cc index e8c2e5401..fcc79fc3c 100644 --- a/bin/common_aoutput.cc +++ b/bin/common_aoutput.cc @@ -203,12 +203,18 @@ static const argp_option io_options[] = "to specify additional options as in --hoa=opt)", 0 }, { "%M, %m", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, "name of the automaton", 0 }, - { "%S, %s", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, - "number of reachable states", 0 }, - { "%E, %e", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, - "number of reachable edges", 0 }, - { "%T, %t", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, - "number of reachable transitions", 0 }, + { "%S, %s, %[LETTER]S, %[LETTER]s", + 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, + "number of states (add one LETTER to select (r) reachable [default], " + "(u) unreachable, (a) all).", 0 }, + { "%E, %e, %[LETTER]E, %[LETTER]e", + 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, + "number of edges (add one LETTER to select (r) reachable [default], " + "(u) unreachable, (a) all).", 0 }, + { "%T, %t, %[LETTER]E, %[LETTER]e", + 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, + "number of transitions (add one LETTER to select (r) reachable " + "[default], (u) unreachable, (a) all).", 0 }, { "%A, %a", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, "number of acceptance sets", 0 }, { "%G, %g, %[LETTERS]G, %[LETTERS]g", 0, nullptr, @@ -268,12 +274,15 @@ static const argp_option o_options[] = "to specify additional options as in --hoa=opt)", 0 }, { "%m", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, "name of the automaton", 0 }, - { "%s", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, - "number of reachable states", 0 }, - { "%e", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, - "number of reachable edges", 0 }, - { "%t", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, - "number of reachable transitions", 0 }, + { "%s, %[LETTER]s", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, + "number of states (add one LETTER to select (r) reachable [default], " + "(u) unreachable, (a) all).", 0 }, + { "%e, %[LETTER]e", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, + "number of edges (add one LETTER to select (r) reachable [default], " + "(u) unreachable, (a) all).", 0 }, + { "%t, %[LETTER]t", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, + "number of transitions (add one LETTER to select (r) reachable " + "[default], (u) unreachable, (a) all).", 0 }, { "%a", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, "number of acceptance sets", 0 }, { "%g, %[LETTERS]g", 0, nullptr, @@ -472,15 +481,15 @@ hoa_stat_printer::print(const spot::const_parsed_aut_ptr& haut, if (has('T')) { spot::twa_sub_statistics s = sub_stats_reachable(haut->aut); - haut_states_ = s.states; - haut_edges_ = s.edges; - haut_trans_ = s.transitions; + haut_states_.set(s.states, haut->aut->num_states()); + haut_edges_.set(s.edges, haut->aut->num_edges()); + haut_trans_.set(s.transitions, count_all_transitions(haut->aut)); } else if (has('E') || has('S')) { spot::twa_statistics s = stats_reachable(haut->aut); - haut_states_ = s.states; - haut_edges_ = s.edges; + haut_states_.set(s.states, haut->aut->num_states()); + haut_edges_.set(s.edges, haut->aut->num_edges()); } if (has('M')) { diff --git a/bin/common_aoutput.hh b/bin/common_aoutput.hh index 0fb2e8d7c..d33b687d2 100644 --- a/bin/common_aoutput.hh +++ b/bin/common_aoutput.hh @@ -166,9 +166,9 @@ private: spot::printable_value aut_word_; spot::printable_value haut_word_; spot::printable_acc_cond haut_gen_acc_; - spot::printable_value haut_states_; - spot::printable_value haut_edges_; - spot::printable_value haut_trans_; + spot::printable_size haut_states_; + spot::printable_size haut_edges_; + spot::printable_long_size haut_trans_; spot::printable_value haut_acc_; printable_varset haut_ap_; printable_varset aut_ap_; diff --git a/doc/org/autfilt.org b/doc/org/autfilt.org index 4ccf09f07..5c8a8f1e5 100644 --- a/doc/org/autfilt.org +++ b/doc/org/autfilt.org @@ -145,7 +145,8 @@ ltl2tgba --help | sed -n '/ sequences:/,/^$/p' | sed '1d;$d' (iw) inherently weak. Use uppercase letters to negate them. %d 1 if the output is deterministic, 0 otherwise - %e number of reachable edges + %e, %[LETTER]e number of edges (add one LETTER to select (r) + reachable [default], (u) unreachable, (a) all). %f the formula, in Spot's syntax %F name of the input file %g, %[LETTERS]g acceptance condition (in HOA syntax); add brackets @@ -170,8 +171,11 @@ ltl2tgba --help | sed -n '/ sequences:/,/^$/p' | sed '1d;$d' LETTERS to restrict to(u) user time, (s) system time, (p) parent process, or (c) children processes. - %s number of reachable states - %t number of reachable transitions + %s, %[LETTER]s number of states (add one LETTER to select (r) + reachable [default], (u) unreachable, (a) all). + %t, %[LETTER]t number of transitions (add one LETTER to select + (r) reachable [default], (u) unreachable, (a) + all). %u, %[e]u number of states (or [e]dges) with universal branching %u, %[LETTER]u 1 if the automaton contains some universal diff --git a/spot/twaalgos/stats.cc b/spot/twaalgos/stats.cc index ddccba5db..4a905e542 100644 --- a/spot/twaalgos/stats.cc +++ b/spot/twaalgos/stats.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2008, 2011-2018, 2020 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// Copyright (C) 2008, 2011-2018, 2020, 2022 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. @@ -33,6 +33,16 @@ namespace spot { + unsigned long long + count_all_transitions(const const_twa_graph_ptr& g) + { + unsigned long long tr = 0; + bdd v = g->ap_vars(); + for (auto& e: g->edges()) + tr += bdd_satcountset(e.cond, v); + return tr; + } + namespace { class stats_bfs: public twa_reachable_iterator_breadth_first @@ -82,6 +92,7 @@ namespace spot }; + template void dfs(const const_twa_graph_ptr& ge, SU state_update, EU edge_update) { @@ -344,10 +355,73 @@ namespace spot << std::string(beg, end + 2) << ", "; tmp << e.what(); throw std::runtime_error(tmp.str()); - } } + void printable_size::print(std::ostream& os, const char* pos) const + { + char p = 'r'; + if (*pos == '[') + { + p = pos[1]; + if (pos[2] != ']' || !(p == 'r' || p == 'u' || p == 'a')) + { + const char* end = strchr(pos + 1, ']'); + std::ostringstream tmp; + tmp << "while processing %" + << std::string(pos, end + 2) << ", " + << "only [a], [r], or [u] is supported."; + throw std::runtime_error(tmp.str()); + } + } + switch (p) + { + case 'r': + os << reachable_; + return; + case 'a': + os << all_; + return; + case 'u': + os << all_ - reachable_; + return; + } + SPOT_UNREACHABLE(); + return; + } + + void printable_long_size::print(std::ostream& os, const char* pos) const + { + char p = 'r'; + if (*pos == '[') + { + p = pos[1]; + if (pos[2] != ']' || !(p == 'r' || p == 'u' || p == 'a')) + { + const char* end = strchr(pos + 1, ']'); + std::ostringstream tmp; + tmp << "while processing %" + << std::string(pos, end + 2) << ", " + << "only [a], [r], or [u] is supported."; + throw std::runtime_error(tmp.str()); + } + } + switch (p) + { + case 'r': + os << reachable_; + return; + case 'a': + os << all_; + return; + case 'u': + os << all_ - reachable_; + return; + } + SPOT_UNREACHABLE(); + return; + } + stat_printer::stat_printer(std::ostream& os, const char* format) : format_(format) @@ -376,15 +450,15 @@ namespace spot if (has('t')) { twa_sub_statistics s = sub_stats_reachable(aut); - states_ = s.states; - edges_ = s.edges; - trans_ = s.transitions; + states_.set(s.states, aut->num_states()); + edges_.set(s.edges, aut->num_edges()); + trans_.set(s.transitions, count_all_transitions(aut)); } else if (has('s') || has('e')) { twa_statistics s = stats_reachable(aut); - states_ = s.states; - edges_ = s.edges; + states_.set(s.states, aut->num_states()); + edges_.set(s.edges, aut->num_edges()); } if (has('a')) diff --git a/spot/twaalgos/stats.hh b/spot/twaalgos/stats.hh index 1caa8324b..24353fc31 100644 --- a/spot/twaalgos/stats.hh +++ b/spot/twaalgos/stats.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2008, 2011-2017, 2020 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// Copyright (C) 2008, 2011-2017, 2020, 2022 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. @@ -55,6 +55,9 @@ namespace spot /// \brief Compute sub statistics for an automaton. SPOT_API twa_sub_statistics sub_stats_reachable(const const_twa_ptr& g); + /// \brief Count all transtitions, even unreachable ones. + SPOT_API unsigned long long + count_all_transitions(const const_twa_graph_ptr& g); class SPOT_API printable_formula: public printable_value { @@ -102,6 +105,36 @@ namespace spot void print(std::ostream& os, const char* pos) const override; }; + class SPOT_API printable_size final: + public spot::printable + { + unsigned reachable_ = 0; + unsigned all_ = 0; + public: + void set(unsigned reachable, unsigned all) + { + reachable_ = reachable; + all_ = all; + } + + void print(std::ostream& os, const char* pos) const override; + }; + + class SPOT_API printable_long_size final: + public spot::printable + { + unsigned long long reachable_ = 0; + unsigned long long all_ = 0; + public: + void set(unsigned long long reachable, unsigned long long all) + { + reachable_ = reachable; + all_ = all; + } + + void print(std::ostream& os, const char* pos) const override; + }; + /// \brief prints various statistics about a TGBA /// /// This object can be configured to display various statistics @@ -123,9 +156,9 @@ namespace spot const char* format_; printable_formula form_; - printable_value states_; - printable_value edges_; - printable_value trans_; + printable_size states_; + printable_size edges_; + printable_long_size trans_; printable_value acc_; printable_scc_info scc_; printable_value nondetstates_; diff --git a/tests/core/format.test b/tests/core/format.test index 4e6f4a4d5..da78e3e7e 100644 --- a/tests/core/format.test +++ b/tests/core/format.test @@ -1,7 +1,7 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2016, 2017 Laboratoire de Recherche et Développement de -# l'Epita (LRDE). +# Copyright (C) 2016, 2017, 2022 Laboratoire de Recherche et +# Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. # @@ -139,18 +139,36 @@ test 3,5 = `ltl2tgba --low --any --stats=%s,%e "$f"` test 3,4 = `ltl2tgba --stats=%s,%e "$f"` cat >foo < stats + +cat >expected <err && exit 1 +grep 'only \[a\], \[r\], or \[u\] is supported' err