From 26ad32d5614962b1c988e5c03ee61a61bddd260e Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 19 Sep 2012 00:28:23 +0200 Subject: [PATCH] ltl2tgba: Add a --stats option. * src/bin/ltl2tgba.cc (--stats): New option. * src/tgbaalgos/stats.cc, src/tgbaalgos/stats.hh (stat_printer): New class. --- src/bin/ltl2tgba.cc | 40 +++++++++-- src/tgbaalgos/stats.cc | 153 ++++++++++++++++++++++++++++++++++++++++- src/tgbaalgos/stats.hh | 27 +++++++- 3 files changed, 212 insertions(+), 8 deletions(-) diff --git a/src/bin/ltl2tgba.cc b/src/bin/ltl2tgba.cc index 2adf7bc68..9c884aaf5 100644 --- a/src/bin/ltl2tgba.cc +++ b/src/bin/ltl2tgba.cc @@ -43,6 +43,7 @@ #include "tgbaalgos/neverclaim.hh" #include "tgbaalgos/postproc.hh" #include "tgbaalgos/save.hh" +#include "tgbaalgos/stats.hh" #include "tgba/bddprint.hh" const char* argp_program_version = "\ @@ -70,6 +71,7 @@ If multiple formulas are supplied, several automata will be output."; #define OPT_DOT 6 #define OPT_LBTT 7 #define OPT_SPOT 8 +#define OPT_STATS 9 static const argp_option options[] = { @@ -85,14 +87,31 @@ static const argp_option options[] = { "spin", 's', 0, 0, "Spin neverclaim (implies --ba)", 0 }, { "spot", OPT_SPOT, 0, 0, "SPOT's format", 0 }, { "utf8", '8', 0, 0, "enable UTF-8 characters in output " - "(works only with --spot or --dot)", 0 }, + "(ignored with --lbtt or --spin)", 0 }, + { "stats", OPT_STATS, "FORMAT", 0, + "output statistics about the automaton", 0 }, /**************************************************/ - { 0, 0, 0, 0, "Translation intent:", 4 }, + { 0, 0, 0, 0, "The FORMAT string passed to --stats may use "\ + "the following interpreted sequences:", 4 }, + { "%s", 0, 0, OPTION_DOC | OPTION_NO_USAGE, "number of states", 0 }, + { "%e", 0, 0, OPTION_DOC | OPTION_NO_USAGE, "number of edges", 0 }, + { "%t", 0, 0, OPTION_DOC | OPTION_NO_USAGE, "number of transitions", 0 }, + { "%a", 0, 0, OPTION_DOC | OPTION_NO_USAGE, + "number of acceptance sets", 0 }, + { "%S", 0, 0, OPTION_DOC | OPTION_NO_USAGE, "number of SCCs", 0 }, + { "%n", 0, 0, OPTION_DOC | OPTION_NO_USAGE, + "number of nondeterministic states", 0 }, + { "%d", 0, 0, OPTION_DOC | OPTION_NO_USAGE, + "1 if the automaton is deterministic, 0 otherwise", 0 }, + { "%%", 0, 0, OPTION_DOC | OPTION_NO_USAGE, + "a single %", 0 }, + /**************************************************/ + { 0, 0, 0, 0, "Translation intent:", 5 }, { "small", OPT_SMALL, 0, 0, "prefer small automata (default)", 0 }, { "deterministic", 'D', 0, 0, "prefer deterministic automata", 0 }, { "any", 'a', 0, 0, "no preference", 0 }, /**************************************************/ - { 0, 0, 0, 0, "Optimization level:", 5 }, + { 0, 0, 0, 0, "Optimization level:", 6 }, { "low", OPT_LOW, 0, 0, "minimal optimizations (fast)", 0 }, { "medium", OPT_MEDIUM, 0, 0, "moderate optimizations", 0 }, { "high", OPT_HIGH, 0, 0, @@ -111,8 +130,9 @@ const struct argp_child children[] = spot::postprocessor::output_type type = spot::postprocessor::TGBA; spot::postprocessor::output_pref pref = spot::postprocessor::Small; spot::postprocessor::optimization_level level = spot::postprocessor::High; -enum output_format { Dot, Lbtt, Spin, Spot } format = Dot; +enum output_format { Dot, Lbtt, Spin, Spot, Stats } format = Dot; bool utf8 = false; +const char* stats = 0; static int parse_opt(int key, char* arg, struct argp_state*) @@ -166,6 +186,12 @@ parse_opt(int key, char* arg, struct argp_state*) case OPT_SPOT: format = Spot; break; + case OPT_STATS: + if (!*arg) + error(2, 0, "empty format string for --stats"); + stats = arg; + format = Stats; + break; case OPT_TGBA: if (format == Spin) error(2, 0, "--spin and --tgba are incompatible"); @@ -190,10 +216,11 @@ namespace public: spot::ltl::ltl_simplifier& simpl; spot::postprocessor& post; + spot::stat_printer statistics; trans_processor(spot::ltl::ltl_simplifier& simpl, spot::postprocessor& post) - : simpl(simpl), post(post) + : simpl(simpl), post(post), statistics(std::cout, stats) { } @@ -252,6 +279,9 @@ namespace case Spin: spot::never_claim_reachable(std::cout, aut, f); break; + case Stats: + statistics.print(aut, f) << "\n"; + break; } delete aut; flush_cout(); diff --git a/src/tgbaalgos/stats.cc b/src/tgbaalgos/stats.cc index 5ac85f884..535b7c5cb 100644 --- a/src/tgbaalgos/stats.cc +++ b/src/tgbaalgos/stats.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2008, 2011 Laboratoire de Recherche et Développement +// Copyright (C) 2008, 2011, 2012 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 @@ -25,6 +25,9 @@ #include "tgba/tgba.hh" #include "stats.hh" #include "reachiter.hh" +#include "ltlvisit/tostring.hh" +#include "tgbaalgos/isdet.hh" +#include "tgbaalgos/scc.hh" namespace spot { @@ -131,4 +134,152 @@ namespace spot d.run(); return s; } + + namespace + { + enum what { + Formula = 1, // %f + States = 2, // %s + Edges = 4, // %e + Trans = 8, // %t + Acc = 16, // %a + Scc = 32, // %S + Nondetstates = 64, // %n + Deterministic = 128 // %d + }; + } + + stat_printer::stat_printer(std::ostream& os, const char* format) + : os_(os), format_(format) + { + needed_ = 0; + // scan the format for needed statistics + for (const char* pos = format; *pos; ++pos) + if (*pos == '%') + { + switch (*++pos) + { + case 'f': + needed_ |= Formula; + break; + case 's': + needed_ |= States; + break; + case 'e': + needed_ |= Edges; + break; + case 't': + needed_ |= Trans; + break; + case 'a': + needed_ |= Acc; + break; + case 'S': + needed_ |= Scc; + break; + case 'n': + needed_ |= Nondetstates; + break; + case 'd': + needed_ |= Deterministic; + break; + case '%': + break; + case 0: + --pos; + break; + } + } + } + + std::ostream& + stat_printer::print(const tgba* aut, + const ltl::formula* f) + { + unsigned states = 0; + unsigned edges = 0; + unsigned trans = 0; + unsigned acc = 0; + unsigned scc = 0; + unsigned nondetstates = 0; + unsigned deterministic = 0; + + if (needed_ & Trans) + { + tgba_sub_statistics s = sub_stats_reachable(aut); + states = s.states; + edges = s.transitions; + trans = s.sub_transitions; + } + else if (needed_ & (States | Edges)) + { + tgba_sub_statistics s = sub_stats_reachable(aut); + states = s.states; + edges = s.transitions; + } + if (needed_ & Acc) + acc = aut->number_of_acceptance_conditions(); + + if (needed_ & Scc) + { + scc_map m(aut); + m.build_map(); + scc = m.scc_count(); + } + + if (needed_ & Nondetstates) + { + nondetstates = count_nondet_states(aut); + deterministic = (nondetstates == 0); + } + else if (needed_ & Deterministic) + { + // This is more efficient than calling count_nondet_state(). + deterministic = is_deterministic(aut); + } + + for (const char* format = format_; *format; ++format) + if (*format != '%') + os_ << *format; + else + switch (*++format) + { + case 'a': + os_ << acc; + break; + case 'e': + os_ << edges; + break; + case 'f': + assert(f); + ltl::to_string(f, os_); + break; + case 'd': + os_ << deterministic; + break; + case 'n': + os_ << nondetstates; + break; + case 's': + os_ << states; + break; + case 'S': + os_ << scc; + break; + case 't': + os_ << trans; + break; + case 0: + --format; + // fall through + case '%': + os_ << '%'; + break; + default: + os_ << '%' << *format; + break; + } + return os_; + } + } diff --git a/src/tgbaalgos/stats.hh b/src/tgbaalgos/stats.hh index dc2b0d6e2..b7b3c2a8e 100644 --- a/src/tgbaalgos/stats.hh +++ b/src/tgbaalgos/stats.hh @@ -1,5 +1,5 @@ -// Copyright (C) 2008, 2011 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// Copyright (C) 2008, 2011, 2012 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,29 @@ namespace spot /// \brief Compute subended statistics for an automaton. tgba_sub_statistics sub_stats_reachable(const tgba* g); + /// \brief prints various statistics about a TGBA + /// + /// This object can be configured to display various statistics + /// about a TGBA. Some %-sequence of characters are interpreted in + /// the format string, and replaced by the corresponding statistics. + class stat_printer + { + public: + stat_printer(std::ostream& os, const char* format); + + /// \brief print the configured statistics. + /// + /// The \a f argument is not needed if the Formula does not need + /// to be output. + std::ostream& + print(const tgba* aut, const ltl::formula* f = 0); + + private: + std::ostream& os_; + const char* format_; + unsigned needed_; + }; + /// @} }