From 9ca5b8c2f1d8b1ca1feb55dd659ff149d9b2fc31 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 11 Apr 2017 15:27:49 +0200 Subject: [PATCH] scc_info: add ways to speedup scc_info * spot/twaalgos/sccinfo.hh, spot/twaalgos/sccinfo.cc: Add an optional argument to abort on accepting SCC, to not keep track of SCC states, and some one_accepting_scc() method. * NEWS: Mention it. * bin/ltlcross.cc, spot/twaalgos/alternation.cc, spot/twaalgos/cobuchi.cc, spot/twaalgos/degen.cc, spot/twaalgos/determinize.cc, spot/twaalgos/dtbasat.cc, spot/twaalgos/dtwasat.cc, spot/twaalgos/isunamb.cc, spot/twaalgos/powerset.cc, spot/twaalgos/remfin.cc, spot/twaalgos/sbacc.cc, spot/twaalgos/sccfilter.cc, spot/twaalgos/totgba.cc: Adjust arguments passed to scc_info. --- NEWS | 7 ++ bin/ltlcross.cc | 24 ++--- spot/twaalgos/alternation.cc | 3 +- spot/twaalgos/cobuchi.cc | 2 +- spot/twaalgos/degen.cc | 7 +- spot/twaalgos/determinize.cc | 2 +- spot/twaalgos/dtbasat.cc | 2 +- spot/twaalgos/dtwasat.cc | 2 +- spot/twaalgos/isunamb.cc | 3 +- spot/twaalgos/powerset.cc | 2 +- spot/twaalgos/remfin.cc | 6 +- spot/twaalgos/sbacc.cc | 2 +- spot/twaalgos/sccfilter.cc | 3 +- spot/twaalgos/sccinfo.cc | 201 ++++++++++++++++++++++------------- spot/twaalgos/sccinfo.hh | 99 +++++++++++++++-- spot/twaalgos/totgba.cc | 4 +- 16 files changed, 257 insertions(+), 112 deletions(-) diff --git a/NEWS b/NEWS index 54402e77a..a7871fc65 100644 --- a/NEWS +++ b/NEWS @@ -41,6 +41,13 @@ New in spot 2.4.1.dev (not yet released) - Rename three methods of spot::scc_info. New names are clearer. The old names have been deprecated. + - scc_info now takes an optional argument to disable some feature + that are expansive and not always necessary. By default scc_info + tracks the list of all states that belong to an SCC (you may now + ask it not to), tracks the successor SCCs of each SCC (that can + but turned off), and explores all SCCs of the automaton (you may + request to stop on the first SCC that is found accepting). + - The new function scc_info::states_on_acc_cycle_of() is able to return all states visited by any accepting cycles of the specified SCC. It must only be called on automata with a diff --git a/bin/ltlcross.cc b/bin/ltlcross.cc index d75a6ff21..7410140a1 100644 --- a/bin/ltlcross.cc +++ b/bin/ltlcross.cc @@ -619,7 +619,10 @@ namespace st->edges = s.edges; st->transitions = s.transitions; st->acc = res->acc().num_sets(); - spot::scc_info m(res); + spot::scc_info + m(res, (opt_strength + ? spot::scc_info_options::TRACK_STATES + : spot::scc_info_options::NONE)); unsigned c = m.scc_count(); st->scc = c; st->nondetstates = spot::count_nondet_states(res); @@ -750,16 +753,9 @@ namespace for (size_t i = 0; i < m; ++i) if (spot::scc_info* m = maps[i]) { - // r == true iff the automaton i is accepting. - bool r = false; - for (auto& scc: *m) - if (scc.is_accepting()) - { - r = true; - break; - } - res[i] = r; - if (r) + bool i_is_accepting = m->one_accepting_scc() >= 0; + res[i] = i_is_accepting; + if (i_is_accepting) ++verified; else ++violated; @@ -1301,7 +1297,8 @@ namespace std::cerr << "info: product has " << p->num_states() << " st., " << p->num_edges() << " ed.\n"; - sm = new spot::scc_info(p); + sm = new + spot::scc_info(p, spot::scc_info_options::TRACK_STATES); } catch (std::bad_alloc&) { @@ -1334,7 +1331,8 @@ namespace std::cerr << "info: product has " << p->num_states() << " st., " << p->num_edges() << " ed.\n"; - sm = new spot::scc_info(p); + sm = new + spot::scc_info(p, spot::scc_info_options::TRACK_STATES); } catch (std::bad_alloc&) { diff --git a/spot/twaalgos/alternation.cc b/spot/twaalgos/alternation.cc index 89d8f26fd..eed14cedd 100644 --- a/spot/twaalgos/alternation.cc +++ b/spot/twaalgos/alternation.cc @@ -333,7 +333,8 @@ namespace spot public: alternation_remover(const const_twa_graph_ptr& aut) - : aut_(aut), si_(aut), class_of_(si_.scc_count(), scc_class::accept) + : aut_(aut), si_(aut, scc_info_options::TRACK_STATES), + class_of_(si_.scc_count(), scc_class::accept) { } diff --git a/spot/twaalgos/cobuchi.cc b/spot/twaalgos/cobuchi.cc index 2cdc98aa6..f8ff881e0 100644 --- a/spot/twaalgos/cobuchi.cc +++ b/spot/twaalgos/cobuchi.cc @@ -202,7 +202,7 @@ namespace spot named_states_(named_states), res_(aug_subset_cons(ref_prod, ref_power, named_states_, pmap_)), res_map_(res_->get_named_prop("product-states")), - si_(scc_info(res_)), + si_(scc_info(res_, scc_info_options::TRACK_STATES)), nb_states_(res_->num_states()), was_rabin_(was_rabin), orig_num_st_(orig_num_st) diff --git a/spot/twaalgos/degen.cc b/spot/twaalgos/degen.cc index 8ba5caa27..1fd83a964 100644 --- a/spot/twaalgos/degen.cc +++ b/spot/twaalgos/degen.cc @@ -310,8 +310,9 @@ namespace spot std::vector> lvl_cache(a->num_states()); // Compute SCCs in order to use any optimization. - std::unique_ptr m = use_scc ? - std::make_unique(a) : nullptr; + std::unique_ptr m = use_scc + ? std::make_unique(a, scc_info_options::NONE) + : nullptr; // Cache for common outgoing/incoming acceptances. inout_acc inout(a, m.get()); @@ -621,7 +622,7 @@ namespace spot if (!remove_extra_scc || res_ns <= a->num_states()) return res; - scc_info si_res(res); + scc_info si_res(res, scc_info_options::TRACK_STATES); unsigned res_scc_count = si_res.scc_count(); if (res_scc_count <= m->scc_count()) return res; diff --git a/spot/twaalgos/determinize.cc b/spot/twaalgos/determinize.cc index e5a7335c3..f013d1e7d 100644 --- a/spot/twaalgos/determinize.cc +++ b/spot/twaalgos/determinize.cc @@ -589,7 +589,7 @@ namespace spot aut2->copy_state_names_from(aut); aut = aut2; } - scc_info scc = scc_info(aut); + scc_info scc = scc_info(aut, scc_info_options::TRACK_SUCCS); std::vector is_connected = find_scc_paths(scc); bdd allap = bddtrue; diff --git a/spot/twaalgos/dtbasat.cc b/spot/twaalgos/dtbasat.cc index 18136956f..f945bd2ef 100644 --- a/spot/twaalgos/dtbasat.cc +++ b/spot/twaalgos/dtbasat.cc @@ -316,7 +316,7 @@ namespace spot nap = 1 << nap; } - scc_info sm(ref); + scc_info sm(ref, scc_info_options::NONE); // Number all the SAT variables we may need. declare_vars(ref, d, ap, state_based, sm); diff --git a/spot/twaalgos/dtwasat.cc b/spot/twaalgos/dtwasat.cc index 7a8f87ad5..a66197ecc 100644 --- a/spot/twaalgos/dtwasat.cc +++ b/spot/twaalgos/dtwasat.cc @@ -557,7 +557,7 @@ namespace spot nap = 1 << nap; } - scc_info sm(ref); + scc_info sm(ref, scc_info_options::TRACK_STATES_IF_FIN_USED); sm.determine_unknown_acceptance(); // Number all the SAT variables we may need. diff --git a/spot/twaalgos/isunamb.cc b/spot/twaalgos/isunamb.cc index 2427f88f9..e0f8af6a0 100644 --- a/spot/twaalgos/isunamb.cc +++ b/spot/twaalgos/isunamb.cc @@ -47,7 +47,8 @@ namespace spot if (aut->num_edges() == 0) return true; - scc_info sccmap(aut); + scc_info sccmap(aut, scc_info_options::TRACK_SUCCS | + scc_info_options::TRACK_STATES_IF_FIN_USED); sccmap.determine_unknown_acceptance(); unsigned autsz = aut->num_states(); std::vector v; diff --git a/spot/twaalgos/powerset.cc b/spot/twaalgos/powerset.cc index 2bc397590..447a2ebf2 100644 --- a/spot/twaalgos/powerset.cc +++ b/spot/twaalgos/powerset.cc @@ -348,7 +348,7 @@ namespace spot { det->copy_acceptance_of(ref); - scc_info sm(det); + scc_info sm(det, scc_info_options::NONE); unsigned scc_count = sm.scc_count(); diff --git a/spot/twaalgos/remfin.cc b/spot/twaalgos/remfin.cc index fc9a9349d..0d25020ff 100644 --- a/spot/twaalgos/remfin.cc +++ b/spot/twaalgos/remfin.cc @@ -271,7 +271,7 @@ namespace spot return nullptr; // if is TBA type - scc_info si{aut}; + scc_info si(aut, scc_info_options::TRACK_STATES); std::vector scc_is_tba_type(si.scc_count(), false); std::vector final(aut->edge_vector().size(), false); std::vector keep(aut->edge_vector().size(), true); @@ -443,7 +443,7 @@ namespace spot true, // complete true, // stutter inv. }); - scc_info si(res); + scc_info si(res, scc_info_options::NONE); // We will modify res in place, and the resulting // automaton will only have one acceptance set. @@ -671,7 +671,7 @@ namespace spot res->prop_state_acc(true); bool sbacc = res->prop_state_acc().is_true(); - scc_info si(aut); + scc_info si(aut, scc_info_options::TRACK_STATES); unsigned nscc = si.scc_count(); std::vector state_map(nst); for (unsigned n = 0; n < nscc; ++n) diff --git a/spot/twaalgos/sbacc.cc b/spot/twaalgos/sbacc.cc index 59701abdb..2dd4d9916 100644 --- a/spot/twaalgos/sbacc.cc +++ b/spot/twaalgos/sbacc.cc @@ -43,7 +43,7 @@ namespace spot return res; } - scc_info si(old); + scc_info si(old, scc_info_options::NONE); unsigned ns = old->num_states(); acc_cond::mark_t all = old->acc().all_sets(); diff --git a/spot/twaalgos/sccfilter.cc b/spot/twaalgos/sccfilter.cc index 80b084528..34bbd92ca 100644 --- a/spot/twaalgos/sccfilter.cc +++ b/spot/twaalgos/sccfilter.cc @@ -288,7 +288,8 @@ namespace spot // Compute scc_info if not supplied. scc_info* si = given_si; if (!si) - si = new scc_info(aut); + si = new scc_info(aut, scc_info_options::TRACK_SUCCS + | scc_info_options::TRACK_STATES_IF_FIN_USED); si->determine_unknown_acceptance(); F filter(si, std::forward(args)...); diff --git a/spot/twaalgos/sccinfo.cc b/spot/twaalgos/sccinfo.cc index 7dc662b5b..e610fa795 100644 --- a/spot/twaalgos/sccinfo.cc +++ b/spot/twaalgos/sccinfo.cc @@ -28,6 +28,23 @@ namespace spot { + void scc_info::report_need_track_states() + { + throw std::runtime_error + ("scc_info was not run with option TRACK_STATES"); + } + + void scc_info::report_need_track_succs() + { + throw std::runtime_error + ("scc_info was not run with option TRACK_SUCCS"); + } + + void scc_info::report_incompatible_stop_on_acc() + { + throw std::runtime_error + ("scc_info was run with option STOP_ON_ACC"); + } namespace { @@ -39,11 +56,11 @@ namespace spot { } - acc_cond::mark_t in_acc; // Acceptance sets on the incoming transition + acc_cond::mark_t in_acc; // Acceptance sets on the incoming transition 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 + int index; // Index of the SCC + bool trivial = true; // Whether the SCC has no cycle bool accepting = false; // Necessarily accepting }; } @@ -51,14 +68,21 @@ namespace spot scc_info::scc_info(const_twa_graph_ptr aut, unsigned initial_state, edge_filter filter, - void* filter_data) + void* filter_data, + scc_info_options options) : aut_(aut), initial_state_(initial_state), - filter_(filter), filter_data_(filter_data) + filter_(filter), filter_data_(filter_data), + options_(options) { unsigned n = aut->num_states(); sccof_.resize(n, -1U); - std::deque live; + if (!!(options & scc_info_options::TRACK_STATES_IF_FIN_USED) + && aut->acc().uses_fin_acceptance()) + options_ = options = options | scc_info_options::TRACK_STATES; + + std::vector live; + live.reserve(n); std::deque root_; // Stack of SCC roots. std::vector h_(n, 0); // Map of visited states. Values > 0 designate maximal SCC. @@ -79,7 +103,6 @@ namespace spot std::stack todo_; auto& gr = aut->get_graph(); - std::deque init_states; std::vector init_seen(n, false); auto push_init = [&](unsigned s) @@ -90,6 +113,76 @@ namespace spot init_states.push_back(s); }; + bool track_states = !!(options & scc_info_options::TRACK_STATES); + bool track_succs = !!(options & scc_info_options::TRACK_SUCCS); + auto backtrack = [&](unsigned curr) + { + if (root_.back().index == h_[curr]) + { + unsigned num = node_.size(); + 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, common, triv); + + auto& succ = node_.back().succ_; + unsigned np1 = num + 1; + auto s = live.rbegin(); + do + { + sccof_[*s] = num; + h_[*s] = np1; + + // Gather all successor SCCs + if (track_succs) + for (auto& t: aut->out(*s)) + for (unsigned d: aut->univ_dests(t)) + { + unsigned n = sccof_[d]; + if (n == num || n == -1U) + continue; + // If edges are cut, we are not able to + // maintain proper successor information. + if (filter_) + switch (filter_(t, d, filter_data_)) + { + case edge_filter_choice::keep: + break; + case edge_filter_choice::ignore: + case edge_filter_choice::cut: + continue; + } + succ.emplace_back(n); + } + } + while (*s++ != curr); + + if (track_states) + { + auto& nbs = node_.back().states_; + nbs.insert(nbs.end(), s.base(), live.end()); + } + + node_.back().one_state_ = curr; + live.erase(s.base(), live.end()); + + if (track_succs) + { + std::sort(succ.begin(), succ.end()); + succ.erase(std::unique(succ.begin(), succ.end()), succ.end()); + } + + bool accept = !triv && root_.back().accepting; + node_.back().accepting_ = accept; + if (accept) + one_acc_scc_ = num; + bool reject = triv || + aut->acc().maybe_accepting(acc, common).is_false(); + node_.back().rejecting_ = reject; + root_.pop_back(); + } + }; + // Setup depth-first search from the initial state. But we may // have a conjunction of initial state in alternating automata. if (initial_state_ == -1U) @@ -128,61 +221,7 @@ namespace spot // remove that SCC from the ARC/ROOT stacks. We must // discard from H all reachable states from this SCC. assert(!root_.empty()); - if (root_.back().index == h_[curr]) - { - unsigned num = node_.size(); - 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, common, triv); - - // Move all elements of this SCC from the live stack - // to the the node. - auto i = std::find(live.rbegin(), live.rend(), curr); - assert(i != live.rend()); - ++i; // Because base() does -1 - auto& nbs = node_.back().states_; - nbs.insert(nbs.end(), i.base(), live.end()); - live.erase(i.base(), live.end()); - - std::set dests; - unsigned np1 = num + 1; - for (unsigned s: nbs) - { - sccof_[s] = num; - h_[s] = np1; - } - // Gather all successor SCCs - for (unsigned s: nbs) - for (auto& t: aut->out(s)) - for (unsigned d: aut->univ_dests(t)) - { - // If edges are cut, we are not able to - // maintain proper successor information. - if (filter_) - switch (filter_(t, d, filter_data_)) - { - case edge_filter_choice::keep: - break; - case edge_filter_choice::ignore: - case edge_filter_choice::cut: - continue; - } - unsigned n = sccof_[d]; - assert(n != -1U); - if (n == num) - continue; - dests.insert(n); - } - auto& succ = node_.back().succ_; - succ.insert(succ.end(), dests.begin(), dests.end()); - bool accept = !triv && root_.back().accepting; - node_.back().accepting_ = accept; - bool reject = triv || - aut->acc().maybe_accepting(acc, common).is_false(); - node_.back().rejecting_ = reject; - root_.pop_back(); - } + backtrack(curr); continue; } @@ -290,9 +329,22 @@ namespace spot || aut->acc().accepting(root_.back().acc); // This SCC is no longer trivial. root_.back().trivial = false; + + if (root_.back().accepting + && !!(options & scc_info_options::STOP_ON_ACC)) + { + while (!todo_.empty()) + { + unsigned curr = todo_.top().src; + todo_.pop(); + backtrack(curr); + } + return; + } } } - determine_usefulness(); + if (track_succs && !(options & scc_info_options::STOP_ON_ACC)) + determine_usefulness(); } void scc_info::determine_usefulness() @@ -317,7 +369,6 @@ namespace spot } } - std::set scc_info::marks_of(unsigned scc) const { std::set res; @@ -376,16 +427,18 @@ namespace spot --s; if (!is_rejecting_scc(s) && !is_accepting_scc(s)) { - if (!aut_->is_existential()) + if (SPOT_UNLIKELY(!aut_->is_existential())) throw std::runtime_error( "scc_info::determine_unknown_acceptance() " "does not support alternating automata"); + if (SPOT_UNLIKELY(!(options_ & scc_info_options::TRACK_STATES))) + report_need_track_states(); auto& node = node_[s]; if (k.empty()) k.resize(aut_->num_states()); for (auto i: node.states_) k[i] = true; - if (mask_keep_accessible_states(aut_, k, node.states_.front()) + if (mask_keep_accessible_states(aut_, k, node.one_state_) ->is_empty()) node.rejecting_ = true; else @@ -394,7 +447,7 @@ namespace spot } } while (s); - if (changed) + if (changed && !!(options_ & scc_info_options::TRACK_SUCCS)) determine_usefulness(); } @@ -451,6 +504,8 @@ namespace spot scc_info::split_on_sets(unsigned scc, acc_cond::mark_t sets, bool preserve_names) const { + if (SPOT_UNLIKELY(!(options_ & scc_info_options::TRACK_STATES))) + report_need_track_states(); std::vector res; std::vector seen(aut_->num_states(), false); @@ -527,12 +582,8 @@ namespace spot scc_info si_tmp(aut); unsigned scccount_tmp = si_tmp.scc_count(); for (unsigned scc_tmp = 0; scc_tmp < scccount_tmp; ++scc_tmp) - si_tmp.states_on_acc_cycle_of_rec(scc_tmp, - all_fin, - all_inf, - nb_pairs, - pairs, - res, + si_tmp.states_on_acc_cycle_of_rec(scc_tmp, all_fin, all_inf, + nb_pairs, pairs, res, *orig_sts); } @@ -559,8 +610,8 @@ namespace spot for (unsigned i = 0; i < nb_states; ++i) old.push_back(i); - acc_cond::mark_t all_fin = 0u; - acc_cond::mark_t all_inf = 0u; + acc_cond::mark_t all_fin = 0U; + acc_cond::mark_t all_inf = 0U; std::tie(all_inf, all_fin) = aut_->get_acceptance().used_inf_fin_sets(); states_on_acc_cycle_of_rec(scc, all_fin, all_inf, nb_pairs, pairs, res, diff --git a/spot/twaalgos/sccinfo.hh b/spot/twaalgos/sccinfo.hh index e4cbca421..7acd009c6 100644 --- a/spot/twaalgos/sccinfo.hh +++ b/spot/twaalgos/sccinfo.hh @@ -219,9 +219,10 @@ namespace spot friend class scc_info; protected: scc_succs succ_; + std::vector states_; // States of the component + unsigned one_state_; 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 bool rejecting_:1; // Necessarily rejecting @@ -286,12 +287,65 @@ namespace spot return states_; } + unsigned one_state() const + { + return one_state_; + } + const scc_succs& succ() const { return succ_; } }; + /// Options to alter the behavior of scc_info + enum class scc_info_options + { + /// Stop exploring when an accepting SCC is found, and do not track + /// the states of each SCC. + NONE = 0, + /// Stop exploring after an accepting SCC has been found. + /// Using this option forbids future uses of is_useful_scc() and + /// is_useful_state(). Using it will also cause the output of + /// succ() to be incomplete. + STOP_ON_ACC = 1, + /// Keep a vector of all states belonging to each SCC. Using this + /// option is a precondition for using states_of(), edges_of(), + /// inner_edges_of(), states_on_acc_cycle_of(), and + /// determine_unknown_acceptance(). + TRACK_STATES = 2, + /// Keep a list of successors of each SCCs. + /// Using this option is a precondition for using succ(), + /// is_useful_scc(), and is_useful_state(). + TRACK_SUCCS = 4, + /// Conditionally track states if the acceptance conditions uses Fin. + /// This is sufficiant for determine_unknown_acceptance(). + TRACK_STATES_IF_FIN_USED = 8, + /// Default behavior: explore everything and track states and succs. + ALL = TRACK_STATES | TRACK_SUCCS, + }; + + inline + bool operator!(scc_info_options me) + { + return me == scc_info_options::NONE; + } + + inline + scc_info_options operator&(scc_info_options left, scc_info_options right) + { + typedef std::underlying_type_t ut; + return static_cast(static_cast(left) + & static_cast(right)); + } + + inline + scc_info_options operator|(scc_info_options left, scc_info_options right) + { + typedef std::underlying_type_t ut; + return static_cast(static_cast(left) + | static_cast(right)); + } /// \brief Compute an SCC map and gather assorted information. /// @@ -356,6 +410,8 @@ namespace spot unsigned initial_state_; edge_filter filter_; void* filter_data_; + int one_acc_scc_ = -1; + scc_info_options options_; // Update the useful_ bits. Called automatically. void determine_usefulness(); @@ -365,14 +421,29 @@ namespace spot return node_[scc]; } - public: +#ifndef SWIG + private: + [[noreturn]] static void report_need_track_states(); + [[noreturn]] static void report_need_track_succs(); + [[noreturn]] static void report_incompatible_stop_on_acc(); +#endif - // Use ~0U instead of -1U to work around a bug in Swig. - // See https://github.com/swig/swig/issues/993 + public: + /// @{ + /// \brief Create the scc_info map for \a aut scc_info(const_twa_graph_ptr aut, + // Use ~0U instead of -1U to work around a bug in Swig. + // See https://github.com/swig/swig/issues/993 unsigned initial_state = ~0U, edge_filter filter = nullptr, - void* filter_data = nullptr); + void* filter_data = nullptr, + scc_info_options options = scc_info_options::ALL); + + scc_info(const_twa_graph_ptr aut, scc_info_options options) + : scc_info(aut, ~0U, nullptr, nullptr, options) + { + } + /// @} const_twa_graph_ptr get_aut() const { @@ -384,6 +455,12 @@ namespace spot return node_.size(); } + /// Return the number of one accepting SCC if any, -1 otherwise. + int one_accepting_scc() const + { + return one_acc_scc_; + } + bool reachable_state(unsigned st) const { return scc_of(st) != -1U; @@ -426,6 +503,8 @@ namespace spot const std::vector& states_of(unsigned scc) const { + if (SPOT_UNLIKELY(!(options_ & scc_info_options::TRACK_STATES))) + report_need_track_states(); return node(scc).states(); } @@ -463,7 +542,7 @@ namespace spot unsigned one_state_of(unsigned scc) const { - return states_of(scc).front(); + return node(scc).one_state(); } /// \brief Get number of the SCC containing the initial state. @@ -475,6 +554,8 @@ namespace spot const scc_succs& succ(unsigned scc) const { + if (SPOT_UNLIKELY(!(options_ & scc_info_options::TRACK_SUCCS))) + report_need_track_succs(); return node(scc).succ(); } @@ -505,12 +586,16 @@ namespace spot bool is_useful_scc(unsigned scc) const { + if (SPOT_UNLIKELY(!!(options_ & scc_info_options::STOP_ON_ACC))) + report_incompatible_stop_on_acc(); + if (SPOT_UNLIKELY(!(options_ & scc_info_options::TRACK_SUCCS))) + report_need_track_succs(); return node(scc).is_useful(); } bool is_useful_state(unsigned st) const { - return reachable_state(st) && node(scc_of(st)).is_useful(); + return reachable_state(st) && is_useful_scc(scc_of(st)); } /// \brief Returns, for each accepting SCC, the set of all marks appearing diff --git a/spot/twaalgos/totgba.cc b/spot/twaalgos/totgba.cc index 199c7e8e3..f77843efe 100644 --- a/spot/twaalgos/totgba.cc +++ b/spot/twaalgos/totgba.cc @@ -310,7 +310,7 @@ namespace spot dnf_to_streett_converter(const const_twa_graph_ptr& in, const acc_cond::acc_code& code) : in_(in), - si_(scc_info(in)), + si_(scc_info(in, scc_info_options::TRACK_STATES)), nb_scc_(si_.scc_count()), max_set_in_(code.used_sets().max_set()), state_based_(in->prop_state_acc() == true), @@ -555,7 +555,7 @@ namespace spot inf_to_finpairs[mark] |= pair.fin; } - scc_info si(in); + scc_info si(in, scc_info_options::NONE); // Compute the acceptance sets present in each SCC unsigned nscc = si.scc_count();