diff --git a/NEWS b/NEWS index 26de8a415..d8d0dc35d 100644 --- a/NEWS +++ b/NEWS @@ -88,6 +88,11 @@ New in spot 2.3.4.dev (not yet released) - spot::scc_info can now be passed a filter function to ignore or cut some edges. + - spot::scc_info now keeps track of acceptance sets that are common + to all edges in an SCC. These can be retrieved using + scc_info::common_sets_of(scc), and they are used by scc_info to + classify some SCCs as rejecting more easily. + Python: - The 'spot.gen' package exports the functions from libspotgen. diff --git a/spot/twaalgos/sccinfo.cc b/spot/twaalgos/sccinfo.cc index 03600684a..59ff4071c 100644 --- a/spot/twaalgos/sccinfo.cc +++ b/spot/twaalgos/sccinfo.cc @@ -40,7 +40,8 @@ namespace spot } acc_cond::mark_t in_acc; // Acceptance sets on the incoming transition - acc_cond::mark_t acc = 0U; // union of all acceptance sets in the SCC + acc_cond::mark_t acc = 0U; // union of all acceptance marks in the SCC + acc_cond::mark_t common = -1U; // intersection of all marks in the SCC int index; // Index of the SCC bool trivial = true; // Whether the SCC has no cycle bool accepting = false; // Necessarily accepting @@ -130,9 +131,10 @@ namespace spot if (root_.back().index == h_[curr]) { unsigned num = node_.size(); - auto acc = root_.back().acc; + acc_cond::mark_t acc = root_.back().acc; + acc_cond::mark_t common = root_.back().common; bool triv = root_.back().trivial; - node_.emplace_back(acc, triv); + node_.emplace_back(acc, common, triv); // Move all elements of this SCC from the live stack // to the the node. @@ -176,33 +178,8 @@ namespace spot succ.insert(succ.end(), dests.begin(), dests.end()); bool accept = !triv && root_.back().accepting; node_.back().accepting_ = accept; - bool reject = triv || !aut->acc().inf_satisfiable(acc); - // If the SCC acceptance is indeterminate, but has - // only self-loops with the same mark, it is - // necessarily rejecting, otherwise we would have - // found it to be accepting. - if (!accept && !reject && nbs.size() == 1) - { - acc_cond::mark_t selfacc = 0; - bool first = true; - reject = true; - for (const auto& e: aut->out(nbs.front())) - for (unsigned d: aut->univ_dests(e)) - if (e.src == d) - { - if (first) - { - selfacc = e.acc; - first = false; - } - else if (selfacc != e.acc) - { - reject = false; - goto break2; - } - } - } - break2: + bool reject = triv || + aut->acc().maybe_accepting(acc, common).is_false(); node_.back().rejecting_ = reject; root_.pop_back(); } @@ -250,7 +227,7 @@ namespace spot continue; } - auto acc = e.acc; + acc_cond::mark_t acc = e.acc; // Are we going to a new state? int spi = h_[dest]; @@ -288,11 +265,15 @@ namespace spot if (dest == e.src) is_accepting = aut->acc().accepting(acc); + acc_cond::mark_t common = acc; assert(!root_.empty()); while (threshold > root_.back().index) { acc |= root_.back().acc; - acc |= root_.back().in_acc; + acc_cond::mark_t in_acc = root_.back().in_acc; + acc |= in_acc; + common &= root_.back().common; + common &= in_acc; is_accepting |= root_.back().accepting; root_.pop_back(); assert(!root_.empty()); @@ -303,9 +284,8 @@ namespace spot // after this loop, the SCC whose index is threshold might have // been merged with a higher SCC. - // Accumulate all acceptance conditions, states, SCC - // successors, and conditions into the merged SCC. root_.back().acc |= acc; + root_.back().common &= common; root_.back().accepting |= is_accepting || aut->acc().accepting(root_.back().acc); // This SCC is no longer trivial. @@ -346,14 +326,6 @@ namespace spot return res; } - acc_cond::mark_t scc_info::acc_sets_of(unsigned scc) const - { - acc_cond::mark_t res = 0U; - for (auto& t: inner_edges_of(scc)) - res |= t.acc; - return res; - } - std::vector> scc_info::used_acc() const { unsigned n = aut_->num_states(); diff --git a/spot/twaalgos/sccinfo.hh b/spot/twaalgos/sccinfo.hh index c688f582b..70a2c0fbe 100644 --- a/spot/twaalgos/sccinfo.hh +++ b/spot/twaalgos/sccinfo.hh @@ -195,6 +195,7 @@ namespace spot protected: scc_succs succ_; acc_cond::mark_t acc_; + acc_cond::mark_t common_; std::vector states_; // States of the component bool trivial_:1; bool accepting_:1; // Necessarily accepting @@ -207,8 +208,10 @@ namespace spot { } - scc_info_node(acc_cond::mark_t acc, bool trivial): - acc_(acc), trivial_(trivial), accepting_(false), + scc_info_node(acc_cond::mark_t acc, + acc_cond::mark_t common, bool trivial): + acc_(acc), common_(common), + trivial_(trivial), accepting_(false), rejecting_(false), useful_(false) { } @@ -246,6 +249,11 @@ namespace spot return acc_; } + acc_cond::mark_t common_marks() const + { + return common_; + } + const std::vector& states() const { return states_; @@ -477,7 +485,18 @@ namespace spot std::set used_acc_of(unsigned scc) const; - acc_cond::mark_t acc_sets_of(unsigned scc) const; + /// sets that contain at least one transition of the SCC + acc_cond::mark_t acc_sets_of(unsigned scc) const + { + // FIXME: Why do we have two name for this method? + return acc(scc); + } + + /// sets that contain the entire SCC + acc_cond::mark_t common_sets_of(unsigned scc) const + { + return node(scc).common_marks(); + } std::vector weak_sccs() const; diff --git a/tests/core/sccdot.test b/tests/core/sccdot.test index 75ddb3dfd..999238e9d 100755 --- a/tests/core/sccdot.test +++ b/tests/core/sccdot.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2015 Laboratoire de Recherche et Développement de +# Copyright (C) 2015, 2017 Laboratoire de Recherche et Développement de # l'Epita # # This file is part of Spot, a model checking library. @@ -186,3 +186,23 @@ State: 7 --END-- EOF diff expected.hoa out.hoa + + +cat >input <<'EOF' +HOA: v1 +States: 2 +Start: 0&1 +AP: 2 "a" "b" +acc-name: Buchi +Acceptance: 2 Inf(0) & Fin(1) +--BODY-- +State: 0 {0 1} +[0&1] 0 +[!0&1] 1 +State: 1 {0 1} +[0&!1] 0 +[!0&!1] 1 +--END-- +EOF +# This has one useless component +autfilt --dot=s input | grep grey