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

Fix a long-standing bug in the stronger rule for R and its recent

Browse source 
clone for M.

* src/ltlvisit/contain.cc (reduce_tau03_visitor): Remove
the stronger rules for R and M.  They were wrong.
* src/ltltest/reduccmp.test: Test a simpple counterexample.
This commit is contained in:
Alexandre Duret-Lutz 2010-04-15 14:57:19 +02:00
parent 1a91208933
commit 5755a531f9
3 changed files with 13 additions and 14 deletions
Download patch file Download diff file Expand all files Collapse all files

9
ChangeLog
View file

@ -1,3 +1,12 @@
2010-04-15 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Fix a long-standing bug in the stronger rule for R and its recent
clone for M.
* src/ltlvisit/contain.cc (reduce_tau03_visitor): Remove
the stronger rules for R and M. They were wrong.
* src/ltltest/reduccmp.test: Test a simpple counterexample.
2010-04-15 Alexandre Duret-Lutz <adl@lrde.epita.fr> 2010-04-15 Alexandre Duret-Lutz <adl@lrde.epita.fr>
More simplifications rules for M. More simplifications rules for M.

2
src/ltltest/reduccmp.test
View file

@ -143,6 +143,8 @@ for x in ../reduccmp ../reductaustr; do
;; ;;
esac esac
run 0 $x 'a R (b W G(c))' 'a R (b W G(c))' #not reduced
# Syntactic implication # Syntactic implication
run 0 $x '(a & b) R (a R c)' '(a & b)R c' run 0 $x '(a & b) R (a R c)' '(a & b)R c'
run 0 $x 'a R ((a & b) R c)' '(a & b)R c' run 0 $x 'a R ((a & b) R c)' '(a & b)R c'

16
src/ltlvisit/contain.cc
View file

@ -228,14 +228,8 @@ namespace spot
} }
break; break;
case binop::R: case binop::R:
// if (a R b) => b, then keep b !
if (stronger && lcc->contained(b, bo))
{
a->destroy();
result_ = b;
}
// if b => a, then a R b = b. // if b => a, then a R b = b.
else if ((!stronger) && lcc->contained(b, a)) if (lcc->contained(b, a))
{ {
a->destroy(); a->destroy();
result_ = b; result_ = b;
@ -252,14 +246,8 @@ namespace spot
} }
break; break;
case binop::M: case binop::M:
// if (a M b) => b, then keep b !
if (stronger && lcc->contained(b, bo))
{
a->destroy();
result_ = b;
}
// if b => a, then a M b = b. // if b => a, then a M b = b.
else if ((!stronger) && lcc->contained(b, a)) if (lcc->contained(b, a))
{ {
a->destroy(); a->destroy();
result_ = b; result_ = b;