From b214fd75d6032a5dceb5a26dc0774acb6efbd2a8 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 15 Jul 2020 11:30:52 +0200 Subject: [PATCH] scc_info: honor filters in edges_of() and inner_edges_of() * spot/twaalgos/sccinfo.hh: Honor filters in edges_of() and inner_edges_of(). * tests/core/sccif.test: Adjust expected output. * NEWS: Mention the bug. --- NEWS | 3 + spot/twaalgos/sccinfo.hh | 128 ++++++++++++++++++++++++++------------- tests/core/sccif.test | 4 +- 3 files changed, 90 insertions(+), 45 deletions(-) diff --git a/NEWS b/NEWS index d04256d35..a775fa78f 100644 --- a/NEWS +++ b/NEWS @@ -71,6 +71,9 @@ New in spot 2.9.0.dev (not yet released) acceptance sets than supported by Spot. This is now diagnosed with --verbose, but does not prevent ltlcross from continuing. + - scc_info::edges_of() and scc_info::inner_edges_of() now correctly + honor any filter passed to scc_info. + New in spot 2.9 (2020-04-30) Command-line tools: diff --git a/spot/twaalgos/sccinfo.hh b/spot/twaalgos/sccinfo.hh index 3c31c3dcd..a76ca3612 100644 --- a/spot/twaalgos/sccinfo.hh +++ b/spot/twaalgos/sccinfo.hh @@ -27,6 +27,38 @@ namespace spot { class scc_info; + /// @{ + /// \ingroup twa_misc + /// \brief An edge_filter may be called on each edge to decide what + /// to do with it. + /// + /// The edge filter is called with an edge and a destination. (In + /// existential automata the destination is already given by the + /// edge, but in alternating automata, one edge may have several + /// destinations, and in this case the filter will be called for + /// each destination.) The filter should return a value from + /// edge_filter_choice. + /// + /// \c keep means to use the edge normally, as if no filter had + /// been given. \c ignore means to pretend the edge does not + /// exist (if the destination is only reachable through this edge, + /// it will not be visited). \c cut also ignores the edge, but + /// it remembers to visit the destination state (as if it were an + /// initial state) in case it is not reachable otherwise. + /// + /// Note that successors between SCCs can only be maintained for + /// edges that are kept. If some edges are ignored or cut, the + /// SCC graph that you can explore with scc_info::initial() and + /// scc_info::succ() will be restricted to the portion reachable + /// with "keep" edges. Additionally SCCs might be created when + /// edges are cut, but those will not be reachable from + /// scc_info::initial().. + enum class edge_filter_choice { keep, ignore, cut }; + typedef edge_filter_choice + (*edge_filter)(const twa_graph::edge_storage_t& e, unsigned dst, + void* filter_data); + /// @} + namespace internal { struct keep_all @@ -100,6 +132,9 @@ namespace spot dv_t* dv_; Filter filt_; + edge_filter efilter_; + void* efilter_data_; + void inc_state_maybe_() { @@ -113,21 +148,49 @@ namespace spot inc_state_maybe_(); } + // Do we ignore the current transition? bool ignore_current() { unsigned dst = (*this)->dst; if ((int)dst >= 0) - // Non-universal branching => a single destination. - return !filt_(&(*this)->dst, 1 + &(*this)->dst); - // Universal branching => multiple destinations. - const unsigned* d = dv_->data() + ~dst; - return !filt_(d + 1, d + *d + 1); + { + // Non-universal branching => a single destination. + if (!filt_(&(*this)->dst, 1 + &(*this)->dst)) + return true; + if (efilter_) + return efilter_((*tv_)[t_], dst, efilter_data_) + != edge_filter_choice::keep; + return false; + } + else + { + // Universal branching => multiple destinations. + const unsigned* d = dv_->data() + ~dst; + if (!filt_(d + 1, d + *d + 1)) + return true; + if (efilter_) + { + // Keep the transition if at least one destination + // is not filtered. + const unsigned* end = d + *d + 1; + for (const unsigned* i = d + 1; i != end; ++i) + { + if (efilter_((*tv_)[t_], *i, efilter_data_) + == edge_filter_choice::keep) + return false; + return true; + } + } + return false; + } } public: scc_edge_iterator(state_iterator begin, state_iterator end, - tv_t* tv, sv_t* sv, dv_t* dv, Filter filt) noexcept - : pos_(begin), end_(end), t_(0), tv_(tv), sv_(sv), dv_(dv), filt_(filt) + tv_t* tv, sv_t* sv, dv_t* dv, Filter filt, + edge_filter efilter, void* efilter_data) noexcept + : pos_(begin), end_(end), t_(0), tv_(tv), sv_(sv), dv_(dv), filt_(filt), + efilter_(efilter), efilter_data_(efilter_data) { if (pos_ == end_) return; @@ -191,22 +254,26 @@ namespace spot sv_t* sv_; dv_t* dv_; Filter filt_; + edge_filter efilter_; + void* efilter_data_; public: scc_edges(state_iterator begin, state_iterator end, - tv_t* tv, sv_t* sv, dv_t* dv, Filter filt) noexcept - : begin_(begin), end_(end), tv_(tv), sv_(sv), dv_(dv), filt_(filt) + tv_t* tv, sv_t* sv, dv_t* dv, Filter filt, + edge_filter efilter, void* efilter_data) noexcept + : begin_(begin), end_(end), tv_(tv), sv_(sv), dv_(dv), filt_(filt), + efilter_(efilter), efilter_data_(efilter_data) { } iter_t begin() const { - return {begin_, end_, tv_, sv_, dv_, filt_}; + return {begin_, end_, tv_, sv_, dv_, filt_, efilter_, efilter_data_}; } iter_t end() const { - return {end_, end_, nullptr, nullptr, nullptr, filt_}; + return {end_, end_, nullptr, nullptr, nullptr, filt_, nullptr, nullptr}; } }; } @@ -378,36 +445,10 @@ namespace spot // support that yet. typedef scc_info_node scc_node; typedef scc_info_node::scc_succs scc_succs; - /// @{ - /// \brief An edge_filter may be called on each edge to decide what - /// to do with it. - /// - /// The edge filter is called with an edge and a destination. (In - /// existential automata the destination is already given by the - /// edge, but in alternating automata, one edge may have several - /// destinations, and in this case the filter will be called for - /// each destination.) The filter should return a value from - /// edge_filter_choice. - /// - /// \c keep means to use the edge normally, as if no filter had - /// been given. \c ignore means to pretend the edge does not - /// exist (if the destination is only reachable through this edge, - /// it will not be visited). \c cut also ignores the edge, but - /// it remembers to visit the destination state (as if it were an - /// initial state) in case it is not reachable otherwise. - /// - /// Note that successors between SCCs can only be maintained for - /// edges that are kept. If some edges are ignored or cut, the - /// SCC graph that you can explore with scc_info::initial() and - /// scc_info::succ() will be restricted to the portion reachable - /// with "keep" edges. Additionally SCCs might be created when - /// edges are cut, but those will not be reachable from - /// scc_info::initial().. - enum class edge_filter_choice { keep, ignore, cut }; - typedef edge_filter_choice - (*edge_filter)(const twa_graph::edge_storage_t& e, unsigned dst, - void* filter_data); - /// @} + + // These types used to be defined here in Spot up to 2.9. + typedef spot::edge_filter_choice edge_filter_choice; + typedef spot::edge_filter edge_filter; protected: @@ -559,7 +600,7 @@ namespace spot return {states.begin(), states.end(), &aut_->edge_vector(), &aut_->states(), &aut_->get_graph().dests_vector(), - internal::keep_all()}; + internal::keep_all(), filter_, const_cast(filter_data_)}; } /// \brief A fake container to iterate over all edges between @@ -576,7 +617,8 @@ namespace spot return {states.begin(), states.end(), &aut_->edge_vector(), &aut_->states(), &aut_->get_graph().dests_vector(), - internal::keep_inner_scc(sccof_, scc)}; + internal::keep_inner_scc(sccof_, scc), filter_, + const_cast(filter_data_)}; } unsigned one_state_of(unsigned scc) const diff --git a/tests/core/sccif.test b/tests/core/sccif.test index 2ee7f314c..2f3441f66 100755 --- a/tests/core/sccif.test +++ b/tests/core/sccif.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2017 Laboratoire de Recherche et Développement +# Copyright (C) 2017, 2020 Laboratoire de Recherche et Développement # de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -79,7 +79,7 @@ SCC#1 succs: 0 SCC#2 states: 2 - edges: 2->2 + edges: succs: 0 1 EOF