From 36f995651ec475b1015823c519e4a7cf50640210 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sun, 28 Dec 2014 12:01:18 +0100 Subject: [PATCH] autfilt: move output functions to a separate file * src/bin/common_aoutput.cc, src/bin/common_aoutput.hh: New files... * src/bin/autfilt.cc: ... extracted from here. * src/bin/Makefile.am: Add them. --- src/bin/Makefile.am | 2 + src/bin/autfilt.cc | 200 +++----------------------------------- src/bin/common_aoutput.cc | 85 ++++++++++++++++ src/bin/common_aoutput.hh | 196 +++++++++++++++++++++++++++++++++++++ 4 files changed, 299 insertions(+), 184 deletions(-) create mode 100644 src/bin/common_aoutput.cc create mode 100644 src/bin/common_aoutput.hh diff --git a/src/bin/Makefile.am b/src/bin/Makefile.am index 597bb871f..7fc7078ac 100644 --- a/src/bin/Makefile.am +++ b/src/bin/Makefile.am @@ -26,6 +26,8 @@ LDADD = libcommon.a $(top_builddir)/lib/libgnu.la ../libspot.la noinst_LIBRARIES = libcommon.a libcommon_a_SOURCES = \ + common_aoutput.cc \ + common_aoutput.hh \ common_cout.hh \ common_cout.cc \ common_finput.cc \ diff --git a/src/bin/autfilt.cc b/src/bin/autfilt.cc index dda420834..b8b26f7f0 100644 --- a/src/bin/autfilt.cc +++ b/src/bin/autfilt.cc @@ -31,16 +31,11 @@ #include "common_setup.hh" #include "common_finput.hh" #include "common_cout.hh" +#include "common_aoutput.hh" #include "common_range.hh" #include "common_post.hh" -#include "tgbaalgos/dotty.hh" -#include "tgbaalgos/lbtt.hh" -#include "tgbaalgos/hoa.hh" -#include "tgbaalgos/neverclaim.hh" #include "tgbaalgos/product.hh" -#include "tgbaalgos/save.hh" -#include "tgbaalgos/stats.hh" #include "tgbaalgos/isdet.hh" #include "tgbaalgos/stutterize.hh" #include "tgbaalgos/closure.hh" @@ -49,11 +44,7 @@ #include "misc/timer.hh" #include "misc/random.hh" #include "hoaparse/public.hh" -#include "tgbaalgos/sccinfo.hh" #include "tgbaalgos/randomize.hh" -#include "tgbaalgos/gtec/gtec.hh" -#include "tgbaalgos/reducerun.hh" -#include "tgbaalgos/word.hh" #include "tgbaalgos/are_isomorphic.hh" #include "tgbaalgos/canonicalize.hh" @@ -207,14 +198,10 @@ static const struct argp_child children[] = { 0, 0, 0, 0 } }; -static enum output_format { Dot, Lbtt, Lbtt_t, Spin, Spot, Stats, Hoa, - Quiet, Count } format = Dot; -const char* opt_dot = nullptr; typedef spot::tgba_digraph::graph_t::trans_storage_t tr_t; typedef std::set> unique_aut_t; static long int match_count = 0; static const char* stats = ""; -static const char* hoa_opt = 0; static spot::option_map extra_options; static bool randomize_st = false; static bool randomize_tr = false; @@ -231,7 +218,6 @@ static bool opt_invert = false; static range opt_states = { 0, std::numeric_limits::max() }; static range opt_edges = { 0, std::numeric_limits::max() }; static range opt_accsets = { 0, std::numeric_limits::max() }; -static const char* opt_name = nullptr; static int opt_max_count = -1; static bool opt_destut = false; static bool opt_instut = false; @@ -270,13 +256,13 @@ parse_opt(int key, char* arg, struct argp_state*) type = spot::postprocessor::BA; break; case 'c': - format = Count; + automaton_format = Count; break; case 'F': jobs.emplace_back(arg, true); break; case 'H': - format = Hoa; + automaton_format = Hoa; hoa_opt = arg; break; case 'M': @@ -286,10 +272,10 @@ parse_opt(int key, char* arg, struct argp_state*) opt_max_count = to_pos_int(arg); break; case 'q': - format = Quiet; + automaton_format = Quiet; break; case 's': - format = Spin; + automaton_format = Spin; if (type != spot::postprocessor::Monitor) type = spot::postprocessor::BA; break; @@ -317,7 +303,7 @@ parse_opt(int key, char* arg, struct argp_state*) break; } case OPT_DOT: - format = Dot; + automaton_format = Dot; opt_dot = arg; break; case OPT_EDGES: @@ -342,13 +328,13 @@ parse_opt(int key, char* arg, struct argp_state*) if (arg) { if (arg[0] == 't' && arg[1] == 0) - format = Lbtt_t; + automaton_format = Lbtt_t; else error(2, 0, "unknown argument for --lbtt: '%s'", arg); } else { - format = Lbtt; + automaton_format = Lbtt; } break; case OPT_NAME: @@ -399,7 +385,7 @@ parse_opt(int key, char* arg, struct argp_state*) opt_seed = to_int(arg); break; case OPT_SPOT: - format = Spot; + automaton_format = Spot; break; case OPT_STATES: opt_states = parse_range(arg, 0, std::numeric_limits::max()); @@ -408,10 +394,10 @@ parse_opt(int key, char* arg, struct argp_state*) if (!*arg) error(2, 0, "empty format string for --stats"); stats = arg; - format = Stats; + automaton_format = Stats; break; case OPT_TGBA: - if (format == Spin) + if (automaton_format == Spin) error(2, 0, "--spin and --tgba are incompatible"); type = spot::postprocessor::TGBA; break; @@ -432,129 +418,15 @@ parse_opt(int key, char* arg, struct argp_state*) namespace { - /// \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 hoa_stat_printer: protected spot::stat_printer - { - public: - hoa_stat_printer(std::ostream& os, const char* format) - : spot::stat_printer(os, format) - { - declare('A', &haut_acc_); - declare('C', &haut_scc_); - declare('E', &haut_edges_); - declare('F', &filename_); - declare('f', &filename_); // Override the formula printer. - declare('L', &haut_loc_); - declare('M', &haut_name_); - declare('m', &aut_name_); - declare('S', &haut_states_); - declare('T', &haut_trans_); - declare('w', &aut_word_); - } - - /// \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 spot::const_hoa_aut_ptr& haut, - const spot::const_tgba_digraph_ptr& aut, - const char* filename, double run_time) - { - filename_ = filename; - haut_loc_ = haut->loc; - - if (has('T')) - { - spot::tgba_sub_statistics s = sub_stats_reachable(haut->aut); - haut_states_ = s.states; - haut_edges_ = s.transitions; - haut_trans_ = s.sub_transitions; - } - else if (has('E')) - { - spot::tgba_sub_statistics s = sub_stats_reachable(haut->aut); - haut_states_ = s.states; - haut_edges_ = s.transitions; - } - if (has('M')) - { - auto n = haut->aut->get_named_prop("automaton-name"); - if (n) - haut_name_ = *n; - else - haut_name_.val().clear(); - } - if (has('m')) - { - auto n = aut->get_named_prop("automaton-name"); - if (n) - aut_name_ = *n; - else - aut_name_.val().clear(); - } - if (has('S')) - { - haut_states_ = haut->aut->num_states(); - } - - if (has('A')) - haut_acc_ = haut->aut->acc().num_sets(); - - if (has('C')) - haut_scc_ = spot::scc_info(haut->aut).scc_count(); - - if (has('w')) - { - auto res = spot::couvreur99(aut)->check(); - if (res) - { - auto run = res->accepting_run(); - assert(run); - run = reduce_run(aut, run); - spot::tgba_word w(run); - w.simplify(); - std::ostringstream out; - w.print(out, aut->get_dict()); - aut_word_ = out.str(); - } - else - { - aut_word_.val().clear(); - } - } - - return this->spot::stat_printer::print(aut, 0, run_time); - } - - private: - spot::printable_value filename_; - spot::printable_value haut_name_; - spot::printable_value aut_name_; - spot::printable_value aut_word_; - spot::printable_value haut_states_; - spot::printable_value haut_edges_; - spot::printable_value haut_trans_; - spot::printable_value haut_acc_; - spot::printable_value haut_scc_; - spot::printable_value haut_loc_; - }; - class hoa_processor: public job_processor { private: spot::postprocessor& post; - hoa_stat_printer statistics; - std::ostringstream name; - hoa_stat_printer namer; + automaton_printer printer; public: hoa_processor(spot::postprocessor& post) - : post(post), statistics(std::cout, stats), namer(name, opt_name) + : post(post), printer(stats) { } @@ -574,7 +446,7 @@ namespace // If --stats or --name is used, duplicate the automaton so we // never modify the original automaton (e.g. with // merge_transitions()) and the statistics about it make sense. - auto aut = ((format == Stats) || opt_name) + auto aut = ((automaton_format == Stats) || opt_name) ? spot::make_tgba_digraph(haut->aut, spot::tgba::prop_set::all()) : haut->aut; @@ -630,47 +502,7 @@ namespace const double conversion_time = sw.stop(); - // Name the output automaton. - if (opt_name) - { - name.str(""); - namer.print(haut, aut, filename, conversion_time); - aut->set_named_prop("automaton-name", new std::string(name.str())); - } - - // Output it. - switch (format) - { - case Count: - case Quiet: - // Do not output anything. - break; - case Dot: - spot::dotty_reachable(std::cout, aut, - (type == spot::postprocessor::BA) - || (type == spot::postprocessor::Monitor), - opt_dot); - break; - case Lbtt: - spot::lbtt_reachable(std::cout, aut, type == spot::postprocessor::BA); - break; - case Lbtt_t: - spot::lbtt_reachable(std::cout, aut, false); - break; - case Hoa: - spot::hoa_reachable(std::cout, aut, hoa_opt) << '\n'; - break; - case Spot: - spot::tgba_save_reachable(std::cout, aut); - break; - case Spin: - spot::never_claim_reachable(std::cout, aut); - break; - case Stats: - statistics.print(haut, aut, filename, conversion_time) << '\n'; - break; - } - flush_cout(); + printer.print(aut, filename, conversion_time, haut); if (opt_max_count >= 0 && match_count >= opt_max_count) abort_run = true; @@ -758,7 +590,7 @@ main(int argc, char** argv) error(2, 0, "%s", e.what()); } - if (format == Count) + if (automaton_format == Count) std::cout << match_count << std::endl; return !match_count; } diff --git a/src/bin/common_aoutput.cc b/src/bin/common_aoutput.cc new file mode 100644 index 000000000..7313a2083 --- /dev/null +++ b/src/bin/common_aoutput.cc @@ -0,0 +1,85 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2012, 2013, 2014 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 3 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 this program. If not, see . + + +#include "common_aoutput.hh" +#include "common_post.hh" +#include "common_cout.hh" + +#include "tgbaalgos/dotty.hh" +#include "tgbaalgos/lbtt.hh" +#include "tgbaalgos/hoa.hh" +#include "tgbaalgos/neverclaim.hh" +#include "tgbaalgos/save.hh" + +automaton_format_t automaton_format = Dot; +const char* opt_dot = nullptr; +const char* hoa_opt = nullptr; +const char* opt_name = nullptr; + +void +automaton_printer::print(const spot::tgba_digraph_ptr& aut, + // Input location for errors and statistics. + const char* filename, + // Time and input automaton for statistics + double time, + const spot::const_hoa_aut_ptr& haut) +{ + // Name the output automaton. + if (opt_name) + { + name.str(""); + namer.print(haut, aut, filename, time); + aut->set_named_prop("automaton-name", new std::string(name.str())); + } + + // Output it. + switch (automaton_format) + { + case Count: + case Quiet: + // Do not output anything. + break; + case Dot: + spot::dotty_reachable(std::cout, aut, + (type == spot::postprocessor::BA) + || (type == spot::postprocessor::Monitor), + opt_dot); + break; + case Lbtt: + spot::lbtt_reachable(std::cout, aut, type == spot::postprocessor::BA); + break; + case Lbtt_t: + spot::lbtt_reachable(std::cout, aut, false); + break; + case Hoa: + spot::hoa_reachable(std::cout, aut, hoa_opt) << '\n'; + break; + case Spot: + spot::tgba_save_reachable(std::cout, aut); + break; + case Spin: + spot::never_claim_reachable(std::cout, aut); + break; + case Stats: + statistics.print(haut, aut, filename, time) << '\n'; + break; + } + flush_cout(); +} diff --git a/src/bin/common_aoutput.hh b/src/bin/common_aoutput.hh new file mode 100644 index 000000000..380fb004a --- /dev/null +++ b/src/bin/common_aoutput.hh @@ -0,0 +1,196 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2014 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 3 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 this program. If not, see . + +#ifndef SPOT_BIN_COMMON_AOUTPUT_HH +#define SPOT_BIN_COMMON_AOUTPUT_HH + +#include "common_sys.hh" + +#include + +#include "hoaparse/public.hh" + +#include "tgbaalgos/stats.hh" +#include "tgbaalgos/sccinfo.hh" +#include "tgbaalgos/gtec/gtec.hh" +#include "tgbaalgos/reducerun.hh" +#include "tgbaalgos/word.hh" +#include "tgbaalgos/isdet.hh" + + +// Format for automaton output +enum automaton_format_t { + Dot, + Lbtt, + Lbtt_t, + Spin, + Spot, + Stats, + Hoa, + Quiet, + Count, +}; + +// The format to use in output_automaton() +extern automaton_format_t automaton_format; +// Any option to pass to Dot +extern const char* opt_dot; +// Options to pass to the HOA printer +extern const char* hoa_opt; +// How to name the automaton +extern const char* opt_name; + +/// \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 hoa_stat_printer: protected spot::stat_printer +{ +public: + hoa_stat_printer(std::ostream& os, const char* format) + : spot::stat_printer(os, format) + { + declare('A', &haut_acc_); + declare('C', &haut_scc_); + declare('E', &haut_edges_); + declare('F', &filename_); + declare('f', &filename_); // Override the formula printer. + declare('L', &haut_loc_); + declare('M', &haut_name_); + declare('m', &aut_name_); + declare('S', &haut_states_); + declare('T', &haut_trans_); + declare('w', &aut_word_); + } + + /// \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 spot::const_hoa_aut_ptr& haut, + const spot::const_tgba_digraph_ptr& aut, + const char* filename, double run_time) + { + filename_ = filename; + haut_loc_ = haut->loc; + + if (has('T')) + { + spot::tgba_sub_statistics s = sub_stats_reachable(haut->aut); + haut_states_ = s.states; + haut_edges_ = s.transitions; + haut_trans_ = s.sub_transitions; + } + else if (has('E')) + { + spot::tgba_sub_statistics s = sub_stats_reachable(haut->aut); + haut_states_ = s.states; + haut_edges_ = s.transitions; + } + if (has('M')) + { + auto n = haut->aut->get_named_prop("automaton-name"); + if (n) + haut_name_ = *n; + else + haut_name_.val().clear(); + } + if (has('m')) + { + auto n = aut->get_named_prop("automaton-name"); + if (n) + aut_name_ = *n; + else + aut_name_.val().clear(); + } + if (has('S')) + { + haut_states_ = haut->aut->num_states(); + } + + if (has('A')) + haut_acc_ = haut->aut->acc().num_sets(); + + if (has('C')) + haut_scc_ = spot::scc_info(haut->aut).scc_count(); + + if (has('w')) + { + auto res = spot::couvreur99(aut)->check(); + if (res) + { + auto run = res->accepting_run(); + assert(run); + run = reduce_run(aut, run); + spot::tgba_word w(run); + w.simplify(); + std::ostringstream out; + w.print(out, aut->get_dict()); + aut_word_ = out.str(); + } + else + { + aut_word_.val().clear(); + } + } + + return this->spot::stat_printer::print(aut, 0, run_time); + } + +private: + spot::printable_value filename_; + spot::printable_value haut_name_; + spot::printable_value aut_name_; + spot::printable_value aut_word_; + spot::printable_value haut_states_; + spot::printable_value haut_edges_; + spot::printable_value haut_trans_; + spot::printable_value haut_acc_; + spot::printable_value haut_scc_; + spot::printable_value haut_loc_; +}; + + +class automaton_printer +{ + hoa_stat_printer statistics; + std::ostringstream name; + hoa_stat_printer namer; + +public: + + automaton_printer(const char* stats) + : statistics(std::cout, stats), namer(name, opt_name) + { + } + + void + print(const spot::tgba_digraph_ptr& aut, + // Input location for errors and statistics. + const char* filename = nullptr, + // Time and input automaton for statistics + double time = 0.0, + const spot::const_hoa_aut_ptr& haut = nullptr); +}; + + + +#endif // SPOT_BIN_COMMON_AOUTPUT_HH