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

partial_degeneralize: force purge_unreachable in some corner case

Browse source 
* spot/twaalgos/degen.cc: If an all-accepting transition has been
redirected, we need to force purge_unreachable_state() to be called,
otherwise we may have unreachable states.
* tests/python/pdegen.py: Add test case.
This commit is contained in:
Alexandre Duret-Lutz 2020-02-10 14:08:05 +01:00
parent 443f638b9c
commit dd8c00fff0
2 changed files with 38 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

20
spot/twaalgos/degen.cc
View file

@ -266,7 +266,8 @@ namespace spot
static void static void
keep_bottommost_copies(twa_graph_ptr& res, keep_bottommost_copies(twa_graph_ptr& res,
scc_info& si_orig, scc_info& si_orig,
std::vector<unsigned>* orig_states) std::vector<unsigned>* orig_states,
bool force_purge = false)
{ {
unsigned res_ns = res->num_states(); unsigned res_ns = res->num_states();
auto a = si_orig.get_aut(); auto a = si_orig.get_aut();
@ -276,7 +277,11 @@ namespace spot
scc_info si_res(res, scc_info_options::TRACK_STATES); scc_info si_res(res, scc_info_options::TRACK_STATES);
unsigned res_scc_count = si_res.scc_count(); unsigned res_scc_count = si_res.scc_count();
if (res_scc_count <= si_orig.scc_count()) if (res_scc_count <= si_orig.scc_count())
{
if (force_purge)
res->purge_unreachable_states();
return; return;
}
// If we reach this place, we have more SCCs in the output than // If we reach this place, we have more SCCs in the output than
// in the input. This means that we have created some redundant // in the input. This means that we have created some redundant
@ -1064,18 +1069,25 @@ namespace spot
} }
} }
// Raise the destination of the "all-accepting" edges to the // Raise the destination of the "all-accepting" edges to the
// highest existing level. // highest existing level. If we do such a redirection, we need
// to force keep_bottommost_copies to purge unreachable_states.
bool force_purge = false;
auto& ev = res->edge_vector(); auto& ev = res->edge_vector();
for (unsigned idx: allaccedges) for (unsigned idx: allaccedges)
{ {
unsigned dst = ev[idx].dst; unsigned dst = ev[idx].dst;
unsigned orig_dst = (*orig_states)[dst]; unsigned orig_dst = (*orig_states)[dst];
unsigned hl = highest_level[orig_dst]; unsigned hl = highest_level[orig_dst];
ev[idx].dst = ds2num[degen_state{orig_dst, hl}]; unsigned new_dst = ds2num[degen_state{orig_dst, hl}];
if (dst != new_dst)
{
ev[idx].dst = new_dst;
force_purge = true;
}
} }
//orders.print(); //orders.print();
res->merge_edges(); res->merge_edges();
keep_bottommost_copies(res, si_orig, orig_states); keep_bottommost_copies(res, si_orig, orig_states, force_purge);
return res; return res;
} }

21
tests/python/pdegen.py
View file

@ -366,3 +366,24 @@ assert dot == """digraph "" {
aut12g = spot.partial_degeneralize(aut12f) aut12g = spot.partial_degeneralize(aut12f)
assert aut12f == aut12g assert aut12f == aut12g
aut13 = spot.automaton("""HOA: v1
States: 2
Start: 0
AP: 4 "p9" "p14" "p10" "p7"
acc-name: generalized-Buchi 3
Acceptance: 3 Inf(0)&Inf(1)&Inf(2)
properties: trans-labels explicit-labels trans-acc deterministic
--BODY--
State: 0
[!0&!1&2] 0 {0 1 2}
[!0&!1&!2] 1 {0 1}
State: 1
[!0&!1&2&!3] 0 {0 1 2}
[!0&!1&!2&!3] 1 {0 1}
[!0&!1&!2&3] 1 {0}
[!0&!1&2&3] 1 {0 2}
--END--""")
aut13g = spot.partial_degeneralize(aut13)
assert aut13g.equivalent_to(aut13)
assert aut13g.num_states() == 3