Commit 0623965b authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

genem: improve handling of co-Büchi

* 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.
parent afdc7dda
Pipeline #8234 failed with stages
in 79 minutes and 40 seconds
......@@ -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 <spot/twaalgos/sccinfo.hh>
%template(scc_info_scc_edges) spot::internal::scc_edges<spot::digraph<spot::twa_graph_state, spot::twa_graph_edge_data> const, spot::internal::keep_all>;
......
......@@ -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)
......
......@@ -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<scc_and_mark_filter*>(&filt), options)
{
}
......
......@@ -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;
}
};
......
......@@ -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])):
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment