diff --git a/NEWS b/NEWS
index 13e1c6c97..151e130ca 100644
--- a/NEWS
+++ b/NEWS
@@ -51,6 +51,9 @@ New in spot 2.0a (not yet released)
* Add missing documentation for the option string passed to
spot::make_emptiness_check_instantiator().
+ * There is a now a spot(7) man page listing all installed
+ command-line tools.
+
Python:
* The tgba_determinize() function is now accessible in Python.
diff --git a/bin/Makefile.am b/bin/Makefile.am
index e0e4254f8..85e5ca059 100644
--- a/bin/Makefile.am
+++ b/bin/Makefile.am
@@ -1,6 +1,6 @@
## -*- coding: utf-8 -*-
-## Copyright (C) 2012, 2013, 2014, 2015 Laboratoire de Recherche et
-## Développement de l'Epita (LRDE).
+## Copyright (C) 2012, 2013, 2014, 2015, 2016 Laboratoire de Recherche
+## et Développement de l'Epita (LRDE).
##
## This file is part of Spot, a model checking library.
##
@@ -68,10 +68,10 @@ bin_PROGRAMS = \
randaut \
randltl
-# 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
+# Dummy programs used just to generate man/spot-x.7 and man/spot.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 spot
autfilt_SOURCES = autfilt.cc
ltlfilt_SOURCES = ltlfilt.cc
@@ -85,6 +85,7 @@ ltlgrind_SOURCES = ltlgrind.cc
ltldo_SOURCES = ltldo.cc
dstar2tgba_SOURCES = dstar2tgba.cc
spot_x_SOURCES = spot-x.cc
+spot_SOURCES = spot.cc
ltlcross_LDADD = $(LDADD) $(LIB_GETHRXTIME)
EXTRA_DIST = options.py
diff --git a/bin/man/Makefile.am b/bin/man/Makefile.am
index 3aa77de5a..b7c9f51bb 100644
--- a/bin/man/Makefile.am
+++ b/bin/man/Makefile.am
@@ -1,5 +1,5 @@
## -*- coding: utf-8 -*-
-## Copyright (C) 2012, 2013, 2014, 2015 Laboratoire de Recherche et
+## Copyright (C) 2012, 2013, 2014, 2015, 2016 Laboratoire de Recherche et
## Développement de l'Epita (LRDE).
##
## This file is part of Spot, a model checking library.
@@ -37,6 +37,7 @@ dist_man1_MANS = \
randaut.1 \
randltl.1
dist_man7_MANS = \
+ spot.7 \
spot-x.7
MAINTAINERCLEANFILES = $(dist_man1_MANS) $(dist_man7_MANS)
@@ -75,5 +76,8 @@ randaut.1: $(common_dep) $(srcdir)/randaut.x $(srcdir)/../randaut.cc
spot-x.7: $(common_dep) $(srcdir)/spot-x.x $(srcdir)/../spot-x.cc
$(convman7) ../spot-x$(EXEEXT) $(srcdir)/spot-x.x $@
+spot.7: $(common_dep) $(srcdir)/spot.x $(srcdir)/../spot.cc
+ $(convman7) ../spot$(EXEEXT) $(srcdir)/spot.x $@
+
ltlgrind.1: $(common_dep) $(srcdir)/ltlgrind.x $(srcdir)/../ltlgrind.cc
$(convman) ../ltlgrind$(EXEEXT) $(srcdir)/ltlgrind.x $@
diff --git a/bin/man/spot.x b/bin/man/spot.x
new file mode 100644
index 000000000..f46305aa5
--- /dev/null
+++ b/bin/man/spot.x
@@ -0,0 +1,28 @@
+[NAME]
+spot \- Command-line tools installed by Spot.
+
+[SYNOPSIS]
+
+Spot is a C++ library for ω-automata and LTL formulas manipulation.
+It also comes with Python bindings and a set of command-line tools
+that are listed below.
+
+[DESCRIPTION]
+.\" Add any additional description here
+
+[SEE ALSO]
+.BR randltl (1)
+.BR genltl (1)
+.BR ltlfilt (1)
+.BR ltlrind (1)
+.BR randaut (1)
+.BR ltl2tgba (1)
+.BR ltl2tgta (1)
+.BR autfilt (1)
+.BR ltlcross (1)
+.BR ltldo (1)
+.BR spot-x (7)
+
+.UR https://spot.lrde.epita.fr/
+The Spot web page.
+.UE
diff --git a/bin/spot.cc b/bin/spot.cc
new file mode 100644
index 000000000..1478f1234
--- /dev/null
+++ b/bin/spot.cc
@@ -0,0 +1,78 @@
+// -*- coding: utf-8 -*-
+// Copyright (C) 2013, 2014, 2015, 2016 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 "common_setup.hh"
+
+const char argp_program_doc[] ="Command-line tools installed by Spot.";
+
+#define DOC(NAME, TXT) NAME, 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, TXT, 0
+
+static const argp_option options[] =
+ {
+ { nullptr, 0, nullptr, 0, "Tools that output LTL/PSL formulas:", 0 },
+ { DOC("randltl", "Generate random LTL or PSL formulas.") },
+ { DOC("genltl", "Generate LTL formulas from scalable patterns.") },
+ { DOC("ltlfilt", "Filter, convert, and transform LTL or PSL formulas.") },
+ { DOC("ltlgrind", "Mutate LTL or PSL formulas to generate similar but "
+ "simpler ones. Use this when looking for shorter formula to "
+ "reproduce a bug.") },
+ { nullptr, 0, nullptr, 0, "Tools that output automata:", 0 },
+ { DOC("randaut", "Generate random ω-automata.") },
+ { DOC("ltl2tgba", "Convert LTL or PSL into variants of Transition-based "
+ "Generalized Büchi Automata.") },
+ { DOC("ltl2tgta", "Convert LTL or PSL into variants of Transition-based "
+ "Generalized Testing Automata.") },
+ { DOC("autfilt", "Filter, convert, and transform ω-automata.") },
+ { DOC("dstar2tgba", "Convert ω-automata into variants of "
+ "Transition-based Büchi automata.") },
+ { nullptr, 0, nullptr, 0, "Tools that run other tools:", 0 },
+ { DOC("ltlcross", "Cross-compare translators of LTL or PSL formulas "
+ "into ω-automata, watch for bugs, and generate statistics.") },
+ { DOC("ltldo", "Wrap any tool that inputs LTL or PSL formulas and possibly "
+ "outputs ω-automata; provides Spot's I/O interface.") },
+ { nullptr, 0, nullptr, 0, nullptr, 0 }
+ };
+
+const struct argp_child children[] =
+ {
+ { &misc_argp_hidden, 0, nullptr, -1 },
+ { nullptr, 0, nullptr, 0 }
+ };
+
+int
+main(int argc, char** argv)
+{
+ setup(argv);
+
+ const argp ap = { options, nullptr, nullptr, argp_program_doc, children,
+ nullptr, nullptr };
+
+ if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, nullptr, nullptr))
+ exit(err);
+
+ std::cerr << "This binary serves no purpose other than generating"
+ << " the spot.7 manpage.\n";
+
+ return 1;
+}
diff --git a/doc/org/tools.org b/doc/org/tools.org
index cb062df47..acdcaa0e9 100644
--- a/doc/org/tools.org
+++ b/doc/org/tools.org
@@ -71,7 +71,8 @@ convenience, you can browse their HTML versions:
[[./man/ltlfilt.1.html][=ltlfilt=]](1),
[[./man/randaut.1.html][=randaut=]](1),
[[./man/randltl.1.html][=randltl=]](1),
-[[./man/spot-x.7.html][=spot-x=]](7).
+[[./man/spot-x.7.html][=spot-x=]](7),
+[[./man/spot.7.html][=spot=]](7).
* Advanced use-cases