Commit d78670ad authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

spot-x.7: new man page for common fine-tuning options

* src/bin/spot-x.cc, src/bin/man/spot-x.x: New files.
* src/bin/Makefile.am, src/bin/man/Makefile.am: Adjust.
* src/bin/man/ltl2tgba.x: Remove all fine-tuning options,
and make a reference spot spot-x (7).
* src/bin/common_setup.hh, src/bin/common_setup.cc: Add
a misc_argp_hidden version of the option, so that --help
and --version are not shown in the --help output used
by help2man to generate spot-x.7.
* src/bin/ltl2tgba.cc: Refer to spot-x.7.
parent 1337c9c3
......@@ -4,6 +4,8 @@ ltl2tgta
randltl
genltl
ltlcross
spot-x
*.a
*.1
*.7
lck-*
## -*- 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)
......@@ -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 };
// -*- 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
......@@ -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 }
};
......
......@@ -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 $@
......@@ -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)
[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)
// -*- 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 <http://www.gnu.org/licenses/>.
#include "common_sys.hh"
#include <string>
#include <iostream>
#include <cstdlib>
#include <argp.h>
#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;
}
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment