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

Fix "BDD Error" in scc_filter().

Browse source 
If all the acceptance set of an SCC but the first one were useless, the
scc_filter() algorithm could abort with a BDD error because of a bug in
the logic.

* src/tgbaalgos/sccfilter.cc (scc_filter): Fix.
* src/tgbatest/sccsimpl.test: Add a test case supplied by Étienne
Renault.
This commit is contained in:
Alexandre Duret-Lutz 2013-06-19 20:58:25 +02:00
parent 372a086cb7
commit fc5d4e1a41
2 changed files with 44 additions and 18 deletions
Download patch file Download diff file Expand all files Collapse all files

47
src/tgbaalgos/sccfilter.cc
View file

@ -351,20 +351,31 @@ namespace spot
//std::cerr << "SCC #" << n << "; used = " << all << std::endl;
// Compute a set of useless acceptance conditions.
// Compute a set of useless acceptance sets.
// If the acceptance combinations occurring in
// the automata are { a, ab, abc, bd }, then
// ALL contains (a&!b&!c&!d)|(a&b&!c&!d)|(a&b&c&!d)|(!a&b&!c&d)
// and we want to find that 'a' and 'b' are useless because
// they always occur with 'c'.
// The way we check if 'a' is useless is to look whether ALL
// implies (x -> a) for some other acceptance condition x.
bdd allconds = bdd_support(negall);
bdd allcondscopy = allconds;
// implies (x -> a) for some other acceptance set x.
//
// The two while() loops in the code perform the equivalent of
// for all a in allconds_a:
// for all x in allconds_x:
// check whether x -> a
// ...
//
// Initially allconds_a = allconds_x contains all acceptance
// sets. However when an acceptance set 'a' is determined to
// be useless, it can be removed from allconds_x from future
// iterations.
bdd allconds_a = bdd_support(negall);
bdd allconds_x = allconds_a;
bdd useless = bddtrue;
while (allconds != bddtrue)
while (allconds_a != bddtrue)
{
// Speed-up the computation of implied acceptance by
// Speed-up the computation of implied acceptance sets by
// removing those that are always present. We detect
// those that appear as conjunction of positive variables
// at the start of ALL.
@ -372,8 +383,8 @@ namespace spot
if (prefix != bddtrue)
{
assert(prefix == bdd_support(prefix));
allcondscopy = bdd_exist(allcondscopy, prefix);
if (allcondscopy != bddtrue)
allconds_a = bdd_exist(allconds_a, prefix);
if (allconds_a != bddtrue)
{
useless &= prefix;
}
@ -383,34 +394,34 @@ namespace spot
useless &= bdd_high(prefix);
break;
}
allconds = bdd_exist(allconds, prefix);
allconds_x = bdd_exist(allconds_x, prefix);
}
// Pick a non-useless acceptance condition a.
bdd a = bdd_ithvar(bdd_var(allconds));
// For all acceptance condition x that is not already useless...
bdd others = allcondscopy;
// Pick an acceptance set 'a'.
bdd a = bdd_ithvar(bdd_var(allconds_a));
// For all acceptance sets 'x' that are not already
// useless...
bdd others = allconds_x;
while (others != bddtrue)
{
bdd x = bdd_ithvar(bdd_var(others));
// ... check whether it always implies a.
// ... check whether 'x' always implies 'a'.
if (x != a && bdd_implies(all, x >> a))
{
// If so, a is useless.
// If so, 'a' is useless.
all = bdd_exist(all, a);
useless &= a;
allcondscopy = bdd_exist(allcondscopy, a);
allconds_x = bdd_exist(allconds_x, a);
break;
}
others = bdd_high(others);
}
allconds = bdd_high(allconds);
allconds_a = bdd_high(allconds_a);
}
// We never remove ALL acceptance marks.
assert(negall == bddtrue || useless != bdd_support(negall));
useless_table[n] = useless;
bdd useful = bdd_exist(negall, useless);

15
src/tgbatest/sccsimpl.test
View file

@ -170,3 +170,18 @@ test `grep '^acc' out8.txt | wc -w` = 4
run 0 ../ltl2tgba -R3 -s -RDS -ks \
'(G(!((b) R (a)))) R (((c) R (!(d))) U (G((a) | (!(G(e))))))' > out9.txt
grep 'states: 6$' out9.txt
# From Spot 1.1 to 1.1.2, this failed with a BDD error because of
# a bug in scc_filter().
run 0 ../ltl2tgba -R3 -k '(a) <-> F(Ga <-> F!(b -> a))' >stdout
cat >expected <<EOF
transitions: 21
states: 8
total SCCs: 6
accepting SCCs: 3
dead SCCs: 0
accepting paths: 4
dead paths: 0
EOF
diff stdout expected