From a989d41b3fcebc1ecd998ee8974e146d4bae84ae Mon Sep 17 00:00:00 2001 From: Thibaud Michaud Date: Wed, 17 Dec 2014 05:01:26 +0100 Subject: [PATCH] option --uniq in autfilt and randaut * src/bin/autfilt.cc: add option --uniq. * src/bin/randaut.cc: add option --uniq. * src/tgbatest/uniq.test: Test it. --- src/bin/autfilt.cc | 28 ++++++++++++++++++++++++---- src/bin/randaut.cc | 20 ++++++++++++++++++++ src/tgbatest/uniq.test | 35 +++++++++++++++++++++++++++++++++++ 3 files changed, 79 insertions(+), 4 deletions(-) create mode 100755 src/tgbatest/uniq.test diff --git a/src/bin/autfilt.cc b/src/bin/autfilt.cc index 14ca7b335..7f45dbf11 100644 --- a/src/bin/autfilt.cc +++ b/src/bin/autfilt.cc @@ -22,6 +22,8 @@ #include #include #include +#include +#include #include #include "error.h" @@ -84,6 +86,7 @@ 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[] = { @@ -167,6 +170,9 @@ 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, + "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 }, { "is-complete", OPT_IS_COMPLETE, 0, 0, "the automaton is complete", 0 }, @@ -200,6 +206,8 @@ static const struct argp_child children[] = static enum output_format { Dot, Lbtt, Lbtt_t, Spin, Spot, Stats, Hoa, Quiet, Count } format = Dot; +typedef spot::tgba_digraph::graph_t::trans_storage_t tr_t; +typedef std::set> unique_aut_t; static long int match_count = 0; static const char* stats = ""; static const char* hoa_opt = 0; @@ -210,7 +218,8 @@ static int opt_seed = 0; static auto dict = spot::make_bdd_dict(); static spot::tgba_digraph_ptr opt_product = nullptr; static bool opt_merge = false; -static std::unique_ptr isomorphism_checker = nullptr; +static std::unique_ptr + isomorphism_checker = nullptr; static spot::tgba_digraph_ptr opt_are_isomorphic = nullptr; static bool opt_is_complete = false; static bool opt_is_deterministic = false; @@ -223,6 +232,7 @@ static int opt_max_count = -1; static bool opt_destut = false; static bool opt_instut = false; static bool opt_is_empty = false; +static std::unique_ptr opt_uniq = nullptr; static int to_int(const char* s) @@ -289,9 +299,6 @@ parse_opt(int key, char* arg, struct argp_state*) error(2, 0, "failed to parse --options near '%s'", opt); } break; - case OPT_DOT: - format = Dot; - break; case OPT_ACC_SETS: opt_accsets = parse_range(arg, 0, std::numeric_limits::max()); break; @@ -305,6 +312,9 @@ parse_opt(int key, char* arg, struct argp_state*) opt_are_isomorphic = std::move(p->aut); break; } + case OPT_DOT: + format = Dot; + break; case OPT_EDGES: opt_edges = parse_range(arg, 0, std::numeric_limits::max()); break; @@ -400,6 +410,10 @@ 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; @@ -578,6 +592,12 @@ 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)); + 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) diff --git a/src/bin/randaut.cc b/src/bin/randaut.cc index ebe88c6d5..1a9b9eadd 100644 --- a/src/bin/randaut.cc +++ b/src/bin/randaut.cc @@ -40,6 +40,7 @@ #include "tgbaalgos/hoa.hh" #include "tgbaalgos/neverclaim.hh" #include "tgbaalgos/randomgraph.hh" +#include "tgbaalgos/canonicalize.hh" const char argp_program_doc[] = "\ @@ -66,6 +67,7 @@ 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[] = { @@ -81,6 +83,9 @@ 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, + "do not output the same automaton twice (same in the sense that they "\ + "are isomorphic)", 0 }, { "seed", OPT_SEED, "INT", 0, "seed for the random number generator (0)", 0 }, { "states", 'S', "RANGE", 0, "number of states to output (10)", 0 }, @@ -109,6 +114,8 @@ static const struct argp_child children[] = { 0, 0, 0, 0 } }; +typedef spot::tgba_digraph::graph_t::trans_storage_t tr_t; +typedef std::set> unique_aut_t; static enum output_format { Dot, Lbtt, Lbtt_t, Spin, Hoa } format = Dot; static const char* hoa_opt = 0; static spot::ltl::atomic_prop_set aprops; @@ -122,6 +129,7 @@ static float opt_acc_prob = 0.2; static bool opt_deterministic = false; static bool opt_state_acc = false; static bool ba_wanted = false; +static std::unique_ptr opt_uniq = nullptr; static int to_int(const char* s) @@ -222,6 +230,9 @@ 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. @@ -293,6 +304,15 @@ main(int argc, char** argv) accs, opt_acc_prob, 0.5, opt_deterministic, opt_state_acc); + if (opt_uniq) + { + auto tmp = make_tgba_digraph(spot::canonicalize(aut)); + std::vector trans(tmp->transition_vector().begin() + 1, + tmp->transition_vector().end()); + if (opt_uniq->emplace(trans).second) + return 0; + } + bool is_ba = accs == 0 || (accs == 1 && opt_state_acc); switch (format) diff --git a/src/tgbatest/uniq.test b/src/tgbatest/uniq.test new file mode 100755 index 000000000..91915a3c1 --- /dev/null +++ b/src/tgbatest/uniq.test @@ -0,0 +1,35 @@ +#!/bin/sh +# Copyright (C) 2012, 2014 Laboratoire de Recherche et Développement +# de l'Epita (LRDE). +# +# This file is part of Spot, a model checking library. +# +# Spot is free software; you can redistribute it and/or modify it +# under the terms of the GNU General Public License as published by +# the Free Software Foundation; either version 3 of the License, or +# (at your option) any later version. +# +# Spot is distributed in the hope that it will be useful, but WITHOUT +# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +# License for more details. +# +# You should have received a copy of the GNU General Public License +# along with this program. If not, see . + +. ./defs +set -e + +../../bin/randaut a b -S5 --hoa > aut1 +../../bin/randaut a b c -S10 --hoa > aut2 +../../bin/autfilt --randomize aut1 --hoa > rand11 +../../bin/autfilt --randomize --seed=1 aut1 --hoa > rand12 +../../bin/autfilt --randomize --seed=2 aut1 --hoa > rand13 +../../bin/autfilt --randomize aut2 --hoa > rand21 +../../bin/autfilt --randomize --seed=1 aut2 --hoa > rand22 +../../bin/autfilt --randomize --seed=2 aut2 --hoa > rand23 + +cat aut1 aut2 > aut +cat aut1 aut2 rand11 rand12 rand13 rand21 rand22 rand23 > all +../../bin/autfilt all --uniq --hoa > out +diff aut out