diff --git a/NEWS b/NEWS index b34463943..11e46add9 100644 --- a/NEWS +++ b/NEWS @@ -73,6 +73,9 @@ New in spot 2.3.3.dev (not yet released) preprocess automata before feeding them to algorithms or tools that expect transitions labeled by letters. + - spot::scc_info has two new methods to easily iterate over the + edges of an SCC: edges_of() and inner_edges_of(). + Python: - The 'spot.gen' package exports the functions from libspotgen. diff --git a/python/spot/impl.i b/python/spot/impl.i index 493dd9f40..a87975dfa 100644 --- a/python/spot/impl.i +++ b/python/spot/impl.i @@ -555,7 +555,18 @@ def state_is_accepting(self, src) -> "bool": %include %traits_swigtype(spot::scc_info_node); %fragment(SWIG_Traits_frag(spot::scc_info_node)); +%nodefaultctor spot::internal::scc_edges; +%typemap(out, optimal="1") spot::internal::scc_edges const, spot::internal::keep_all> { + $result = SWIG_NewPointerObj((new $1_ltype($1)), $&1_descriptor, SWIG_POINTER_OWN); +} +%typemap(out, optimal="1") spot::internal::scc_edges const, spot::internal::keep_inner_scc> { + $result = SWIG_NewPointerObj((new $1_ltype($1)), $&1_descriptor, SWIG_POINTER_OWN); +} +%noexception spot::scc_info::edges_of; +%noexception spot::scc_info::inner_edges_of; %include +%template(scc_info_scc_edges) spot::internal::scc_edges const, spot::internal::keep_all>; +%template(scc_info_inner_scc_edges) spot::internal::scc_edges const, spot::internal::keep_inner_scc>; %include %include %include @@ -800,6 +811,22 @@ def state_is_accepting(self, src) -> "bool": } } +%extend spot::internal::scc_edges const, spot::internal::keep_all> { + swig::SwigPyIterator* __iter__(PyObject **PYTHON_SELF) + { + return swig::make_forward_iterator(self->begin(), self->begin(), + self->end(), *PYTHON_SELF); + } +} + +%extend spot::internal::scc_edges const, spot::internal::keep_inner_scc> { + swig::SwigPyIterator* __iter__(PyObject **PYTHON_SELF) + { + return swig::make_forward_iterator(self->begin(), self->begin(), + self->end(), *PYTHON_SELF); + } +} + %extend spot::twa_graph { unsigned new_univ_edge(unsigned src, const std::vector& v, bdd cond, acc_cond::mark_t acc = 0U) diff --git a/spot/twa/twagraph.hh b/spot/twa/twagraph.hh index 1c41db02f..e71eb481c 100644 --- a/spot/twa/twagraph.hh +++ b/spot/twa/twagraph.hh @@ -349,6 +349,11 @@ namespace spot return i->pos(); } + unsigned edge_number(const edge_storage_t& e) const + { + return g_.index_of_edge(e); + } + twa_graph_edge_data& edge_data(const twa_succ_iterator* it) { return g_.edge_data(edge_number(it)); diff --git a/spot/twaalgos/sccinfo.cc b/spot/twaalgos/sccinfo.cc index 1e5bc0108..1f9c81328 100644 --- a/spot/twaalgos/sccinfo.cc +++ b/spot/twaalgos/sccinfo.cc @@ -294,20 +294,16 @@ namespace spot std::set scc_info::used_acc_of(unsigned scc) const { std::set res; - for (auto src: states_of(scc)) - for (auto& t: aut_->out(src)) - if (scc_of(t.dst) == scc) - res.insert(t.acc); + for (auto& t: inner_edges_of(scc)) + res.insert(t.acc); return res; } acc_cond::mark_t scc_info::acc_sets_of(unsigned scc) const { acc_cond::mark_t res = 0U; - for (auto src: states_of(scc)) - for (auto& t: aut_->out(src)) - if (scc_of(t.dst) == scc) - res |= t.acc; + for (auto& t: inner_edges_of(scc)) + res |= t.acc; return res; } @@ -345,9 +341,8 @@ namespace spot bdd scc_info::scc_ap_support(unsigned scc) const { bdd support = bddtrue; - for (auto s: states_of(scc)) - for (auto& t: aut_->out(s)) - support &= bdd_support(t.cond); + for (auto& t: edges_of(scc)) + support &= bdd_support(t.cond); return support; } diff --git a/spot/twaalgos/sccinfo.hh b/spot/twaalgos/sccinfo.hh index 0ed2f2cf0..8f2b2eb9d 100644 --- a/spot/twaalgos/sccinfo.hh +++ b/spot/twaalgos/sccinfo.hh @@ -24,6 +24,168 @@ namespace spot { + class scc_info; + + namespace internal + { + struct keep_all + { + template + bool operator()(const Edge&) const noexcept + { + return true; + } + }; + + struct keep_inner_scc + { + private: + const std::vector& sccof_; + unsigned desired_scc_; + public: + keep_inner_scc(const std::vector& sccof, unsigned desired_scc) + : sccof_(sccof), desired_scc_(desired_scc) + { + } + + template + bool operator()(const Edge& ed) const noexcept + { + return sccof_[ed.dst] == desired_scc_; + } + }; + + template + class SPOT_API scc_edge_iterator + { + public: + typedef typename std::conditional::value, + const typename Graph::edge_storage_t, + typename Graph::edge_storage_t>::type + value_type; + typedef value_type& reference; + typedef value_type* pointer; + typedef std::ptrdiff_t difference_type; + typedef std::forward_iterator_tag iterator_category; + + typedef std::vector::const_iterator state_iterator; + + typedef typename std::conditional::value, + const typename Graph::edge_vector_t, + typename Graph::edge_vector_t>::type + tv_t; + + typedef typename std::conditional::value, + const typename Graph::state_vector, + typename Graph::state_vector>::type + sv_t; + protected: + + state_iterator pos_; + state_iterator end_; + unsigned t_; + tv_t* tv_; + sv_t* sv_; + Filter filt_; + + void inc_state_maybe_() + { + while (!t_ && (++pos_ != end_)) + t_ = (*sv_)[*pos_].succ; + } + + void inc_() + { + t_ = (*tv_)[t_].next_succ; + inc_state_maybe_(); + } + + public: + scc_edge_iterator(state_iterator begin, state_iterator end, + tv_t* tv, sv_t* sv, Filter filt) noexcept + : pos_(begin), end_(end), tv_(tv), sv_(sv), filt_(filt) + { + if (pos_ == end_) + return; + + t_ = (*sv_)[*pos_].succ; + inc_state_maybe_(); + while (pos_ != end_ && !filt_(**this)) + inc_(); + } + + scc_edge_iterator& operator++() + { + do + inc_(); + while (pos_ != end_ && !filt_(**this)); + return *this; + } + + scc_edge_iterator operator++(int) + { + scc_edge_iterator old = *this; + ++*this; + return old; + } + + bool operator==(scc_edge_iterator o) const + { + return pos_ == o.pos_ && t_ == o.t_; + } + + bool operator!=(scc_edge_iterator o) const + { + return pos_ != o.pos_ || t_ != o.t_; + } + + reference operator*() const + { + return (*tv_)[t_]; + } + + pointer operator->() const + { + return &**this; + } + }; + + + template + class SPOT_API scc_edges + { + public: + typedef scc_edge_iterator iter_t; + typedef typename iter_t::tv_t tv_t; + typedef typename iter_t::sv_t sv_t; + typedef typename iter_t::state_iterator state_iterator; + private: + state_iterator begin_; + state_iterator end_; + unsigned t_; + tv_t* tv_; + sv_t* sv_; + Filter filt_; + public: + + scc_edges(state_iterator begin, state_iterator end, + tv_t* tv, sv_t* sv, Filter filt) noexcept + : begin_(begin), end_(end), tv_(tv), sv_(sv), filt_(filt) + { + } + + iter_t begin() const + { + return {begin_, end_, tv_, sv_, filt_}; + } + + iter_t end() const + { + return {end_, end_, nullptr, nullptr, filt_}; + } + }; + } + /// Storage for SCC related information. class SPOT_API scc_info_node @@ -189,6 +351,37 @@ namespace spot return node(scc).states(); } + /// \brief A fake container to iterate over all edges leaving any + /// state of an SCC. + /// + /// The difference with inner_edges_of() is that edges_of() include + /// outgoing edges from all the states, even if they leave the SCC. + internal::scc_edges + edges_of(unsigned scc) const + { + auto& states = states_of(scc); + return {states.begin(), states.end(), + &aut_->edge_vector(), &aut_->states(), + internal::keep_all()}; + } + + /// \brief A fake container to iterate over all edges between + /// states of an SCC. + /// + /// The difference with edges_of() is that inner_edges_of() ignores + /// edges leaving the SCC are ignored. + internal::scc_edges + inner_edges_of(unsigned scc) const + { + if (!aut_->is_existential()) + throw std::runtime_error + ("inner_edges_of(): alternating automata are not supported"); + auto& states = states_of(scc); + return {states.begin(), states.end(), + &aut_->edge_vector(), &aut_->states(), + internal::keep_inner_scc(sccof_, scc)}; + } + unsigned one_state_of(unsigned scc) const { return states_of(scc).front(); diff --git a/spot/twaalgos/strength.cc b/spot/twaalgos/strength.cc index 418583c78..d9c43bf16 100644 --- a/spot/twaalgos/strength.cc +++ b/spot/twaalgos/strength.cc @@ -51,25 +51,24 @@ namespace spot bool first = true; acc_cond::mark_t m = 0U; if (is_weak) - for (auto src: si->states_of(i)) - for (auto& t: aut->out(src)) - // In case of a universal edge we only need to check - // the first destination of an inside the SCC, because - // the other have the same t.acc. - if (si->scc_of(*aut->univ_dests(t.dst).begin()) == i) - { - if (first) - { - first = false; - m = t.acc; - } - else if (m != t.acc) - { - is_weak = false; - if (!inweak) - goto exit; - } - } + for (auto& t: si->edges_of(i)) + // In case of a universal edge we only need to check if + // the first destination of an edge is inside the SCC, + // because the others have the same t.acc. + if (si->scc_of(*aut->univ_dests(t.dst).begin()) == i) + { + if (first) + { + first = false; + m = t.acc; + } + else if (m != t.acc) + { + is_weak = false; + if (!inweak) + goto exit; + } + } if (!is_weak && si->is_accepting_scc(i)) { assert(inweak); diff --git a/tests/python/sccinfo.py b/tests/python/sccinfo.py index 38295fc4f..19c5d21c1 100644 --- a/tests/python/sccinfo.py +++ b/tests/python/sccinfo.py @@ -52,15 +52,28 @@ l3 = si.states_of(3) l = sorted(list(l0) + list(l1) + list(l2) + list(l3)) assert l == [0, 1, 2, 3, 4] + + i = si.initial() todo = {i} seen = {i} +trans = [] +transi = [] while todo: e = todo.pop() + for t in si.edges_of(e): + trans.append((t.src, t.dst)) + for t in si.inner_edges_of(e): + transi.append((t.src, t.dst, a.edge_number(t))) for s in si.succ(e): if s not in seen: seen.add(s) todo.add(s) assert seen == {0, 1, 2, 3} +assert trans == [(1, 0), (1, 1), (1, 2), (1, 3), + (2, 1), (2, 2), (2, 3), (2, 4), + (0, 0), (3, 3), (4, 3), (4, 4)] +assert transi == [(1, 1, 3), (1, 2, 4), (2, 1, 6), (2, 2, 7), + (0, 0, 1), (3, 3, 10), (4, 4, 12)] assert not spot.is_weak_automaton(a, si)