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

Fix a segfault in WDBA minimization.

Browse source 
* src/tgbaalgos/minimize.cc (build_result, minimize_dfa,
minimize_wdba): Correctly handle (i.e. ignore) useless states.
* src/tgbatest/ltl2tgba.test: Add two more tests.
This commit is contained in:
Alexandre Duret-Lutz 2011-02-06 16:48:52 +01:00
parent 97df5b4285
commit c019a44c49
3 changed files with 38 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

8
ChangeLog
View file

@ -1,3 +1,11 @@
2011-02-06 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Fix a segfault in WDBA minimization.
* src/tgbaalgos/minimize.cc (build_result, minimize_dfa,
minimize_wdba): Correctly handle (i.e. ignore) useless states.
* src/tgbatest/ltl2tgba.test: Add two more tests.
2011-02-05 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Fix call to scc_filter in the CGI script.

27
src/tgbaalgos/minimize.cc
View file

@ -150,9 +150,11 @@ namespace spot
for (succit->first(); !succit->done(); succit->next())
{
const state* dst = succit->current_state();
unsigned dst_num = state_num[dst];
hash_map::const_iterator i = state_num.find(dst);
dst->destroy();
trs* t = res->create_transition(src_num, dst_num);
if (i == state_num.end()) // Ignore useless destinations.
continue;
trs* t = res->create_transition(src_num, i->second);
res->add_conditions(t, succit->current_condition());
if (accepting)
res->add_acceptance_condition(t, ltl::constant::true_instance());
@ -382,9 +384,17 @@ namespace spot
for (si->first(); !si->done(); si->next())
{
const state* dst = si->current_state();
unsigned dst_set = state_set_map[dst];
hash_map::const_iterator i = state_set_map.find(dst);
dst->destroy();
f |= (bdd_ithvar(dst_set) & si->current_condition());
if (i == state_set_map.end())
// The destination state is not in our
// partition. This can happen if the initial
// FINAL and NON_FINAL supplied to the algorithm
// do not cover the whole automaton (because we
// want to ignore some useless states). Simply
// ignore these states here.
continue;
f |= (bdd_ithvar(i->second) & si->current_condition());
}
delete si;
@ -547,7 +557,7 @@ namespace spot
continue;
}
// Trivial SCCs are accepting if all their
// successors are accepting.
// useful successors are accepting.
// This corresponds to the algorithm in Fig. 1 of
// "Efficient minimization of deterministic weak
@ -561,8 +571,11 @@ namespace spot
for (scc_map::succ_type::const_iterator i = succ.begin();
i != succ.end(); ++i)
{
is_useless &= useless[i->first];
acc &= accepting[i->first];
if (!useless[i->first])
{
is_useless = false;
acc &= accepting[i->first];
}
}
}
else

10
src/tgbatest/ltl2tgba.test
View file

@ -114,3 +114,13 @@ cat >expected <<EOF
1 -> 1 [label="1\n"]
EOF
cmp stdout expected
# This formula caused a segfault with Spot 0.7.
run 0 ../ltl2tgba -Rm -ks -f "Gq|Gr|(G(q|FGp)&G(r|FG!p))" >stdout
grep 'transitions: 5$' stdout
grep 'states: 3$' stdout
# Adding -R3 used to make it work...
run 0 ../ltl2tgba -R3 -Rm -ks -f "Gq|Gr|(G(q|FGp)&G(r|FG!p))" >stdout
grep 'transitions: 5$' stdout
grep 'states: 3$' stdout