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

 ## -*- 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

src/bin/autfilt.cc

+// -*- 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 <http://www.gnu.org/licenses/>.
+
+#include "common_sys.hh"
+
+#include <string>
+#include <iostream>
+
+#include <argp.h>
+#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<const char*> filename_;
+    spot::printable_value<unsigned> haut_states_;
+    spot::printable_value<unsigned> haut_edges_;
+    spot::printable_value<unsigned> haut_trans_;
+    spot::printable_value<unsigned> haut_acc_;
+    spot::printable_value<unsigned> 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;
+}

src/bin/common_post.cc

 // -*- 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 };

src/bin/common_post.hh

 // -*- 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 <argp.h>
 
-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

src/bin/man/Makefile.am

 ## -*- 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 $@
 

src/bin/man/autfilt.x

+[NAME]
+autfilt \- filter, convert, and transform Büchi automata
+[DESCRIPTION]
+.\" Add any additional description here
+[SEE ALSO]
+.BR spot-x (7)