From 0623965b43a8b0f0e1cce61c1caac7b66da18189 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 12 Apr 2019 23:14:29 +0200 Subject: [PATCH] =?UTF-8?q?genem:=20improve=20handling=20of=20co-B=C3=BCch?= =?UTF-8?q?i?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * spot/twaalgos/sccinfo.cc, spot/twaalgos/sccinfo.hh: Make sure scc_and_mark_filter does not install a filter if there is nothing to filter. * tests/python/genem.py, spot/twaalgos/genem.cc, python/spot/impl.i: Adjust. --- python/spot/impl.i | 2 +- spot/twaalgos/genem.cc | 5 ++--- spot/twaalgos/sccinfo.cc | 5 +++-- spot/twaalgos/sccinfo.hh | 12 ++++++++---- tests/python/genem.py | 9 ++++++--- 5 files changed, 20 insertions(+), 13 deletions(-) diff --git a/python/spot/impl.i b/python/spot/impl.i index 799dd98fb..56603e15b 100644 --- a/python/spot/impl.i +++ b/python/spot/impl.i @@ -654,7 +654,7 @@ def state_is_accepting(self, src) -> "bool": %noexception spot::scc_info::edges_of; %noexception spot::scc_info::inner_edges_of; %rename(scc_info_with_options) spot::scc_info::scc_info(const_twa_graph_ptr aut, scc_info_options options); -%rename(scc_info_with_options) spot::scc_info::scc_info(scc_and_mark_filter& filt, scc_info_options options); +%rename(scc_info_with_options) spot::scc_info::scc_info(const scc_and_mark_filter& filt, scc_info_options options); %include %template(scc_info_scc_edges) spot::internal::scc_edges const, spot::internal::keep_all>; diff --git a/spot/twaalgos/genem.cc b/spot/twaalgos/genem.cc index 2f7a50739..2d3142077 100644 --- a/spot/twaalgos/genem.cc +++ b/spot/twaalgos/genem.cc @@ -108,9 +108,8 @@ namespace spot } return true; } - // FIXME: If there is acc.fin_unit() it, is - // probably a good idea to filter right away. - scc_info si(aut, scc_info_options::STOP_ON_ACC); + scc_info si(scc_and_mark_filter(aut, aut_acc.fin_unit()), + scc_info_options::STOP_ON_ACC); const int accepting_scc = si.one_accepting_scc(); if (accepting_scc >= 0) diff --git a/spot/twaalgos/sccinfo.cc b/spot/twaalgos/sccinfo.cc index 2b45987f7..773582ea1 100644 --- a/spot/twaalgos/sccinfo.cc +++ b/spot/twaalgos/sccinfo.cc @@ -75,9 +75,10 @@ namespace spot }; } - scc_info::scc_info(scc_and_mark_filter& filt, scc_info_options options) + scc_info::scc_info(const scc_and_mark_filter& filt, scc_info_options options) : scc_info(filt.get_aut(), filt.start_state(), - filt.get_filter(), &filt, options) + filt.get_filter(), + const_cast(&filt), options) { } diff --git a/spot/twaalgos/sccinfo.hh b/spot/twaalgos/sccinfo.hh index a79daf043..edae2ac84 100644 --- a/spot/twaalgos/sccinfo.hh +++ b/spot/twaalgos/sccinfo.hh @@ -457,12 +457,12 @@ namespace spot /// This is usually used to prevent some edges from being /// considered as part of cycles, and can additionally restrict /// to exploration to some SCC discovered by another SCC. - scc_info(scc_and_mark_filter& filt, scc_info_options options); + scc_info(const scc_and_mark_filter& filt, scc_info_options options); // we separate the two functions so that we can rename // scc_info(x,options) into scc_info_with_options(x,options) in Python. // Otherwrise calling scc_info(aut,options) can be confused with // scc_info(aut,initial_state). - scc_info(scc_and_mark_filter& filt) + scc_info(const scc_and_mark_filter& filt) : scc_info(filt, scc_info_options::ALL) { } @@ -814,9 +814,13 @@ namespace spot return aut_->get_init_state_number(); } - scc_info::edge_filter get_filter() + scc_info::edge_filter get_filter() const { - return lower_si_ ? filter_scc_and_mark_ : filter_mark_; + if (lower_si_) + return filter_scc_and_mark_; + if (cut_sets_) + return filter_mark_; + return nullptr; } }; diff --git a/tests/python/genem.py b/tests/python/genem.py index cdfae4505..064a16b32 100644 --- a/tests/python/genem.py +++ b/tests/python/genem.py @@ -207,6 +207,9 @@ def is_scc_empty1(si, scc_num, acc=None): return True def is_empty2(g): + return is_empty2_rec(spot.scc_and_mark_filter(g, g.acc().fin_unit())) + +def is_empty2_rec(g): si = spot.scc_info_with_options(g, spot.scc_info_options_STOP_ON_ACC) if si.one_accepting_scc() >= 0: return False @@ -224,13 +227,13 @@ def is_scc_empty2(si, scc_num, acc=None): acc = acc.restrict_to(occur) acc = acc.remove(common, False) # 3 stop conditions removed here, because they are caught by - # one_accepting_scc() or is_rejecting_scc() in is_empty2() + # one_accepting_scc() or is_rejecting_scc() in is_empty2_rec() for cl in acc.top_disjuncts(): fu = cl.fin_unit() # Is there Fin at the top level if fu: with spot.scc_and_mark_filter(si, scc_num, fu) as filt: filt.override_acceptance(cl.remove(fu, True)) - if not is_empty1(filt): + if not is_empty2_rec(filt): return False else: # Pick some Fin term anywhere in the formula @@ -238,7 +241,7 @@ def is_scc_empty2(si, scc_num, acc=None): # Try to solve assuming Fin(fo)=True with spot.scc_and_mark_filter(si, scc_num, [fo]) as filt: filt.override_acceptance(cl.remove([fo], True)) - if not is_empty2(filt): + if not is_empty2_rec(filt): return False # Try to solve assuming Fin(fo)=False if not is_scc_empty2(si, scc_num, acc.force_inf([fo])):