From 45e3f7fc2a62b73868cccdc7bdf69b3c576e2e01 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Mon, 24 Sep 2012 10:42:20 +0200
Subject: [PATCH] Add two event_univ rewriting rules.

* src/ltlvisit/simplify.cc: Here.
* doc/tl/tl.tex: Document them.
* src/ltltest/reduccmp.test: Test them.
---
 doc/tl/tl.tex             |  4 ++--
 src/ltltest/reduccmp.test |  3 +++
 src/ltlvisit/simplify.cc  | 35 +++++++++++++++++++++++++++++------
 3 files changed, 34 insertions(+), 8 deletions(-)

diff --git a/doc/tl/tl.tex b/doc/tl/tl.tex
index 100a3a1f7..b6e5eda59 100644
--- a/doc/tl/tl.tex
+++ b/doc/tl/tl.tex
@@ -1546,8 +1546,8 @@ $q,\,q_i$           & a pure eventuality that is also purely universal \\
 \end{center}
 
 \begin{align*}
-  \F e &\equiv e & f \U e &\equiv e & e \M f &\equiv e\AND f \\
-  \G u &\equiv u & f \R u &\equiv u &  u \W f &\equiv u\OR f \\
+  \F e &\equiv e & f \U e &\equiv e & e \M f &\equiv e\AND f & u_1 \M u_2 &\equiV (\F u_1) \AND u_2 \\
+  \G u &\equiv u & f \R u &\equiv u &  u \W f &\equiv u\OR f & e_1 \W e_2 &\equiV (\G e_1) \OR e_2 \\
   \X q &\equiv q & q \AND \X f &\equiv \X(q \AND f) & q\OR \X f &\equiv \X(q \OR f)
 \end{align*}
 \begin{align*}
diff --git a/src/ltltest/reduccmp.test b/src/ltltest/reduccmp.test
index 46830d576..0f8bcce2f 100755
--- a/src/ltltest/reduccmp.test
+++ b/src/ltltest/reduccmp.test
@@ -178,6 +178,9 @@ for x in ../reduccmp ../reductaustr; do
      run 0 $x 'G(a R b)' 'Gb'
      run 0 $x 'G(a W b)' 'G(a | b)'
 
+     run 0 $x 'Fa W Fb' 'F(GFa | b)'
+     run 0 $x 'Ga M Gb' 'FGa & Gb'
+
      run 0 $x 'a & XGa' 'Ga'
      run 0 $x 'a & XG(a&b)' '(XGb)&(Ga)'
      run 0 $x 'a & b & XG(a&b)'  'G(a&b)'
diff --git a/src/ltlvisit/simplify.cc b/src/ltlvisit/simplify.cc
index c817d986e..f01b9cbc7 100644
--- a/src/ltlvisit/simplify.cc
+++ b/src/ltlvisit/simplify.cc
@@ -1752,18 +1752,41 @@ namespace spot
 		 If a is a pure universality formula a W b = a|b. */
 	      if (a->is_eventual() && (op == binop::M))
 		{
-		  const formula* tmp = multop::instance(multop::And, a, b);
-		  result_ = recurse(tmp);
-		  tmp->destroy();
+		  result_ =
+		    recurse_destroy(multop::instance(multop::And, a, b));
 		  return;
 		}
 	      if (a->is_universal() && (op == binop::W))
 		{
-		  const formula* tmp = multop::instance(multop::Or, a, b);
-		  result_ = recurse(tmp);
-		  tmp->destroy();
+		  result_ =
+		    recurse_destroy(multop::instance(multop::Or, a, b));
 		  return;
 		}
+
+
+	      // e₁ W e₂ = Ge₁ | e₂
+	      // u₁ M u₂ = Fu₁ & u₂
+	      if (!opt_.reduce_size_strictly)
+		{
+		  if (op == binop::W && a->is_eventual() && b->is_eventual())
+		    {
+		      result_ =
+			recurse_destroy(multop::instance
+					(multop::Or,
+					 unop::instance(unop::G, a), b));
+		      return;
+		    }
+		  if (op == binop::M && a->is_universal() && b->is_universal())
+		    {
+		      result_ =
+			recurse_destroy(multop::instance
+					(multop::And,
+					 unop::instance(unop::F, a), b));
+		      return;
+		    }
+		}
+
+
 	      trace << "bo: no eventuniv rule matched" << std::endl;
 	    }