1 // -*- coding: utf-8 -*- 2 // Copyright (C) 2017-2021 Laboratoire de Recherche et Développement 3 // de l'Epita. 4 // 5 // This file is part of Spot, a model checking library. 6 // 7 // Spot is free software; you can redistribute it and/or modify it 8 // under the terms of the GNU General Public License as published by 9 // the Free Software Foundation; either version 3 of the License, or 10 // (at your option) any later version. 11 // 12 // Spot is distributed in the hope that it will be useful, but WITHOUT 13 // ANY WARRANTY; without even the implied warranty of MERCHANTABILITY 14 // or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public 15 // License for more details. 16 // 17 // You should have received a copy of the GNU General Public License 18 // along with this program. If not, see <http://www.gnu.org/licenses/>. 19 20 #include "config.h" 21 #include <spot/twaalgos/split.hh> 22 #include <spot/misc/minato.hh> 23 #include <spot/misc/bddlt.hh> 24 #include <spot/priv/robin_hood.hh> 25 26 #include <algorithm> 27 #include <map> 28 29 namespace spot 30 { split_edges(const const_twa_graph_ptr & aut)31 twa_graph_ptr split_edges(const const_twa_graph_ptr& aut) 32 { 33 twa_graph_ptr out = make_twa_graph(aut->get_dict()); 34 out->copy_acceptance_of(aut); 35 out->copy_ap_of(aut); 36 out->prop_copy(aut, twa::prop_set::all()); 37 out->new_states(aut->num_states()); 38 out->set_init_state(aut->get_init_state_number()); 39 40 // We use a cache to avoid the costly loop around minterms_of(). 41 // Cache entries have the form (id, [begin, end]) where id is the 42 // number of a BDD that as been (or will be) split, and begin/end 43 // denotes a range of existing transition numbers that cover the 44 // split. 45 typedef std::pair<unsigned, unsigned> cached_t; 46 robin_hood::unordered_map<unsigned, cached_t> split_cond; 47 48 bdd all = aut->ap_vars(); 49 internal::univ_dest_mapper<twa_graph::graph_t> uniq(out->get_graph()); 50 51 for (auto& e: aut->edges()) 52 { 53 bdd cond = e.cond; 54 if (cond == bddfalse) 55 continue; 56 unsigned dst = e.dst; 57 if (aut->is_univ_dest(dst)) 58 { 59 auto d = aut->univ_dests(dst); 60 dst = uniq.new_univ_dests(d.begin(), d.end()); 61 } 62 63 auto& [begin, end] = split_cond[cond.id()]; 64 if (begin == end) 65 { 66 begin = out->num_edges() + 1; 67 for (bdd minterm: minterms_of(cond, all)) 68 out->new_edge(e.src, dst, minterm, e.acc); 69 end = out->num_edges() + 1; 70 } 71 else 72 { 73 auto& g = out->get_graph(); 74 for (unsigned i = begin; i < end; ++i) 75 out->new_edge(e.src, dst, g.edge_storage(i).cond, e.acc); 76 } 77 } 78 return out; 79 } 80 } 81