diff --git a/ChangeLog b/ChangeLog index dbdfd48ad..39afdb2c5 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,10 @@ +2010-04-15 Alexandre Duret-Lutz + + Fix simplification of "a M true" as Fa. + + * src/ltlvisit/simpfg.cc: Typo. + * src/ltltest/reduccmp.test: Add more tests. + 2010-04-15 Alexandre Duret-Lutz * HACKING: Bison 2.4.2 has a bugfix we rely on. diff --git a/src/ltltest/reduccmp.test b/src/ltltest/reduccmp.test index b35e89258..62a5374e2 100755 --- a/src/ltltest/reduccmp.test +++ b/src/ltltest/reduccmp.test @@ -66,6 +66,10 @@ for x in ../reduccmp ../reductaustr; do run 0 $x 'a | (b U a) | a' '(b U a)' run 0 $x 'a U (b U a)' '(b U a)' + run 0 $x 'a M 1' 'Fa' + run 0 $x 'a W 0' 'Ga' + run 0 $x '1 U a' 'Fa' + run 0 $x '0 R a' 'Ga' # Basics reduction run 0 $x 'X(true)' 'true' diff --git a/src/ltlvisit/simpfg.cc b/src/ltlvisit/simpfg.cc index f91d58c6c..f4a0f9210 100644 --- a/src/ltlvisit/simpfg.cc +++ b/src/ltlvisit/simpfg.cc @@ -78,8 +78,8 @@ namespace spot return; /* f1 M true == F(f1) */ case binop::M: - if (f1 == constant::true_instance()) - result_ = unop::instance(unop::F, f2); + if (f2 == constant::true_instance()) + result_ = unop::instance(unop::F, f1); else result_ = binop::instance(binop::M, f1, f2); return;