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

@@ -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 \\
+  \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 \\
+  \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*}

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)'

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_ =
-		  result_ = recurse(tmp);
+		    recurse_destroy(multop::instance(multop::And, a, b));
-		  tmp->destroy();
 		  return;
 		}
 	      if (a->is_universal() && (op == binop::W))
 		{
-		  const formula* tmp = multop::instance(multop::Or, a, b);
+		  result_ =
-		  result_ = recurse(tmp);
+		    recurse_destroy(multop::instance(multop::Or, a, b));
-		  tmp->destroy();
 		  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;
 	    }