rename cleanup_acceptance() as cleanup_acceptance_here()
And add a cleanup_acceptance() version that copies. * src/tgbaalgos/cleanacc.cc, src/tgbaalgos/cleanacc.hh: Rename and add the second version. * src/bin/autfilt.cc, src/bin/ltlcross.cc, src/tgbaalgos/dtgbacomp.cc, src/tgbaalgos/remfin.cc: Use cleanup_acceptance_here.
This commit is contained in:
parent
c5ecd09fb6
commit
df981a0676
6 changed files with 22 additions and 11 deletions
|
|
@ -476,7 +476,7 @@ namespace
|
||||||
if (opt_merge)
|
if (opt_merge)
|
||||||
aut->merge_transitions();
|
aut->merge_transitions();
|
||||||
if (opt_clean_acc || opt_rem_fin)
|
if (opt_clean_acc || opt_rem_fin)
|
||||||
cleanup_acceptance(aut);
|
cleanup_acceptance_here(aut);
|
||||||
if (opt_complement_acc)
|
if (opt_complement_acc)
|
||||||
aut->set_acceptance(aut->acc().num_sets(),
|
aut->set_acceptance(aut->acc().num_sets(),
|
||||||
aut->get_acceptance().complement());
|
aut->get_acceptance().complement());
|
||||||
|
|
|
||||||
|
|
@ -1110,7 +1110,7 @@ namespace
|
||||||
{
|
{
|
||||||
#define DO(x, prefix, suffix) if (x[i]) \
|
#define DO(x, prefix, suffix) if (x[i]) \
|
||||||
{ \
|
{ \
|
||||||
cleanup_acceptance(x[i]); \
|
cleanup_acceptance_here(x[i]); \
|
||||||
if (x[i]->acc().uses_fin_acceptance()) \
|
if (x[i]->acc().uses_fin_acceptance()) \
|
||||||
{ \
|
{ \
|
||||||
auto st = x[i]->num_states(); \
|
auto st = x[i]->num_states(); \
|
||||||
|
|
|
||||||
|
|
@ -21,11 +21,11 @@
|
||||||
|
|
||||||
namespace spot
|
namespace spot
|
||||||
{
|
{
|
||||||
void cleanup_acceptance(tgba_digraph_ptr& aut)
|
tgba_digraph_ptr cleanup_acceptance_here(tgba_digraph_ptr aut)
|
||||||
{
|
{
|
||||||
auto& acc = aut->acc();
|
auto& acc = aut->acc();
|
||||||
if (acc.num_sets() == 0)
|
if (acc.num_sets() == 0)
|
||||||
return;
|
return aut;
|
||||||
|
|
||||||
auto& c = aut->get_acceptance();
|
auto& c = aut->get_acceptance();
|
||||||
acc_cond::mark_t used_in_cond = c.used_sets();
|
acc_cond::mark_t used_in_cond = c.used_sets();
|
||||||
|
|
@ -39,7 +39,7 @@ namespace spot
|
||||||
auto useless = acc.comp(useful);
|
auto useless = acc.comp(useful);
|
||||||
|
|
||||||
if (!useless)
|
if (!useless)
|
||||||
return;
|
return aut;
|
||||||
|
|
||||||
// Remove useless marks from the automaton
|
// Remove useless marks from the automaton
|
||||||
for (auto& t: aut->transitions())
|
for (auto& t: aut->transitions())
|
||||||
|
|
@ -50,7 +50,14 @@ namespace spot
|
||||||
|
|
||||||
// This may in turn cause even more set to be unused, because of
|
// This may in turn cause even more set to be unused, because of
|
||||||
// some simplifications, so do it again.
|
// some simplifications, so do it again.
|
||||||
return cleanup_acceptance(aut);
|
return cleanup_acceptance_here(aut);
|
||||||
}
|
}
|
||||||
|
|
||||||
|
tgba_digraph_ptr cleanup_acceptance(const_tgba_digraph_ptr aut)
|
||||||
|
{
|
||||||
|
return cleanup_acceptance_here(make_tgba_digraph(aut,
|
||||||
|
tgba::prop_set::all()));
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -24,6 +24,11 @@
|
||||||
namespace spot
|
namespace spot
|
||||||
{
|
{
|
||||||
/// \brief Remove useless acceptance sets
|
/// \brief Remove useless acceptance sets
|
||||||
SPOT_API void
|
/// @{
|
||||||
cleanup_acceptance(tgba_digraph_ptr& aut);
|
SPOT_API tgba_digraph_ptr
|
||||||
|
cleanup_acceptance_here(tgba_digraph_ptr aut);
|
||||||
|
|
||||||
|
SPOT_API tgba_digraph_ptr
|
||||||
|
cleanup_acceptance(const_tgba_digraph_ptr aut);
|
||||||
|
/// @}
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -173,8 +173,7 @@ namespace spot
|
||||||
{
|
{
|
||||||
// Simply complete the automaton, and complement its
|
// Simply complete the automaton, and complement its
|
||||||
// acceptance.
|
// acceptance.
|
||||||
auto res = tgba_complete(aut);
|
auto res = cleanup_acceptance_here(tgba_complete(aut));
|
||||||
cleanup_acceptance(res);
|
|
||||||
res->set_acceptance(res->acc().num_sets(),
|
res->set_acceptance(res->acc().num_sets(),
|
||||||
res->get_acceptance().complement());
|
res->get_acceptance().complement());
|
||||||
return res;
|
return res;
|
||||||
|
|
|
||||||
|
|
@ -333,7 +333,7 @@ namespace spot
|
||||||
}
|
}
|
||||||
res->purge_dead_states();
|
res->purge_dead_states();
|
||||||
trace << "before cleanup: " << res->get_acceptance() << '\n';
|
trace << "before cleanup: " << res->get_acceptance() << '\n';
|
||||||
cleanup_acceptance(res);
|
cleanup_acceptance_here(res);
|
||||||
trace << "after cleanup: " << res->get_acceptance() << '\n';
|
trace << "after cleanup: " << res->get_acceptance() << '\n';
|
||||||
return res;
|
return res;
|
||||||
}
|
}
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue