Commit 21dcc73d authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

randaut: fix --uniq

* src/bin/autfilt.cc: Also accept '-u' for '--uniq'.
* src/bin/randaut.cc: Likewise, plus fix the unicity check.
* src/tgbatest/uniq.test: Really test it.
parent 36f99565
......@@ -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<unique_aut_t>(new std::set<std::vector<tr_t>>());
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<unique_aut_t>(new std::set<std::vector<tr_t>>());
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)
......
......@@ -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<unique_aut_t>(new std::set<std::vector<tr_t>>());
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<unique_aut_t>(new std::set<std::vector<tr_t>>());
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<tr_t> 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)
......
......@@ -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 <<EOF
[!0&!1] 0
[!0&1] 0
[0&!1] 0
[0&1] 0
EOF
diff out expected
# This should fail: the random automaton generator can only generate 4
# different one-state automaton with two atomic propositions.
../../bin/randaut -Hl -u -n 5 -S1 a b >out 2>stderr && exit 1
test $? = 2
grep 'failed to generate a new unique automaton' stderr
test 4 = `wc -l < out`
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment