From 54d4a0a09338b0d48e3247c7eb9c4fafb25cefe5 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Wed, 11 Jan 2012 11:15:54 +0100
Subject: [PATCH] Rewrite F(a M b) as F(a & b), and G(a W b) as G(a | b).

* src/ltlvisit/simplify.cc: Implement these rules.
* src/ltltest/reduccmp.test: Add tests.
* doc/tl/tl.tex: Document them.
---
 doc/tl/tl.tex             | 11 +++----
 src/ltltest/reduccmp.test |  7 ++++-
 src/ltlvisit/simplify.cc  | 63 ++++++++++++++++++++++++++++++++-------
 3 files changed, 65 insertions(+), 16 deletions(-)

diff --git a/doc/tl/tl.tex b/doc/tl/tl.tex
index 174be93f2..b9ac0d1a7 100644
--- a/doc/tl/tl.tex
+++ b/doc/tl/tl.tex
@@ -1309,14 +1309,15 @@ These simplifications are enabled with
 The following are simplification rules for unary operators (applied
 from left to right, as usual):
 \begin{align*}
-  \X\F\G f &\equiv \F\G f   & \X\G\F f &\equiv \G\F f \\
-  \F(f\U g) &\equiv \F g     & \F\X f &\equiv \X\F f \\
-  \G(f \R g) &\equiv \G g    & \G\X f &\equiv \X\G f
+  \X\F\G f & \equiv \F\G f & \F\X f    & \equiv \X\F f       & \G\X f     & \equiv \X\G f\\
+  \X\G\F f & \equiv \G\F f & \F(f\U g) & \equiv \F g         & \G(f \R g) & \equiv \G g       \\
+           &               & \F(f\M g) & \equiv \F (f\AND g) & \G(f \W g) & \equiv \G(f\OR g)
 \end{align*}
 \begin{align*}
-  \G(f_1\OR\ldots\OR f_n \OR \G\F(g_1)\OR\ldots\OR \G\F(g_m))&\equiv \G(f_1\OR\ldots\OR f_n)\OR \G\F(g_1\OR\ldots\OR g_m)
+  \G(f_1\OR\ldots\OR f_n \OR \G\F(g_1)\OR\ldots\OR \G\F(g_m)) & \equiv \G(f_1\OR\ldots\OR f_n)\OR \G\F(g_1\OR\ldots\OR g_m)
 \end{align*}
-Note that the latter three rewriting rules for $\G$ have no dual:
+
+Note that the latter rewriting rules for $\G$ has no dual:
 rewriting $\F(f \AND \G\F g)$ to $\F(f) \AND \G\F(g)$ (instance as
 suggested by~\citet{somenzi.00.cav}) goes against our goal of moving
 the $\F$ operator in front of the formula.  Conceptually, it is also
diff --git a/src/ltltest/reduccmp.test b/src/ltltest/reduccmp.test
index 1cb05516b..dc910354a 100755
--- a/src/ltltest/reduccmp.test
+++ b/src/ltltest/reduccmp.test
@@ -1,4 +1,4 @@
- #! /bin/sh
+#! /bin/sh
 # Copyright (C) 2009, 2010, 2011, 2012 Laboratoire de Recherche et Developpement
 # de l'Epita (LRDE).
 # Copyright (C) 2004, 2006 Laboratoire d'Informatique de Paris 6 (LIP6),
@@ -166,6 +166,11 @@ for x in ../reduccmp ../reductaustr; do
      run 0 $x 'a R (!a M a)' '0'
      run 0 $x 'a W (!a M a)' 'Ga'
 
+     run 0 $x 'F(a U b)' 'Fb'
+     run 0 $x 'F(a M b)' 'F(a & b)'
+     run 0 $x 'G(a R b)' 'Gb'
+     run 0 $x 'G(a W b)' 'G(a | b)'
+
      # 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/simplify.cc b/src/ltlvisit/simplify.cc
index 824ff7b16..ead628177 100644
--- a/src/ltlvisit/simplify.cc
+++ b/src/ltlvisit/simplify.cc
@@ -736,6 +736,24 @@ namespace spot
 	return is_binop(f, binop::U);
       }
 
+      binop*
+      is_M(formula* f)
+      {
+	return is_binop(f, binop::M);
+      }
+
+      binop*
+      is_R(formula* f)
+      {
+	return is_binop(f, binop::R);
+      }
+
+      binop*
+      is_W(formula* f)
+      {
+	return is_binop(f, binop::W);
+      }
+
       formula*
       unop_multop(unop::type uop, multop::type mop, multop::vec* v)
       {
@@ -1061,6 +1079,20 @@ namespace spot
 		      return;
 		    }
 
+		  // F(a M b) = F(a & b)
+		  bo = is_M(result_);
+		  if (bo)
+		    {
+		      formula* r =
+			unop::instance(unop::F,
+				       multop::instance(multop::And,
+							bo->first()->clone(),
+							bo->second()->clone()));
+		      bo->destroy();
+		      result_ = recurse_destroy(r);
+		      return;
+		    }
+
 		  // FX(a) = XF(a)
 		  {
 		    unop* u = is_X(result_);
@@ -1113,17 +1145,28 @@ namespace spot
 		{
 
 		  // G(a R b) = G(b)
-		  if (result_->kind() == formula::BinOp)
+		  binop* bo = is_R(result_);
+		  if (bo)
 		    {
-		      binop* bo = static_cast<binop*>(result_);
-		      if (bo->op() == binop::R)
-			{
-			  formula* r =
-			    unop::instance(unop::G, bo->second()->clone());
-			  bo->destroy();
-			  result_ = recurse_destroy(r);
-			  return;
-			}
+		      formula* r =
+			unop::instance(unop::G, bo->second()->clone());
+		      bo->destroy();
+		      result_ = recurse_destroy(r);
+		      return;
+		    }
+
+		  // G(a W b) = G(a | b)
+		  bo = is_W(result_);
+		  if (bo)
+		    {
+		      formula* r =
+			unop::instance(unop::G,
+				       multop::instance(multop::Or,
+							bo->first()->clone(),
+							bo->second()->clone()));
+		      bo->destroy();
+		      result_ = recurse_destroy(r);
+		      return;
 		    }
 
 		  // GX(a) = XG(a)