From 37c1a19b39117506641dc15e25b043d3f3f33312 Mon Sep 17 00:00:00 2001 From: Alexandre GBAGUIDI AISSE Date: Sat, 17 Jun 2017 19:27:10 +0200 Subject: [PATCH] twaalgos/scc_info: Add states_on_acc_cycle_of() method * NEWS: Update. * spot/twaalgos/sccinfo.hh: Declare states_on_acc_cycle_of(). * spot/twaalgos/sccinfo.cc: Implement it. --- NEWS | 5 ++ spot/twaalgos/sccinfo.cc | 118 +++++++++++++++++++++++++++++++++++++++ spot/twaalgos/sccinfo.hh | 26 +++++++++ 3 files changed, 149 insertions(+) diff --git a/NEWS b/NEWS index a7cb523ec..76c98a759 100644 --- a/NEWS +++ b/NEWS @@ -14,6 +14,11 @@ New in spot 2.4.0.dev (not yet released) - Rename three methods of spot::scc_info. New names are clearer. The old names have been deprecated. + - 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 + Streett-like acceptance condition. + Deprecation notices: (These functions still work but compilers emit warnings.) diff --git a/spot/twaalgos/sccinfo.cc b/spot/twaalgos/sccinfo.cc index 54fd09b9c..67768fa96 100644 --- a/spot/twaalgos/sccinfo.cc +++ b/spot/twaalgos/sccinfo.cc @@ -441,4 +441,122 @@ namespace spot return out; } + std::vector + scc_info::split_on_sets(unsigned scc, acc_cond::mark_t sets) const + { + std::vector res; + + std::vector seen(aut_->num_states(), false); + std::vector cur(aut_->num_states(), false); + + for (unsigned init: states_of(scc)) + { + if (seen[init]) + continue; + cur.assign(aut_->num_states(), false); + + auto copy = make_twa_graph(aut_->get_dict()); + copy->copy_acceptance_of(aut_); + copy->prop_state_acc(aut_->prop_state_acc()); + transform_accessible(aut_, copy, [&](unsigned src, + bdd& cond, + acc_cond::mark_t& m, + unsigned dst) + { + cur[src] = seen[src] = true; + if (scc_of(dst) != scc + || (m & sets) + || (seen[dst] && !cur[dst])) + { + cond = bddfalse; + return; + } + }, + init); + if (copy->num_edges()) + res.push_back(copy); + } + return res; + } + + void + scc_info::states_on_acc_cycle_of_rec(unsigned scc, + acc_cond::mark_t all_fin, + acc_cond::mark_t all_inf, + unsigned nb_pairs, + std::vector& pairs, + std::vector& res, + std::vector& old) const + { + if (!is_rejecting_scc(scc)) + { + acc_cond::mark_t all_acc = acc_sets_of(scc); + acc_cond::mark_t fin = all_fin & all_acc; + acc_cond::mark_t inf = all_inf & all_acc; + + // Get all Fin acceptance set that appears in the SCC and does not have + // their corresponding Inf appearing in the SCC. + acc_cond::mark_t m = 0u; + if (fin) + for (unsigned p = 0; p < nb_pairs; ++p) + if (fin & pairs[p].fin && !(inf & pairs[p].inf)) + m |= pairs[p].fin; + + if (m) + for (const twa_graph_ptr& aut : split_on_sets(scc, m)) + { + auto orig_sts = aut->get_named_prop + >("original-states"); + + // Update mapping of state numbers between the current automaton + // and the starting one. + for (unsigned i = 0; i < orig_sts->size(); ++i) + (*orig_sts)[i] = old[(*orig_sts)[i]]; + + 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, + *orig_sts); + } + + else // Accepting cycle found. + for (unsigned s : states_of(scc)) + res.push_back(old[s]); + } + } + + std::vector + scc_info::states_on_acc_cycle_of(unsigned scc) const + { + std::vector pairs; + if (!aut_->acc().is_streett_like(pairs)) + throw std::runtime_error("states_on_acc_cycle_of only works with " + "Streett-like acceptance condition"); + unsigned nb_pairs = pairs.size(); + + std::vector res; + if (!is_rejecting_scc(scc)) + { + std::vector old; + unsigned nb_states = aut_->num_states(); + 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; + 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, + old); + } + + return res; + } + } diff --git a/spot/twaalgos/sccinfo.hh b/spot/twaalgos/sccinfo.hh index 91f90ac2f..cccf31f8c 100644 --- a/spot/twaalgos/sccinfo.hh +++ b/spot/twaalgos/sccinfo.hh @@ -541,6 +541,32 @@ namespace spot std::vector weak_sccs() const; bdd scc_ap_support(unsigned scc) const; + + protected: + /// \brief: Remove in 'scc', edges containing any mark in 'sets'. + /// + /// Such a deletion may split the SCC, in which case, the function builds + /// and returns more than one automaton representing the specified SCC. + std::vector + split_on_sets(unsigned scc, acc_cond::mark_t sets) const; + + /// \brief: Recursive function used by states_on_acc_cycle_of(). + void + states_on_acc_cycle_of_rec(unsigned scc, + acc_cond::mark_t all_fin, + acc_cond::mark_t all_inf, + unsigned nb_pairs, + std::vector& pairs, + std::vector& res, + std::vector& old) const; + public: + /// \brief: Get all states visited by any accepting cycles of the 'scc'. + /// + /// Throws an exception if the automaton does not have a 'Streett-like' + /// acceptance condition. + std::vector + states_on_acc_cycle_of(unsigned scc) const; + };