diff --git a/src/graph/graph.hh b/src/graph/graph.hh index 9a16e4801..248308d52 100644 --- a/src/graph/graph.hh +++ b/src/graph/graph.hh @@ -26,6 +26,8 @@ #include #include #include +#include +#include namespace spot { @@ -68,6 +70,11 @@ namespace spot { return label; } + + bool operator<(const boxed_label& other) const + { + return label < other.label; + } }; template <> @@ -143,14 +150,16 @@ namespace spot // Again two implementation: one with label, and one without. - template + template struct SPOT_API trans_storage: public Trans_Data { typedef Transition transition; - State dst; // destination + StateOut dst; // destination Transition next_succ; // next outgoing transition with same // source, or 0 + StateIn src; // source explicit trans_storage() : Trans_Data{} @@ -158,11 +167,26 @@ namespace spot } template - trans_storage(State dst, Transition next_succ, Args&&... args) + trans_storage(StateOut dst, Transition next_succ, + StateIn src, Args&&... args) : Trans_Data{std::forward(args)...}, - dst(dst), next_succ(next_succ) + dst(dst), next_succ(next_succ), src(src) { } + + bool operator<(const trans_storage& other) const + { + if (src < other.src) + return true; + if (src > other.src) + return false; + // This might be costly if the destination is a vector + if (dst < other.dst) + return true; + if (dst < other.dst) + return false; + return this->data() < other.data(); + } }; ////////////////////////////////////////////////// @@ -200,12 +224,12 @@ namespace spot { } - bool operator==(trans_iterator o) + bool operator==(trans_iterator o) const { return t_ == o.t_; } - bool operator!=(trans_iterator o) + bool operator!=(trans_iterator o) const { return t_ != o.t_; } @@ -387,7 +411,7 @@ namespace spot typedef internal::distate_storage> state_storage_t; - typedef internal::trans_storage> trans_storage_t; typedef std::vector state_vector; @@ -520,7 +544,7 @@ namespace spot assert(src < states_.size()); transition t = transitions_.size(); - transitions_.emplace_back(dst, 0, std::forward(args)...); + transitions_.emplace_back(dst, 0, src, std::forward(args)...); transition st = states_[src].succ_tail; assert(st < t || !st); @@ -610,40 +634,95 @@ namespace spot return t.next_succ == index_of_transition(t); } - 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. + // To help debugging + void dump_storage(std::ostream& o) const + { unsigned tend = transitions_.size(); - std::vector newidx(tend); - unsigned dest = 1; + for (unsigned t = 1; t < tend; ++t) + { + o << 't' << t << ": (s" + << transitions_[t].src << ", s" + << transitions_[t].dst << ") t" + << transitions_[t].next_succ << '\n'; + } + unsigned send = states_.size(); + for (unsigned s = 0; s < send; ++s) + { + o << 's' << s << ": t" + << states_[s].succ << " t" + << states_[s].succ_tail << '\n'; + } + } + + // Remove all dead transitions. The transitions_ vector is left + // in a state that is incorrect and should eventually be fixed by + // a call to chain_transitions_() before any iteration on the + // successor of a state is performed. + void remove_dead_transitions_() + { + if (killed_trans_ == 0) + return; + auto i = std::remove_if(transitions_.begin() + 1, transitions_.end(), + [this](const trans_storage_t& t) { + return this->is_dead_transition(t); + }); + transitions_.erase(i, transitions_.end()); + killed_trans_ = 0; + } + + // This will invalidate all iterators, and also destroy transition + // chains. Call chain_transitions_() immediately afterwards + // unless you know what you are doing. + template> + void sort_transitions_(Predicate p = Predicate()) + { + //std::cerr << "\nbefore\n"; + //dump_storage(std::cerr); + std::sort(transitions_.begin() + 1, transitions_.end(), p); + } + + // Should be called only when it is known that all transitions + // with the same destination are consecutive in the vector. + void chain_transitions_() + { + state last_src = -1U; + transition tend = transitions_.size(); 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; + state src = transitions_[t].src; + if (src != last_src) + { + states_[src].succ = t; + if (last_src != -1U) + { + states_[last_src].succ_tail = t - 1; + transitions_[t - 1].next_succ = 0; + } + while (++last_src != src) + { + states_[last_src].succ = 0; + states_[last_src].succ_tail = 0; + } + } + else + { + transitions_[t - 1].next_succ = t; + } } - - 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_) + if (last_src != -1U) { - s.succ = newidx[s.succ]; - s.succ_tail = newidx[s.succ_tail]; + states_[last_src].succ_tail = tend - 1; + transitions_[tend - 1].next_succ = 0; } + unsigned send = states_.size(); + while (++last_src != send) + { + states_[last_src].succ = 0; + states_[last_src].succ_tail = 0; + } + //std::cerr << "\nafter\n"; + //dump_storage(std::cerr); } void defrag_states(std::vector&& newst, unsigned used_states) @@ -651,6 +730,9 @@ namespace spot assert(newst.size() == states_.size()); assert(used_states > 0); + //std::cerr << "\nbefore defrag\n"; + //dump_storage(std::cerr); + // Shift all states in states_, as indicated by newst. unsigned send = states_.size(); for (state s = 0; s < send; ++s) @@ -696,6 +778,7 @@ namespace spot auto& tr = transitions_[t]; tr.next_succ = newidx[tr.next_succ]; tr.dst = newst[tr.dst]; + tr.src = newst[tr.src]; assert(tr.dst != -1U); } @@ -705,6 +788,9 @@ namespace spot s.succ = newidx[s.succ]; s.succ_tail = newidx[s.succ_tail]; } + + //std::cerr << "\nafter defrag\n"; + //dump_storage(std::cerr); } }; diff --git a/src/tgba/tgbagraph.cc b/src/tgba/tgbagraph.cc index 2264fa2cd..5f721bbe6 100644 --- a/src/tgba/tgbagraph.cc +++ b/src/tgba/tgbagraph.cc @@ -25,41 +25,62 @@ 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()) + g_.remove_dead_transitions_(); + + typedef graph_t::trans_storage_t tr_t; + g_.sort_transitions_([](const tr_t& lhs, const tr_t& rhs) + { + if (lhs.src < rhs.src) + return true; + if (lhs.src > rhs.src) + return false; + if (lhs.dst < rhs.dst) + return true; + if (lhs.dst > rhs.dst) + return false; + return lhs.acc < rhs.acc; + // Do not sort on conditions, we'll merge + // them. + }); + + auto& trans = this->transitions(); + unsigned tend = trans.size(); + unsigned out = 0; + unsigned in = 1; + // Skip any leading false transition. + while (in < tend && trans[in].cond == bddfalse) + ++in; + if (in < tend) { - // Get a clear map for each state. - trmap.clear(); - - auto t = g_.out_iteraser(s); - while (t) + ++out; + if (out != in) + trans[out] = trans[in]; + for (++in; in < tend; ++in) { - // Simply skip false transitions. - if (t->cond == bddfalse) + if (trans[in].cond == bddfalse) // Unusable transition + continue; + // Merge transitions with the same source, destination, and + // acceptance. (We test the source last, because this is the + // most likely test to be true as transitions are ordered by + // sources and then destinations.) + if (trans[out].dst == trans[in].dst + && trans[out].acc == trans[in].acc + && trans[out].src == trans[in].src) { - t.erase(); - continue; - } - - key_t k(t->dst, t->acc); - auto p = trmap.emplace(k, t.trans()); - if (!p.second) - { - // A previous transitions exists for k. Merge the - // condition, and schedule the transition for removal. - g_.trans_data(p.first->second).cond |= t->cond; - t.erase(); + trans[out].cond |= trans[in].cond; } else { - ++t; + ++out; + if (in != out) + trans[out] = trans[in]; } } } - g_.defrag(); + if (++out != tend) + trans.resize(out); + + g_.chain_transitions_(); } void tgba_digraph::purge_unreachable_states() diff --git a/src/tgba/tgbagraph.hh b/src/tgba/tgbagraph.hh index 9f0bcf7a8..981dac2a8 100644 --- a/src/tgba/tgbagraph.hh +++ b/src/tgba/tgbagraph.hh @@ -87,6 +87,15 @@ namespace spot : cond(cond), acc(acc) { } + + bool operator<(const tgba_graph_trans_data& other) const + { + if (cond.id() < other.cond.id()) + return true; + if (cond.id() > other.cond.id()) + return false; + return acc < other.acc; + } }; diff --git a/src/tgbatest/degenlskip.test b/src/tgbatest/degenlskip.test index 3074f294e..b15c18cd4 100755 --- a/src/tgbatest/degenlskip.test +++ b/src/tgbatest/degenlskip.test @@ -38,15 +38,15 @@ digraph G { 0 -> 1 1 [label="0", peripheries=2] 1 -> 1 [label="a & b\n{0}"] - 1 -> 2 [label="!a & b\n{0}"] - 1 -> 3 [label="!b\n{0}"] + 1 -> 2 [label="!b\n{0}"] + 1 -> 3 [label="!a & b\n{0}"] 2 [label="1"] - 2 -> 1 [label="a"] - 2 -> 2 [label="!a"] + 2 -> 1 [label="a & b"] + 2 -> 2 [label="!b"] + 2 -> 3 [label="!a & b"] 3 [label="2"] - 3 -> 1 [label="a & b"] - 3 -> 2 [label="!a & b"] - 3 -> 3 [label="!b"] + 3 -> 1 [label="a"] + 3 -> 3 [label="!a"] } EOF @@ -58,13 +58,14 @@ digraph G { 1 [label="0", peripheries=2] 1 -> 2 [label="1\n{0}"] 2 [label="1"] - 2 -> 3 [label="b"] 2 -> 2 [label="!b"] + 2 -> 3 [label="b"] 3 [label="2"] 3 -> 1 [label="a"] 3 -> 3 [label="!a"] } EOF +# FIXME: use are-isomorphic once it is available diff out2 expected2 diff out3 expected3 diff --git a/src/tgbatest/det.test b/src/tgbatest/det.test index 3b56bbf2e..410e9cedc 100755 --- a/src/tgbatest/det.test +++ b/src/tgbatest/det.test @@ -72,23 +72,24 @@ EOF # FIXME: we should improve this output cat >ex.tgba <<'EOF' acc = "0"; -"0", "1", "a",; "0", "0", "!a",; +"0", "1", "a",; "0", "3", "!a",; -"1", "2", "a",; "1", "0", "!a",; +"1", "2", "a",; "1", "3", "!a",; "3", "3", "!a", "0"; -"2", "2", "a",; "2", "0", "!a",; -"2", "5", "a",; +"2", "2", "a",; "2", "3", "!a",; -"5", "5", "a", "0"; +"2", "5", "a",; "5", "3", "!a", "0"; +"5", "5", "a", "0"; EOF run 0 ../ltl2tgba -b -DC -X in.tgba > out.tgba +# FIXME: use are-isomorphic once it is available diff out.tgba ex.tgba diff --git a/src/tgbatest/ltl2ta.test b/src/tgbatest/ltl2ta.test index 3a97bde17..700f1282b 100755 --- a/src/tgbatest/ltl2ta.test +++ b/src/tgbatest/ltl2ta.test @@ -403,7 +403,7 @@ in: FG((WaitRight4 M (HasRight1 W GWaitLeft0)) M HasLeft4) -TA -DS -RT | 42 | 600 | 19 -TA -DS -lv | 55 | 800 | 19 -TA -DS -lv -RT | 44 | 694 | 13 --TA -DS -sp | 54 | 797 | 18 +-TA -DS -sp | 54 | 795 | 18 -TA -DS -sp -RT | 43 | 683 | 12 -TA -DS -lv -sp | 55 | 800 | 19 -TA -DS -lv -sp -RT | 44 | 694 | 13 diff --git a/src/tgbatest/neverclaimread.test b/src/tgbatest/neverclaimread.test index a8f74c924..d615afa6b 100755 --- a/src/tgbatest/neverclaimread.test +++ b/src/tgbatest/neverclaimread.test @@ -51,9 +51,9 @@ digraph G { 1 -> 1 [label="1"] 1 -> 2 [label="p0 & p1"] 2 [label="1"] - 2 -> 3 [label="p1 & !p0"] - 2 -> 2 [label="!p1"] 2 -> 1 [label="!p1"] + 2 -> 2 [label="!p1"] + 2 -> 3 [label="p1 & !p0"] 3 [label="2", peripheries=2] 3 -> 3 [label="1\n{0}"] } @@ -63,6 +63,7 @@ EOF # (The order is not guaranteed by SPOT.) sed -e 's/!p0 & p1/p1 \& !p0/g' -e 's/p1 & p0/p0 \& p1/g' stdout \ > tmp_ && mv tmp_ stdout +# FIXME: use are-isomorphic once it is available diff stdout expected rm input stdout expected @@ -95,9 +96,9 @@ digraph G { 1 -> 1 [label="1"] 1 -> 2 [label="p0 & p1"] 2 [label="1"] - 2 -> 3 [label="p1 & !p0"] - 2 -> 2 [label="!p1"] 2 -> 1 [label="!p1"] + 2 -> 2 [label="!p1"] + 2 -> 3 [label="p1 & !p0"] 3 [label="2", peripheries=2] 3 -> 3 [label="1\n{0}"] } @@ -107,6 +108,7 @@ EOF # (The order is not guaranteed by SPOT.) sed -e 's/!p0 & p1/p1 \& !p0/g' -e 's/p1 & p0/p0 \& p1/g' stdout \ > tmp_ && mv tmp_ stdout +# FIXME: use are-isomorphic once it is available diff stdout expected rm input stdout expected diff --git a/src/tgbatest/readsave.test b/src/tgbatest/readsave.test index 6b605e22c..16615cf66 100755 --- a/src/tgbatest/readsave.test +++ b/src/tgbatest/readsave.test @@ -72,13 +72,14 @@ EOF cat >expected <<\EOF acc = "0"; -"0", "1", "a", "0"; "0", "1", "!b",; +"0", "1", "a", "0"; "1", "0", "!b",; "1", "0", "a", "0"; EOF run 0 ../ltl2tgba -b -X input > stdout +# FIXME: use are-isomorphic once it is available diff stdout expected # Likewise, with a randomly generated TGBA.