are_isomorphic: return the mapping found, not just true or false

* src/bin/autfilt.cc: Here.
* src/tgbaalgos/are_isomorphic.cc, src/tgbaalgos/are_isomorphic.hh:
Here.
This commit is contained in:
Thibaud Michaud 2014-12-08 21:42:27 +01:00 committed by Alexandre Duret-Lutz
parent 97fdea9d71
commit 1b9354c9b5
3 changed files with 17 additions and 17 deletions

View file

@ -415,12 +415,16 @@ namespace
// Do this first, because it is cheap and will help most // Do this first, because it is cheap and will help most
// algorithms. // algorithms.
if (opt_merge) if (opt_merge)
aut->merge_transitions(); {
aut->merge_transitions();
if (opt_are_isomorphic)
opt_are_isomorphic->merge_transitions();
}
if (opt_product) if (opt_product)
aut = spot::product(std::move(aut), 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; return 0;
aut = post.run(aut, nullptr); aut = post.run(aut, nullptr);

View file

@ -187,12 +187,12 @@ namespace
namespace spot namespace spot
{ {
bool std::vector<unsigned>
are_isomorphic(const const_tgba_digraph_ptr a1, are_isomorphic(const const_tgba_digraph_ptr a1,
const const_tgba_digraph_ptr a2) const const_tgba_digraph_ptr a2)
{ {
if (are_trivially_different(a1, a2)) if (are_trivially_different(a1, a2))
return false; return std::vector<unsigned>();
unsigned n = a1->num_states(); unsigned n = a1->num_states();
assert(n == a2->num_states()); assert(n == a2->num_states());
class2states_t a1_classes = map_class_states(a1); 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 // 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. // the number of class or the size of the classes do not match.
if (!(mapping_from_classes(mapping, a1_classes, a2_classes))) if (!(mapping_from_classes(mapping, a1_classes, a2_classes)))
return false; return std::vector<unsigned>();
while (!is_isomorphism(mapping, a1, a2)) while (!is_isomorphism(mapping, a1, a2))
{ {
if (!next_class_permutation(a2_classes)) if (!next_class_permutation(a2_classes))
return false; return std::vector<unsigned>();
mapping_from_classes(mapping, a1_classes, a2_classes); mapping_from_classes(mapping, a1_classes, a2_classes);
} }
return true; return mapping;
} }
} }

View file

@ -21,20 +21,16 @@
# define SPOT_TGBAALGOS_ARE_ISOMORPHIC_HH # define SPOT_TGBAALGOS_ARE_ISOMORPHIC_HH
#include "tgba/tgbagraph.hh" #include "tgba/tgbagraph.hh"
#include <vector>
namespace spot namespace spot
{ {
/// \ingroup tgba_misc /// \ingroup tgba_misc
/// \brief Check whether two automata are isomorphic. /// \brief Return an isomorphism between a1 and a2 if such an isomorphism
/// Two automata a1 and a2 are said to be isomorphic if there is a bijection /// exists. Otherwise, return an empty vector.
/// f between the states of a1 and a2 such that for every pair of state (s1, /// The return value is a vector indexed by states of a1, and containing
/// s2) of a1: /// states of a2.
/// - there is a transition from s1 to s2 iff there is a transition from f(s1) SPOT_API std::vector<unsigned> are_isomorphic(const const_tgba_digraph_ptr a1,
/// 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); const const_tgba_digraph_ptr a2);
} }