bin: make sure that all options are in a named section
This also fixes some empty lines and unsorted options that appeared in some tools. * tests/sanity/bin.test: Ensure this is done. * bin/README: Add a new paragraph about this. * bin/autcross.cc, bin/ltlcross.cc: Move the output options in their own section. * bin/common_color.cc: Assume color options are in group -15. * bin/common_finput.cc, bin/common_finput.hh: Add a headless variant. * bin/genltl.cc, bin/ltlfilt.cc, bin/ltlgrind.cc, bin/randaut.cc, bin/randltl.cc: Do not force the children groups, so that the options are correctly sorted. * bin/ltlsynt.cc: Add missing groups.
This commit is contained in:
Alexandre Duret-Lutz
parent
002e6ed96b
commit
69daf9c261
13 changed files with 83 additions and 35 deletions
|
|
@ -50,3 +50,10 @@ Recommendations when adding new tools or features:
|
|||
randaut -n N means --automata=N
|
||||
but in all cases, the intent is to specify the number of items
|
||||
to output.
|
||||
|
||||
- In the --help output, all options should appear in a named
|
||||
section (like "Input options:", "Output options:"), and those
|
||||
sections are best ordered according to one's mental view
|
||||
of how the tool works: first, it reads the input, then
|
||||
it processes it, then it outputs the result. Keep --help
|
||||
and --version at the very bottom.
|
||||
|
|
|
|||
|
|
@ -112,11 +112,16 @@ static const argp_option options[] =
|
|||
{ "high", OPT_HIGH, nullptr, 0,
|
||||
"all available optimizations (slow, default)", 0 },
|
||||
/**************************************************/
|
||||
{ nullptr, 0, nullptr, 0, "Miscellaneous options:", -2 },
|
||||
{ nullptr, 0, nullptr, 0, "Output options:", -15 },
|
||||
{ "save-bogus", OPT_BOGUS, "[>>]FILENAME", 0,
|
||||
"save formulas for which problems were detected in FILENAME", 0 },
|
||||
"save formulas for which problems were detected in FILENAME", -1 },
|
||||
{ "verbose", OPT_VERBOSE, nullptr, 0,
|
||||
"print what is being done, for debugging", 0 },
|
||||
"print what is being done, for debugging", -1 },
|
||||
{ nullptr, 0, nullptr, 0,
|
||||
"If an output FILENAME is prefixed with '>>', it is open "
|
||||
"in append mode instead of being truncated.", -14 },
|
||||
/**************************************************/
|
||||
{ nullptr, 0, nullptr, 0, "Miscellaneous options:", -1 },
|
||||
{ nullptr, 0, nullptr, 0, nullptr, 0 }
|
||||
};
|
||||
|
||||
|
|
@ -124,7 +129,7 @@ const struct argp_child children[] =
|
|||
{
|
||||
{ &autproc_argp, 0, nullptr, 0 },
|
||||
{ &hoaread_argp, 0, "Parsing of automata:", 4 },
|
||||
{ &misc_argp, 0, nullptr, -2 },
|
||||
{ &misc_argp, 0, nullptr, -1 },
|
||||
{ &color_argp, 0, nullptr, 0 },
|
||||
{ nullptr, 0, nullptr, 0 }
|
||||
};
|
||||
|
|
|
|||
|
|
@ -69,7 +69,7 @@ static const argp_option options_color[] =
|
|||
{ "color", OPT_COLOR, "WHEN", OPTION_ARG_OPTIONAL,
|
||||
"colorize output; WHEN can be 'never', 'always' (the default if "
|
||||
"--color is used without argument), or "
|
||||
"'auto' (the default if --color is not used)", -2 },
|
||||
"'auto' (the default if --color is not used)", -15 },
|
||||
{ nullptr, 0, nullptr, 0, nullptr, 0 }
|
||||
};
|
||||
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
// -*- coding: utf-8 -*-
|
||||
// Copyright (C) 2012, 2013, 2014, 2015, 2016 Laboratoire de Recherche
|
||||
// Copyright (C) 2012-2017 Laboratoire de Recherche
|
||||
// et Développement de l'Epita (LRDE).
|
||||
//
|
||||
// This file is part of Spot, a model checking library.
|
||||
|
|
@ -37,16 +37,16 @@ static bool lenient = false;
|
|||
static const argp_option options[] =
|
||||
{
|
||||
{ nullptr, 0, nullptr, 0, "Input options:", 1 },
|
||||
{ "formula", 'f', "STRING", 0, "process the formula STRING", 0 },
|
||||
{ "formula", 'f', "STRING", 0, "process the formula STRING", 1 },
|
||||
{ "file", 'F', "FILENAME[/COL]", 0,
|
||||
"process each line of FILENAME as a formula; if COL is a "
|
||||
"positive integer, assume a CSV file and read column COL; use "
|
||||
"a negative COL to drop the first line of the CSV file", 0 },
|
||||
"a negative COL to drop the first line of the CSV file", 1 },
|
||||
{ "lbt-input", OPT_LBT, nullptr, 0,
|
||||
"read all formulas using LBT's prefix syntax", 0 },
|
||||
"read all formulas using LBT's prefix syntax", 1 },
|
||||
{ "lenient", OPT_LENIENT, nullptr, 0,
|
||||
"parenthesized blocks that cannot be parsed as subformulas "
|
||||
"are considered as atomic properties", 0 },
|
||||
"are considered as atomic properties", 1 },
|
||||
{ nullptr, 0, nullptr, 0, nullptr, 0 }
|
||||
};
|
||||
|
||||
|
|
@ -54,6 +54,11 @@ const struct argp finput_argp = { options, parse_opt_finput,
|
|||
nullptr, nullptr, nullptr,
|
||||
nullptr, nullptr };
|
||||
|
||||
const struct argp finput_argp_headless = { options + 1, parse_opt_finput,
|
||||
nullptr, nullptr, nullptr,
|
||||
nullptr, nullptr };
|
||||
|
||||
|
||||
int
|
||||
parse_opt_finput(int key, char* arg, struct argp_state*)
|
||||
{
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
// -*- coding: utf-8 -*-
|
||||
// Copyright (C) 2012, 2013, 2015, 2016 Laboratoire de Recherche et
|
||||
// Développement de l'Epita (LRDE).
|
||||
// Copyright (C) 2012-2017 Laboratoire de Recherche et Développement
|
||||
// de l'Epita (LRDE).
|
||||
//
|
||||
// This file is part of Spot, a model checking library.
|
||||
//
|
||||
|
|
@ -41,6 +41,7 @@ extern jobs_t jobs;
|
|||
extern bool lbt_input;
|
||||
|
||||
extern const struct argp finput_argp;
|
||||
extern const struct argp finput_argp_headless;
|
||||
|
||||
int parse_opt_finput(int key, char* arg, struct argp_state* state);
|
||||
|
||||
|
|
|
|||
|
|
@ -174,6 +174,7 @@ static const argp_option options[] =
|
|||
{ "%%", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
|
||||
"a single %", 0 },
|
||||
COMMON_LTL_OUTPUT_SPECS,
|
||||
/**************************************************/
|
||||
{ nullptr, 0, nullptr, 0, "Miscellaneous options:", -1 },
|
||||
{ nullptr, 0, nullptr, 0, nullptr, 0 }
|
||||
};
|
||||
|
|
@ -191,8 +192,8 @@ bool opt_negative = false;
|
|||
|
||||
const struct argp_child children[] =
|
||||
{
|
||||
{ &output_argp, 0, nullptr, -20 },
|
||||
{ &misc_argp, 0, nullptr, -1 },
|
||||
{ &output_argp, 0, nullptr, 0 },
|
||||
{ &misc_argp, 0, nullptr, 0 },
|
||||
{ nullptr, 0, nullptr, 0 }
|
||||
};
|
||||
|
||||
|
|
|
|||
|
|
@ -153,7 +153,7 @@ static const argp_option options[] =
|
|||
"[not supported for alternating automata]", 0 },
|
||||
{ "unambiguous", 0, nullptr, OPTION_ALIAS, nullptr, 0 },
|
||||
/**************************************************/
|
||||
{ nullptr, 0, nullptr, 0, "Miscellaneous options:", -2 },
|
||||
{ nullptr, 0, nullptr, 0, "Output options:", -15 },
|
||||
{ "grind", OPT_GRIND, "[>>]FILENAME", 0,
|
||||
"for each formula for which a problem was detected, write a simpler " \
|
||||
"formula that fails on the same test in FILENAME", 0 },
|
||||
|
|
@ -162,8 +162,10 @@ static const argp_option options[] =
|
|||
{ "verbose", OPT_VERBOSE, nullptr, 0,
|
||||
"print what is being done, for debugging", 0 },
|
||||
{ nullptr, 0, nullptr, 0,
|
||||
"If an output FILENAME is prefixed with '>>', is it open "
|
||||
"in append mode instead of being truncated.", -1 },
|
||||
"If an output FILENAME is prefixed with '>>', it is open "
|
||||
"in append mode instead of being truncated.", -14 },
|
||||
/**************************************************/
|
||||
{ nullptr, 0, nullptr, 0, "Miscellaneous options:", -1 },
|
||||
{ nullptr, 0, nullptr, 0, nullptr, 0 }
|
||||
};
|
||||
|
||||
|
|
@ -172,8 +174,8 @@ const struct argp_child children[] =
|
|||
{ &finput_argp, 0, nullptr, 1 },
|
||||
{ &trans_argp, 0, nullptr, 0 },
|
||||
{ &hoaread_argp, 0, "Parsing of automata:", 4 },
|
||||
{ &misc_argp, 0, nullptr, -2 },
|
||||
{ &color_argp, 0, nullptr, 0 },
|
||||
{ &misc_argp, 0, nullptr, -1 },
|
||||
{ nullptr, 0, nullptr, 0 }
|
||||
};
|
||||
|
||||
|
|
|
|||
|
|
@ -255,6 +255,7 @@ static const argp_option options[] =
|
|||
{ "%%", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
|
||||
"a single %", 0 },
|
||||
COMMON_LTL_OUTPUT_SPECS,
|
||||
/**************************************************/
|
||||
{ nullptr, 0, nullptr, 0, "Miscellaneous options:", -1 },
|
||||
{ nullptr, 0, nullptr, 0, nullptr, 0 }
|
||||
};
|
||||
|
|
@ -262,8 +263,8 @@ static const argp_option options[] =
|
|||
const struct argp_child children[] =
|
||||
{
|
||||
{ &finput_argp, 0, nullptr, 1 },
|
||||
{ &output_argp, 0, nullptr, -20 },
|
||||
{ &misc_argp, 0, nullptr, -1 },
|
||||
{ &output_argp, 0, nullptr, 0 },
|
||||
{ &misc_argp, 0, nullptr, 0 },
|
||||
{ nullptr, 0, nullptr, 0 }
|
||||
};
|
||||
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
// -*- coding: utf-8 -*-
|
||||
// Copyright (C) 2014, 2015, 2016 Laboratoire de Recherche et
|
||||
// Copyright (C) 2014, 2015, 2016, 2017 Laboratoire de Recherche et
|
||||
// Développement de l'Epita (LRDE).
|
||||
//
|
||||
// This file is part of Spot, a model checking library.
|
||||
|
|
@ -75,13 +75,14 @@ static const argp_option options[] = {
|
|||
{ "simplify-bounds", OPT_SIMPLIFY_BOUNDS, nullptr, 0,
|
||||
"on a bounded unary operator, decrement one of the bounds, or set min to "
|
||||
"0 or max to unbounded", 15 },
|
||||
{ nullptr, 0, nullptr, 0, "Output options:", 20 },
|
||||
{ "max-count", 'n', "NUM", 0, "maximum number of mutations to output", 20 },
|
||||
/**************************************************/
|
||||
{ nullptr, 0, nullptr, 0, "Output options:", -20 },
|
||||
{ "max-count", 'n', "NUM", 0, "maximum number of mutations to output", 0 },
|
||||
{ "mutations", 'm', "NUM", 0, "number of mutations to apply to the "
|
||||
"formulae (default: 1)", 0 },
|
||||
{ "sort", OPT_SORT, nullptr, 0, "sort the result by formula size", 0 },
|
||||
{ nullptr, 0, nullptr, 0, "The FORMAT string passed to --format may use "
|
||||
"the following interpreted sequences:", 21 },
|
||||
"the following interpreted sequences:", -19 },
|
||||
{ "%f", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
|
||||
"the formula (in the selected syntax)", 0 },
|
||||
{ "%F", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
|
||||
|
|
@ -97,14 +98,15 @@ static const argp_option options[] = {
|
|||
{ "%%", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
|
||||
"a single %", 0 },
|
||||
COMMON_LTL_OUTPUT_SPECS,
|
||||
/**************************************************/
|
||||
{ nullptr, 0, nullptr, 0, "Miscellaneous options:", -1 },
|
||||
{ nullptr, 0, nullptr, 0, nullptr, 0 }
|
||||
};
|
||||
|
||||
static const argp_child children[] = {
|
||||
{ &finput_argp, 0, nullptr, 10 },
|
||||
{ &output_argp, 0, nullptr, 20 },
|
||||
{ &misc_argp, 0, nullptr, -1 },
|
||||
{ &output_argp, 0, nullptr, 0 },
|
||||
{ &misc_argp, 0, nullptr, 0 },
|
||||
{ nullptr, 0, nullptr, 0 }
|
||||
};
|
||||
|
||||
|
|
|
|||
|
|
@ -62,27 +62,35 @@ enum solver
|
|||
|
||||
static const argp_option options[] =
|
||||
{
|
||||
{ "algo", OPT_ALGO, "ALGO", 0,
|
||||
"choose the parity game algorithm, valid ones are rec (Zielonka's"
|
||||
" recursive algorithm, default) and qp (Calude et al.'s quasi-polynomial"
|
||||
" time algorithm)", 0 },
|
||||
/**************************************************/
|
||||
{ nullptr, 0, nullptr, 0, "Input options:", 1 },
|
||||
{ "input", OPT_INPUT, "PROPS", 0,
|
||||
"comma-separated list of uncontrollable (a.k.a. input) atomic"
|
||||
" propositions", 0},
|
||||
{ "output", OPT_OUTPUT, "PROPS", 0,
|
||||
"comma-separated list of controllable (a.k.a. output) atomic"
|
||||
" propositions", 0},
|
||||
/**************************************************/
|
||||
{ nullptr, 0, nullptr, 0, "Fine tuning:", 10 },
|
||||
{ "algo", OPT_ALGO, "ALGO", 0,
|
||||
"choose the parity game algorithm, valid ones are rec (Zielonka's"
|
||||
" recursive algorithm, default) and qp (Calude et al.'s quasi-polynomial"
|
||||
" time algorithm)", 0 },
|
||||
/**************************************************/
|
||||
{ nullptr, 0, nullptr, 0, "Output options:", 20 },
|
||||
{ "print-pg", OPT_PRINT, nullptr, 0,
|
||||
"print the parity game in the pgsolver format, do not solve it", 0},
|
||||
{ "realizability", OPT_REAL, nullptr, 0,
|
||||
"realizability only, do not synthesize the circuit", 0},
|
||||
/**************************************************/
|
||||
{ nullptr, 0, nullptr, 0, "Miscellaneous options:", -1 },
|
||||
{ nullptr, 0, nullptr, 0, nullptr, 0 },
|
||||
};
|
||||
|
||||
const struct argp_child children[] =
|
||||
{
|
||||
{ &finput_argp, 0, nullptr, 1 },
|
||||
{ &misc_argp, 0, nullptr, -1 },
|
||||
{ &finput_argp_headless, 0, nullptr, 0 },
|
||||
{ &misc_argp, 0, nullptr, 0 },
|
||||
{ nullptr, 0, nullptr, 0 }
|
||||
};
|
||||
|
||||
|
|
|
|||
|
|
@ -128,7 +128,7 @@ static const struct argp_child children[] =
|
|||
{
|
||||
{ &aoutput_argp, 0, nullptr, 3 },
|
||||
{ &aoutput_o_format_argp, 0, nullptr, 4 },
|
||||
{ &misc_argp, 0, nullptr, -1 },
|
||||
{ &misc_argp, 0, nullptr, 0 },
|
||||
{ nullptr, 0, nullptr, 0 }
|
||||
};
|
||||
|
||||
|
|
|
|||
|
|
@ -120,6 +120,7 @@ static const argp_option options[] =
|
|||
{ "%%", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
|
||||
"a single %", 0 },
|
||||
COMMON_LTL_OUTPUT_SPECS,
|
||||
/**************************************************/
|
||||
{ nullptr, 0, nullptr, 0, "Miscellaneous options:", -1 },
|
||||
{ nullptr, 0, nullptr, 0, nullptr, 0 }
|
||||
};
|
||||
|
|
@ -127,8 +128,8 @@ static const argp_option options[] =
|
|||
|
||||
const struct argp_child children[] =
|
||||
{
|
||||
{ &output_argp, 0, nullptr, -20 },
|
||||
{ &misc_argp, 0, nullptr, -1 },
|
||||
{ &output_argp, 0, nullptr, 0 },
|
||||
{ &misc_argp, 0, nullptr, 0 },
|
||||
{ nullptr, 0, nullptr, 0 }
|
||||
};
|
||||
|
||||
|
|
|
|||
|
|
@ -76,6 +76,21 @@ do
|
|||
exit_status=2
|
||||
fi
|
||||
esac
|
||||
|
||||
# Check --help text. Set a high rmargin to workaround some
|
||||
# bug in argp where an extra line it sometimes added if the end
|
||||
# of the document string fall right into the rmargin.
|
||||
ARGP_HELP_FMT=rmargin=10000 \
|
||||
$top_builddir/bin/$binary --help > help-$binary.tmp
|
||||
if ! perl -ne '/\n\s*\n(\s*-.*\n)/ && print("$1") && exit(1)' \
|
||||
-0777 help-$binary.tmp > help-err
|
||||
then
|
||||
echo "bin/$binary --help has options after blank line;" \
|
||||
"missing section header?"
|
||||
cat help-err
|
||||
fi
|
||||
rm -f help-$binary.tmp help-err
|
||||
|
||||
done
|
||||
|
||||
exit $exit_status
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue