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

ltlsynt: fix documentation of --aiger option

Browse source 
* bin/ltlsynt.cc: Here.
This commit is contained in:
Alexandre Duret-Lutz 2022-09-14 11:29:18 +02:00
parent b3b22388c9
commit ef0aeed228
1 changed files with 5 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

10
bin/ltlsynt.cc
View file

@ -114,13 +114,13 @@ static const argp_option options[] =
"realizability only, do not compute a winning strategy", 0}, "realizability only, do not compute a winning strategy", 0},
{ "aiger", OPT_PRINT_AIGER, "ite|isop|both[+ud][+dc]" { "aiger", OPT_PRINT_AIGER, "ite|isop|both[+ud][+dc]"
"[+sub0|sub1|sub2]", OPTION_ARG_OPTIONAL, "[+sub0|sub1|sub2]", OPTION_ARG_OPTIONAL,
"prints a winning strategy as an AIGER circuit. The first, and only " "prints a winning strategy as an AIGER circuit. The first word "
"mandatory option defines the method to be used. \"ite\" for " "indicates the encoding to used: \"ite\" for "
"If-then-else normal form; " "If-Then-Else normal form; "
"\"isop\" for irreducible sum of producs; " "\"isop\" for irreducible sum of producs; "
"\"both\" tries both encodings and keeps the smaller one. " "\"both\" tries both and keeps the smaller one. "
"The other options further " "The other options further "
"refine the encoding, see aiger::encode_bdd.", 0}, "refine the encoding, see aiger::encode_bdd. Defaults to \"ite\".", 0},
{ "verbose", OPT_VERBOSE, nullptr, 0, { "verbose", OPT_VERBOSE, nullptr, 0,
"verbose mode", -1 }, "verbose mode", -1 },
{ "verify", OPT_VERIFY, nullptr, 0, { "verify", OPT_VERIFY, nullptr, 0,