alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

remfin: simplify, thanks to previous patch

Browse source 
* spot/twaalgos/remfin.cc: Get rid of for_each_edge since edges_of()
and inner_edges_of() are now honoring the filters.
This commit is contained in:
Alexandre Duret-Lutz 2020-07-15 11:41:14 +02:00
parent b214fd75d6
commit 94c189b29d
1 changed files with 13 additions and 37 deletions
Download patch file Download diff file Expand all files Collapse all files

50
spot/twaalgos/remfin.cc
View file

@ -38,22 +38,6 @@ namespace spot
{ {
namespace namespace
{ {
using EdgeMask = std::vector<bool>;
template< typename Edges, typename Apply >
void for_each_edge(const const_twa_graph_ptr& aut,
const Edges& edges,
const EdgeMask& mask,
Apply apply)
{
for (const auto& e: edges)
{
unsigned edge_id = aut->edge_number(e);
if (mask[edge_id])
apply(edge_id);
}
}
// Transforms automaton from transition based acceptance to state based // Transforms automaton from transition based acceptance to state based
// acceptance. // acceptance.
void make_state_acc(twa_graph_ptr & aut) void make_state_acc(twa_graph_ptr & aut)
@ -87,7 +71,6 @@ namespace spot
bool is_scc_tba_type(const_twa_graph_ptr aut, bool is_scc_tba_type(const_twa_graph_ptr aut,
const scc_info& si, const scc_info& si,
const unsigned scc, const unsigned scc,
const std::vector<bool>& keep,
const rs_pairs_view& aut_pairs, const rs_pairs_view& aut_pairs,
std::vector<bool>& final) std::vector<bool>& final)
{ {
@ -101,10 +84,8 @@ namespace spot
auto aut_fin_alone = aut_pairs.fins_alone(); auto aut_fin_alone = aut_pairs.fins_alone();
if ((scc_acc & aut_fin_alone) != aut_fin_alone) if ((scc_acc & aut_fin_alone) != aut_fin_alone)
{ {
for_each_edge(aut, si.edges_of(scc), keep, [&](unsigned e) for (auto& e: si.edges_of(scc))
{ final[aut->edge_number(e)] = true;
final[e] = true;
});
return true; return true;
} }
@ -126,14 +107,14 @@ namespace spot
// final. Otherwise we do not know: it is possible that there is // final. Otherwise we do not know: it is possible that there is
// a non-accepting cycle in the SCC that does not visit Fᵢ. // a non-accepting cycle in the SCC that does not visit Fᵢ.
std::set<unsigned> unknown; std::set<unsigned> unknown;
for_each_edge(aut, si.inner_edges_of(scc), keep, [&](unsigned e) for (auto& ed: si.inner_edges_of(scc))
{ {
const auto& ed = aut->edge_data(e); unsigned e = aut->edge_number(ed);
if (ed.acc & scc_infs_alone) if (ed.acc & scc_infs_alone)
final[e] = true; final[e] = true;
else else
unknown.insert(e); unknown.insert(e);
}); }
// Erase edges that cannot belong to a cycle, i.e., the edges // Erase edges that cannot belong to a cycle, i.e., the edges
// whose 'dst' is not 'src' of any unknown edges. // whose 'dst' is not 'src' of any unknown edges.
@ -182,13 +163,11 @@ namespace spot
for (unsigned uscc = 0; uscc < si.scc_count(); ++uscc) for (unsigned uscc = 0; uscc < si.scc_count(); ++uscc)
{ {
for_each_edge(aut, si.edges_of(uscc), keep, [&](unsigned e) for (auto& e: si.edges_of(uscc))
{ unknown.erase(aut->edge_number(e));
unknown.erase(e);
});
if (si.is_rejecting_scc(uscc)) if (si.is_rejecting_scc(uscc))
continue; continue;
if (!is_scc_tba_type(aut, si, uscc, keep, aut_pairs, final)) if (!is_scc_tba_type(aut, si, uscc, aut_pairs, final))
return false; return false;
} }
} }
@ -229,10 +208,9 @@ namespace spot
scc_info si(aut, scc_info_options::TRACK_STATES); scc_info si(aut, scc_info_options::TRACK_STATES);
std::vector<bool> scc_is_tba_type(si.scc_count(), false); std::vector<bool> scc_is_tba_type(si.scc_count(), false);
std::vector<bool> final(aut->edge_vector().size(), false); std::vector<bool> final(aut->edge_vector().size(), false);
std::vector<bool> keep(aut->edge_vector().size(), true);
for (unsigned scc = 0; scc < si.scc_count(); ++scc) for (unsigned scc = 0; scc < si.scc_count(); ++scc)
scc_is_tba_type[scc] = is_scc_tba_type(aut, si, scc, keep, scc_is_tba_type[scc] = is_scc_tba_type(aut, si, scc,
aut_pairs, final); aut_pairs, final);
auto res = make_twa_graph(aut->get_dict()); auto res = make_twa_graph(aut->get_dict());
@ -804,10 +782,9 @@ namespace spot
// if is TBA type // if is TBA type
scc_info si(aut, scc_info_options::TRACK_STATES); scc_info si(aut, scc_info_options::TRACK_STATES);
std::vector<bool> final(aut->edge_vector().size(), false); std::vector<bool> final(aut->edge_vector().size(), false);
std::vector<bool> keep(aut->edge_vector().size(), true);
for (unsigned scc = 0; scc < si.scc_count(); ++scc) for (unsigned scc = 0; scc < si.scc_count(); ++scc)
if (!is_scc_tba_type(aut, si, scc, keep, aut_pairs, final)) if (!is_scc_tba_type(aut, si, scc, aut_pairs, final))
return false; return false;
return true; return true;
@ -827,10 +804,9 @@ namespace spot
scc_info si(aut, scc_info_options::TRACK_STATES); scc_info si(aut, scc_info_options::TRACK_STATES);
std::vector<bool> final(aut->edge_vector().size(), false); std::vector<bool> final(aut->edge_vector().size(), false);
std::vector<bool> keep(aut->edge_vector().size(), true);
for (unsigned scc = 0; scc < si.scc_count(); ++scc) for (unsigned scc = 0; scc < si.scc_count(); ++scc)
if (!is_scc_tba_type(aut, si, scc, keep, aut_pairs, final)) if (!is_scc_tba_type(aut, si, scc, aut_pairs, final))
return nullptr; return nullptr;
auto res = make_twa_graph(aut, twa::prop_set::all()); auto res = make_twa_graph(aut, twa::prop_set::all());