From 5aff262844986b5b8e5511505eb265fd19b42309 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 19 Nov 2014 17:46:44 +0100 Subject: [PATCH] autfilt: first stub * src/bin/autfilt.cc, src/bin/man/autfilt.x: New files. * src/bin/Makefile.am, src/bin/man/Makefile.am: Add them. * src/bin/common_post.cc, src/bin/common_post.hh: Adjust. --- src/bin/Makefile.am | 9 +- src/bin/autfilt.cc | 369 ++++++++++++++++++++++++++++++++++++++++ src/bin/common_post.cc | 28 ++- src/bin/common_post.hh | 9 +- src/bin/man/Makefile.am | 6 +- src/bin/man/autfilt.x | 6 + 6 files changed, 415 insertions(+), 12 deletions(-) create mode 100644 src/bin/autfilt.cc create mode 100644 src/bin/man/autfilt.x diff --git a/src/bin/Makefile.am b/src/bin/Makefile.am index 616cc0256..eea317fbd 100644 --- a/src/bin/Makefile.am +++ b/src/bin/Makefile.am @@ -1,6 +1,6 @@ ## -*- coding: utf-8 -*- -## Copyright (C) 2012, 2013 Laboratoire de Recherche et Développement -## de l'Epita (LRDE). +## 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. ## @@ -42,14 +42,15 @@ libcommon_a_SOURCES = \ common_setup.hh \ common_sys.hh -bin_PROGRAMS = ltlfilt genltl randltl ltl2tgba ltl2tgta ltlcross \ - dstar2tgba ltlgrind +bin_PROGRAMS = autfilt ltlfilt genltl randltl ltl2tgba ltl2tgta \ + ltlcross dstar2tgba ltlgrind # Dummy program used just to generate man/spot-x.7 in a way that is # consistent with the other man pages (e.g., with a version number that # is automatically updated). noinst_PROGRAMS = spot-x +autfilt_SOURCES = autfilt.cc ltlfilt_SOURCES = ltlfilt.cc genltl_SOURCES = genltl.cc randltl_SOURCES = randltl.cc diff --git a/src/bin/autfilt.cc b/src/bin/autfilt.cc new file mode 100644 index 000000000..852a09dd8 --- /dev/null +++ b/src/bin/autfilt.cc @@ -0,0 +1,369 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 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_sys.hh" + +#include +#include + +#include +#include "error.h" + +#include "common_setup.hh" +#include "common_finput.hh" +#include "common_cout.hh" +#include "common_post.hh" + +#include "tgbaalgos/dotty.hh" +#include "tgbaalgos/lbtt.hh" +#include "tgbaalgos/hoaf.hh" +#include "tgbaalgos/neverclaim.hh" +#include "tgbaalgos/save.hh" +#include "tgbaalgos/stats.hh" +#include "tgba/bddprint.hh" +#include "misc/optionmap.hh" +#include "misc/timer.hh" +#include "hoaparse/public.hh" +#include "tgbaalgos/sccinfo.hh" + + +const char argp_program_doc[] ="\ +Convert, transform, and filter Büchi automata.\n\ +"; + + +#define OPT_TGBA 1 +#define OPT_DOT 2 +#define OPT_LBTT 3 +#define OPT_SPOT 4 +#define OPT_STATS 5 + +static const argp_option options[] = + { + /**************************************************/ + { 0, 0, 0, 0, "Input:", 1 }, + { "file", 'F', "FILENAME", 0, + "process the automaton in FILENAME", 0 }, + /**************************************************/ + { 0, 0, 0, 0, "Output automaton type:", 2 }, + { "tgba", OPT_TGBA, 0, 0, + "Transition-based Generalized Büchi Automaton (default)", 0 }, + { "ba", 'B', 0, 0, "Büchi Automaton", 0 }, + { "monitor", 'M', 0, 0, "Monitor (accepts all finite prefixes " + "of the given formula)", 0 }, + /**************************************************/ + { 0, 0, 0, 0, "Output format:", 3 }, + { "dot", OPT_DOT, 0, 0, "GraphViz's format (default)", 0 }, + { "hoaf", 'H', "s|t|m|l", OPTION_ARG_OPTIONAL, + "Output the automaton in HOA format. Add letters to select " + "(s) state-based acceptance, (t) transition-based acceptance, " + "(m) mixed acceptance, (l) single-line output", 0 }, + { "lbtt", OPT_LBTT, "t", OPTION_ARG_OPTIONAL, + "LBTT's format (add =t to force transition-based acceptance even" + " on Büchi automata)", 0 }, + { "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 " + "(ignored with --lbtt or --spin)", 0 }, + { "stats", OPT_STATS, "FORMAT", 0, + "output statistics about the automaton", 0 }, + /**************************************************/ + { 0, 0, 0, 0, "The FORMAT string passed to --stats may use "\ + "the following interpreted sequences (capitals for input," + " minuscules for output):", 4 }, + { "%F", 0, 0, OPTION_DOC | OPTION_NO_USAGE, + "name of the input file", 0 }, + { "%S, %s", 0, 0, OPTION_DOC | OPTION_NO_USAGE, + "number of states", 0 }, + { "%E, %e", 0, 0, OPTION_DOC | OPTION_NO_USAGE, + "number of edges", 0 }, + { "%T, %t", 0, 0, OPTION_DOC | OPTION_NO_USAGE, + "number of transitions", 0 }, + { "%A, %a", 0, 0, OPTION_DOC | OPTION_NO_USAGE, + "number of acceptance pairs or sets", 0 }, + { "%C, %c", 0, 0, OPTION_DOC | OPTION_NO_USAGE, + "number of SCCs", 0 }, + { "%n", 0, 0, OPTION_DOC | OPTION_NO_USAGE, + "number of nondeterministic states in output", 0 }, + { "%d", 0, 0, OPTION_DOC | OPTION_NO_USAGE, + "1 if the output is deterministic, 0 otherwise", 0 }, + { "%p", 0, 0, OPTION_DOC | OPTION_NO_USAGE, + "1 if the output is complete, 0 otherwise", 0 }, + { "%r", 0, 0, OPTION_DOC | OPTION_NO_USAGE, + "conversion time (including post-processings, but not parsing)" + " in seconds", 0 }, + { "%%", 0, 0, OPTION_DOC | OPTION_NO_USAGE, + "a single %", 0 }, + /**************************************************/ + { 0, 0, 0, 0, "Miscellaneous options:", -1 }, + { "extra-options", 'x', "OPTS", 0, + "fine-tuning options (see spot-x (7))", 0 }, + { 0, 0, 0, 0, 0, 0 } + }; + +const struct argp_child children[] = + { + { &post_argp_disabled, 0, 0, 20 }, + { &misc_argp, 0, 0, -1 }, + { 0, 0, 0, 0 } + }; + +enum output_format { Dot, Lbtt, Lbtt_t, Spin, Spot, Stats, Hoa } format = Dot; +bool utf8 = false; +const char* stats = ""; +const char* hoaf_opt = 0; +spot::option_map extra_options; + +static int +parse_opt(int key, char* arg, struct argp_state*) +{ + // This switch is alphabetically-ordered. + switch (key) + { + case '8': + spot::enable_utf8(); + break; + case 'B': + type = spot::postprocessor::BA; + break; + case 'F': + jobs.emplace_back(arg, true); + break; + case 'H': + format = Hoa; + hoaf_opt = arg; + break; + case 'M': + type = spot::postprocessor::Monitor; + break; + case 's': + format = Spin; + if (type != spot::postprocessor::Monitor) + type = spot::postprocessor::BA; + break; + case 'x': + { + const char* opt = extra_options.parse_options(arg); + if (opt) + error(2, 0, "failed to parse --options near '%s'", opt); + } + break; + case OPT_DOT: + format = Dot; + break; + case OPT_LBTT: + if (arg) + { + if (arg[0] == 't' && arg[1] == 0) + format = Lbtt_t; + else + error(2, 0, "unknown argument for --lbtt: '%s'", arg); + } + else + { + format = Lbtt; + } + break; + 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"); + type = spot::postprocessor::TGBA; + break; + case ARGP_KEY_ARG: + jobs.emplace_back(arg, true); + break; + + default: + return ARGP_ERR_UNKNOWN; + } + return 0; +} + + +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('S', &haut_states_); + declare('T', &haut_trans_); + } + + /// \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; + + 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; + } + else 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(); + + return this->spot::stat_printer::print(aut, 0, run_time); + } + + private: + spot::printable_value filename_; + 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_; + }; + + + class hoa_processor: public job_processor + { + public: + spot::postprocessor& post; + hoa_stat_printer statistics; + + hoa_processor(spot::postprocessor& post) + : post(post), statistics(std::cout, stats) + { + } + + int + process_formula(const spot::ltl::formula*, const char*, int) + { + SPOT_UNREACHABLE(); + } + + + int + process_file(const char* filename) + { + spot::hoa_parse_error_list pel; + auto haut = spot::hoa_parse(filename, pel, spot::make_bdd_dict()); + if (spot::format_hoa_parse_errors(std::cerr, filename, pel)) + return 2; + if (!haut) + error(2, 0, "failed to read automaton from %s", filename); + + spot::stopwatch sw; + sw.start(); + auto aut = post.run(haut->aut, nullptr); + const double conversion_time = sw.stop(); + + switch (format) + { + case Dot: + spot::dotty_reachable(std::cout, aut, + (type == spot::postprocessor::BA) + || (type == spot::postprocessor::Monitor)); + 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::hoaf_reachable(std::cout, aut, hoaf_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(); + return 0; + } + }; +} + +int +main(int argc, char** argv) +{ + setup(argv); + + const argp ap = { options, parse_opt, "[FILENAMES...]", + argp_program_doc, children, 0, 0 }; + + // Disable post-processing as much as possible by default. + level = spot::postprocessor::Low; + pref = spot::postprocessor::Any; + if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, 0, 0)) + exit(err); + + if (jobs.empty()) + jobs.emplace_back("-", true); + + spot::postprocessor post(&extra_options); + post.set_pref(pref | comp); + post.set_type(type); + post.set_level(level); + + hoa_processor processor(post); + if (processor.run()) + return 2; + return 0; +} diff --git a/src/bin/common_post.cc b/src/bin/common_post.cc index fa9e06a45..d0841e7b3 100644 --- a/src/bin/common_post.cc +++ b/src/bin/common_post.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2013 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// 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. // @@ -49,6 +49,24 @@ static const argp_option options[] = { 0, 0, 0, 0, 0, 0 } }; +static const argp_option options_disabled[] = + { + /**************************************************/ + { 0, 0, 0, 0, "Translation intent:", 20 }, + { "small", OPT_SMALL, 0, 0, "prefer small automata", 0 }, + { "deterministic", 'D', 0, 0, "prefer deterministic automata", 0 }, + { "any", 'a', 0, 0, "no preference (default)", 0 }, + { "complete", 'C', 0, 0, "output a complete automaton (combine " + "with other intents)", 0 }, + /**************************************************/ + { 0, 0, 0, 0, "Optimization level:", 21 }, + { "low", OPT_LOW, 0, 0, "minimal optimizations (fast, default)", 0 }, + { "medium", OPT_MEDIUM, 0, 0, "moderate optimizations", 0 }, + { "high", OPT_HIGH, 0, 0, + "all available optimizations (slow)", 0 }, + { 0, 0, 0, 0, 0, 0 } + }; + static int parse_opt_post(int key, char*, struct argp_state*) { @@ -85,5 +103,7 @@ parse_opt_post(int key, char*, struct argp_state*) return 0; } -const struct argp post_argp = { options, parse_opt_post, 0, 0, 0, 0, 0 }; - +const struct argp post_argp = + { options, parse_opt_post, 0, 0, 0, 0, 0 }; +const struct argp post_argp_disabled = + { options_disabled, parse_opt_post, 0, 0, 0, 0, 0 }; diff --git a/src/bin/common_post.hh b/src/bin/common_post.hh index f2fcc0cb1..3c8aac529 100644 --- a/src/bin/common_post.hh +++ b/src/bin/common_post.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2013 Laboratoire de Recherche et Développement de -// l'Epita (LRDE). +// 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. // @@ -24,11 +24,14 @@ #include "tgbaalgos/postproc.hh" #include -extern const struct argp post_argp; +extern const struct argp post_argp; // postprocessing enabled +extern const struct argp post_argp_disabled; // postprocessing disabled extern spot::postprocessor::output_type type; extern spot::postprocessor::output_pref pref; extern spot::postprocessor::output_pref comp; extern spot::postprocessor::optimization_level level; + + #endif // SPOT_BIN_COMMON_FINPUT_HH diff --git a/src/bin/man/Makefile.am b/src/bin/man/Makefile.am index c77d653ec..5215d8dc6 100644 --- a/src/bin/man/Makefile.am +++ b/src/bin/man/Makefile.am @@ -1,5 +1,5 @@ ## -*- coding: utf-8 -*- -## Copyright (C) 2012, 2013 Laboratoire de Recherche et Développement +## 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. @@ -23,6 +23,7 @@ convman = ARGP_HELP_FMT=header-col=0 $(SHELL) "$(x_to_1)" \ "$(PERL)" "$(top_srcdir)/tools/help2man -N -L 'en_US.UTF-8'" dist_man1_MANS = \ + autfilt.1 \ dstar2tgba.1 \ genltl.1 \ ltl2tgba.1 \ @@ -37,6 +38,9 @@ dist_man7_MANS = \ MAINTAINERCLEANFILES = $(dist_man1_MANS) $(dist_man7_MANS) EXTRA_DIST = $(dist_man1_MANS:.1=.x) $(dist_man7_MANS:.7=.x) +autfilt.1: $(common_dep) $(srcdir)/autfilt.x $(srcdir)/../autfilt.cc + $(convman) ../autfilt$(EXEEXT) $(srcdir)/autfilt.x $@ + dstar2tgba.1: $(common_dep) $(srcdir)/dstar2tgba.x $(srcdir)/../dstar2tgba.cc $(convman) ../dstar2tgba$(EXEEXT) $(srcdir)/dstar2tgba.x $@ diff --git a/src/bin/man/autfilt.x b/src/bin/man/autfilt.x new file mode 100644 index 000000000..159fb5b6e --- /dev/null +++ b/src/bin/man/autfilt.x @@ -0,0 +1,6 @@ +[NAME] +autfilt \- filter, convert, and transform Büchi automata +[DESCRIPTION] +.\" Add any additional description here +[SEE ALSO] +.BR spot-x (7)