Add a genaut binary.

Similarly to genltl that generates LTL formulas for various classes that
appear in the literature, genaut generates automata.

* NEWS: Mention the modification.
* bin/Makefile.am: Build the new binary.
* bin/genaut.cc: The new binary itself.

NEWS

@@ -8,6 +8,11 @@ New in spot 2.3.3.dev (not yet released)
   - In autfilt, the option --dualize is now available to obtain the dual
     of any automaton.
 
+  - Add a new binary: genaut. Similarly to genltl that produces LTL
+    formulas from the literature, this tool produces automata from
+    the literature. It currently features only one class of
+    automata.
+
   Library:
 
   - Add a new library libspotgen. It is intended to be place to gather

bin/Makefile.am

@@ -1,5 +1,5 @@
 ## -*- coding: utf-8 -*-
-## Copyright (C) 2012, 2013, 2014, 2015, 2016 Laboratoire de Recherche
+## Copyright (C) 2012, 2013, 2014, 2015, 2016-2017 Laboratoire de Recherche
 ## et Développement de l'Epita (LRDE).
 ##
 ## This file is part of Spot, a model checking library.
@@ -58,6 +58,7 @@ libcommon_a_SOURCES =				\
 bin_PROGRAMS = \
   autfilt \
   dstar2tgba \
+  genaut \
   genltl \
   ltl2tgba \
   ltl2tgta \
@@ -75,6 +76,8 @@ noinst_PROGRAMS = spot-x spot
 
 autfilt_SOURCES = autfilt.cc
 ltlfilt_SOURCES = ltlfilt.cc
+genaut_SOURCES = genaut.cc
+genaut_LDADD = $(top_builddir)/spot/gen/libspotgen.la $(LDADD)
 genltl_SOURCES = genltl.cc
 randaut_SOURCES = randaut.cc
 randltl_SOURCES = randltl.cc

bin/genaut.cc

@@ -0,0 +1,199 @@
+// -*- coding: utf-8 -*-
+// Copyright (C) 2017 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 <iostream>
+#include <fstream>
+#include <argp.h>
+#include <cstdlib>
+#include "error.h"
+#include <vector>
+
+#include "common_setup.hh"
+#include "common_aoutput.hh"
+#include "common_range.hh"
+#include "common_cout.hh"
+
+#include <cassert>
+#include <iostream>
+#include <sstream>
+#include <set>
+#include <string>
+#include <cmath>
+#include <cstdlib>
+#include <cstring>
+#include <spot/gen/automata.hh>
+
+using namespace spot;
+
+const char argp_program_doc[] ="\
+Generate omega automata from predefined patterns.";
+
+enum {
+  FIRST_CLASS = 256,
+  OPT_KS_COBUCHI = FIRST_CLASS,
+  LAST_CLASS,
+};
+/*
+const char* const class_name[LAST_CLASS - FIRST_CLASS] =
+  {
+    "ks-cobuchi",
+  };
+*/
+
+#define OPT_ALIAS(o) { #o, 0, nullptr, OPTION_ALIAS, nullptr, 0 }
+
+static const argp_option options[] =
+  {
+    /**************************************************/
+    // Keep this alphabetically sorted (expect for aliases).
+    { nullptr, 0, nullptr, 0, "Pattern selection:", 1},
+    { "ks-cobuchi", OPT_KS_COBUCHI, "N", 0,
+      "A co-Bûchi automaton with 2N+1 states for which any equivalent "
+      "deterministic co-Büchi automaton has at least 2^N/(2N+1) states.", 0},
+  /**************************************************/
+    { nullptr, 0, nullptr, 0, "Miscellaneous options:", -1 },
+    { nullptr, 0, nullptr, 0, nullptr, 0 }
+  };
+
+struct job
+{
+  int pattern;
+  struct range range;
+};
+
+typedef std::vector<job> jobs_t;
+static jobs_t jobs;
+
+const struct argp_child children[] =
+  {
+    { &aoutput_argp, 0, nullptr, -20 },
+    { &misc_argp, 0, nullptr, -1 },
+    { nullptr, 0, nullptr, 0 }
+  };
+
+static void
+enqueue_job(int pattern, const char* range_str)
+{
+  job j;
+  j.pattern = pattern;
+  j.range = parse_range(range_str);
+  jobs.push_back(j);
+}
+/*
+static void
+enqueue_job(int pattern, int min, int max)
+{
+  job j;
+  j.pattern = pattern;
+  j.range = {min, max};
+  jobs.push_back(j);
+}
+*/
+static int
+parse_opt(int key, char* arg, struct argp_state*)
+{
+  // This switch is alphabetically-ordered.
+  switch (key)
+    {
+    case OPT_KS_COBUCHI:
+      enqueue_job(key, arg);
+      break;
+    default:
+      return ARGP_ERR_UNKNOWN;
+    }
+  return 0;
+}
+/*
+static void
+bad_number(const char* pattern, int n, int max = 0)
+{
+  std::ostringstream err;
+  err << "no pattern " << n << " for " << pattern
+      << ", supported range is 1..";
+  if (max)
+    err << max;
+  throw std::runtime_error(err.str());
+}
+*/
+static void
+output_pattern(int pattern, int n)
+{
+  twa_graph_ptr aut = nullptr;
+  switch (pattern)
+    {
+      // Keep this alphabetically-ordered!
+    case OPT_KS_COBUCHI:
+      aut = spot::gen::ks_cobuchi(n);
+      break;
+    default:
+      error(100, 0, "internal error: pattern not implemented");
+    }
+
+  process_timer timer;
+  automaton_printer printer;
+  printer.print(aut, timer);
+}
+
+static void
+run_jobs()
+{
+  for (auto& j: jobs)
+    {
+      int inc = (j.range.max < j.range.min) ? -1 : 1;
+      int n = j.range.min;
+      for (;;)
+        {
+          output_pattern(j.pattern, n);
+          if (n == j.range.max)
+            break;
+          n += inc;
+        }
+    }
+}
+
+
+int
+main(int argc, char** argv)
+{
+  setup(argv);
+
+  const argp ap = { options, parse_opt, nullptr, argp_program_doc,
+                    children, nullptr, nullptr };
+
+  if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, nullptr, nullptr))
+    exit(err);
+
+  if (jobs.empty())
+    error(1, 0, "Nothing to do.  Try '%s --help' for more information.",
+          program_name);
+
+  try
+    {
+      run_jobs();
+    }
+  catch (const std::runtime_error& e)
+    {
+      error(2, 0, "%s", e.what());
+    }
+
+  flush_cout();
+  return 0;
+}