diff --git a/doc/org/oaut.org b/doc/org/oaut.org index a056628e0..965bc0310 100644 --- a/doc/org/oaut.org +++ b/doc/org/oaut.org @@ -676,7 +676,6 @@ they visit some the transitions in the set #0 infinitely often. The strongly connected components are displayed using the following colors: - *green* components contain an accepting cycle - *red* components contain no accepting cycle -- *orange* components may or may not contain an accepting cycle. Such an indecision occur only when using =Fin= acceptance primitive, deciding that would require a better algorithm than what the output routine is using. - *black* components are trivial (i.e., they contain no cycle) - *gray* components are useless (i.e., they are non-accepting, and are only followed by non-accepting components) @@ -741,12 +740,12 @@ digraph G { 6 [label="6"] } subgraph cluster_1 { - color=orange + color=grey label="" 0 [label="0"] } subgraph cluster_2 { - color=orange + color=green label="" 8 [label="8"] 9 [label="9"] diff --git a/src/tests/sccdot.test b/src/tests/sccdot.test index fd203ba17..c89f090b1 100755 --- a/src/tests/sccdot.test +++ b/src/tests/sccdot.test @@ -86,12 +86,12 @@ digraph G { 6 [label="6"] } subgraph cluster_1 { - color=orange + color=grey label="" 0 [label="0"] } subgraph cluster_2 { - color=orange + color=green label="" 9 [label="9"] 10 [label="10"] @@ -148,3 +148,41 @@ digraph G { EOF diff out.dot expected + +# While we are here, make sure scc_filter remove those grey SCCs. +../../bin/autfilt --small -x simul=0 in.hoa -H > out.hoa +cat >expected.hoa <determine_unknown_acceptance(); + unsigned sccs = si->scc_count(); for (unsigned i = 0; i < sccs; ++i) { @@ -493,6 +495,8 @@ namespace spot else if (si->is_rejecting_scc(i)) os_ << " color=red\n"; else + // May only occur if the call to + // determine_unknown_acceptance() above is removed. os_ << " color=orange\n"; if (name_ || opt_show_acc_) diff --git a/src/twaalgos/sccfilter.cc b/src/twaalgos/sccfilter.cc index e7a77fa33..c883996b0 100644 --- a/src/twaalgos/sccfilter.cc +++ b/src/twaalgos/sccfilter.cc @@ -264,6 +264,7 @@ namespace spot scc_info* si = given_si; if (!si) si = new scc_info(aut); + si->determine_unknown_acceptance(); F filter(si, std::forward(args)...); diff --git a/src/twaalgos/sccfilter.hh b/src/twaalgos/sccfilter.hh index b47d5d13e..3447539b5 100644 --- a/src/twaalgos/sccfilter.hh +++ b/src/twaalgos/sccfilter.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2010, 2012, 2013, 2014 Laboratoire de Recherche et -// Developpement de l'Epita (LRDE). +// Copyright (C) 2009, 2010, 2012, 2013, 2014, 2015 Laboratoire de +// Recherche et Developpement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -35,16 +35,16 @@ namespace spot /// dead SCCs (i.e. SCC that are not accepting, and those with no /// exit path leading to an accepting SCC). /// - /// Additionally, this will try to remove useless acceptance - /// conditions. This operation may diminish the number of - /// acceptance condition of the automaton (for instance when two - /// acceptance conditions are always used together we only keep one) - /// but it will never remove all acceptance conditions, even if it - /// would be OK to have zero. + /// Additionally, for Generalized Büchi acceptance, this will try to + /// remove useless acceptance conditions. This operation may + /// diminish the number of acceptance condition of the automaton + /// (for instance when two acceptance conditions are always used + /// together we only keep one) but it will never remove all + /// acceptance conditions, even if it would be OK to have zero. /// - /// Acceptance conditions on transitions going to non-accepting SCC - /// are all removed. Acceptance conditions going to an accepting - /// SCC and coming from another SCC are only removed if \a + /// Acceptance conditions on transitions going to rejecting SCCs are + /// all removed. Acceptance conditions going to an accepting SCC + /// and coming from another SCC are only removed if \a /// remove_all_useless is set. The default value of \a /// remove_all_useless is \c false because some algorithms (like the /// degeneralization) will work better if transitions going to an @@ -53,7 +53,7 @@ namespace spot /// If \a given_sm is supplied, the function will use its result /// without computing a map of its own. /// - /// \warning Calling scc_filter on a TGBA that has the SBA property + /// \warning Calling scc_filter on a TωA that has the SBA property /// (i.e., transitions leaving accepting states are all marked as /// accepting) may destroy this property. Use scc_filter_states() /// instead. @@ -63,10 +63,10 @@ namespace spot /// \brief Prune unaccepting SCCs. /// - /// This is an abridged version of scc_filter(), that only remove + /// This is an abridged version of scc_filter(), that only removes /// useless states, without touching at the acceptance conditions. /// - /// Especially, if the input TGBA has the SBA property, (i.e., + /// Especially, if the input TωA has the SBA property, (i.e., /// transitions leaving accepting states are all marked as /// accepting), then the output TGBA will also have that property. SPOT_API twa_graph_ptr diff --git a/src/twaalgos/sccinfo.cc b/src/twaalgos/sccinfo.cc index 3b6bae76b..80d3805ee 100644 --- a/src/twaalgos/sccinfo.cc +++ b/src/twaalgos/sccinfo.cc @@ -22,6 +22,7 @@ #include #include #include "twa/bddprint.hh" +#include "twaalgos/mask.hh" #include "misc/escape.hh" namespace spot @@ -225,16 +226,23 @@ namespace spot root_.front().node.trivial_ = false; } + determine_usefulness(); + } + + void scc_info::determine_usefulness() + { // An SCC is useful if it is not rejecting or it has a successor // SCC that is useful. unsigned scccount = scc_count(); for (unsigned i = 0; i < scccount; ++i) { + if (!node_[i].is_rejecting()) { node_[i].useful_ = true; continue; } + node_[i].useful_ = false; for (auto j: node_[i].succ()) if (node_[j.dst].is_useful()) { @@ -295,6 +303,29 @@ namespace spot return support; } + void scc_info::determine_unknown_acceptance() + { + 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)) + { + auto& node = node_[s]; + if (k.empty()) + k.resize(aut_->num_states()); + for (auto i: node.states_) + k[i] = true; + if (mask_keep_states(aut_, k, node.states_.front())->is_empty()) + node.rejecting_ = true; + else + node.accepting_ = true; + changed = true; + } + if (changed) + determine_usefulness(); + } + std::ostream& dump_scc_info_dot(std::ostream& out, const_twa_graph_ptr aut, scc_info* sccinfo) diff --git a/src/twaalgos/sccinfo.hh b/src/twaalgos/sccinfo.hh index 835a75f16..25a2051a0 100644 --- a/src/twaalgos/sccinfo.hh +++ b/src/twaalgos/sccinfo.hh @@ -58,7 +58,8 @@ namespace spot } scc_node(acc_cond::mark_t acc, bool trivial): - acc_(acc), trivial_(trivial), accepting_(false), useful_(false) + acc_(acc), trivial_(trivial), accepting_(false), + rejecting_(false), useful_(false) { } @@ -112,6 +113,8 @@ namespace spot std::vector node_; const_twa_graph_ptr aut_; + // Update the useful_ bits. Called automatically. + void determine_usefulness(); const scc_node& node(unsigned scc) const { @@ -198,6 +201,10 @@ namespace spot return node(scc).is_rejecting(); } + // Study the SCC that are currently reported neither as accepting + // nor rejecting because of the presence of Fin sets + void determine_unknown_acceptance(); + bool is_useful_scc(unsigned scc) const { return node(scc).is_useful();