diff --git a/src/bin/.gitignore b/src/bin/.gitignore
index 0bdbab80b..1ee77695d 100644
--- a/src/bin/.gitignore
+++ b/src/bin/.gitignore
@@ -4,6 +4,8 @@ ltl2tgta
randltl
genltl
ltlcross
+spot-x
*.a
*.1
+*.7
lck-*
diff --git a/src/bin/Makefile.am b/src/bin/Makefile.am
index fdb1a5027..d7c2fa3f4 100644
--- a/src/bin/Makefile.am
+++ b/src/bin/Makefile.am
@@ -1,5 +1,5 @@
## -*- coding: utf-8 -*-
-## Copyright (C) 2012 Laboratoire de Recherche et Développement
+## Copyright (C) 2012, 2013 Laboratoire de Recherche et Développement
## de l'Epita (LRDE).
##
## This file is part of Spot, a model checking library.
@@ -43,10 +43,17 @@ libcommon_a_SOURCES = \
common_sys.hh
bin_PROGRAMS = ltlfilt genltl randltl ltl2tgba ltl2tgta ltlcross
+
+# 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
+
ltlfilt_SOURCES = ltlfilt.cc
genltl_SOURCES = genltl.cc
randltl_SOURCES = randltl.cc
ltl2tgba_SOURCES = ltl2tgba.cc
ltl2tgta_SOURCES = ltl2tgta.cc
ltlcross_SOURCES = ltlcross.cc
+spot_x_SOURCES = spot-x.cc
ltlcross_LDADD = $(LDADD) $(LIB_GETHRXTIME)
diff --git a/src/bin/common_setup.cc b/src/bin/common_setup.cc
index 1329a9f30..68947831e 100644
--- a/src/bin/common_setup.cc
+++ b/src/bin/common_setup.cc
@@ -66,6 +66,15 @@ static const argp_option options[] =
{ 0, 0, 0, 0, 0, 0 }
};
+static const argp_option options_hidden[] =
+ {
+ { "version", OPT_VERSION, 0, OPTION_HIDDEN, "print program version", -1 },
+ { "help", OPT_HELP, 0, OPTION_HIDDEN, "print this help", -1 },
+ // We support this option just in case, but we don't advertise it.
+ { "usage", OPT_USAGE, 0, OPTION_HIDDEN, "show short usage", -1 },
+ { 0, 0, 0, 0, 0, 0 }
+ };
+
static int
parse_opt_misc(int key, char*, struct argp_state* state)
{
@@ -91,3 +100,6 @@ parse_opt_misc(int key, char*, struct argp_state* state)
const struct argp misc_argp = { options, parse_opt_misc, 0, 0, 0, 0, 0 };
+
+const struct argp misc_argp_hidden = { options_hidden, parse_opt_misc,
+ 0, 0, 0, 0, 0 };
diff --git a/src/bin/common_setup.hh b/src/bin/common_setup.hh
index 50ef32822..8d6a0d96a 100644
--- a/src/bin/common_setup.hh
+++ b/src/bin/common_setup.hh
@@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
-// Copyright (C) 2012 Laboratoire de Recherche et Développement de
+// Copyright (C) 2012, 2013 Laboratoire de Recherche et Développement de
// l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
@@ -26,5 +26,6 @@
void setup(char** progname);
extern const struct argp misc_argp;
+extern const struct argp misc_argp_hidden;
#endif // SPOT_BIN_COMMON_SETUP_HH
diff --git a/src/bin/ltl2tgba.cc b/src/bin/ltl2tgba.cc
index ac480cba6..1aac05b23 100644
--- a/src/bin/ltl2tgba.cc
+++ b/src/bin/ltl2tgba.cc
@@ -93,7 +93,7 @@ static const argp_option options[] =
/**************************************************/
{ 0, 0, 0, 0, "Miscellaneous options:", -1 },
{ "extra-options", 'x', "OPTS", 0,
- "fine-tuning options (see man page)", 0 },
+ "fine-tuning options (see spot-x (7))", 0 },
{ 0, 0, 0, 0, 0, 0 }
};
diff --git a/src/bin/man/Makefile.am b/src/bin/man/Makefile.am
index cf4d03c08..cc56ce8ae 100644
--- a/src/bin/man/Makefile.am
+++ b/src/bin/man/Makefile.am
@@ -28,7 +28,8 @@ dist_man1_MANS = \
ltl2tgta.1 \
ltlcross.1 \
ltlfilt.1 \
- randltl.1
+ randltl.1 \
+ spot-x.7
MAINTAINERCLEANFILES = $(dist_man1_MANS)
EXTRA_DIST = $(dist_man1_MANS:.1=.x)
@@ -50,3 +51,6 @@ genltl.1: $(common_dep) $(srcdir)/genltl.x $(srcdir)/../genltl.cc
randltl.1: $(common_dep) $(srcdir)/randltl.x $(srcdir)/../randltl.cc
$(convman) ../randltl$(EXEEXT) $(srcdir)/randltl.x $@
+
+spot-x.7: $(common_dep) $(srcdir)/spot-x.x $(srcdir)/../spot-x.cc
+ $(convman) ../spot-x$(EXEEXT) $(srcdir)/spot-x.x $@
diff --git a/src/bin/man/ltl2tgba.x b/src/bin/man/ltl2tgba.x
index 6a2ff04f0..20ddafdbf 100644
--- a/src/bin/man/ltl2tgba.x
+++ b/src/bin/man/ltl2tgba.x
@@ -2,51 +2,5 @@
ltl2tgba \- translate LTL/PSL formulas into Büchi automata
[DESCRIPTION]
.\" Add any additional description here
-[FINE-TUNING OPTIONS]
-
-The \fB\-\-extra\-options\fR argument is a comma-separated list of
-\fIKEY\fR=\fIINT\fR assignments that are passed to the post-processing
-routines (they may be passed to other algorithms in the future).
-These options are mostly used for benchmarking and debugging
-purpose. \fIKEY\fR (without any value) is a
-shorthand for \fIKEY\fR=1, and !\fIKEY\fR is a shorthand for
-\fIKEY\fR=0.
-
-Supported options are:
-.TP
-\fBscc\-filter\fR
-Set to 1 (the default) to enable SCC-pruning and acceptance
-simplification at the beginning of post-processing. Transitions that
-are outside of accepting SCC are removed from accepting sets, except
-those that enter into an accepting SCC. Set to 2 to remove even these
-entering transition from the accepting sets. Set to 0 to disable this
-SCC-pruning and acceptance simpification pass.
-.TP
-\fBdegen\-reset\fR
-If non-zero (the default), the degeneralization algorithm will reset
-its level any time it exits a non-accepting SCC.
-.TP
-\fBdegen\-lcache\fR
-If non-zero (the default), whenever the degeneralization algorithm enters
-an SCC on a state that has already been associated to a level elsewhere,
-it should reuse that level. The "lcache" stands for "level cache".
-.TP
-\fBdegen\-order\fR
-If non-zero, the degeneralization algorithm will compute one degeneralization
-order for each SCC it processes. This is currently disabled by default.
-.TP
-\fBsimul\fR
-Set to 0 to disable simulation-based reductions. Set to 1 to use only
-direct simulation. Set to 2 to use only reverse simulation. Set to 3
-to iterate both direct and reverse simulations. Set to 4 to apply
-only "don't care" direct simulation. Set to 5 to iterate "don't care"
-direct simulation and reverse simulation. The default is 3, except
-when option \fB\-\-low\fR is specified, in which case the default is
-1.
-.TP
-\fBsimul-limit\fR
-Can be set to a positive integer to cap the number of "don't care"
-transitions considered by the "don't care"-simulation algorithm. A
-negative value (the default) does not enforce any limit. Note that if
-there are \fIN\fR "don't care" transitions, the algorithm may
-potentially test 2^\fIN\fR configurations.
+[SEE ALSO]
+.BR spot-x (7)
diff --git a/src/bin/man/spot-x.x b/src/bin/man/spot-x.x
new file mode 100644
index 000000000..c892e26d7
--- /dev/null
+++ b/src/bin/man/spot-x.x
@@ -0,0 +1,10 @@
+[NAME]
+spot-x \- Common fine-tuning options.
+[SYNOPSIS]
+.B \-\-extra-options STRING
+.br
+.B \-x STRING
+[DESCRIPTION]
+.\" Add any additional description here
+[SEE ALSO]
+.BR ltl2tgba (1)
diff --git a/src/bin/spot-x.cc b/src/bin/spot-x.cc
new file mode 100644
index 000000000..c097ffa19
--- /dev/null
+++ b/src/bin/spot-x.cc
@@ -0,0 +1,93 @@
+// -*- coding: utf-8 -*-
+// Copyright (C) 2013 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[] ="\
+Common fine-tuning options for binaries built with Spot.\n\
+\n\
+The argument of -x or --extra-options is a comma-separated list of KEY=INT \
+assignments that are passed to the post-processing routines (they may \
+be passed to other algorithms in the future). These options are \
+mostly used for benchmarking and debugging purpose. KEYR (without any \
+value) is a shorthand for KEY=1, while !KEY is a shorthand for KEY=0.";
+
+#define DOC(NAME, TXT) NAME, 0, 0, OPTION_DOC | OPTION_NO_USAGE, TXT, 0
+
+static const argp_option options[] =
+ {
+ { 0, 0, 0, 0, "Postprocessing options:", 0 },
+ { DOC("scc-filter", "Set to 1 (the default) to enable \
+SCC-pruning and acceptance simplification at the beginning of \
+post-processing. Transitions that are outside of accepting SCC are \
+removed from accepting sets, except those that enter into an accepting \
+SCC. Set to 2 to remove even these entering transition from the \
+accepting sets. Set to 0 to disable this SCC-pruning and acceptance \
+simpification pass.") },
+ { DOC("degen-reset", "If non-zero (the default), the \
+degeneralization algorithm will reset its level any time it exits \
+a non-accepting SCC.") },
+ { DOC("degen-lcache", "If non-zero (the default), whenever the \
+degeneralization algorithm enters an SCC on a state that has already \
+been associated to a level elsewhere, it should reuse that level. \
+The \"lcache\" stands for \"level cache\".") },
+ { DOC("degen-order", "If non-zero, the degeneralization algorithm \
+will compute one degeneralization order for each SCC it processes. \
+This is currently disabled by default.") },
+ { DOC("simul", "Set to 0 to disable simulation-based reductions. \
+Set to 1 to use only direct simulation. Set to 2 to use only reverse \
+simulation. Set to 3 to iterate both direct and reverse simulations. \
+Set to 4 to apply only \"don't care\" direct simulation. Set to 5 to \
+iterate \"don't care\" direct simulation and reverse simulation. The \
+default is 3, except when option --low is specified, in which case the \
+default is 1.") },
+ { DOC("simul-limit", "Can be set to a positive integer to cap the \
+number of \"don't care\" transitions considered by the \
+\"don't care\"-simulation algorithm. A negative value (the default) \
+does not enforce any limit. Note that if there are N \"don't care\" \
+transitions, the algorithm may potentially test 2^N configurations.") },
+ { 0, 0, 0, 0, 0, 0 }
+ };
+
+const struct argp_child children[] =
+ {
+ { &misc_argp_hidden, 0, 0, -1 },
+ { 0, 0, 0, 0 }
+ };
+
+int
+main(int argc, char** argv)
+{
+ setup(argv);
+
+ const argp ap = { options, 0, 0, argp_program_doc, children, 0, 0 };
+
+ if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, 0, 0))
+ exit(err);
+
+ std::cerr << "This binary serves no purpose other than generating"
+ << " the spot-x.7 manpage.\n";
+
+ return 1;
+}