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

Do not rewrite F(a & GF(b)) = F(a) & GF(b), this can be harmful.

Browse source 
* src/ltlvisit/basicreduce.cc (basic_reduce_visitor::recurse):
Disable this rule unconditionally.
* src/ltltest/reduccmp.test: Adjust tests.
This commit is contained in:
Alexandre Duret-Lutz 2010-03-06 19:28:39 +01:00
parent 629dc4c0c9
commit 3cf2ddbcb0
3 changed files with 34 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

8
ChangeLog
View file

@ -1,3 +1,11 @@
2010-03-07 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Do not rewrite F(a & GF(b)) = F(a) & GF(b), this can be harmful.
* src/ltlvisit/basicreduce.cc (basic_reduce_visitor::recurse):
Disable this rule unconditionally.
* src/ltltest/reduccmp.test: Adjust tests.
2010-03-06 Alexandre Duret-Lutz <adl@lrde.epita.fr> 2010-03-06 Alexandre Duret-Lutz <adl@lrde.epita.fr>
* src/tgba/tgbatba.cc: Fix English in comments. * src/tgba/tgbatba.cc: Fix English in comments.

14
src/ltltest/reduccmp.test
View file

@ -1,5 +1,5 @@
#! /bin/sh #! /bin/sh
# Copyright (C) 2009 Laboratoire de Recherche et Développement # Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement
# de l'Epita (LRDE). # de l'Epita (LRDE).
# Copyright (C) 2004, 2006 Laboratoire d'Informatique de Paris 6 (LIP6), # Copyright (C) 2004, 2006 Laboratoire d'Informatique de Paris 6 (LIP6),
# département Systèmes Répartis Coopératifs (SRC), Université Pierre # département Systèmes Répartis Coopératifs (SRC), Université Pierre
@ -86,12 +86,20 @@ for x in ../reduccmp ../reductaustr; do
run 0 $x 'X(a & GFb)' 'Xa & GFb' run 0 $x 'X(a & GFb)' 'Xa & GFb'
run 0 $x 'X(a | GFb)' 'Xa | GFb' run 0 $x 'X(a | GFb)' 'Xa | GFb'
run 0 $x 'F(a & GFb)' 'Fa & GFb' # The following is not reduced to F(a) & GFb. because
# (1) is does not help the translate the formula into a
# smaller automaton, and ...
run 0 $x 'F(a & GFb)' 'F(a & GFb)'
# (2) ... it would hinder this useful reduction (that helps to
# produce a smaller automaton)
run 0 $x 'F(f1 & GF(f2)) | F(a & GF(b))' 'F((f1&GFf2)|(a&GFb))'
run 0 $x 'G(a | GFb)' 'Ga | GFb' run 0 $x 'G(a | GFb)' 'Ga | GFb'
run 0 $x 'X(a & GFb & c)' 'X(a & c) & GFb' run 0 $x 'X(a & GFb & c)' 'X(a & c) & GFb'
run 0 $x 'X(a | GFb | c)' 'X(a | c) | GFb' run 0 $x 'X(a | GFb | c)' 'X(a | c) | GFb'
run 0 $x 'F(a & GFb & c)' 'F(a & c) & GFb' # The following is not reduced to F(a & c) & GF(b) for the same
# reason as above.
run 0 $x 'F(a & GFb & c)' 'F(a & GFb & c)'
run 0 $x 'G(a | GFb | c)' 'G(a | c) | GFb' run 0 $x 'G(a | GFb | c)' 'G(a | c) | GFb'
;; ;;
esac esac

15
src/ltlvisit/basicreduce.cc
View file

@ -169,13 +169,28 @@ namespace spot
return; return;
} }
#if 0
// F(f1 & GF(f2)) = F(f1) & GF(F2) // F(f1 & GF(f2)) = F(f1) & GF(F2)
//
// As is, these two formulae are translated into
// equivalent Büchi automata so the rewriting is
// useless.
//
// However when taken in a larger formulae such as F(f1
// & GF(f2)) | F(a & GF(b)), this rewriting used to
// produce (F(f1) & GF(f2)) | (F(a) & GF(b)), missing
// the opportunity to apply the F(E1)|F(E2) = F(E1|E2)
// rule which really helps the translation. F((f1 &
// GF(f2)) | (a & GF(b))) is indeed easier to translate.
//
// So let's not consider this rewriting rule.
mo = dynamic_cast<multop*>(result_); mo = dynamic_cast<multop*>(result_);
if (mo && mo->op() == multop::And) if (mo && mo->op() == multop::And)
{ {
result_ = param_case(mo, unop::F, multop::And); result_ = param_case(mo, unop::F, multop::And);
return; return;
} }
#endif
result_ = unop::instance(unop::F, result_); result_ = unop::instance(unop::F, result_);
return; return;