From fbbf584bbbd49bea59545ec53d9f0fd3ec33edee Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 8 Dec 2014 12:04:09 +0100 Subject: [PATCH] graph: let transitions() iterate only on valid transitions This fixes #6. * src/graph/graph.hh: Rename the old transitions() as transition_vector(), and implement a new transitions() that iterates only on non-dead transitions. * src/tgba/tgbagraph.hh, src/tgba/tgbagraph.cc, src/graph/ngraph.hh: Adjust wrappers. * src/hoaparse/hoaparse.yy, src/tgbaalgos/complete.cc, src/tgbaalgos/dtbasat.cc, src/tgbaalgos/dtgbasat.cc, src/tgbaalgos/randomize.cc, src/tgbaalgos/safety.cc: Adjust calls. --- src/graph/graph.hh | 132 ++++++++++++++++++++++++++++++++++++- src/graph/ngraph.hh | 2 +- src/hoaparse/hoaparse.yy | 4 +- src/tgba/tgbagraph.cc | 2 +- src/tgba/tgbagraph.hh | 5 ++ src/tgbaalgos/complete.cc | 2 +- src/tgbaalgos/dtbasat.cc | 3 +- src/tgbaalgos/dtgbasat.cc | 3 +- src/tgbaalgos/randomize.cc | 6 +- src/tgbaalgos/safety.cc | 5 +- 10 files changed, 147 insertions(+), 17 deletions(-) diff --git a/src/graph/graph.hh b/src/graph/graph.hh index 9f946c8ff..e7027e2c8 100644 --- a/src/graph/graph.hh +++ b/src/graph/graph.hh @@ -373,8 +373,121 @@ namespace spot transition t_; }; + ////////////////////////////////////////////////// + // all_trans + ////////////////////////////////////////////////// + + template + class SPOT_API all_trans_iterator: + std::iterator::value, + const typename Graph::trans_storage_t, + typename Graph::trans_storage_t>::type> + { + typedef + std::iterator::value, + const typename Graph::trans_storage_t, + typename Graph::trans_storage_t>::type> + super; + + typedef typename std::conditional::value, + const typename Graph::trans_vector, + typename Graph::trans_vector>::type + tv_t; + + unsigned t_; + tv_t& tv_; + + void skip_() + { + unsigned s = tv_.size(); + do + ++t_; + while (t_ < s && tv_[t_].next_succ == t_); + } + + public: + all_trans_iterator(unsigned pos, tv_t& tv) + : t_(pos), tv_(tv) + { + skip_(); + } + + all_trans_iterator(tv_t& tv) + : t_(tv.size()), tv_(tv) + { + } + + all_trans_iterator& operator++() + { + skip_(); + return *this; + } + + all_trans_iterator operator++(int) + { + all_trans_iterator old = *this; + ++*this; + return old; + } + + bool operator==(all_trans_iterator o) const + { + return t_ == o.t_; + } + + bool operator!=(all_trans_iterator o) const + { + return t_ != o.t_; + } + + typename super::reference + operator*() + { + return tv_[t_]; + } + + typename super::pointer + operator->() + { + return &tv_[t_]; + } + }; + + + template + class SPOT_API all_trans + { + typedef typename std::conditional::value, + const typename Graph::trans_vector, + typename Graph::trans_vector>::type + tv_t; + typedef all_trans_iterator iter_t; + tv_t& tv_; + public: + + all_trans(tv_t& tv) + : tv_(tv) + { + } + + iter_t begin() + { + return {0, tv_}; + } + + iter_t end() + { + return {tv_}; + } + }; + } + // The actual graph implementation template @@ -614,12 +727,27 @@ namespace spot return states_; } - const trans_vector& transitions() const + internal::all_trans transitions() const { return transitions_; } - trans_vector& transitions() + internal::all_trans transitions() + { + return transitions_; + } + + // When using this method, beware that the first entry (transition + // #0) is not a real transition, and that any transition with + // next_succ pointing to itself is an erased transition. + // + // You should probably use transitions() instead. + const trans_vector& transition_vector() const + { + return transitions_; + } + + trans_vector& transition_vector() { return transitions_; } diff --git a/src/graph/ngraph.hh b/src/graph/ngraph.hh index 684fc42f2..8232008c6 100644 --- a/src/graph/ngraph.hh +++ b/src/graph/ngraph.hh @@ -91,7 +91,7 @@ namespace spot auto old = p.first->second; p.first->second = s; // Add the successor of OLD to those of S. - auto& trans = g_.transitions(); + auto& trans = g_.transition_vector(); auto& states = g_.states(); trans[states[s].succ_tail].next_succ = states[old].succ; states[s].succ_tail = states[old].succ_tail; diff --git a/src/hoaparse/hoaparse.yy b/src/hoaparse/hoaparse.yy index 624e48aeb..3746223b3 100644 --- a/src/hoaparse/hoaparse.yy +++ b/src/hoaparse/hoaparse.yy @@ -953,7 +953,7 @@ static void fix_acceptance(result_& r) // If a set x appears only as Inf(!x), we can complement it so that // we work with Inf(x) instead. auto onlyneg = r.neg_acc_sets - r.pos_acc_sets; - for (auto& t: r.h->aut->transitions()) + for (auto& t: r.h->aut->transition_vector()) t.acc ^= onlyneg; // However if set x is used elsewhere, for instance in @@ -968,7 +968,7 @@ static void fix_acceptance(result_& r) auto v = acc.sets(both); auto vs = v.size(); unsigned base = acc.add_sets(vs); - for (auto& t: r.h->aut->transitions()) + for (auto& t: r.h->aut->transition_vector()) if ((t.acc & both) != both) for (unsigned i = 0; i < vs; ++i) if (!t.acc.has(i)) diff --git a/src/tgba/tgbagraph.cc b/src/tgba/tgbagraph.cc index 5f721bbe6..9b7abd606 100644 --- a/src/tgba/tgbagraph.cc +++ b/src/tgba/tgbagraph.cc @@ -43,7 +43,7 @@ namespace spot // them. }); - auto& trans = this->transitions(); + auto& trans = this->transition_vector(); unsigned tend = trans.size(); unsigned out = 0; unsigned in = 1; diff --git a/src/tgba/tgbagraph.hh b/src/tgba/tgbagraph.hh index 981dac2a8..ac5c951a8 100644 --- a/src/tgba/tgbagraph.hh +++ b/src/tgba/tgbagraph.hh @@ -405,6 +405,11 @@ namespace spot auto transitions() SPOT_RETURN(g_.transitions()); + auto transition_vector() const + SPOT_RETURN(g_.transition_vector()); + auto transition_vector() + SPOT_RETURN(g_.transition_vector()); + auto is_dead_transition(const graph_t::trans_storage_t& t) const SPOT_RETURN(g_.is_dead_transition(t)); diff --git a/src/tgbaalgos/complete.cc b/src/tgbaalgos/complete.cc index c56aef9a5..c318df5b4 100644 --- a/src/tgbaalgos/complete.cc +++ b/src/tgbaalgos/complete.cc @@ -32,7 +32,7 @@ namespace spot // acceptance set as the added sink would become accepting. // In this case, add an acceptance set to all transitions. allacc = aut->set_single_acceptance_set(); - for (auto& t: aut->transitions()) + for (auto& t: aut->transition_vector()) t.acc = allacc; } else diff --git a/src/tgbaalgos/dtbasat.cc b/src/tgbaalgos/dtbasat.cc index f4a1ccaf2..c581d7361 100644 --- a/src/tgbaalgos/dtbasat.cc +++ b/src/tgbaalgos/dtbasat.cc @@ -303,8 +303,7 @@ namespace spot // Compute the AP used in the hard way. bdd ap = bddtrue; for (auto& t: ref->transitions()) - if (!ref->is_dead_transition(t)) - ap &= bdd_support(t.cond); + ap &= bdd_support(t.cond); // Count the number of atomic propositions int nap = 0; diff --git a/src/tgbaalgos/dtgbasat.cc b/src/tgbaalgos/dtgbasat.cc index 805569feb..ab0999494 100644 --- a/src/tgbaalgos/dtgbasat.cc +++ b/src/tgbaalgos/dtgbasat.cc @@ -432,8 +432,7 @@ namespace spot // Compute the AP used in the hard way. bdd ap = bddtrue; for (auto& t: ref->transitions()) - if (!ref->is_dead_transition(t)) - ap &= bdd_support(t.cond); + ap &= bdd_support(t.cond); // Count the number of atomic propositions int nap = 0; diff --git a/src/tgbaalgos/randomize.cc b/src/tgbaalgos/randomize.cc index 285b7aedb..a5a6d8a8a 100644 --- a/src/tgbaalgos/randomize.cc +++ b/src/tgbaalgos/randomize.cc @@ -42,9 +42,9 @@ namespace spot } if (randomize_transitions) { - auto begin = g.transitions().begin() + 1; - auto end = g.transitions().end(); - std::random_shuffle(begin, end, spot::mrand); + g.remove_dead_transitions_(); + auto& v = g.transition_vector(); + std::random_shuffle(v.begin() + 1, v.end(), spot::mrand); } typedef tgba_digraph::graph_t::trans_storage_t tr_t; diff --git a/src/tgbaalgos/safety.cc b/src/tgbaalgos/safety.cc index 52f146f15..56e01e835 100644 --- a/src/tgbaalgos/safety.cc +++ b/src/tgbaalgos/safety.cc @@ -66,9 +66,8 @@ namespace spot bool is_safety_mwdba(const const_tgba_digraph_ptr& aut) { for (auto& t: aut->transitions()) - if (!aut->is_dead_transition(t)) - if (!aut->acc().accepting(t.acc)) - return false; + if (!aut->acc().accepting(t.acc)) + return false; return true; }