alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

ltlsynt: remove superfluous output options

Browse source 
No point in having options such as --spin, --lbtt, --check, etc.
Also --dot was documented twice...

* bin/ltlsynt.cc (children): Remove aoutput_argp.
(options): Add explicit support for -d, -H, -q.
* bin/common_aoutput.cc, bin/common_aoutput.hh: Share the HOA help
text.
This commit is contained in:
Alexandre Duret-Lutz 2025-02-07 21:26:08 +01:00
parent d0e404fec0
commit b1b06ef7bd
3 changed files with 33 additions and 20 deletions
Download patch file Download diff file Expand all files Collapse all files

26
bin/common_aoutput.cc
View file

@ -91,6 +91,19 @@ enum {
OPT_CHECK,
};
const char* hoa_option_doc_short = "1.1|b|i|k|l|m|s|t|v";
const char* hoa_option_doc_long =
"Output the automaton in HOA format (default). Add letters to select "
"(1.1) version 1.1 of the format, "
"(b) create an alias basis if >=2 AP are used, "
"(i) use implicit labels for complete deterministic automata, "
"(s) prefer state-based acceptance when possible [default], "
"(t) force transition-based acceptance, "
"(m) mix state and transition-based acceptance, "
"(k) use state labels when possible, "
"(l) single-line output, "
"(v) verbose properties";
static const argp_option options[] =
{
/**************************************************/
@ -129,17 +142,8 @@ static const argp_option options[] =
"(+INT) add INT to all set numbers, "
"(<INT) display at most INT states, "
"(#) show internal edge numbers", 0 },
{ "hoaf", 'H', "1.1|i|k|l|m|s|t|v", OPTION_ARG_OPTIONAL,
"Output the automaton in HOA format (default). Add letters to select "
"(1.1) version 1.1 of the format, "
"(b) create an alias basis if >=2 AP are used, "
"(i) use implicit labels for complete deterministic automata, "
"(s) prefer state-based acceptance when possible [default], "
"(t) force transition-based acceptance, "
"(m) mix state and transition-based acceptance, "
"(k) use state labels when possible, "
"(l) single-line output, "
"(v) verbose properties", 0 },
{ "hoaf", 'H', hoa_option_doc_short, OPTION_ARG_OPTIONAL,
hoa_option_doc_long, 0 },
{ "lbtt", OPT_LBTT, "t", OPTION_ARG_OPTIONAL,
"LBTT's format (add =t to force transition-based acceptance even"
" on Büchi automata)", 0 },

4
bin/common_aoutput.hh
View file

@ -52,6 +52,10 @@ extern const char* opt_name;
// Output options
extern const struct argp aoutput_argp;
// help text for --hoaf
extern const char* hoa_option_doc_short;
extern const char* hoa_option_doc_long;
// help text for %F and %L
extern char F_doc[32];
extern char L_doc[32];

23
bin/ltlsynt.cc
View file

@ -53,7 +53,6 @@ enum
OPT_CSV_WITH_FORMULA,
OPT_CSV_WITHOUT_FORMULA,
OPT_DECOMPOSE,
OPT_DOT,
OPT_FROM_PGAME,
OPT_GEQUIV,
OPT_HIDE,
@ -143,13 +142,15 @@ static const argp_option options[] =
"\"both\" tries both and keeps the smaller one. "
"Other options further "
"refine the encoding, see aiger::encode_bdd. Defaults to \"ite\".", 0 },
{ "dot", OPT_DOT, "options", OPTION_ARG_OPTIONAL,
{ "dot", 'd', "options", OPTION_ARG_OPTIONAL,
"Use dot format when printing the result (game, strategy, or "
"AIG circuit, depending on other options). The options that "
"may be passed to --dot depend on the nature of what is printed. "
"For games and strategies, standard automata rendering "
"options are supported (e.g., see ltl2tgba --dot). For AIG circuit, "
"use (h) for horizontal and (v) for vertical layouts.", 0 },
{ "hoaf", 'H', hoa_option_doc_short, OPTION_ARG_OPTIONAL,
hoa_option_doc_long, 0 },
{ "csv", OPT_CSV_WITHOUT_FORMULA, "[>>]FILENAME", OPTION_ARG_OPTIONAL,
"output statistics as CSV in FILENAME or on standard output "
"(if '>>' is used to request append mode, the header line is "
@ -159,8 +160,9 @@ static const argp_option options[] =
OPTION_ARG_OPTIONAL,
"like --csv, but with an additional 'fomula' column", 0 },
{ "hide-status", OPT_HIDE, nullptr, 0,
"Hide the REALIZABLE or UNREALIZABLE line. (Hint: exit status "
"hide the REALIZABLE or UNREALIZABLE line (The exit status "
"is enough of an indication.)", 0 },
{ "quiet", 'q', nullptr, 0, "suppress all normal output", 0 },
/**************************************************/
{ nullptr, 0, nullptr, 0, "Miscellaneous options:", -1 },
{ "extra-options", 'x', "OPTS", 0,
@ -174,7 +176,6 @@ static const argp_option options[] =
static const struct argp_child children[] =
{
{ &finput_argp_headless, 0, nullptr, 0 },
{ &aoutput_argp, 0, nullptr, 0 },
{ &misc_argp, 0, nullptr, 0 },
{ nullptr, 0, nullptr, 0 }
};
@ -1044,6 +1045,15 @@ parse_opt(int key, char *arg, struct argp_state *)
BEGIN_EXCEPTION_PROTECT;
switch (key)
{
case 'd':
opt_dot = true;
automaton_format_opt = opt_dot_arg = arg;
automaton_format = Dot;
break;
case 'q':
automaton_format = Quiet;
show_status = false;
break;
case OPT_ALGO:
gi->s = XARGMATCH("--algo", arg, algo_args, algo_types);
break;
@ -1062,11 +1072,6 @@ parse_opt(int key, char *arg, struct argp_state *)
opt_decompose_ltl = XARGMATCH("--decompose", arg,
decompose_args, decompose_values);
break;
case OPT_DOT:
opt_dot = true;
automaton_format_opt = opt_dot_arg = arg;
automaton_format = Dot;
break;
case OPT_FROM_PGAME:
jobs.emplace_back(arg, job_type::AUT_FILENAME);
break;