From 69daf9c261db614711ac73da775a49e1a55dc81f Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 26 Sep 2017 21:28:16 +0200 Subject: [PATCH] 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. --- bin/README | 7 +++++++ bin/autcross.cc | 13 +++++++++---- bin/common_color.cc | 2 +- bin/common_finput.cc | 15 ++++++++++----- bin/common_finput.hh | 5 +++-- bin/genltl.cc | 5 +++-- bin/ltlcross.cc | 10 ++++++---- bin/ltlfilt.cc | 5 +++-- bin/ltlgrind.cc | 14 ++++++++------ bin/ltlsynt.cc | 20 ++++++++++++++------ bin/randaut.cc | 2 +- bin/randltl.cc | 5 +++-- tests/sanity/bin.test | 15 +++++++++++++++ 13 files changed, 83 insertions(+), 35 deletions(-) diff --git a/bin/README b/bin/README index 63d6ac607..84f574a55 100644 --- a/bin/README +++ b/bin/README @@ -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. diff --git a/bin/autcross.cc b/bin/autcross.cc index 78b3c6000..15a12ed09 100644 --- a/bin/autcross.cc +++ b/bin/autcross.cc @@ -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 } }; diff --git a/bin/common_color.cc b/bin/common_color.cc index b25f9cb0e..7b6330356 100644 --- a/bin/common_color.cc +++ b/bin/common_color.cc @@ -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 } }; diff --git a/bin/common_finput.cc b/bin/common_finput.cc index f2f3ef22d..79900f386 100644 --- a/bin/common_finput.cc +++ b/bin/common_finput.cc @@ -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*) { diff --git a/bin/common_finput.hh b/bin/common_finput.hh index 41eaa0216..54f31458a 100644 --- a/bin/common_finput.hh +++ b/bin/common_finput.hh @@ -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); diff --git a/bin/genltl.cc b/bin/genltl.cc index a93572727..edf79607f 100644 --- a/bin/genltl.cc +++ b/bin/genltl.cc @@ -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 } }; diff --git a/bin/ltlcross.cc b/bin/ltlcross.cc index f6c1f1b3a..d75a6ff21 100644 --- a/bin/ltlcross.cc +++ b/bin/ltlcross.cc @@ -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 } }; diff --git a/bin/ltlfilt.cc b/bin/ltlfilt.cc index 3513af238..1c07612d2 100644 --- a/bin/ltlfilt.cc +++ b/bin/ltlfilt.cc @@ -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 } }; diff --git a/bin/ltlgrind.cc b/bin/ltlgrind.cc index 4676dd8d2..10cc6e24a 100644 --- a/bin/ltlgrind.cc +++ b/bin/ltlgrind.cc @@ -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 } }; diff --git a/bin/ltlsynt.cc b/bin/ltlsynt.cc index 0d31bf67f..de03ec43d 100644 --- a/bin/ltlsynt.cc +++ b/bin/ltlsynt.cc @@ -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 } }; diff --git a/bin/randaut.cc b/bin/randaut.cc index e4dc0cb03..38b9e8b5b 100644 --- a/bin/randaut.cc +++ b/bin/randaut.cc @@ -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 } }; diff --git a/bin/randltl.cc b/bin/randltl.cc index 3d27e5b31..8da179e8e 100644 --- a/bin/randltl.cc +++ b/bin/randltl.cc @@ -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 } }; diff --git a/tests/sanity/bin.test b/tests/sanity/bin.test index 5f35f4a40..f51e06b9a 100644 --- a/tests/sanity/bin.test +++ b/tests/sanity/bin.test @@ -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