diff --git a/NEWS b/NEWS
index 9c9c56fd1..699775ede 100644
--- a/NEWS
+++ b/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
diff --git a/bin/Makefile.am b/bin/Makefile.am
index 85e5ca059..761474db2 100644
--- a/bin/Makefile.am
+++ b/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
diff --git a/bin/genaut.cc b/bin/genaut.cc
new file mode 100644
index 000000000..0e0526566
--- /dev/null
+++ b/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 .
+
+#include "common_sys.hh"
+
+#include
+#include
+#include
+#include
+#include "error.h"
+#include
+
+#include "common_setup.hh"
+#include "common_aoutput.hh"
+#include "common_range.hh"
+#include "common_cout.hh"
+
+#include
+#include
+#include
+#include
+#include
+#include
+#include
+#include
+#include
+
+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 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;
+}