From d78670ad443e39fbf4441f2ed6247d21fedc7bb5 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sat, 23 Mar 2013 17:08:28 +0100 Subject: [PATCH] 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. --- src/bin/.gitignore | 2 + src/bin/Makefile.am | 9 +++- src/bin/common_setup.cc | 12 ++++++ src/bin/common_setup.hh | 3 +- src/bin/ltl2tgba.cc | 2 +- src/bin/man/Makefile.am | 6 ++- src/bin/man/ltl2tgba.x | 50 +--------------------- src/bin/man/spot-x.x | 10 +++++ src/bin/spot-x.cc | 93 +++++++++++++++++++++++++++++++++++++++++ 9 files changed, 135 insertions(+), 52 deletions(-) create mode 100644 src/bin/man/spot-x.x create mode 100644 src/bin/spot-x.cc 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; +}