From 5755a531f9da0c4dbedd28e9bf9bc3af90fb2b89 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Thu, 15 Apr 2010 14:57:19 +0200
Subject: [PATCH] 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.
---
 ChangeLog                 |  9 +++++++++
 src/ltltest/reduccmp.test |  2 ++
 src/ltlvisit/contain.cc   | 16 ++--------------
 3 files changed, 13 insertions(+), 14 deletions(-)

diff --git a/ChangeLog b/ChangeLog
index cedc70695..0a9fb1d5b 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -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>
 
 	More simplifications rules for M.
diff --git a/src/ltltest/reduccmp.test b/src/ltltest/reduccmp.test
index bf2bc072d..fb3ecac97 100755
--- a/src/ltltest/reduccmp.test
+++ b/src/ltltest/reduccmp.test
@@ -143,6 +143,8 @@ for x in ../reduccmp ../reductaustr; do
      ;;
   esac
 
+  run 0 $x 'a R (b W G(c))' 'a R (b W G(c))' #not reduced
+
   # Syntactic implication
   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'
diff --git a/src/ltlvisit/contain.cc b/src/ltlvisit/contain.cc
index 6a11b3bc1..0c0dc87d5 100644
--- a/src/ltlvisit/contain.cc
+++ b/src/ltlvisit/contain.cc
@@ -228,14 +228,8 @@ namespace spot
 		}
 	      break;
 	    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.
-	      else if ((!stronger) && lcc->contained(b, a))
+	      if (lcc->contained(b, a))
 		{
 		  a->destroy();
 		  result_ = b;
@@ -252,14 +246,8 @@ namespace spot
 		}
 	      break;
 	    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.
-	      else if ((!stronger) && lcc->contained(b, a))
+	      if (lcc->contained(b, a))
 		{
 		  a->destroy();
 		  result_ = b;