From 1878bfd0fcfb32947e380dbf7f6bd6aac9cf5b2a Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Thu, 17 Mar 2011 11:55:56 +0100
Subject: [PATCH] Improve a reduction rule for "a M b".

* src/ltlvisit/reduce.cc (reduce_visitor): Always reduce "a M b"
to "a & b" if "a" is a pure eventual formula, remove the
constraint on "b".
* src/ltltest/reduccmp.test: Add two tests.
---
 ChangeLog                 | 9 +++++++++
 src/ltltest/reduccmp.test | 8 ++++++--
 src/ltlvisit/reduce.cc    | 6 +++---
 3 files changed, 18 insertions(+), 5 deletions(-)

diff --git a/ChangeLog b/ChangeLog
index 723ace063..c1f305e08 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,3 +1,12 @@
+2011-03-17  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
+
+	Improve a reduction rule for "a M b".
+
+	* src/ltlvisit/reduce.cc (reduce_visitor): Always reduce "a M b"
+	to "a & b" if "a" is a pure eventual formula, remove the
+	constraint on "b".
+	* src/ltltest/reduccmp.test: Add two tests.
+
 2011-03-11  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
 
 	* NEWS: Mention recent changes to dotty_reachable.
diff --git a/src/ltltest/reduccmp.test b/src/ltltest/reduccmp.test
index 0f4415e14..a4a44215f 100755
--- a/src/ltltest/reduccmp.test
+++ b/src/ltltest/reduccmp.test
@@ -1,5 +1,5 @@
 #! /bin/sh
-# Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement
+# Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et Developpement
 # de l'Epita (LRDE).
 # Copyright (C) 2004, 2006 Laboratoire d'Informatique de Paris 6 (LIP6),
 # département Systèmes Répartis Coopératifs (SRC), Université Pierre
@@ -153,6 +153,10 @@ for x in ../reduccmp ../reductaustr; do
      run 0 $x 'a M ((a & b) M c)' '(a & b)M c'
      run 0 $x '(a & b) M (a R c)' '(a & b)M c'
      run 0 $x '(a & b) M (a M c)' '(a & b)M c'
+
+     # Eventuality and universality class reductions
+     run 0 $x 'Fa M b' 'Fa & b'
+     run 0 $x 'GFa M b' 'GFa & b'
      ;;
   esac
 
@@ -161,7 +165,7 @@ for x in ../reduccmp ../reductaustr; do
   run 0 $x 'a M ((a&b) R c)' 'a M ((a&b) R c)' #not reduced.
   run 0 $x '(a&b) W (a U c)' '(a&b) W (a U c)' #not reduced.
 
-  # Eventuality and universality class reduction
+  # Eventuality and universality class reductions
   run 0 $x 'FFa' 'Fa'
   run 0 $x 'FGFa' 'GFa'
   run 0 $x 'b U Fa' 'Fa'
diff --git a/src/ltlvisit/reduce.cc b/src/ltlvisit/reduce.cc
index a36c8ee68..d506e7e60 100644
--- a/src/ltlvisit/reduce.cc
+++ b/src/ltlvisit/reduce.cc
@@ -1,4 +1,4 @@
-// Copyright (C) 2008, 2009, 2010 Laboratoire de Recherche et
+// Copyright (C) 2008, 2009, 2010, 2011 Laboratoire de Recherche et
 // Développement de l'Epita (LRDE).
 // Copyright (C) 2004, 2006, 2007 Laboratoire d'Informatique de
 // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
@@ -285,9 +285,9 @@ namespace spot
 	  eu_info f1i = { recurse_eu(f1) };
 	  if (opt_ & Reduce_Eventuality_And_Universality)
 	    {
-	      /* If a&b is a pure eventuality formula then a M b = a & b.
+	      /* If a is a pure eventuality formula then a M b = a & b.
 		 If a is a pure universality formula a W b = a|b. */
-	      if (f1i.is.eventual && f2i.is.eventual && (op == binop::M))
+	      if (f1i.is.eventual && (op == binop::M))
 		{
 		  result_ = multop::instance(multop::And, f1, f2);
 		  return;