autfilt: easier simplification defaults
This is motivated by an email from Fanda. * src/bin/common_post.cc, src/bin/common_post.hh: Add variables to detect when level or pref are sets. * src/bin/autfilt.cc: Adjust default for pref/sets. * src/tests/readsave.test: Add test cases. * NEWS: Mention it.
This commit is contained in:
parent
2ae1b6a6f0
commit
e3682a2301
5 changed files with 40 additions and 2 deletions
8
NEWS
8
NEWS
|
|
@ -5,6 +5,14 @@ New in spot 1.99.4a (not yet released)
|
||||||
* autfilt has gained a --complement option.
|
* autfilt has gained a --complement option.
|
||||||
It currently work only for deterministic automata.
|
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:
|
Library:
|
||||||
|
|
||||||
* Rename dtgba_complement() as dtwa_complement(), rename the header
|
* Rename dtgba_complement() as dtwa_complement(), rename the header
|
||||||
|
|
|
||||||
|
|
@ -210,6 +210,14 @@ static const argp_option options[] =
|
||||||
{ "acc-sets", OPT_ACC_SETS, "RANGE", 0,
|
{ "acc-sets", OPT_ACC_SETS, "RANGE", 0,
|
||||||
"keep automata whose number of acceptance sets are in RANGE", 0 },
|
"keep automata whose number of acceptance sets are in RANGE", 0 },
|
||||||
RANGE_DOC_FULL,
|
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 },
|
{ nullptr, 0, nullptr, 0, "Miscellaneous options:", -1 },
|
||||||
{ "extra-options", 'x', "OPTS", 0,
|
{ "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))
|
if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, nullptr, nullptr))
|
||||||
exit(err);
|
exit(err);
|
||||||
|
|
||||||
|
if (level_set && !pref_set)
|
||||||
|
pref = spot::postprocessor::Small;
|
||||||
|
if (pref_set && !level_set)
|
||||||
|
level = spot::postprocessor::High;
|
||||||
|
|
||||||
if (jobs.empty())
|
if (jobs.empty())
|
||||||
jobs.emplace_back("-", true);
|
jobs.emplace_back("-", true);
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -27,6 +27,9 @@ spot::postprocessor::output_pref comp = spot::postprocessor::Any;
|
||||||
spot::postprocessor::output_pref sbacc = spot::postprocessor::Any;
|
spot::postprocessor::output_pref sbacc = spot::postprocessor::Any;
|
||||||
spot::postprocessor::optimization_level level = spot::postprocessor::High;
|
spot::postprocessor::optimization_level level = spot::postprocessor::High;
|
||||||
|
|
||||||
|
bool level_set = false;
|
||||||
|
bool pref_set = false;
|
||||||
|
|
||||||
enum {
|
enum {
|
||||||
OPT_HIGH = 1,
|
OPT_HIGH = 1,
|
||||||
OPT_LOW,
|
OPT_LOW,
|
||||||
|
|
@ -63,7 +66,7 @@ static const argp_option options_disabled[] =
|
||||||
{ "small", OPT_SMALL, nullptr, 0, "prefer small automata", 0 },
|
{ "small", OPT_SMALL, nullptr, 0, "prefer small automata", 0 },
|
||||||
{ "deterministic", 'D', nullptr, 0, "prefer deterministic automata", 0 },
|
{ "deterministic", 'D', nullptr, 0, "prefer deterministic automata", 0 },
|
||||||
{ "any", 'a', nullptr, 0, "no preference, do not bother making it small "
|
{ "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 "
|
{ "complete", 'C', nullptr, 0, "output a complete automaton (combine "
|
||||||
"with other intents)", 0 },
|
"with other intents)", 0 },
|
||||||
{ "state-based-acceptance", 'S', nullptr, 0,
|
{ "state-based-acceptance", 'S', nullptr, 0,
|
||||||
|
|
@ -71,7 +74,7 @@ static const argp_option options_disabled[] =
|
||||||
{ "sbacc", 0, nullptr, OPTION_ALIAS, nullptr, 0 },
|
{ "sbacc", 0, nullptr, OPTION_ALIAS, nullptr, 0 },
|
||||||
/**************************************************/
|
/**************************************************/
|
||||||
{ nullptr, 0, nullptr, 0, "Optimization level:", 21 },
|
{ 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 },
|
{ "medium", OPT_MEDIUM, nullptr, 0, "moderate optimizations", 0 },
|
||||||
{ "high", OPT_HIGH, nullptr, 0,
|
{ "high", OPT_HIGH, nullptr, 0,
|
||||||
"all available optimizations (slow)", 0 },
|
"all available optimizations (slow)", 0 },
|
||||||
|
|
@ -86,12 +89,14 @@ parse_opt_post(int key, char*, struct argp_state*)
|
||||||
{
|
{
|
||||||
case 'a':
|
case 'a':
|
||||||
pref = spot::postprocessor::Any;
|
pref = spot::postprocessor::Any;
|
||||||
|
pref_set = true;
|
||||||
break;
|
break;
|
||||||
case 'C':
|
case 'C':
|
||||||
comp = spot::postprocessor::Complete;
|
comp = spot::postprocessor::Complete;
|
||||||
break;
|
break;
|
||||||
case 'D':
|
case 'D':
|
||||||
pref = spot::postprocessor::Deterministic;
|
pref = spot::postprocessor::Deterministic;
|
||||||
|
pref_set = true;
|
||||||
break;
|
break;
|
||||||
case 'S':
|
case 'S':
|
||||||
sbacc = spot::postprocessor::SBAcc;
|
sbacc = spot::postprocessor::SBAcc;
|
||||||
|
|
@ -99,17 +104,21 @@ parse_opt_post(int key, char*, struct argp_state*)
|
||||||
case OPT_HIGH:
|
case OPT_HIGH:
|
||||||
level = spot::postprocessor::High;
|
level = spot::postprocessor::High;
|
||||||
simplification_level = 3;
|
simplification_level = 3;
|
||||||
|
level_set = true;
|
||||||
break;
|
break;
|
||||||
case OPT_LOW:
|
case OPT_LOW:
|
||||||
level = spot::postprocessor::Low;
|
level = spot::postprocessor::Low;
|
||||||
simplification_level = 1;
|
simplification_level = 1;
|
||||||
|
level_set = true;
|
||||||
break;
|
break;
|
||||||
case OPT_MEDIUM:
|
case OPT_MEDIUM:
|
||||||
level = spot::postprocessor::Medium;
|
level = spot::postprocessor::Medium;
|
||||||
simplification_level = 2;
|
simplification_level = 2;
|
||||||
|
level_set = true;
|
||||||
break;
|
break;
|
||||||
case OPT_SMALL:
|
case OPT_SMALL:
|
||||||
pref = spot::postprocessor::Small;
|
pref = spot::postprocessor::Small;
|
||||||
|
pref_set = true;
|
||||||
break;
|
break;
|
||||||
default:
|
default:
|
||||||
return ARGP_ERR_UNKNOWN;
|
return ARGP_ERR_UNKNOWN;
|
||||||
|
|
|
||||||
|
|
@ -31,3 +31,7 @@ extern spot::postprocessor::output_pref pref;
|
||||||
extern spot::postprocessor::output_pref comp;
|
extern spot::postprocessor::output_pref comp;
|
||||||
extern spot::postprocessor::output_pref sbacc;
|
extern spot::postprocessor::output_pref sbacc;
|
||||||
extern spot::postprocessor::optimization_level level;
|
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;
|
||||||
|
|
|
||||||
|
|
@ -715,6 +715,8 @@ State: 2 {0 1} [0] 2
|
||||||
EOF
|
EOF
|
||||||
|
|
||||||
$autfilt -H --small --high input4 >output4
|
$autfilt -H --small --high input4 >output4
|
||||||
|
$autfilt -H --small input4 >output4b
|
||||||
|
$autfilt -H --high input4 >output4c
|
||||||
cat output4
|
cat output4
|
||||||
|
|
||||||
cat >expect4<<EOF
|
cat >expect4<<EOF
|
||||||
|
|
@ -737,3 +739,5 @@ State: 2 {0}
|
||||||
EOF
|
EOF
|
||||||
|
|
||||||
diff output4 expect4
|
diff output4 expect4
|
||||||
|
diff output4b expect4
|
||||||
|
diff output4c expect4
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue