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

remove_fin: never return acceptance "f"

Browse source 
Fixes #333.

* spot/twaalgos/remfin.cc, spot/twaalgos/remfin.hh,
spot/twaalgos/totgba.cc: Adjust.  The assert() added
to remove_fin() triggered a lot of failure in the test
suite before the different functions were fixed.
* tests/core/remfin.test, tests/python/tra2tba.py:
Adjust expected result.
* NEWS: Mention the bug.
This commit is contained in:
Alexandre Duret-Lutz 2018-03-16 13:52:39 +01:00
parent f2b3653226
commit 1db3472a99
6 changed files with 64 additions and 14 deletions
Download patch file Download diff file Expand all files Collapse all files

39
spot/twaalgos/remfin.cc
View file

@ -465,6 +465,20 @@ namespace spot
twa_graph_ptr trivial_strategy(const const_twa_graph_ptr& aut)
{
if (aut->acc().is_f())
{
// The original acceptance was equivalent to
// "f". Simply return an empty automaton with "t"
// acceptance.
auto res = make_twa_graph(aut->get_dict());
res->set_generalized_buchi(0);
res->set_init_state(res->new_state());
res->prop_stutter_invariant(true);
res->prop_weak(true);
res->prop_complete(false);
return res;
}
return (!aut->acc().uses_fin_acceptance())
? std::const_pointer_cast<twa_graph>(aut)
: nullptr;
@ -515,10 +529,14 @@ namespace spot
if (acccode.is_f())
{
// The original acceptance was equivalent to
// "f". Simply return an empty automaton.
// "f". Simply return an empty automaton with "t"
// acceptance.
auto res = make_twa_graph(aut->get_dict());
res->set_acceptance(0, acccode);
res->set_generalized_buchi(0);
res->set_init_state(res->new_state());
res->prop_stutter_invariant(true);
res->prop_weak(true);
res->prop_complete(false);
return res;
}
}
@ -748,6 +766,18 @@ namespace spot
trace << "before cleanup: " << res->get_acceptance() << '\n';
cleanup_acceptance_here(res);
trace << "after cleanup: " << res->get_acceptance() << '\n';
if (res->acc().is_f())
{
// "f" is not generalized-Büchi. Just return an
// empty automaton instead.
auto res2 = make_twa_graph(res->get_dict());
res2->set_generalized_buchi(0);
res2->set_init_state(res2->new_state());
res2->prop_stutter_invariant(true);
res2->prop_weak(true);
res2->prop_complete(false);
return res2;
}
res->merge_edges();
return res;
}
@ -824,6 +854,9 @@ namespace spot
twa_graph_ptr remove_fin(const const_twa_graph_ptr& aut)
{
return remove_fin_impl(aut);
twa_graph_ptr res = remove_fin_impl(aut);
assert(!res->acc().uses_fin_acceptance());
assert(!res->acc().is_f());
return res;
}
}