diff --git a/src/graph/graph.hh b/src/graph/graph.hh index 7147413af..aa6e6bcea 100644 --- a/src/graph/graph.hh +++ b/src/graph/graph.hh @@ -239,11 +239,80 @@ namespace spot return t_; } + transition trans() const + { + return t_; + } + protected: Graph* g_; transition t_; }; + template + class SPOT_API killer_trans_iterator: public trans_iterator + { + typedef trans_iterator super; + public: + typedef typename Graph::state_storage_t state_storage_t; + typedef typename Graph::transition transition; + + killer_trans_iterator(Graph* g, transition t, state_storage_t& src): + super(g, t), src_(src), prev_(0) + { + } + + killer_trans_iterator operator++() + { + prev_ = this->t_; + this->t_ = this->operator*().next_succ; + return *this; + } + + killer_trans_iterator operator++(int) + { + killer_trans_iterator ti = *this; + prev_ = this->t_; + this->t_ = this->operator*().next_succ; + return ti; + } + + // Erase the current transition and advance the iterator. + void erase() + { + transition next = this->operator*().next_succ; + + // Update source state and previous transitions + if (prev_) + { + this->g_->trans_storage(prev_).next_succ = next; + } + else + { + if (src_.succ == this->t_) + src_.succ = next; + } + if (src_.succ_tail == this->t_) + { + src_.succ_tail = prev_; + assert(next == 0); + } + + // Erased transitions have themselves as next_succ. + this->operator*().next_succ = this->t_; + + // Advance iterator to next transitions. + this->t_ = next; + + ++this->g_->killed_trans_; + } + + protected: + state_storage_t& src_; + transition prev_; + }; + + ////////////////////////////////////////////////// // State OUT ////////////////////////////////////////////////// @@ -289,6 +358,7 @@ namespace spot { friend class internal::trans_iterator; friend class internal::trans_iterator; + friend class internal::killer_trans_iterator; public: typedef internal::trans_iterator iterator; @@ -325,7 +395,8 @@ namespace spot protected: state_vector states_; trans_vector transitions_; - + // Number of erased transitions. + unsigned killed_trans_; public: /// \brief construct an empty graph /// @@ -334,6 +405,7 @@ namespace spot /// limits, but just hints to pre-allocate a data structure that /// may hold that much items. digraph(unsigned max_states = 10, unsigned max_trans = 0) + : killed_trans_(0) { states_.reserve(max_states); if (max_trans == 0) @@ -351,7 +423,15 @@ namespace spot unsigned num_transitions() const { - return transitions_.size(); + return transitions_.size() - killed_trans_ - 1; + } + + bool valid_trans(transition t) const + { + // Erased transitions have their next_succ pointing to + // themselves. + return (t < transitions_.size() && + transitions_[t].next_succ != t); } template @@ -449,26 +529,52 @@ namespace spot return t; } + state index_of_state(state_storage_t& ss) + { + assert(!states_.empty()); + return &ss - &states_.front(); + } + + transition index_of_transition(trans_storage_t& tt) + { + assert(!transitions_.empty()); + return &tt - &transitions_.front(); + } + internal::state_out out(state src) { return {this, states_[src].succ}; } + internal::state_out + out(state_storage_t& src) + { + return out(index_of_state(src)); + } + internal::state_out out(state src) const { return {this, states_[src].succ}; } - unsigned nb_states() const + internal::state_out + out(state_storage_t& src) const { - return states_.size(); + return out(index_of_state(src)); } - unsigned nb_trans() const + internal::killer_trans_iterator + out_iteraser(state_storage_t& src) { - return transitions_.size(); + return {this, src.succ, src}; + } + + internal::killer_trans_iterator + out_iteraser(state src) + { + return out_iteraser(state_storage(src)); } const state_vector& states() const @@ -481,6 +587,42 @@ namespace spot return states_; } + void defrag() + { + if (killed_trans_ == 0) // Nothing to do. + return; + + // Shift all transitions in transitions_. The algorithm is + // similar to remove_if, but it also keeps the correspondence + // between the old and new index as newidx[old] = new. + unsigned tend = transitions_.size(); + std::vector newidx(tend); + unsigned dest = 1; + for (transition t = 1; t < tend; ++t) + { + if (transitions_[t].next_succ == t) + continue; + if (t != dest) + transitions_[dest] = std::move(transitions_[t]); + newidx[t] = dest; + ++dest; + } + + transitions_.resize(dest); + killed_trans_ = 0; + + // Adjust next_succ pointers in all transitions. + for (transition t = 1; t < dest; ++t) + transitions_[t].next_succ = newidx[transitions_[t].next_succ]; + + // Adjust succ and succ_tails pointers in all states. + for (auto& s: states_) + { + s.succ = newidx[s.succ]; + s.succ_tail = newidx[s.succ_tail]; + } + } + }; } diff --git a/src/graphtest/graph.cc b/src/graphtest/graph.cc index 4a7d0bbc9..f981e894c 100644 --- a/src/graphtest/graph.cc +++ b/src/graphtest/graph.cc @@ -55,7 +55,7 @@ void dot(std::ostream& out, spot::digraph& g) { out << "digraph {\n"; - unsigned c = g.nb_states(); + unsigned c = g.num_states(); for (unsigned s = 0; s < c; ++s) { out << ' ' << s; diff --git a/src/graphtest/ngraph.cc b/src/graphtest/ngraph.cc index 62542577b..3ab980c4f 100644 --- a/src/graphtest/ngraph.cc +++ b/src/graphtest/ngraph.cc @@ -73,7 +73,7 @@ void dot(std::ostream& out, const spot::digraph& g) { out << "digraph {\n"; - unsigned c = g.nb_states(); + unsigned c = g.num_states(); for (unsigned s = 0; s < c; ++s) { out << ' ' << s; @@ -93,7 +93,7 @@ dot(std::ostream& out, const spot::named_graph& g) { out << "digraph {\n"; auto& gg = g.graph(); - unsigned c = gg.nb_states(); + unsigned c = gg.num_states(); for (unsigned s = 0; s < c; ++s) { out << ' ' << s; diff --git a/src/graphtest/tgbagraph.cc b/src/graphtest/tgbagraph.cc index 67a3df7e6..ddbf7bdc0 100644 --- a/src/graphtest/tgbagraph.cc +++ b/src/graphtest/tgbagraph.cc @@ -44,6 +44,7 @@ void f1() auto s1 = g.new_state(); auto s2 = g.new_state(); auto s3 = g.new_state(); + g.new_transition(s1, s1, bddfalse, bddfalse); g.new_transition(s1, s2, p1, bddfalse); g.new_transition(s1, s3, p2, !a1 & a2); g.new_transition(s2, s3, p1 & p2, a1 & !a2); @@ -52,6 +53,36 @@ void f1() g.new_transition(s3, s3, bddtrue, (!a1 & a2) | (a1 & !a2)); spot::dotty_reachable(std::cout, &tg); + + { + auto i = g.out_iteraser(s3); + ++i; + i.erase(); + i.erase(); + assert(!i); + spot::dotty_reachable(std::cout, &tg); + } + + { + auto i = g.out_iteraser(s3); + i.erase(); + assert(!i); + spot::dotty_reachable(std::cout, &tg); + } + + g.new_transition(s3, s1, p1 | p2, (!a1 & a2) | (a1 & !a2)); + g.new_transition(s3, s2, p1 >> p2, bddfalse); + g.new_transition(s3, s1, bddtrue, (!a1 & a2) | (a1 & !a2)); + + std::cerr << tg.num_transitions() << '\n'; + assert(tg.num_transitions() == 7); + + spot::dotty_reachable(std::cout, &tg); + tg.merge_transitions(); + spot::dotty_reachable(std::cout, &tg); + + std::cerr << tg.num_transitions() << '\n'; + assert(tg.num_transitions() == 5); } int main() diff --git a/src/graphtest/tgbagraph.test b/src/graphtest/tgbagraph.test index 23f58c5d8..ea8f4ef8d 100755 --- a/src/graphtest/tgbagraph.test +++ b/src/graphtest/tgbagraph.test @@ -37,6 +37,7 @@ digraph G { 0 [label="", style=invis, height=0] 0 -> 1 1 [label="0"] + 1 -> 1 [label="0\n"] 1 -> 2 [label="p1\n"] 1 -> 3 [label="p2\n{Acc[p2]}"] 2 [label="1"] @@ -46,6 +47,55 @@ digraph G { 3 -> 2 [label="!p1 | p2\n"] 3 -> 3 [label="1\n{Acc[p2], Acc[p1]}"] } +digraph G { + 0 [label="", style=invis, height=0] + 0 -> 1 + 1 [label="0"] + 1 -> 1 [label="0\n"] + 1 -> 2 [label="p1\n"] + 1 -> 3 [label="p2\n{Acc[p2]}"] + 2 [label="1"] + 2 -> 3 [label="p1 & p2\n{Acc[p1]}"] + 3 [label="2"] + 3 -> 1 [label="p1 | p2\n{Acc[p2], Acc[p1]}"] +} +digraph G { + 0 [label="", style=invis, height=0] + 0 -> 1 + 1 [label="0"] + 1 -> 1 [label="0\n"] + 1 -> 2 [label="p1\n"] + 1 -> 3 [label="p2\n{Acc[p2]}"] + 2 [label="1"] + 2 -> 3 [label="p1 & p2\n{Acc[p1]}"] + 3 [label="2"] +} +digraph G { + 0 [label="", style=invis, height=0] + 0 -> 1 + 1 [label="0"] + 1 -> 1 [label="0\n"] + 1 -> 2 [label="p1\n"] + 1 -> 3 [label="p2\n{Acc[p2]}"] + 2 [label="1"] + 2 -> 3 [label="p1 & p2\n{Acc[p1]}"] + 3 [label="2"] + 3 -> 1 [label="p1 | p2\n{Acc[p2], Acc[p1]}"] + 3 -> 2 [label="!p1 | p2\n"] + 3 -> 1 [label="1\n{Acc[p2], Acc[p1]}"] +} +digraph G { + 0 [label="", style=invis, height=0] + 0 -> 1 + 1 [label="0"] + 1 -> 2 [label="p1\n"] + 1 -> 3 [label="p2\n{Acc[p2]}"] + 2 [label="1"] + 2 -> 3 [label="p1 & p2\n{Acc[p1]}"] + 3 [label="2"] + 3 -> 1 [label="1\n{Acc[p2], Acc[p1]}"] + 3 -> 2 [label="!p1 | p2\n"] +} EOF diff stdout expected diff --git a/src/misc/hash.hh b/src/misc/hash.hh index 625337bf3..9a8ae8cb8 100644 --- a/src/misc/hash.hh +++ b/src/misc/hash.hh @@ -75,6 +75,18 @@ namespace spot return s; } }; + + + struct pair_hash + { + template + std::size_t operator()(const std::pair &p) const + { + return wang32_hash(static_cast(p.first) ^ + static_cast(p.second)); + } + }; + } #endif // SPOT_MISC_HASH_HH diff --git a/src/tgba/tgbagraph.hh b/src/tgba/tgbagraph.hh index 559e5e51a..4db5c46d2 100644 --- a/src/tgba/tgbagraph.hh +++ b/src/tgba/tgbagraph.hh @@ -233,7 +233,7 @@ namespace spot { auto s = down_cast(st); assert(s); - assert(s->succ < g_.num_transitions()); + assert(!s->succ || g_.valid_trans(s->succ)); if (this->iter_cache_) { @@ -308,6 +308,47 @@ namespace spot { return bddtrue; } + + /// Iterate over all transitions, and merge those with compatible + /// extremities and acceptance. + void merge_transitions() + { + for (auto& s: g_.states()) + { + // Map a pair (dest state, acc) to the first transition seen + // with such characteristic. + + typedef std::pair key_t; + std::unordered_map trmap; + + auto t = g_.out_iteraser(s); + while (t) + { + // Simply skip false transitions. + if (t->cond == bddfalse) + { + t.erase(); + continue; + } + + key_t k(t->dst, t->acc.id()); + auto p = trmap.insert(make_pair(k, t.trans())); + if (!p.second) + { + // A previous transitions exist for k, merge the + // condition, and schedule the transition for + // removal. + g_.trans_data(p.first->second).cond |= t->cond; + t.erase(); + } + else + { + ++t; + } + } + } + g_.defrag(); + } }; }