diff --git a/NEWS b/NEWS index 62e6d647e..2711f5dc5 100644 --- a/NEWS +++ b/NEWS @@ -5,6 +5,14 @@ New in spot 1.99.4a (not yet released) * autfilt has gained a --complement option. It currently work only for deterministic automata. + * By default, autfilt does not simplify automata (this has not + changed), as if the --low --any options where used. But now, if + one of --small, --deterministic, or --any is given, the + optimization level automatically defaults to --high (unless + specified otherwise). For symmetry, if one of --low, --medium, or + --high is given, thn the translation intent defaults to --small + (unless specified otherwise). + Library: * Rename dtgba_complement() as dtwa_complement(), rename the header diff --git a/src/bin/autfilt.cc b/src/bin/autfilt.cc index 9ef68a3b2..c890e2721 100644 --- a/src/bin/autfilt.cc +++ b/src/bin/autfilt.cc @@ -210,6 +210,14 @@ static const argp_option options[] = { "acc-sets", OPT_ACC_SETS, "RANGE", 0, "keep automata whose number of acceptance sets are in RANGE", 0 }, RANGE_DOC_FULL, + { nullptr, 0, nullptr, 0, + "If any option among --small, --deterministic, or --any is given, " + "then the optimization level defaults to --high unless specified " + "otherwise. If any option among --low, --medium, or --high is given, " + "then the translation intent defaults to --small unless specified " + "otherwise. If none of those options are specified, then autfilt " + "acts as is --any --low were given: these actually disable the " + "simplification routines.", 22 }, /**************************************************/ { nullptr, 0, nullptr, 0, "Miscellaneous options:", -1 }, { "extra-options", 'x', "OPTS", 0, @@ -714,6 +722,11 @@ main(int argc, char** argv) if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, nullptr, nullptr)) exit(err); + if (level_set && !pref_set) + pref = spot::postprocessor::Small; + if (pref_set && !level_set) + level = spot::postprocessor::High; + if (jobs.empty()) jobs.emplace_back("-", true); diff --git a/src/bin/common_post.cc b/src/bin/common_post.cc index 0acfc79f4..89568f8ff 100644 --- a/src/bin/common_post.cc +++ b/src/bin/common_post.cc @@ -27,6 +27,9 @@ spot::postprocessor::output_pref comp = spot::postprocessor::Any; spot::postprocessor::output_pref sbacc = spot::postprocessor::Any; spot::postprocessor::optimization_level level = spot::postprocessor::High; +bool level_set = false; +bool pref_set = false; + enum { OPT_HIGH = 1, OPT_LOW, @@ -63,7 +66,7 @@ static const argp_option options_disabled[] = { "small", OPT_SMALL, nullptr, 0, "prefer small automata", 0 }, { "deterministic", 'D', nullptr, 0, "prefer deterministic automata", 0 }, { "any", 'a', nullptr, 0, "no preference, do not bother making it small " - "or deterministic (default)", 0 }, + "or deterministic", 0 }, { "complete", 'C', nullptr, 0, "output a complete automaton (combine " "with other intents)", 0 }, { "state-based-acceptance", 'S', nullptr, 0, @@ -71,7 +74,7 @@ static const argp_option options_disabled[] = { "sbacc", 0, nullptr, OPTION_ALIAS, nullptr, 0 }, /**************************************************/ { nullptr, 0, nullptr, 0, "Optimization level:", 21 }, - { "low", OPT_LOW, nullptr, 0, "minimal optimizations (fast, default)", 0 }, + { "low", OPT_LOW, nullptr, 0, "minimal optimizations (fast)", 0 }, { "medium", OPT_MEDIUM, nullptr, 0, "moderate optimizations", 0 }, { "high", OPT_HIGH, nullptr, 0, "all available optimizations (slow)", 0 }, @@ -86,12 +89,14 @@ parse_opt_post(int key, char*, struct argp_state*) { case 'a': pref = spot::postprocessor::Any; + pref_set = true; break; case 'C': comp = spot::postprocessor::Complete; break; case 'D': pref = spot::postprocessor::Deterministic; + pref_set = true; break; case 'S': sbacc = spot::postprocessor::SBAcc; @@ -99,17 +104,21 @@ parse_opt_post(int key, char*, struct argp_state*) case OPT_HIGH: level = spot::postprocessor::High; simplification_level = 3; + level_set = true; break; case OPT_LOW: level = spot::postprocessor::Low; simplification_level = 1; + level_set = true; break; case OPT_MEDIUM: level = spot::postprocessor::Medium; simplification_level = 2; + level_set = true; break; case OPT_SMALL: pref = spot::postprocessor::Small; + pref_set = true; break; default: return ARGP_ERR_UNKNOWN; diff --git a/src/bin/common_post.hh b/src/bin/common_post.hh index 2d0d73c1f..31443d8c9 100644 --- a/src/bin/common_post.hh +++ b/src/bin/common_post.hh @@ -31,3 +31,7 @@ extern spot::postprocessor::output_pref pref; extern spot::postprocessor::output_pref comp; extern spot::postprocessor::output_pref sbacc; extern spot::postprocessor::optimization_level level; +// True if --low, --medium, or --high has been given +extern bool level_set; +// True if --any, --small, or --deterministic has been given +extern bool pref_set; diff --git a/src/tests/readsave.test b/src/tests/readsave.test index 01912d4ab..5abfcee16 100755 --- a/src/tests/readsave.test +++ b/src/tests/readsave.test @@ -715,6 +715,8 @@ State: 2 {0 1} [0] 2 EOF $autfilt -H --small --high input4 >output4 +$autfilt -H --small input4 >output4b +$autfilt -H --high input4 >output4c cat output4 cat >expect4<