From 223b0c6a9e7901b4896bb4402ded8c885be6c225 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 3 Aug 2017 18:27:47 +0200 Subject: [PATCH] is_weak_scc and friend: make them work for alternating automata * spot/twaalgos/isweakscc.cc, spot/twaalgos/isweakscc.hh, spot/twaalgos/mask.cc, spot/twaalgos/mask.hh: Adjust to work with alternating automata. * spot/twaalgos/sccinfo.cc, spot/twaalgos/sccinfo.hh (determine_unknown_acceptance): Do not complain about not supporting alternating automata if there is not indeterminate acceptance. * spot/twaalgos/stats.cc: Fix a bug were %[iw]c was read as %[iww]c. * tests/core/alternating.test: Test is_inherently_weak_scc() and is_weak_scc(). * python/spot/impl.i: Add missing python bindings for isweakscc.hh. --- python/spot/impl.i | 2 ++ spot/twaalgos/isweakscc.cc | 50 ++++++++++++++++++------------ spot/twaalgos/isweakscc.hh | 6 ++-- spot/twaalgos/mask.cc | 19 ++++++++++-- spot/twaalgos/mask.hh | 50 +++++++++++++++++++++++------- spot/twaalgos/sccinfo.cc | 6 ++-- spot/twaalgos/sccinfo.hh | 62 ++++++++++++++++++++++++++----------- spot/twaalgos/stats.cc | 18 ++++++++--- tests/core/alternating.test | 2 ++ 9 files changed, 154 insertions(+), 61 deletions(-) diff --git a/python/spot/impl.i b/python/spot/impl.i index d629c0cc5..771da0fb3 100644 --- a/python/spot/impl.i +++ b/python/spot/impl.i @@ -143,6 +143,7 @@ #include #include #include +#include #include #include #include @@ -574,6 +575,7 @@ def state_is_accepting(self, src) -> "bool": %include %include %include +%include %include %include %include diff --git a/spot/twaalgos/isweakscc.cc b/spot/twaalgos/isweakscc.cc index feafb2cd3..02d22a4f3 100644 --- a/spot/twaalgos/isweakscc.cc +++ b/spot/twaalgos/isweakscc.cc @@ -23,20 +23,29 @@ namespace spot { + namespace + { + [[noreturn]] static void + invalid_scc_number(const char* fn) + { + throw std::invalid_argument(std::string(fn) + "(): invalid SCC number"); + } + } + bool scc_has_rejecting_cycle(scc_info& map, unsigned scc) { + if (SPOT_UNLIKELY(scc >= map.scc_count())) + invalid_scc_number("scc_has_rejecting_cycle"); auto aut = map.get_aut(); - if (!aut->is_existential()) - throw std::runtime_error - ("scc_has_rejecting_cycle() does not support alternation"); // We check that by cloning the SCC and complementing its // acceptance condition. std::vector keep(aut->num_states(), false); auto& states = map.states_of(scc); for (auto s: states) keep[s] = true; - auto sccaut = mask_keep_accessible_states(aut, keep, states.front()); + auto sccaut = mask_keep_accessible_states(aut, keep, states.front(), + /* drop_univ_branch = */ true); sccaut->set_acceptance(sccaut->acc().num_sets(), sccaut->get_acceptance().complement()); return !sccaut->is_empty(); @@ -45,9 +54,8 @@ namespace spot bool is_inherently_weak_scc(scc_info& map, unsigned scc) { - if (!map.get_aut()->is_existential()) - throw std::runtime_error - ("is_inherently_weak_scc() does not support alternation"); + if (SPOT_UNLIKELY(scc >= map.scc_count())) + invalid_scc_number("is_inherently_weak_scc"); // Weak SCCs are inherently weak. if (is_weak_scc(map, scc)) return true; @@ -60,10 +68,8 @@ namespace spot bool is_weak_scc(scc_info& map, unsigned scc) { - if (!map.get_aut()->is_existential()) - throw std::runtime_error - ("is_weak_scc() does not support alternation"); - + if (SPOT_UNLIKELY(scc >= map.scc_count())) + invalid_scc_number("is_weak_scc"); // Rejecting SCCs are weak. if (map.is_rejecting_scc(scc)) return true; @@ -74,10 +80,9 @@ namespace spot bool is_complete_scc(scc_info& map, unsigned scc) { + if (SPOT_UNLIKELY(scc >= map.scc_count())) + invalid_scc_number("is_complete_scc"); auto a = map.get_aut(); - if (!a->is_existential()) - throw std::runtime_error - ("is_complete_scc() does not support alternation"); for (auto s: map.states_of(scc)) { bool has_succ = false; @@ -85,8 +90,16 @@ namespace spot for (auto& t: a->out(s)) { has_succ = true; - if (map.scc_of(t.dst) == scc) - sumall |= t.cond; + bool in = true; + for (auto d: a->univ_dests(t.dst)) + if (map.scc_of(d) != scc) + { + in = false; + break; + } + if (!in) + continue; + sumall |= t.cond; if (sumall == bddtrue) break; } @@ -99,9 +112,8 @@ namespace spot bool is_terminal_scc(scc_info& map, unsigned scc) { - if (!map.get_aut()->is_existential()) - throw std::runtime_error - ("is_terminal_scc() does not support alternation"); + if (SPOT_UNLIKELY(scc >= map.scc_count())) + invalid_scc_number("is_terminal_scc"); // If all transitions use all acceptance conditions, the SCC is weak. return (map.is_accepting_scc(scc) diff --git a/spot/twaalgos/isweakscc.hh b/spot/twaalgos/isweakscc.hh index d2a473396..bc296519f 100644 --- a/spot/twaalgos/isweakscc.hh +++ b/spot/twaalgos/isweakscc.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et +// Copyright (C) 2012, 2013, 2014, 2017 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -54,7 +54,9 @@ namespace spot /// \brief Whether the SCC number \a scc in \a map is complete. /// /// An SCC is complete iff for all states and all label there exists - /// a transition that stays into this SCC. + /// a transition that stays into this SCC. For this function, + /// universal transitions are considered in the SCC if all there + /// destination are into the SCC. SPOT_API bool is_complete_scc(scc_info& map, unsigned scc); diff --git a/spot/twaalgos/mask.cc b/spot/twaalgos/mask.cc index 7a2b666c1..70fbb22e5 100644 --- a/spot/twaalgos/mask.cc +++ b/spot/twaalgos/mask.cc @@ -69,7 +69,8 @@ namespace spot twa_graph_ptr mask_keep_accessible_states(const const_twa_graph_ptr& in, std::vector& to_keep, - unsigned int init) + unsigned int init, + bool drop_univ_branches) { if (to_keep.size() < in->num_states()) to_keep.resize(in->num_states(), false); @@ -83,9 +84,21 @@ namespace spot acc_cond::mark_t&, unsigned dst) { - if (!to_keep[src] || !to_keep[dst]) + if (!to_keep[src]) + { + cond = bddfalse; + return; + } + bool want = false; + for (auto d: in->univ_dests(dst)) + if (to_keep[d]) + { + want = true; + break; + } + if (!want) cond = bddfalse; - }, init); + }, init, drop_univ_branches); return res; } diff --git a/spot/twaalgos/mask.hh b/spot/twaalgos/mask.hh index 2f40368c0..8d21022d1 100644 --- a/spot/twaalgos/mask.hh +++ b/spot/twaalgos/mask.hh @@ -44,16 +44,16 @@ namespace spot /// `aut->get_named_prop>("original-states")` /// to retrieve it. /// + /// If \a drop_univ_branches branch is set, universal branching is replaced + /// by existential branching during the copy. + /// /// \param init The optional new initial state. template void transform_accessible(const const_twa_graph_ptr& old, twa_graph_ptr& cpy, - Trans trans, unsigned int init) + Trans trans, unsigned int init, + bool drop_univ_branches = false) { - if (!old->is_existential()) - throw std::runtime_error - ("transform_accessible() does not support alternation"); - std::vector todo; std::vector seen(old->num_states(), -1U); @@ -75,7 +75,27 @@ namespace spot return tmp; }; - cpy->set_init_state(new_state(init)); + // Deal with alternating automata, possibly. + std::map, unsigned> uniq; + auto new_univ_state = + [&](unsigned old_state) -> unsigned + { + if (!old->is_univ_dest(old_state)) + return new_state(old_state); + + std::vector tmp; + for (auto s: old->univ_dests(old_state)) + tmp.emplace_back(new_state(s)); + std::sort(tmp.begin(), tmp.end()); + tmp.erase(std::unique(tmp.begin(), tmp.end()), tmp.end()); + auto p = uniq.emplace(tmp, 0); + if (p.second) + p.first->second = + cpy->get_graph().new_univ_dests(tmp.begin(), tmp.end()); + return p.first->second; + }; + + cpy->set_init_state(new_univ_state(init)); if (seen[init] != 0) throw std::runtime_error ("the destination automaton of transform_accessible() should be empty"); @@ -93,13 +113,15 @@ namespace spot bdd cond = t.cond; acc_cond::mark_t acc = t.acc; trans(t.src, cond, acc, t.dst); - - if (cond != bddfalse) - cpy->new_edge(new_src, new_state(t.dst), - cond, acc); + if (cond == bddfalse) + continue; + if (drop_univ_branches) + for (unsigned d: old->univ_dests(t.dst)) + cpy->new_edge(new_src, new_state(d), cond, acc); + else + cpy->new_edge(new_src, new_univ_state(t.dst), cond, acc); } } - orig_states->shrink_to_fit(); } @@ -186,9 +208,13 @@ namespace spot /// will be set to \a init. Only states that are accessible from \a /// init via states in \a to_keep will be preserved. /// + /// If \a drop_univ_branches branch is set, universal branching is replaced + /// by existential branching during the copy. + /// /// \see mask_keep_states SPOT_API twa_graph_ptr mask_keep_accessible_states(const const_twa_graph_ptr& in, std::vector& to_keep, - unsigned int init); + unsigned int init, + bool drop_univ_branches = false); } diff --git a/spot/twaalgos/sccinfo.cc b/spot/twaalgos/sccinfo.cc index 59ff4071c..eda86b5b8 100644 --- a/spot/twaalgos/sccinfo.cc +++ b/spot/twaalgos/sccinfo.cc @@ -367,15 +367,15 @@ namespace spot void scc_info::determine_unknown_acceptance() { - if (!aut_->is_existential()) - throw std::runtime_error("scc_info::determine_unknown_acceptance() " - "does not support alternating automata"); std::vector k; unsigned n = scc_count(); bool changed = false; for (unsigned s = 0; s < n; ++s) if (!is_rejecting_scc(s) && !is_accepting_scc(s)) { + if (!aut_->is_existential()) + throw std::runtime_error("scc_info::determine_unknown_acceptance() " + "does not support alternating automata"); auto& node = node_[s]; if (k.empty()) k.resize(aut_->num_states()); diff --git a/spot/twaalgos/sccinfo.hh b/spot/twaalgos/sccinfo.hh index 70a2c0fbe..2ce129377 100644 --- a/spot/twaalgos/sccinfo.hh +++ b/spot/twaalgos/sccinfo.hh @@ -30,13 +30,15 @@ namespace spot { struct keep_all { - template - bool operator()(const Edge&) const noexcept + template + bool operator()(Iterator, Iterator) const noexcept { return true; } }; + // Keep only transitions that have at least one destination in the + // current SCC. struct keep_inner_scc { private: @@ -48,10 +50,17 @@ namespace spot { } - template - bool operator()(const Edge& ed) const noexcept + template + bool operator()(Iterator begin, Iterator end) const noexcept { - return sccof_[ed.dst] == desired_scc_; + bool want = false; + while (begin != end) + if (sccof_[*begin++] == desired_scc_) + { + want = true; + break; + } + return want; } }; @@ -79,6 +88,7 @@ namespace spot const typename Graph::state_vector, typename Graph::state_vector>::type sv_t; + typedef const typename Graph::dests_vector_t dv_t; protected: state_iterator pos_; @@ -86,6 +96,8 @@ namespace spot unsigned t_; tv_t* tv_; sv_t* sv_; + dv_t* dv_; + Filter filt_; void inc_state_maybe_() @@ -100,17 +112,28 @@ namespace spot inc_state_maybe_(); } + 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); + } + public: scc_edge_iterator(state_iterator begin, state_iterator end, - tv_t* tv, sv_t* sv, Filter filt) noexcept - : pos_(begin), end_(end), t_(0), tv_(tv), sv_(sv), filt_(filt) + 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) { if (pos_ == end_) return; t_ = (*sv_)[*pos_].succ; inc_state_maybe_(); - while (pos_ != end_ && !filt_(**this)) + while (pos_ != end_ && ignore_current()) inc_(); } @@ -118,7 +141,7 @@ namespace spot { do inc_(); - while (pos_ != end_ && !filt_(**this)); + while (pos_ != end_ && ignore_current()); return *this; } @@ -158,29 +181,31 @@ namespace spot 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::dv_t dv_t; typedef typename iter_t::state_iterator state_iterator; private: state_iterator begin_; state_iterator end_; tv_t* tv_; sv_t* sv_; + dv_t* dv_; 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) + tv_t* tv, sv_t* sv, dv_t* dv, Filter filt) noexcept + : begin_(begin), end_(end), tv_(tv), sv_(sv), dv_(dv), filt_(filt) { } iter_t begin() const { - return {begin_, end_, tv_, sv_, filt_}; + return {begin_, end_, tv_, sv_, dv_, filt_}; } iter_t end() const { - return {end_, end_, nullptr, nullptr, filt_}; + return {end_, end_, nullptr, nullptr, nullptr, filt_}; } }; } @@ -408,23 +433,24 @@ namespace spot auto& states = states_of(scc); return {states.begin(), states.end(), &aut_->edge_vector(), &aut_->states(), + &aut_->get_graph().dests_vector(), 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. + /// The difference with edges_of() is that inner_edges_of() + /// ignores edges leaving the SCC are ignored. In the case of + /// alternating automaton, an edge is considered to be part of the + /// SCC of one of its destination is in the SCC. 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(), + &aut_->get_graph().dests_vector(), internal::keep_inner_scc(sccof_, scc)}; } diff --git a/spot/twaalgos/stats.cc b/spot/twaalgos/stats.cc index db9c998b7..b4b151f5f 100644 --- a/spot/twaalgos/stats.cc +++ b/spot/twaalgos/stats.cc @@ -256,15 +256,25 @@ namespace spot break; case 'i': if (pos[1] == 'w') - inherently_weak = true; + { + inherently_weak = true; + ++pos; + } else - error(std::string(pos, pos + 2)); + { + error(std::string(pos, pos + 2)); + } break; case 'I': if (pos[1] == 'W') - non_inherently_weak = true; + { + non_inherently_weak = true; + ++pos; + } else - error(std::string(pos, pos + 2)); + { + error(std::string(pos, pos + 2)); + } break; case ' ': case '\t': diff --git a/tests/core/alternating.test b/tests/core/alternating.test index 8bad81e12..1686f774f 100755 --- a/tests/core/alternating.test +++ b/tests/core/alternating.test @@ -1840,6 +1840,7 @@ State: 2 "t" EOF autfilt --tgba in 2>out && exit 1 grep 'autfilt.*weak.*alternating' out +test '0 2 2 1' = "`autfilt --stats='%[Wiw]c %[w]c %[iw]c %[W]c' in`" cat >in <out && exit 1 grep 'autfilt.*weak.*alternating' out +test '2 0 2 2' = "`autfilt --stats='%[Wiw]c %[w]c %[iw]c %[W]c' in`"