From a303c8603c00f9dafb3b0001f5905738f517f4e7 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 4 Oct 2012 09:05:23 +0200 Subject: [PATCH] Factor the %-formating machinery. * src/misc/formater.hh: New file. * src/misc/Makefile.am: Add it. * src/tgbaalgos/stats.cc, src/tgbaalgos/stats.hh: Use it. --- src/misc/Makefile.am | 3 +- src/misc/formater.hh | 195 +++++++++++++++++++++++++++++++++++++++++ src/tgbaalgos/stats.cc | 149 +++++++------------------------ src/tgbaalgos/stats.hh | 29 +++++- 4 files changed, 256 insertions(+), 120 deletions(-) create mode 100644 src/misc/formater.hh diff --git a/src/misc/Makefile.am b/src/misc/Makefile.am index a287212ec..15a1d8b0b 100644 --- a/src/misc/Makefile.am +++ b/src/misc/Makefile.am @@ -1,4 +1,4 @@ -## Copyright (C) 2011 Laboratoire de Recherche et Développement +## Copyright (C) 2011, 2012 Laboratoire de Recherche et Développement ## de l'Epita (LRDE). ## Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de ## Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), @@ -37,6 +37,7 @@ misc_HEADERS = \ casts.hh \ escape.hh \ fixpool.hh \ + formater.hh \ freelist.hh \ hash.hh \ hashfunc.hh \ diff --git a/src/misc/formater.hh b/src/misc/formater.hh new file mode 100644 index 000000000..cd121d631 --- /dev/null +++ b/src/misc/formater.hh @@ -0,0 +1,195 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2012 Laboratoire de Recherche et Développement de +// l'Epita (LRDE). +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + +#ifndef SPOT_SRC_MISC_FORMATER_HH +#define SPOT_SRC_MISC_FORMATER_HH + +#include +#include +#include + +namespace spot +{ + class printable + { + public: + ~printable() + { + } + virtual void + print(std::ostream&, const char*) const = 0; + }; + + + template + class printable_value: public printable + { + protected: + T val_; + public: + operator T() const + { + return val_; + } + + printable_value& + operator=(const T& new_val) + { + val_ = new_val; + return *this; + } + + virtual void + print(std::ostream& os, const char*) const + { + os << val_; + } + }; + + /// The default callback simply writes "%c". + class printable_id: public printable + { + public: + virtual void + print(std::ostream& os, const char* x) const + { + os << '%' << *x; + } + }; + + /// Called by default for "%%" and "%\0". + class printable_percent: public printable + { + public: + virtual void + print(std::ostream& os, const char*) const + { + os << '%'; + } + }; + + + class formater + { + printable_id id; + printable_percent percent; + public: + + formater() + : has_(256), call_(256, &id) + { + call_['%'] = call_[0] = &percent; + } + + /// Collect the %-sequences occurring in \a fmt. + void + prime(const char* fmt) + { + for (const char* pos = fmt; *pos; ++pos) + if (*pos == '%') + { + char c = *++pos; + has_[c] = true; + if (!c) + break; + } + } + + /// Collect the %-sequences occurring in \a fmt. + void + prime(const std::string& fmt) + { + prime(fmt.c_str()); + } + + /// Whether %c occurred in the primed formats. + bool + has(char c) const + { + return has_[c]; + } + + /// Declare a callback function for %c. + void + declare(char c, const printable* f) + { + call_[c] = f; + } + + /// Remember where to output any string. + void + set_output(std::ostream& output) + { + output_ = &output; + } + + /// Expand the %-sequences in \a fmt, write the result on \a output_. + std::ostream& + format(const char* fmt) + { + for (const char* pos = fmt; *pos; ++pos) + if (*pos != '%') + { + *output_ << *pos; + } + else + { + char c = *++pos; + call_[c]->print(*output_, pos); + if (!c) + break; + } + return *output_; + } + + /// Expand the %-sequences in \a fmt, write the result on \a output. + std::ostream& + format(std::ostream& output, const char* fmt) + { + set_output(output); + return format(fmt); + } + + /// Expand the %-sequences in \a fmt, write the result on \a output_. + std::ostream& + format(const std::string& fmt) + { + return format(fmt.c_str()); + } + + /// Expand the %-sequences in \a fmt, write the result on \a output. + std::ostream& + format(std::ostream& output, const std::string& fmt) + { + return format(output, fmt.c_str()); + } + + private: + std::vector has_; + std::vector call_; + protected: + std::ostream* output_; + const char* pos_; + }; + +} + +#endif // SPOT_SRC_MISC_FORMATER_HH diff --git a/src/tgbaalgos/stats.cc b/src/tgbaalgos/stats.cc index a5f43fcee..55d1e56a5 100644 --- a/src/tgbaalgos/stats.cc +++ b/src/tgbaalgos/stats.cc @@ -133,151 +133,68 @@ namespace spot return s; } - namespace + void printable_formula::print(std::ostream& os, const char*) const { - 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 - }; - } + ltl::to_string(val_, os); + }; stat_printer::stat_printer(std::ostream& os, const char* format) - : os_(os), format_(format) + : 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; - } - } + declare('a', &acc_); + declare('d', &deterministic_); + declare('e', &edges_); + declare('f', &form_); + declare('n', &nondetstates_); + declare('s', &states_); + declare('S', &scc_); + declare('t', &trans_); + set_output(os); + prime(format); } 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; + form_ = f; - if (needed_ & Trans) + if (has('t')) { tgba_sub_statistics s = sub_stats_reachable(aut); - states = s.states; - edges = s.transitions; - trans = s.sub_transitions; + states_ = s.states; + edges_ = s.transitions; + trans_ = s.sub_transitions; } - else if (needed_ & (States | Edges)) + else if (has('s') || has('e')) { tgba_sub_statistics s = sub_stats_reachable(aut); - states = s.states; - edges = s.transitions; + states_ = s.states; + edges_ = s.transitions; } - if (needed_ & Acc) - acc = aut->number_of_acceptance_conditions(); - if (needed_ & Scc) + if (has('a')) + acc_ = aut->number_of_acceptance_conditions(); + + if (has('S')) { scc_map m(aut); m.build_map(); - scc = m.scc_count(); + scc_ = m.scc_count(); } - if (needed_ & Nondetstates) + if (has('n')) { - nondetstates = count_nondet_states(aut); - deterministic = (nondetstates == 0); + nondetstates_ = count_nondet_states(aut); + deterministic_ = (nondetstates_ == 0); } - else if (needed_ & Deterministic) + else if (has('d')) { // This is more efficient than calling count_nondet_state(). - deterministic = is_deterministic(aut); + 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_; + return format(format_); } } diff --git a/src/tgbaalgos/stats.hh b/src/tgbaalgos/stats.hh index 654c05a9b..1882d67d4 100644 --- a/src/tgbaalgos/stats.hh +++ b/src/tgbaalgos/stats.hh @@ -24,6 +24,7 @@ #include "tgba/tgba.hh" #include +#include "misc/formater.hh" namespace spot { @@ -53,12 +54,27 @@ namespace spot /// \brief Compute subended statistics for an automaton. tgba_sub_statistics sub_stats_reachable(const tgba* g); + + class printable_formula: public printable_value + { + public: + printable_formula& + operator=(const ltl::formula* new_val) + { + val_ = new_val; + return *this; + } + + virtual void + print(std::ostream& os, const char*) const; + }; + /// \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 + class stat_printer: protected formater { public: stat_printer(std::ostream& os, const char* format); @@ -71,9 +87,16 @@ namespace spot print(const tgba* aut, const ltl::formula* f = 0); private: - std::ostream& os_; const char* format_; - unsigned needed_; + + printable_formula form_; + printable_value states_; + printable_value edges_; + printable_value trans_; + printable_value acc_; + printable_value scc_; + printable_value nondetstates_; + printable_value deterministic_; }; /// @}