diff --git a/NEWS b/NEWS index 2d64b20dc..54402e77a 100644 --- a/NEWS +++ b/NEWS @@ -34,6 +34,8 @@ New in spot 2.4.1.dev (not yet released) - ltlsynt is a new tool for synthesizing AIGER circuits from LTL/PSL formulas. + - ltldo learned to limit the number of automata it outputs using -n. + Library: - Rename three methods of spot::scc_info. New names are clearer. The diff --git a/bin/ltldo.cc b/bin/ltldo.cc index 159e56b5e..e99d7d29c 100644 --- a/bin/ltldo.cc +++ b/bin/ltldo.cc @@ -57,10 +57,12 @@ enum { static const argp_option options[] = { + /**************************************************/ { nullptr, 0, nullptr, 0, "Error handling:", 4 }, { "errors", OPT_ERRORS, "abort|warn|ignore", 0, "how to deal with tools returning with non-zero exit codes or " "automata that ltldo cannot parse (default: abort)", 0 }, + /**************************************************/ { nullptr, 0, nullptr, 0, "Output selection:", 5 }, { "smallest", OPT_SMALLEST, "FORMAT", OPTION_ARG_OPTIONAL, "for each formula select the smallest automaton given by all " @@ -68,6 +70,8 @@ static const argp_option options[] = { "greatest", OPT_GREATEST, "FORMAT", OPTION_ARG_OPTIONAL, "for each formula select the greatest automaton given by all " "translators, using FORMAT for ordering (default is %s,%e)", 0 }, + { "max-count", 'n', "NUM", 0, "output at most NUM automata", 0 }, + /**************************************************/ { nullptr, 0, nullptr, 0, "Miscellaneous options:", -1 }, { nullptr, 0, nullptr, 0, nullptr, 0 } }; @@ -121,6 +125,7 @@ static errors_type errors_opt; static int best_type = 0; // -1 smallest, 1 greatest, 0 no selection static const char* best_format = "%s,%e"; +static int opt_max_count = -1; static char const *const errors_args[] = { @@ -167,6 +172,9 @@ parse_opt(int key, char* arg, struct argp_state*) if (arg) best_format = arg; break; + case 'n': + opt_max_count = to_pos_int(arg); + break; case ARGP_KEY_ARG: if (arg[0] == '-' && !arg[1]) jobs.emplace_back(arg, true); @@ -318,6 +326,19 @@ namespace return 0; } + void output_aut(const spot::twa_graph_ptr& aut, + spot::process_timer& ptimer, + spot::formula f, + const char* filename, int loc, + const char* csv_prefix, const char* csv_suffix) + { + static long int output_count = 0; + ++output_count; + printer.print(aut, ptimer, f, filename, loc, nullptr, + csv_prefix, csv_suffix); + if (opt_max_count >= 0 && output_count >= opt_max_count) + abort_run = true; + } int process_formula(spot::formula f, @@ -385,17 +406,18 @@ namespace } else { - printer.print(aut, timer, f, filename, linenum, - nullptr, prefix, suffix); + output_aut(aut, timer, f, filename, linenum, + prefix, suffix); + if (abort_run) + break; } } } if (best_aut) { cmdname = best_cmdname; - printer.print(best_aut, best_timer, - f, filename, linenum, - nullptr, prefix, suffix); + output_aut(best_aut, best_timer, f, filename, linenum, + prefix, suffix); } spot::cleanup_tmpfiles(); diff --git a/tests/core/ltldo.test b/tests/core/ltldo.test index aeaa15c0f..36e5e45d2 100755 --- a/tests/core/ltldo.test +++ b/tests/core/ltldo.test @@ -148,6 +148,10 @@ $ltldo '{name} foo/bar/ltl2baextended' -f GFa 2>stderr && exit 1 grep 'error:.*foo/bar/ltl2baextended -f .*>.*' stderr +test 2 = `genltl --and-gf=1..4 | ltldo ltl2tgba -n2 | autfilt -c` +test 3 = `genltl --and-gf=1..2 | ltldo ltl2tgba 'ltl2tgba -s' -n3 | autfilt -c` + + genltl --rv-counter=9 | ltldo ltl2tgba --stats=' print("%[up]R + %[uc]R + %[sp]R + %[sc]R - %R\n"); die if abs(%[up]R + %[uc]R + %[sp]R + %[sc]R - %R) > 0.02;' > code.pl