diff --git a/src/bin/autfilt.cc b/src/bin/autfilt.cc index b8b26f7f0..40e323da7 100644 --- a/src/bin/autfilt.cc +++ b/src/bin/autfilt.cc @@ -77,7 +77,6 @@ Exit status:\n\ #define OPT_DESTUT 22 #define OPT_INSTUT 23 #define OPT_IS_EMPTY 24 -#define OPT_UNIQ 25 static const argp_option options[] = { @@ -164,7 +163,7 @@ static const argp_option options[] = { 0, 0, 0, 0, "Filters:", 6 }, { "are-isomorphic", OPT_ARE_ISOMORPHIC, "FILENAME", 0, "keep automata that are isomorphic to the automaton in FILENAME", 0 }, - { "uniq", OPT_UNIQ, 0, 0, + { "uniq", 'u', 0, 0, "do not output the same automaton twice (same in the sense that they "\ "are isomorphic)", 0 }, { "isomorphic", 0, 0, OPTION_ALIAS | OPTION_HIDDEN, 0, 0 }, @@ -279,6 +278,10 @@ parse_opt(int key, char* arg, struct argp_state*) if (type != spot::postprocessor::Monitor) type = spot::postprocessor::BA; break; + case 'u': + opt_uniq = + std::unique_ptr(new std::set>()); + break; case 'v': opt_invert = true; break; @@ -401,10 +404,6 @@ parse_opt(int key, char* arg, struct argp_state*) error(2, 0, "--spin and --tgba are incompatible"); type = spot::postprocessor::TGBA; break; - case OPT_UNIQ: - opt_uniq = - std::unique_ptr(new std::set>()); - break; case ARGP_KEY_ARG: jobs.emplace_back(arg, true); break; @@ -470,14 +469,6 @@ namespace matched &= isomorphism_checker->is_isomorphic(aut); if (opt_is_empty) matched &= aut->is_empty(); - if (opt_uniq) - { - auto tmp = - spot::canonicalize(make_tgba_digraph(aut, - spot::tgba::prop_set::all())); - matched = opt_uniq->emplace(tmp->transition_vector().begin() + 1, - tmp->transition_vector().end()).second; - } // Drop or keep matched automata depending on the --invert option if (matched == opt_invert) @@ -502,6 +493,16 @@ namespace const double conversion_time = sw.stop(); + if (opt_uniq) + { + auto tmp = + spot::canonicalize(make_tgba_digraph(aut, + spot::tgba::prop_set::all())); + if (!opt_uniq->emplace(tmp->transition_vector().begin() + 1, + tmp->transition_vector().end()).second) + return 0; + } + printer.print(aut, filename, conversion_time, haut); if (opt_max_count >= 0 && match_count >= opt_max_count) diff --git a/src/bin/randaut.cc b/src/bin/randaut.cc index 37e79d14e..1e0d08c41 100644 --- a/src/bin/randaut.cc +++ b/src/bin/randaut.cc @@ -67,7 +67,6 @@ states, 1 to 3 acceptance sets, and three atomic propositions:\n\ #define OPT_LBTT 3 #define OPT_SEED 4 #define OPT_STATE_ACC 5 -#define OPT_UNIQ 6 static const argp_option options[] = { @@ -83,7 +82,7 @@ static const argp_option options[] = { "density", 'd', "FLOAT", 0, "density of the transitions (0.2)", 0 }, { "deterministic", 'D', 0, 0, "build a complete, deterministic automaton ", 0 }, - { "uniq", OPT_UNIQ, 0, 0, + { "uniq", 'u', 0, 0, "do not output the same automaton twice (same in the sense that they "\ "are isomorphic)", 0 }, { "seed", OPT_SEED, "INT", 0, @@ -212,6 +211,10 @@ parse_opt(int key, char* arg, struct argp_state* as) if (opt_states.min > opt_states.max) std::swap(opt_states.min, opt_states.max); break; + case 'u': + opt_uniq = + std::unique_ptr(new std::set>()); + break; case OPT_DOT: format = Dot; opt_dot = arg; @@ -235,9 +238,6 @@ parse_opt(int key, char* arg, struct argp_state* as) case OPT_STATE_ACC: opt_state_acc = true; break; - case OPT_UNIQ: - opt_uniq = - std::unique_ptr(new std::set>()); case ARGP_KEY_ARG: // If this is the unique non-option argument, it can // be a number of atomic propositions to build. @@ -294,7 +294,10 @@ main(int argc, char** argv) spot::srand(opt_seed); auto d = spot::make_bdd_dict(); - while (opt_automata < 0 || opt_automata--) + constexpr unsigned max_trials = 10000; + unsigned trials = max_trials; + + while (opt_automata) { int size = opt_states.min; if (size != opt_states.max) @@ -316,10 +319,20 @@ main(int argc, char** argv) spot::tgba::prop_set::all())); std::vector trans(tmp->transition_vector().begin() + 1, tmp->transition_vector().end()); - if (opt_uniq->emplace(trans).second) - return 0; + if (!opt_uniq->emplace(trans).second) + { + --trials; + if (trials == 0) + error(2, 0, "failed to generate a new unique automaton" + " after %d trials", max_trials); + continue; + } + trials = max_trials; } + if (opt_automata > 0) + --opt_automata; + bool is_ba = accs == 0 || (accs == 1 && opt_state_acc); switch (format) diff --git a/src/tgbatest/uniq.test b/src/tgbatest/uniq.test index 91915a3c1..779feb5fc 100755 --- a/src/tgbatest/uniq.test +++ b/src/tgbatest/uniq.test @@ -33,3 +33,21 @@ cat aut1 aut2 > aut cat aut1 aut2 rand11 rand12 rand13 rand21 rand22 rand23 > all ../../bin/autfilt all --uniq --hoa > out diff aut out + + +run 0 ../../bin/randaut -Hl -u -n 4 -S1 a b | sort | + ../../bin/autfilt -H | grep '&' > out +cat >expected <out 2>stderr && exit 1 +test $? = 2 +grep 'failed to generate a new unique automaton' stderr +test 4 = `wc -l < out`