diff --git a/src/graph/graph.hh b/src/graph/graph.hh index 85d71b418..d09cd1139 100644 --- a/src/graph/graph.hh +++ b/src/graph/graph.hh @@ -273,8 +273,7 @@ namespace spot killer_trans_iterator operator++(int) { killer_trans_iterator ti = *this; - prev_ = this->t_; - this->t_ = this->operator*().next_succ; + ++*this; return ti; } @@ -302,7 +301,7 @@ namespace spot // Erased transitions have themselves as next_succ. this->operator*().next_succ = this->t_; - // Advance iterator to next transitions. + // Advance iterator to next transition. this->t_ = next; ++this->g_->killed_trans_; @@ -647,6 +646,57 @@ namespace spot } } + void defrag_states(std::vector&& newst, unsigned used_states) + { + assert(newst.size() == states_.size()); + assert(used_states > 0); + + // Shift all states in states_, as indicated by newst. + unsigned send = states_.size(); + for (state s = 0; s < send; ++s) + { + state dst = newst[s]; + if (dst == s || dst == -1U) + continue; + states_[dst] = std::move(states_[s]); + } + states_.resize(used_states); + + // 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 (is_dead_transition(t)) + continue; + if (t != dest) + transitions_[dest] = std::move(transitions_[t]); + newidx[t] = dest; + ++dest; + } + transitions_.resize(dest); + killed_trans_ = 0; + + // Adjust next_succ and dst pointers in all transitions. + for (transition t = 1; t < dest; ++t) + { + auto& tr = transitions_[t]; + tr.next_succ = newidx[tr.next_succ]; + tr.dst = newst[tr.dst]; + assert(tr.dst != -1U); + } + + // 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/tgba/tgbagraph.cc b/src/tgba/tgbagraph.cc index 54f03bf0c..2cfa6d53c 100644 --- a/src/tgba/tgbagraph.cc +++ b/src/tgba/tgbagraph.cc @@ -25,13 +25,14 @@ namespace spot void tgba_digraph::merge_transitions() { + // Map a pair (dest state, acc) to the first transition seen + // with such characteristic. + typedef std::pair key_t; + std::unordered_map trmap; 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; + // Get a clear map for each state. + trmap.clear(); auto t = g_.out_iteraser(s); while (t) @@ -61,4 +62,57 @@ namespace spot g_.defrag(); } + void tgba_digraph::purge_dead_states() + { + unsigned num_states = g_.num_states(); + if (num_states == 0) + return; + std::vector info(num_states, 0); + // In this loop, info[s] means that the state is useless. + bool untouched; + do + { + untouched = true; + for (unsigned s = 0; s < num_states; ++s) + { + if (info[s]) + continue; + bool useless = true; + auto t = g_.out_iteraser(s); + while (t) + { + // Erase any transition to a unused state. + if (info[t->dst]) + { + t.erase(); + continue; + } + // if we have a transition, to a used state, + // then the state is useful. + useless = false; + ++t; + } + if (useless) + { + info[s] = true; + untouched = false; + } + } + } + while (!untouched); + + // Assume that the initial state is useful. + info[init_number_] = false; + // Now renumber each used state. + unsigned current = 0; + for (auto& v: info) + if (v) + v = -1U; + else + v = current++; + if (current == info.size()) + return; // No useless state. + init_number_ = info[init_number_]; + g_.defrag_states(std::move(info), current); + } } diff --git a/src/tgba/tgbagraph.hh b/src/tgba/tgbagraph.hh index 5d44878b5..84f49c674 100644 --- a/src/tgba/tgbagraph.hh +++ b/src/tgba/tgbagraph.hh @@ -388,6 +388,9 @@ namespace spot /// extremities and acceptance. void merge_transitions(); + /// Remove all states without successors. + void purge_dead_states(); + bool state_is_accepting(unsigned s) const { assert(has_state_based_acc()); diff --git a/src/tgbaalgos/dtgbacomp.cc b/src/tgbaalgos/dtgbacomp.cc index 36707918b..c64c8ae20 100644 --- a/src/tgbaalgos/dtgbacomp.cc +++ b/src/tgbaalgos/dtgbacomp.cc @@ -101,7 +101,7 @@ namespace spot res->new_transition(src, sink, missingcond); } res->merge_transitions(); - // FIXME: Remove unreachable states. + res->purge_dead_states(); return res; } diff --git a/src/tgbatest/det.test b/src/tgbatest/det.test index fc34a3cc0..1d9a6b952 100755 --- a/src/tgbatest/det.test +++ b/src/tgbatest/det.test @@ -105,7 +105,7 @@ digraph G { 2 -> 4 [label="!b"] 3 [label="3"] 3 -> 3 [label="!a\n{0}"] - 4 [label="5"] + 4 [label="4"] 4 -> 4 [label="!b\n{0}"] } EOF