diff --git a/src/bin/autfilt.cc b/src/bin/autfilt.cc
index b5db0bfcb..db9cda1ae 100644
--- a/src/bin/autfilt.cc
+++ b/src/bin/autfilt.cc
@@ -44,6 +44,7 @@
#include "hoaparse/public.hh"
#include "tgbaalgos/sccinfo.hh"
#include "tgbaalgos/randomize.hh"
+#include "tgbaalgos/are_isomorphic.hh"
static const char argp_program_doc[] ="\
@@ -60,6 +61,7 @@ Convert, transform, and filter Büchi automata.\n\
#define OPT_SEED 7
#define OPT_PRODUCT 8
#define OPT_MERGE 9
+#define OPT_ISOMORPH 10
static const argp_option options[] =
{
@@ -127,6 +129,11 @@ static const argp_option options[] =
"randomize states and transitions (specify 's' or 't' to"
"randomize only states or transitions)", 0 },
/**************************************************/
+ { 0, 0, 0, 0, "Filter:", -1 },
+ { "isomorph", 'I', "FILENAME", 0,
+ "print only the automata that are isomorph to the automaton "\
+ "described in FILENAME", 0 },
+ /**************************************************/
{ 0, 0, 0, 0, "Miscellaneous options:", -1 },
{ "extra-options", 'x', "OPTS", 0,
"fine-tuning options (see spot-x (7))", 0 },
@@ -153,6 +160,7 @@ 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 spot::tgba_digraph_ptr opt_isomorph = nullptr;
static int
to_int(const char* s)
@@ -164,6 +172,24 @@ to_int(const char* s)
return res;
}
+// spot::tgba_digraph_ptr
+// hoa_parse(const char* filename)
+// {
+// spot::hoa_parse_error_list pel;
+// auto b = spot::make_bdd_dict();
+// auto hp = spot::hoa_stream_parser(filename);
+//
+// pel.clear();
+// auto haut = hp.parse(pel, b);
+// if (!haut && pel.empty())
+// error(2, 0, "no automaton to parse from %s", filename);
+// if (spot::format_hoa_parse_errors(std::cerr, filename, pel))
+// error(2, 0, "failed to parse automaton from %s", filename);;
+// if (!haut)
+// error(2, 0, "failed to read automaton from %s", filename);
+// return haut->aut;
+// }
+
static int
parse_opt(int key, char* arg, struct argp_state*)
{
@@ -183,6 +209,15 @@ parse_opt(int key, char* arg, struct argp_state*)
format = Hoa;
hoa_opt = arg;
break;
+ case 'I':
+ {
+ spot::hoa_parse_error_list pel;
+ auto p = hoa_parse(arg, pel, dict);
+ if (spot::format_hoa_parse_errors(std::cerr, arg, pel)
+ || !p || p->aborted)
+ error(2, 0, "failed to read automaton from %s", arg);
+ opt_isomorph = std::move(p->aut);
+ }
case 'M':
type = spot::postprocessor::Monitor;
break;
@@ -385,6 +420,9 @@ namespace
if (opt_product)
aut = spot::product(std::move(aut), opt_product);
+ if (opt_isomorph && !are_isomorphic(aut, opt_isomorph))
+ return 0;
+
aut = post.run(aut, nullptr);
if (randomize_st || randomize_tr)
@@ -450,7 +488,7 @@ namespace
else if (haut->aborted)
err = std::max(err, aborted(haut, filename));
else
- process_automaton(haut, filename);
+ process_automaton(haut, filename);
}
return err;
diff --git a/src/tgbaalgos/Makefile.am b/src/tgbaalgos/Makefile.am
index 803f271a2..301efda74 100644
--- a/src/tgbaalgos/Makefile.am
+++ b/src/tgbaalgos/Makefile.am
@@ -28,6 +28,7 @@ AM_CXXFLAGS = $(WARNING_CXXFLAGS)
tgbaalgosdir = $(pkgincludedir)/tgbaalgos
tgbaalgos_HEADERS = \
+ are_isomorphic.hh \
bfssteps.hh \
closure.hh \
complete.hh \
@@ -80,6 +81,7 @@ tgbaalgos_HEADERS = \
noinst_LTLIBRARIES = libtgbaalgos.la
libtgbaalgos_la_SOURCES = \
+ are_isomorphic.cc \
bfssteps.cc \
closure.cc \
complete.cc \
diff --git a/src/tgbaalgos/are_isomorphic.cc b/src/tgbaalgos/are_isomorphic.cc
new file mode 100644
index 000000000..0f3a7c026
--- /dev/null
+++ b/src/tgbaalgos/are_isomorphic.cc
@@ -0,0 +1,215 @@
+// -*- coding: utf-8 -*-
+// Copyright (C) 2014 Laboratoire de Recherche et
+// Développement de l'Epita (LRDE).
+// Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
+// département Systèmes Répartis Coopératifs (SRC), Université Pierre
+// et Marie Curie.
+//
+// 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 .
+
+#include "tgba/tgbagraph.hh"
+#include "tgbaalgos/are_isomorphic.hh"
+#include
+#include
+#include
+#include "misc/hashfunc.hh"
+
+namespace
+{
+ typedef size_t class_t;
+ typedef std::vector states_t;
+ typedef std::unordered_map class2states_t;
+ typedef std::vector state2class_t;
+ typedef spot::tgba_digraph::graph_t::trans_storage_t trans_storage_t;
+
+ bool
+ trans_lessthan(trans_storage_t ts1, trans_storage_t ts2)
+ {
+ return
+ ts1.src != ts2.src ?
+ ts1.src < ts2.src :
+ ts1.dst != ts2.dst ?
+ ts1.dst < ts2.dst :
+ ts1.acc != ts2.acc ?
+ ts1.acc < ts2.acc :
+ ts1.cond.id() < ts2.cond.id();
+ }
+
+ std::function
+ trans_lessthan_mapped(const std::vector& mapping)
+ {
+ return [mapping](trans_storage_t ts1,
+ trans_storage_t ts2)
+ {
+ return
+ mapping[ts1.src] != mapping[ts2.src] ?
+ mapping[ts1.src] < mapping[ts2.src] :
+ mapping[ts1.dst] != mapping[ts2.dst] ?
+ mapping[ts1.dst] < mapping[ts2.dst] :
+ ts1.acc != ts2.acc ?
+ ts1.acc < ts2.acc :
+ ts1.cond.id() < ts2.cond.id();
+ };
+ }
+
+ state2class_t
+ map_state_class(const spot::const_tgba_digraph_ptr a)
+ {
+ state2class_t hashin(a->num_states(), 0);
+ state2class_t hashout(a->num_states(), 0);
+ state2class_t state2class(a->num_states());
+
+ for (auto& t: a->transitions())
+ {
+ if (!a->is_dead_transition(t))
+ {
+ hashout[t.src] ^= spot::wang32_hash(t.cond.id());
+ hashout[t.src] ^= spot::wang32_hash(t.acc);
+ hashin[t.dst] ^= spot::wang32_hash(t.cond.id());
+ hashin[t.dst] ^= spot::wang32_hash(t.acc);
+ }
+ }
+
+ for (unsigned i = 0; i < a->num_states(); ++i)
+ // Rehash the ingoing transitions so that the total hash differs for
+ // different (in, out) pairs of ingoing and outgoing transitions, even if
+ // the union of in and out is the same.
+ state2class[i] = spot::wang32_hash(hashin[i]) ^ hashout[i];
+
+ return state2class;
+ }
+
+ class2states_t
+ map_class_states(const spot::const_tgba_digraph_ptr a)
+ {
+ unsigned n = a->num_states();
+ std::vector res;
+ class2states_t class2states;
+ auto state2class = map_state_class(a);
+
+ for (unsigned s = 0; s < n; ++s)
+ {
+ class_t c1 = state2class[s];
+ (*(class2states.emplace(c1, std::vector()).first)).second.
+ emplace_back(s);
+ }
+
+ return class2states;
+ }
+
+ bool
+ mapping_from_classes(std::vector& mapping,
+ class2states_t classes1,
+ class2states_t classes2)
+ {
+ if (classes1.size() != classes2.size())
+ return false;
+ for (auto& p : classes1)
+ {
+ if (p.second.size() != classes2[p.first].size())
+ return false;
+ for (unsigned j = 0; j < p.second.size(); ++j)
+ mapping[p.second[j]] = classes2[p.first][j];
+ }
+ return true;
+ }
+
+ bool
+ next_class_permutation(class2states_t& classes)
+ {
+ for (auto& p : classes)
+ if (std::next_permutation(p.second.begin(), p.second.end()))
+ return true;
+ return false;
+ }
+
+ bool
+ is_isomorphism(const std::vector& mapping,
+ const spot::const_tgba_digraph_ptr a1,
+ const spot::const_tgba_digraph_ptr a2)
+ {
+ unsigned n = a1->num_states();
+ assert(n == a2->num_states());
+ std::vector trans1;
+ std::vector trans2;
+
+ for (auto& t: a1->transitions())
+ if (!(a1->is_dead_transition(t)))
+ trans1.push_back(t);
+
+ for (auto& t: a2->transitions())
+ if (!(a2->is_dead_transition(t)))
+ trans2.push_back(t);
+
+ // Sort the vectors of transitions so that they can be compared.
+ // To use the same metric, the transitions of a1 have to be mapped to
+ // a2.
+ std::sort(trans1.begin(), trans1.end(), trans_lessthan_mapped(mapping));
+ std::sort(trans2.begin(), trans2.end(), trans_lessthan);
+
+ for (unsigned i = 0; i < trans1.size(); ++i)
+ {
+ auto ts1 = trans1[i];
+ auto ts2 = trans2[i];
+ if (!(ts2.src == mapping[ts1.src] &&
+ ts2.dst == mapping[ts1.dst] &&
+ ts1.acc == ts2.acc &&
+ ts1.cond.id() == ts2.cond.id()))
+ {
+ return false;
+ }
+ }
+
+ return true;
+ }
+
+ bool
+ are_trivially_different(const spot::const_tgba_digraph_ptr a1,
+ const spot::const_tgba_digraph_ptr a2)
+ {
+ return (a1->num_states() != a2->num_states() ||
+ a1->num_transitions() != a2->num_transitions());
+ }
+}
+
+namespace spot
+{
+ bool
+ are_isomorphic(const const_tgba_digraph_ptr a1,
+ const const_tgba_digraph_ptr a2)
+ {
+ if (are_trivially_different(a1, a2))
+ return false;
+ unsigned n = a1->num_states();
+ assert(n == a2->num_states());
+ class2states_t a1_classes = map_class_states(a1);
+ class2states_t a2_classes = map_class_states(a2);
+ std::vector mapping(n);
+
+ // Get the first possible mapping between a1 and a2, or return false if
+ // the number of class or the size of the classes do not match.
+ if (!(mapping_from_classes(mapping, a1_classes, a2_classes)))
+ return false;
+
+ while (!is_isomorphism(mapping, a1, a2))
+ {
+ if (!next_class_permutation(a2_classes))
+ return false;
+ mapping_from_classes(mapping, a1_classes, a2_classes);
+ }
+ return true;
+ }
+}
diff --git a/src/tgbaalgos/are_isomorphic.hh b/src/tgbaalgos/are_isomorphic.hh
new file mode 100644
index 000000000..e4b3b38ff
--- /dev/null
+++ b/src/tgbaalgos/are_isomorphic.hh
@@ -0,0 +1,41 @@
+// -*- coding: utf-8 -*-
+// Copyright (C) 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 .
+
+#ifndef SPOT_TGBAALGOS_ARE_ISOMORPHIC_HH
+# define SPOT_TGBAALGOS_ARE_ISOMORPHIC_HH
+
+#include "tgba/tgbagraph.hh"
+
+namespace spot
+{
+ /// \ingroup tgba_misc
+ /// \brief Check whether two automata are isomorphic.
+ /// Two automata a1 and a2 are said to be isomorphic if there is a bijection
+ /// f between the states of a1 and a2 such that for every pair of state (s1,
+ /// s2) of a1:
+ /// - there is a transition from s1 to s2 iff there is a transition from f(s1)
+ /// to f(s2)
+ /// - if there is such a transition, then the acceptance set and acceptance
+ /// condition are the same on the transition from s1 to s2 and from f(s1) to
+ /// f(s2)
+ SPOT_API bool are_isomorphic(const const_tgba_digraph_ptr a1,
+ const const_tgba_digraph_ptr a2);
+}
+
+#endif
diff --git a/src/tgbatest/Makefile.am b/src/tgbatest/Makefile.am
index aa357cf84..34d0598ed 100644
--- a/src/tgbatest/Makefile.am
+++ b/src/tgbatest/Makefile.am
@@ -118,6 +118,7 @@ TESTS = \
ltl2ta2.test \
randaut.test \
randtgba.test \
+ isomorph.test \
emptchk.test \
emptchke.test \
dfs.test \
diff --git a/src/tgbatest/isomorph.test b/src/tgbatest/isomorph.test
new file mode 100755
index 000000000..22bbcada2
--- /dev/null
+++ b/src/tgbatest/isomorph.test
@@ -0,0 +1,136 @@
+#!/bin/sh
+# -*- coding: utf-8 -*-
+# Copyright (C) 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 -S10 --hoa >filt
+
+randomize()
+{
+ for i in `seq 1 5`
+ do
+ ../../bin/autfilt --seed=$i --randomize=$1 -F filt --hoa >> autiso
+ done
+}
+
+randomize s
+randomize t
+randomize
+
+run 0 ../../bin/autfilt -F autiso --isomorph filt --hoa >out
+test `grep HOA out | wc -l` -eq 15
+
+cat >notiso <>notiso <out
+test `grep HOA out | wc -l` -eq 0 || exit 1