1 // -*- coding: utf-8 -*- 2 // Copyright (C) 2014-2018 Laboratoire de Recherche et Développement 3 // de l'Epita (LRDE). 4 // Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), 5 // département Systèmes Répartis Coopératifs (SRC), Université Pierre 6 // et Marie Curie. 7 // 8 // This file is part of Spot, a model checking library. 9 // 10 // Spot is free software; you can redistribute it and/or modify it 11 // under the terms of the GNU General Public License as published by 12 // the Free Software Foundation; either version 3 of the License, or 13 // (at your option) any later version. 14 // 15 // Spot is distributed in the hope that it will be useful, but WITHOUT 16 // ANY WARRANTY; without even the implied warranty of MERCHANTABILITY 17 // or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public 18 // License for more details. 19 // 20 // You should have received a copy of the GNU General Public License 21 // along with this program. If not, see <http://www.gnu.org/licenses/>. 22 23 #include "config.h" 24 #include <spot/twa/twagraph.hh> 25 #include <spot/twaalgos/are_isomorphic.hh> 26 #include <spot/twaalgos/canonicalize.hh> 27 #include <spot/twaalgos/isdet.hh> 28 #include <vector> 29 #include <queue> 30 31 namespace 32 { 33 typedef spot::twa_graph::graph_t::edge_storage_t tr_t; 34 static bool tr_t_less_than(const tr_t & t1,const tr_t & t2)35 tr_t_less_than(const tr_t& t1, const tr_t& t2) 36 { 37 return t1.cond.id() < t2.cond.id(); 38 } 39 40 static bool operator !=(const tr_t & t1,const tr_t & t2)41 operator!=(const tr_t& t1, const tr_t& t2) 42 { 43 return t1.cond.id() != t2.cond.id(); 44 } 45 46 static bool are_isomorphic_det(const spot::const_twa_graph_ptr aut1,const spot::const_twa_graph_ptr aut2)47 are_isomorphic_det(const spot::const_twa_graph_ptr aut1, 48 const spot::const_twa_graph_ptr aut2) 49 { 50 typedef std::pair<unsigned, unsigned> state_pair_t; 51 std::queue<state_pair_t> workqueue; 52 workqueue.emplace(aut1->get_init_state_number(), 53 aut2->get_init_state_number()); 54 std::vector<unsigned> map(aut1->num_states(), -1U); 55 map[aut1->get_init_state_number()] = aut2->get_init_state_number(); 56 std::vector<tr_t> trans1; 57 std::vector<tr_t> trans2; 58 state_pair_t current_state; 59 while (!workqueue.empty()) 60 { 61 current_state = workqueue.front(); 62 workqueue.pop(); 63 64 for (auto& t : aut1->out(current_state.first)) 65 trans1.emplace_back(t); 66 for (auto& t : aut2->out(current_state.second)) 67 trans2.emplace_back(t); 68 69 if (trans1.size() != trans2.size()) 70 return false; 71 72 std::sort(trans1.begin(), trans1.end(), tr_t_less_than); 73 std::sort(trans2.begin(), trans2.end(), tr_t_less_than); 74 75 for (auto t1 = trans1.begin(), t2 = trans2.begin(); 76 t1 != trans1.end() && t2 != trans2.end(); 77 ++t1, ++t2) 78 { 79 if (*t1 != *t2) 80 { 81 return false; 82 } 83 if (map[t1->dst] == -1U) 84 { 85 map[t1->dst] = t2->dst; 86 workqueue.emplace(t1->dst, t2->dst); 87 } 88 else if (map[t1->dst] != t2->dst) 89 { 90 return false; 91 } 92 } 93 94 trans1.clear(); 95 trans2.clear(); 96 } 97 return true; 98 } 99 100 bool trivially_different(const spot::const_twa_graph_ptr aut1,const spot::const_twa_graph_ptr aut2)101 trivially_different(const spot::const_twa_graph_ptr aut1, 102 const spot::const_twa_graph_ptr aut2) 103 { 104 return aut1->num_states() != aut2->num_states() || 105 aut1->num_edges() != aut2->num_edges() || 106 // FIXME: At some point, it would be nice to support reordering 107 // of acceptance sets (issue #58). 108 aut1->acc().get_acceptance() != aut2->acc().get_acceptance(); 109 } 110 } 111 112 namespace spot 113 { isomorphism_checker(const const_twa_graph_ptr ref)114 isomorphism_checker::isomorphism_checker(const const_twa_graph_ptr ref) 115 { 116 ref_ = make_twa_graph(ref, twa::prop_set::all()); 117 trival prop_det = ref_->prop_universal(); 118 if (prop_det) 119 { 120 ref_deterministic_ = true; 121 } 122 else 123 { 124 // Count the number of state even if we know that the 125 // automaton is non-deterministic, as this can be used to 126 // decide if two automata are non-isomorphic. 127 nondet_states_ = spot::count_nondet_states(ref_); 128 ref_deterministic_ = (nondet_states_ == 0); 129 } 130 canonicalize(ref_); 131 } 132 133 bool is_isomorphic_(const const_twa_graph_ptr aut)134 isomorphism_checker::is_isomorphic_(const const_twa_graph_ptr aut) 135 { 136 if (!aut->is_existential()) 137 throw std::runtime_error 138 ("isomorphism_checker does not yet support alternation"); 139 trival autdet = aut->prop_universal(); 140 if (ref_deterministic_) 141 { 142 if (!spot::is_universal(aut)) 143 return false; 144 return are_isomorphic_det(ref_, aut); 145 } 146 if (autdet || nondet_states_ != spot::count_nondet_states(aut)) 147 return false; 148 149 auto tmp = make_twa_graph(aut, twa::prop_set::all()); 150 spot::canonicalize(tmp); 151 return *tmp == *ref_; 152 } 153 154 bool is_isomorphic(const const_twa_graph_ptr aut)155 isomorphism_checker::is_isomorphic(const const_twa_graph_ptr aut) 156 { 157 if (trivially_different(ref_, aut)) 158 return false; 159 return is_isomorphic_(aut); 160 } 161 162 bool are_isomorphic(const const_twa_graph_ptr ref,const const_twa_graph_ptr aut)163 isomorphism_checker::are_isomorphic(const const_twa_graph_ptr ref, 164 const const_twa_graph_ptr aut) 165 { 166 if (trivially_different(ref, aut)) 167 return false; 168 isomorphism_checker c(ref); 169 return c.is_isomorphic_(aut); 170 } 171 } 172