diff --git a/spot/twaalgos/zlktree.cc b/spot/twaalgos/zlktree.cc index 698d260f8..0940ae46c 100644 --- a/spot/twaalgos/zlktree.cc +++ b/spot/twaalgos/zlktree.cc @@ -368,20 +368,51 @@ namespace spot } acd::acd(const const_twa_graph_ptr& aut) - : acd(scc_info(aut)) + : si_(new scc_info(aut)), own_si_(true), trees_(si_->scc_count()) { + build_(); } acd::acd(const scc_info& si) - : trees_(si.scc_count()) + : si_(&si), own_si_(false), trees_(si_->scc_count()) { - unsigned scc_count = scc_count_ = si.scc_count(); - const_twa_graph_ptr aut = aut_ = si.get_aut(); + build_(); + } + + acd::~acd() + { + if (own_si_) + delete si_; + } + + void acd::build_() + { + unsigned scc_count = scc_count_ = si_->scc_count(); + const_twa_graph_ptr aut = aut_ = si_->get_aut(); unsigned nedges = aut->get_graph().edge_vector().size(); unsigned nstates = aut->num_states(); acc_cond posacc = aut->acc(); acc_cond negacc(posacc.num_sets(), posacc.get_acceptance().complement()); + // The bitvectors store edge and state-vectors that are shared + // among the different trees. + auto allocate_vectors_maybe = [&](unsigned n) + { + if (bitvectors.size() > 2 * n) + return; + bitvectors.emplace_back(nedges, false); + bitvectors.emplace_back(nstates, false); + }; + auto edge_vector = [&] (unsigned n) -> std::vector& + { + return bitvectors[2 * n]; + }; + auto state_vector = [&] (unsigned n) -> std::vector& + { + return bitvectors[2 * n + 1]; + }; + allocate_vectors_maybe(0); + // Remember the max level since of each tree of different parity. // We will use that to decide if the output should have parity // "min even" or "min odd" so as to minimize the number of colors @@ -391,20 +422,19 @@ namespace spot for (unsigned scc = 0; scc < scc_count; ++scc) { - if ((trees_[scc].trivial = si.is_trivial(scc))) + if ((trees_[scc].trivial = si_->is_trivial(scc))) continue; + trees_[scc].num_nodes = 1; unsigned root = nodes_.size(); trees_[scc].root = root; - bool is_even = si.is_maximally_accepting_scc(scc); + bool is_even = si_->is_maximally_accepting_scc(scc); trees_[scc].is_even = is_even; - nodes_.emplace_back(); + nodes_.emplace_back(edge_vector(0), state_vector(0)); auto& n = nodes_.back(); n.parent = root; n.level = 0; n.scc = scc; - n.edges.resize(nedges); - n.states.resize(nstates); - for (auto& e: si.inner_edges_of(scc)) + for (auto& e: si_->inner_edges_of(scc)) { n.edges[aut->edge_number(e)] = true; n.states[e.src] = true; @@ -420,13 +450,13 @@ namespace spot auto callback = [&](scc_info si, unsigned siscc) { - nodes_.emplace_back(); + unsigned vnum = trees_[scc].num_nodes++; + allocate_vectors_maybe(vnum); + nodes_.emplace_back(edge_vector(vnum), state_vector(vnum)); auto& n = nodes_.back(); n.parent = node; n.level = lvl + 1; n.scc = scc; - n.edges.resize(nedges); - n.states.resize(nstates); for (auto& e: si.inner_edges_of(siscc)) { n.edges[aut->edge_number(e)] = true; @@ -435,7 +465,7 @@ namespace spot }; unsigned before_size = nodes_.size(); - maximal_accepting_loops_for_scc(si, scc, + maximal_accepting_loops_for_scc(*si_, scc, accepting_node ? negacc : posacc, nodes_[node].edges, callback); unsigned after_size = nodes_.size(); @@ -586,7 +616,8 @@ namespace spot const char* sep = "T: "; for (unsigned n = 1; n <= nedges; ++n) { - bool val = n < nedges ? edges[n] : false; + bool val = n < nedges && edges[n] + && si_->scc_of(aut_->edge_storage(n).dst) == scc; if (val != lastval) { if (lastval) @@ -617,7 +648,7 @@ namespace spot sep = "\nQ: "; for (unsigned n = 0; n <= nstates; ++n) { - bool val = n < nstates ? states[n] : false; + bool val = n < nstates && states[n] && si_->scc_of(n) == scc; if (val != lastval) { if (lastval) diff --git a/spot/twaalgos/zlktree.hh b/spot/twaalgos/zlktree.hh index 152d6383c..3d395541d 100644 --- a/spot/twaalgos/zlktree.hh +++ b/spot/twaalgos/zlktree.hh @@ -162,6 +162,8 @@ namespace spot acd(const scc_info& si); acd(const const_twa_graph_ptr& aut); + ~acd(); + /// \brief Walk through the ACD. /// /// Given a \a branch number, and an edge, this returns @@ -246,6 +248,20 @@ namespace spot void dot(std::ostream&) const; private: + const scc_info* si_; + bool own_si_ = false; + + // This structure is used to represent one node in the ACD forest. + // The tree use a left-child / right-sibling representation + // (called here first_child, next_sibling). Each node + // additionally store a level (depth in the ACD, adjusted at the + // end of the construction so that all node on the same level have + // the same parity), the SCC (which is also it's tree number), and + // some bit vectors representing the edges and states of that + // node. Those bit vectors are as large as the original + // automaton, and they are shared among nodes from the different + // trees of the ACD forest (since each tree correspond to a + // different SCC, they cannot share state or edges). struct acd_node { unsigned parent; @@ -253,24 +269,48 @@ namespace spot unsigned first_child = 0; unsigned level; unsigned scc; - std::vector edges; - std::vector states; + std::vector& edges; + std::vector& states; + acd_node(std::vector& e, std::vector& s) noexcept + : edges(e), states(s) + { + } }; + // We store the nodes in a deque so that their addresses do not + // change. std::deque nodes_; + // Likewise for bitvectors: this is the support for all edge vectors + // and state vectors used in acd_node. + std::deque> bitvectors; + // Information about a tree of the ACD. Each tree correspond + // to an SCC. struct scc_data { - bool trivial; - unsigned root = 0; - bool is_even; - unsigned max_level = 0; + bool trivial; // whether the SCC is trivial we do + // not store any node for trivial + // SCCs. + unsigned root = 0; // root node of a non-trivial SCC. + bool is_even; // parity of the tree, used at the end + // of the construction to adjust + // levels. + unsigned max_level = 0; // Maximum level for this SCC. + unsigned num_nodes = 0; // Number of node in this tree. This + // is only used to share bitvectors + // between SCC: node with the same + // "rank" in each tree share the same + // bitvectors. }; std::vector trees_; unsigned scc_count_; const_twa_graph_ptr aut_; + // Information about the overall ACD. bool is_even_; bool has_rabin_shape_ = true; bool has_streett_shape_ = true; + // Build the ACD structure. Called by the constructors. + void build_(); + // leftmost branch of \a node that contains \a state unsigned leftmost_branch_(unsigned node, unsigned state);