diff --git a/src/bin/autfilt.cc b/src/bin/autfilt.cc index 2fdb1ca31..14ca7b335 100644 --- a/src/bin/autfilt.cc +++ b/src/bin/autfilt.cc @@ -210,6 +210,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 std::unique_ptr isomorphism_checker = nullptr; static spot::tgba_digraph_ptr opt_are_isomorphic = nullptr; static bool opt_is_complete = false; static bool opt_is_deterministic = false; @@ -574,10 +575,7 @@ namespace if (opt_is_deterministic) matched &= is_deterministic(aut); if (opt_are_isomorphic) - { - spot::tgba_digraph_ptr tmp = make_tgba_digraph(aut); - matched &= (*spot::canonicalize(tmp) == *opt_are_isomorphic); - } + matched &= isomorphism_checker->is_isomorphic(aut); if (opt_is_empty) matched &= aut->is_empty(); @@ -708,7 +706,8 @@ main(int argc, char** argv) { if (opt_merge) opt_are_isomorphic->merge_transitions(); - spot::canonicalize(opt_are_isomorphic); + isomorphism_checker = std::unique_ptr( + new spot::isomorphism_checker(opt_are_isomorphic)); } diff --git a/src/tgbaalgos/are_isomorphic.cc b/src/tgbaalgos/are_isomorphic.cc index acf54dba4..8e622c339 100644 --- a/src/tgbaalgos/are_isomorphic.cc +++ b/src/tgbaalgos/are_isomorphic.cc @@ -23,17 +23,127 @@ #include "tgba/tgbagraph.hh" #include "tgbaalgos/are_isomorphic.hh" #include "tgbaalgos/canonicalize.hh" +#include "tgbaalgos/isdet.hh" +#include +#include + +namespace +{ + typedef spot::tgba_digraph::graph_t::trans_storage_t tr_t; + bool + tr_t_less_than(const tr_t& t1, const tr_t& t2) + { + return t1.cond.id() < t2.cond.id(); + } + + bool + operator!=(const tr_t& t1, const tr_t& t2) + { + return t1.cond.id() != t2.cond.id(); + } + + bool + are_isomorphic_det(const spot::const_tgba_digraph_ptr aut1, + const spot::const_tgba_digraph_ptr aut2) + { + typedef std::pair state_pair_t; + std::queue workqueue; + workqueue.emplace(aut1->get_init_state_number(), + aut2->get_init_state_number()); + std::vector map(aut1->num_states(), -1U); + map[aut1->get_init_state_number()] = aut2->get_init_state_number(); + std::vector trans1; + std::vector trans2; + state_pair_t current_state; + while (!workqueue.empty()) + { + current_state = workqueue.front(); + workqueue.pop(); + + for (auto& t : aut1->out(current_state.first)) + trans1.emplace_back(t); + for (auto& t : aut2->out(current_state.second)) + trans2.emplace_back(t); + + if (trans1.size() != trans2.size()) + return false; + + std::sort(trans1.begin(), trans1.end(), tr_t_less_than); + std::sort(trans2.begin(), trans2.end(), tr_t_less_than); + + for (auto t1 = trans1.begin(), t2 = trans2.begin(); + t1 != trans1.end() && t2 != trans2.end(); + ++t1, ++t2) + { + if (*t1 != *t2) + { + return false; + } + if (map[t1->dst] == -1U) + { + map[t1->dst] = t2->dst; + workqueue.emplace(t1->dst, t2->dst); + } + else if (map[t1->dst] != t2->dst) + { + return false; + } + } + + trans1.clear(); + trans2.clear(); + } + return true; + } + + bool + trivially_different(const spot::const_tgba_digraph_ptr aut1, + const spot::const_tgba_digraph_ptr aut2) + { + return aut1->num_states() != aut2->num_states() || + aut1->num_transitions() != aut2->num_transitions() || + aut1->acc().num_sets() != aut2->acc().num_sets(); + } +} namespace spot { - bool - are_isomorphic(const const_tgba_digraph_ptr aut1, - const const_tgba_digraph_ptr aut2) + isomorphism_checker::isomorphism_checker(const const_tgba_digraph_ptr ref) { - auto tmp1 = make_tgba_digraph(aut1); - auto tmp2 = make_tgba_digraph(aut2); - spot::canonicalize(tmp1); - spot::canonicalize(tmp2); - return *tmp1 == *tmp2; + ref_ = make_tgba_digraph(ref); + ref_deterministic_ = ref_->is_deterministic(); + if (!ref_deterministic_) + { + nondet_states_ = spot::count_nondet_states(ref_); + ref_deterministic_ = (nondet_states_ == 0); + } + canonicalize(ref_); + } + + bool + isomorphism_checker::is_isomorphic(const const_tgba_digraph_ptr aut) + { + if (trivially_different(ref_, aut)) + return false; + + if (ref_deterministic_) + { + if (aut->is_deterministic() || spot::is_deterministic(aut)) + { + return are_isomorphic_det(ref_, aut); + } + } + else + { + if (aut->is_deterministic() || + nondet_states_ != spot::count_nondet_states(aut)) + { + return false; + } + } + + auto tmp = make_tgba_digraph(aut); + spot::canonicalize(tmp); + return *tmp == *ref_; } } diff --git a/src/tgbaalgos/are_isomorphic.hh b/src/tgbaalgos/are_isomorphic.hh index 81ad0b138..5a1c2ac6d 100644 --- a/src/tgbaalgos/are_isomorphic.hh +++ b/src/tgbaalgos/are_isomorphic.hh @@ -25,19 +25,33 @@ namespace spot { - /// \ingroup tgba_misc - /// \brief Check whether two automata are isomorphic. - /// - /// 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); + /// Check if two automata are isomorphic. + class SPOT_API isomorphism_checker + { + public: + isomorphism_checker(const const_tgba_digraph_ptr ref); + + /// \ingroup tgba_misc + /// \brief Check whether an automaton is isomorphic to the one passed to + /// the constructor. + /// + /// 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), but is_isomorphic can do some + /// optimizations in some cases. + bool + is_isomorphic(const const_tgba_digraph_ptr aut); + + private: + tgba_digraph_ptr ref_; + bool ref_deterministic_ = false; + unsigned nondet_states_ = 0; + std::vector reftrans_; + }; } #endif diff --git a/src/tgbatest/isomorph.test b/src/tgbatest/isomorph.test index 34d5d6766..bb59a5170 100755 --- a/src/tgbatest/isomorph.test +++ b/src/tgbatest/isomorph.test @@ -22,13 +22,17 @@ set -e -for i in 0 1 2 3 4; do +for i in 0 1 2; do ../../bin/randaut a b --seed=$i -S10 --hoa >iso$i ../../bin/autfilt iso$i --randomize --hoa >aut$i done +for i in 3 4 5; do + ../../bin/randaut a b --seed=$i -S10 -D --hoa >iso$i + ../../bin/autfilt iso$i --randomize --hoa >aut$i +done -cat aut0 aut1 aut2 aut3 aut4 > all -(for i in 0 1 2 3 4; do +cat aut0 aut1 aut2 aut3 aut4 aut5 > all +(for i in 0 1 2 3 4 5; do run 0 ../../bin/autfilt all --are-isomorphic iso$i --hoa done) > output diff all output