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.
This commit is contained in:
Thibaud Michaud
parent
176878554e
commit
a989d41b3f
3 changed files with 79 additions and 4 deletions
|
|
@ -22,6 +22,8 @@
|
|||
#include <string>
|
||||
#include <iostream>
|
||||
#include <limits>
|
||||
#include <set>
|
||||
#include <memory>
|
||||
|
||||
#include <argp.h>
|
||||
#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<std::vector<tr_t>> 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<spot::isomorphism_checker> isomorphism_checker = nullptr;
|
||||
static std::unique_ptr<spot::isomorphism_checker>
|
||||
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<unique_aut_t> 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<int>::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<int>::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<unique_aut_t>(new std::set<std::vector<tr_t>>());
|
||||
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)
|
||||
|
|
|
|||
|
|
@ -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<std::vector<tr_t>> 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<unique_aut_t> 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<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.
|
||||
|
|
@ -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<tr_t> 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)
|
||||
|
|
|
|||
35
src/tgbatest/uniq.test
Executable file
35
src/tgbatest/uniq.test
Executable file
|
|
@ -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 <http://www.gnu.org/licenses/>.
|
||||
|
||||
. ./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
|
||||
Loading…
Add table
Add a link
Reference in a new issue