From ef0aeed22844bd58041c6a1e9e4c3ba9422eb7eb Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 14 Sep 2022 11:29:18 +0200 Subject: [PATCH] ltlsynt: fix documentation of --aiger option * bin/ltlsynt.cc: Here. --- bin/ltlsynt.cc | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/bin/ltlsynt.cc b/bin/ltlsynt.cc index 06c29db88..1779211ef 100644 --- a/bin/ltlsynt.cc +++ b/bin/ltlsynt.cc @@ -114,13 +114,13 @@ static const argp_option options[] = "realizability only, do not compute a winning strategy", 0}, { "aiger", OPT_PRINT_AIGER, "ite|isop|both[+ud][+dc]" "[+sub0|sub1|sub2]", OPTION_ARG_OPTIONAL, - "prints a winning strategy as an AIGER circuit. The first, and only " - "mandatory option defines the method to be used. \"ite\" for " - "If-then-else normal form; " + "prints a winning strategy as an AIGER circuit. The first word " + "indicates the encoding to used: \"ite\" for " + "If-Then-Else normal form; " "\"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 " - "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 mode", -1 }, { "verify", OPT_VERIFY, nullptr, 0,