diff --git a/src/bin/autfilt.cc b/src/bin/autfilt.cc index 02c36f8a6..2fdb1ca31 100644 --- a/src/bin/autfilt.cc +++ b/src/bin/autfilt.cc @@ -53,6 +53,7 @@ #include "tgbaalgos/reducerun.hh" #include "tgbaalgos/word.hh" #include "tgbaalgos/are_isomorphic.hh" +#include "tgbaalgos/canonicalize.hh" static const char argp_program_doc[] ="\ @@ -573,7 +574,10 @@ namespace if (opt_is_deterministic) matched &= is_deterministic(aut); if (opt_are_isomorphic) - matched &= !are_isomorphic(aut, opt_are_isomorphic).empty(); + { + spot::tgba_digraph_ptr tmp = make_tgba_digraph(aut); + matched &= (*spot::canonicalize(tmp) == *opt_are_isomorphic); + } if (opt_is_empty) matched &= aut->is_empty(); @@ -700,8 +704,13 @@ main(int argc, char** argv) if (jobs.empty()) jobs.emplace_back("-", true); - if (opt_are_isomorphic && opt_merge) - opt_are_isomorphic->merge_transitions(); + if (opt_are_isomorphic) + { + if (opt_merge) + opt_are_isomorphic->merge_transitions(); + spot::canonicalize(opt_are_isomorphic); + } + spot::srand(opt_seed); diff --git a/src/graph/graph.hh b/src/graph/graph.hh index e7027e2c8..663f5636d 100644 --- a/src/graph/graph.hh +++ b/src/graph/graph.hh @@ -183,10 +183,17 @@ namespace spot // This might be costly if the destination is a vector if (dst < other.dst) return true; - if (dst < other.dst) + if (dst > other.dst) return false; return this->data() < other.data(); } + + bool operator==(const trans_storage& other) const + { + return src == other.src && + dst == other.dst && + this->data() == other.data(); + } }; ////////////////////////////////////////////////// diff --git a/src/tgba/tgbagraph.hh b/src/tgba/tgbagraph.hh index ac5c951a8..945d1332d 100644 --- a/src/tgba/tgbagraph.hh +++ b/src/tgba/tgbagraph.hh @@ -96,6 +96,12 @@ namespace spot return false; return acc < other.acc; } + + bool operator==(const tgba_graph_trans_data& other) const + { + return cond.id() == other.cond.id() && + acc == other.acc; + } }; @@ -458,6 +464,17 @@ namespace spot return state_is_accepting(state_number(s)); } + bool operator==(const tgba_digraph& aut) const + { + if (num_states() != aut.num_states() || + num_transitions() != aut.num_transitions() || + acc().num_sets() != aut.acc().num_sets()) + return false; + auto& trans1 = transition_vector(); + auto& trans2 = aut.transition_vector(); + return std::equal(trans1.begin() + 1, trans1.end(), + trans2.begin() + 1); + } }; inline tgba_digraph_ptr make_tgba_digraph(const bdd_dict_ptr& dict) diff --git a/src/tgbaalgos/Makefile.am b/src/tgbaalgos/Makefile.am index 301efda74..2de18b746 100644 --- a/src/tgbaalgos/Makefile.am +++ b/src/tgbaalgos/Makefile.am @@ -30,6 +30,7 @@ tgbaalgosdir = $(pkgincludedir)/tgbaalgos tgbaalgos_HEADERS = \ are_isomorphic.hh \ bfssteps.hh \ + canonicalize.hh \ closure.hh \ complete.hh \ compsusp.hh \ @@ -83,6 +84,7 @@ noinst_LTLIBRARIES = libtgbaalgos.la libtgbaalgos_la_SOURCES = \ are_isomorphic.cc \ bfssteps.cc \ + canonicalize.cc \ closure.cc \ complete.cc \ compsusp.cc \ diff --git a/src/tgbaalgos/are_isomorphic.cc b/src/tgbaalgos/are_isomorphic.cc index 3f95850af..acf54dba4 100644 --- a/src/tgbaalgos/are_isomorphic.cc +++ b/src/tgbaalgos/are_isomorphic.cc @@ -22,182 +22,18 @@ #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; - - struct transition - { - unsigned src; - unsigned dst; - int cond; - spot::acc_cond::mark_t acc; - - - transition(unsigned src, unsigned dst, int cond, spot::acc_cond::mark_t acc) - : src(src), dst(dst), cond(cond), acc(acc) - { - } - - bool operator==(const transition& o) const - { - return src == o.src && dst == o.dst && cond == o.cond && acc == o.acc; - } - }; - - static bool - trans_lessthan(const transition& ts1, const transition& 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 < ts2.cond; - } - - static 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()) - { - 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]; - - // XOR the initial state's hash with a pseudo random value so that it is - // in its own class. - state2class[a->get_init_state_number()] ^= 2654435761U; - return state2class; - } - - static 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]; - auto& states = - class2states.emplace(c1, std::vector()).first->second; - states.emplace_back(s); - } - - return class2states; - } - - static bool - mapping_from_classes(std::vector& mapping, - class2states_t classes1, - class2states_t classes2) - { - if (classes1.size() != classes2.size()) - return false; - for (auto& p : classes1) - { - auto& c2 = classes2[p.first]; - if (p.second.size() != c2.size()) - return false; - auto ps = p.second.size(); - for (unsigned j = 0; j < ps; ++j) - mapping[p.second[j]] = c2[j]; - } - return true; - } - - static 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; - } - - static 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() - || a1->acc().num_sets() != a2->acc().num_sets()); - } -} +#include "tgbaalgos/canonicalize.hh" namespace spot { - std::vector - are_isomorphic(const const_tgba_digraph_ptr a1, - const const_tgba_digraph_ptr a2) + bool + are_isomorphic(const const_tgba_digraph_ptr aut1, + const const_tgba_digraph_ptr aut2) { - if (are_trivially_different(a1, a2)) - return {}; - 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 {}; - - unsigned tend = a1->num_transitions(); - assert(tend == a2->num_transitions()); - - // a2 is our reference automaton. Keep a sorted list of its - // transition for easy comparison. - std::vector trans2; - trans2.reserve(tend); - for (auto& t: a2->transitions()) - trans2.emplace_back(t.src, t.dst, t.acc, t.cond.id()); - std::sort(trans2.begin(), trans2.end(), trans_lessthan); - - std::vector trans1; - trans1.reserve(tend); - - for (;;) - { - // Check if current mapping matches the reference automaton - trans1.clear(); - for (auto& t: a1->transitions()) - trans1.emplace_back(mapping[t.src], mapping[t.dst], - t.acc, t.cond.id()); - std::sort(trans1.begin(), trans1.end(), trans_lessthan); - if (trans1 == trans2) - return mapping; - - // Consider next mapping - if (!next_class_permutation(a2_classes)) - return {}; - mapping_from_classes(mapping, a1_classes, a2_classes); - } + auto tmp1 = make_tgba_digraph(aut1); + auto tmp2 = make_tgba_digraph(aut2); + spot::canonicalize(tmp1); + spot::canonicalize(tmp2); + return *tmp1 == *tmp2; } } diff --git a/src/tgbaalgos/are_isomorphic.hh b/src/tgbaalgos/are_isomorphic.hh index 91ea1e059..81ad0b138 100644 --- a/src/tgbaalgos/are_isomorphic.hh +++ b/src/tgbaalgos/are_isomorphic.hh @@ -26,16 +26,18 @@ namespace spot { /// \ingroup tgba_misc - /// \brief Check whether two automate are isormorphic. + /// \brief Check whether two automata are isomorphic. /// - /// Return an isomorphism between a1 and a2 if such an isomorphism - /// exists. Otherwise, return an empty vector. - /// - /// \return a vector indexed by states of \a a1, and containing - /// states of \a a2. - SPOT_API std::vector - are_isomorphic(const const_tgba_digraph_ptr a1, - const const_tgba_digraph_ptr a2); + /// Two automata are considered isomorphic if there exists a bijection f + /// between the states of a1 and the states of a2 such that for any pair of + /// states (s1, s2) of a1, there is a transition from s1 to s2 with + /// condition c and acceptance set A iff there is a transition with + /// condition c and acceptance set A between f(s1) and f(s2) in a2. + /// This can be done simply by checking if + /// canonicalize(aut1) == canonicalize(aut2). + SPOT_API bool + are_isomorphic(const const_tgba_digraph_ptr aut1, + const const_tgba_digraph_ptr aut2); } #endif diff --git a/src/tgbaalgos/canonicalize.cc b/src/tgbaalgos/canonicalize.cc new file mode 100644 index 000000000..868fd1df8 --- /dev/null +++ b/src/tgbaalgos/canonicalize.cc @@ -0,0 +1,109 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2014 Laboratoire de Recherche et +// Developpement 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 . + +#include "canonicalize.hh" +#include "tgba/tgbagraph.hh" +#include +#include + +namespace +{ + typedef std::pair + trans_sig_t; + + struct signature_t + { + std::vector ingoing; + std::vector outgoing; + unsigned classnum; + + bool + operator<(const signature_t& o) const + { + return ingoing != o.ingoing ? ingoing < o.ingoing : + outgoing != o.outgoing ? outgoing < o.outgoing : + classnum < o.classnum; + } + }; + + typedef std::map> sig2states_t; + + static sig2states_t + sig_to_states(spot::tgba_digraph_ptr aut, std::vector& state2class) + { + std::vector signature(aut->num_states(), signature_t()); + + for (auto& t : aut->transitions()) + { + signature[t.dst].ingoing.emplace_back(t.data(), state2class[t.src]); + signature[t.src].outgoing.emplace_back(t.data(), state2class[t.dst]); + } + + sig2states_t sig2states; + for (unsigned s = 0; s < aut->num_states(); ++s) + { + std::sort(signature[s].ingoing.begin(), signature[s].ingoing.end()); + std::sort(signature[s].outgoing.begin(), signature[s].outgoing.end()); + signature[s].classnum = state2class[s]; + sig2states[signature[s]].push_back(s); + } + + return sig2states; + } +} + +namespace spot +{ + tgba_digraph_ptr + canonicalize(tgba_digraph_ptr aut) + { + std::vector state2class(aut->num_states(), 0); + state2class[aut->get_init_state_number()] = 1; + size_t distinct_classes = 2; + sig2states_t sig2states = sig_to_states(aut, state2class); + + while (sig2states.size() != distinct_classes && + sig2states.size() != aut->num_states()) + { + distinct_classes = sig2states.size(); + + unsigned classnum = 0; + for (auto& s: sig2states) + { + for (auto& state: s.second) + state2class[state] = classnum; + ++classnum; + } + + sig2states = sig_to_states(aut, state2class); + } + + unsigned classnum = 0; + for (auto& s: sig2states) + for (auto& state: s.second) + state2class[state] = classnum++; + + auto& g = aut->get_graph(); + g.rename_states_(state2class); + aut->set_init_state(state2class[aut->get_init_state_number()]); + g.sort_transitions_(); + g.chain_transitions_(); + return aut; + } +} diff --git a/src/tgbaalgos/canonicalize.hh b/src/tgbaalgos/canonicalize.hh new file mode 100644 index 000000000..46178fd79 --- /dev/null +++ b/src/tgbaalgos/canonicalize.hh @@ -0,0 +1,32 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2014 Laboratoire de Recherche et +// Developpement 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_CANONICALIZE_HH +# define SPOT_TGBAALGOS_CANONICALIZE_HH + +#include "tgba/tgbagraph.hh" +namespace spot +{ + /// \ingroup tgba_misc + /// \brief Reorder the states and transitions of aut in a way that will be the + /// same for every isomorphic automata. + SPOT_API tgba_digraph_ptr canonicalize(tgba_digraph_ptr aut); +} + +#endif diff --git a/src/tgbatest/isomorph.test b/src/tgbatest/isomorph.test index 4ce8ebc82..34d5d6766 100755 --- a/src/tgbatest/isomorph.test +++ b/src/tgbatest/isomorph.test @@ -23,7 +23,7 @@ set -e for i in 0 1 2 3 4; do - ../../bin/randaut a --seed=$i -S4 --hoa >iso$i + ../../bin/randaut a b --seed=$i -S10 --hoa >iso$i ../../bin/autfilt iso$i --randomize --hoa >aut$i done @@ -32,3 +32,73 @@ cat aut0 aut1 aut2 aut3 aut4 > all run 0 ../../bin/autfilt all --are-isomorphic iso$i --hoa done) > output diff all output + +# Test if two isomorphic automata with different initial states are detected. +cat >aut1 <aut2 <aut3 <aut4 <