diff --git a/src/bin/autfilt.cc b/src/bin/autfilt.cc index db9cda1ae..c814e384a 100644 --- a/src/bin/autfilt.cc +++ b/src/bin/autfilt.cc @@ -415,12 +415,16 @@ namespace // Do this first, because it is cheap and will help most // algorithms. if (opt_merge) - aut->merge_transitions(); + { + aut->merge_transitions(); + if (opt_are_isomorphic) + opt_are_isomorphic->merge_transitions(); + } if (opt_product) aut = spot::product(std::move(aut), opt_product); - if (opt_isomorph && !are_isomorphic(aut, opt_isomorph)) + if (opt_isomorph && are_isomorphic(aut, opt_isomorph).empty()) return 0; aut = post.run(aut, nullptr); diff --git a/src/tgbaalgos/are_isomorphic.cc b/src/tgbaalgos/are_isomorphic.cc index 0f3a7c026..86e3a2692 100644 --- a/src/tgbaalgos/are_isomorphic.cc +++ b/src/tgbaalgos/are_isomorphic.cc @@ -187,12 +187,12 @@ namespace namespace spot { - bool + std::vector are_isomorphic(const const_tgba_digraph_ptr a1, const const_tgba_digraph_ptr a2) { if (are_trivially_different(a1, a2)) - return false; + return std::vector(); unsigned n = a1->num_states(); assert(n == a2->num_states()); class2states_t a1_classes = map_class_states(a1); @@ -202,14 +202,14 @@ namespace spot // 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; + return std::vector(); while (!is_isomorphism(mapping, a1, a2)) { if (!next_class_permutation(a2_classes)) - return false; + return std::vector(); mapping_from_classes(mapping, a1_classes, a2_classes); } - return true; + return mapping; } } diff --git a/src/tgbaalgos/are_isomorphic.hh b/src/tgbaalgos/are_isomorphic.hh index e4b3b38ff..9e8273754 100644 --- a/src/tgbaalgos/are_isomorphic.hh +++ b/src/tgbaalgos/are_isomorphic.hh @@ -21,20 +21,16 @@ # define SPOT_TGBAALGOS_ARE_ISOMORPHIC_HH #include "tgba/tgbagraph.hh" +#include 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, + /// \brief Return an isomorphism between a1 and a2 if such an isomorphism + /// exists. Otherwise, return an empty vector. + /// The return value is a vector indexed by states of a1, and containing + /// states of a2. + SPOT_API std::vector are_isomorphic(const const_tgba_digraph_ptr a1, const const_tgba_digraph_ptr a2); }