From 28094c87daafc2d9cace1300930a9b713f2a016e Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Wed, 14 Apr 2010 18:46:04 +0200
Subject: [PATCH] More LTL reductions for W and M.

* src/ltlvisit/basicreduce.cc: Perform the following reductions:
(a R b) | Gb = a R b
(a M b) | Gb = a R b
(a U b) & Fb = a U b
(a W b) & Fb = a U b
* src/ltltest/reduccmp.test: Test them.
---
 ChangeLog                   | 11 +++++++++++
 src/ltltest/reduccmp.test   |  6 ++++++
 src/ltlvisit/basicreduce.cc | 35 +++++++++++++++++++++++++++++++++++
 3 files changed, 52 insertions(+)

diff --git a/ChangeLog b/ChangeLog
index 432c9b97b..7321157a5 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,3 +1,14 @@
+2010-04-14  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
+
+	More LTL reductions for W and M.
+
+	* src/ltlvisit/basicreduce.cc: Perform the following reductions:
+	(a R b) | Gb = a R b
+	(a M b) | Gb = a R b
+	(a U b) & Fb = a U b
+	(a W b) & Fb = a U b
+	* src/ltltest/reduccmp.test: Test them.
+
 2010-04-12  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
 
 	* wrap/python/cgi-bin/ltl2tgba.in: Document W and M operators.
diff --git a/src/ltltest/reduccmp.test b/src/ltltest/reduccmp.test
index f84135027..b35e89258 100755
--- a/src/ltltest/reduccmp.test
+++ b/src/ltltest/reduccmp.test
@@ -130,6 +130,12 @@ for x in ../reduccmp ../reductaustr; do
      run 0 $x '(a W b) & (c W b)' '(a & c) W b'
      run 0 $x '(a R b) | (c M b)' '(a | c) R b'
      run 0 $x '(a M b) | (c M b)' '(a | c) M b'
+
+     run 0 $x '(a R b) | Gb' 'a R b'
+     run 0 $x '(a M b) | Gb' 'a R b'
+     run 0 $x '(a U b) & Fb' 'a U b'
+     run 0 $x '(a W b) & Fb' 'a U b'
+     run 0 $x '(a M b) | Gb | (c M b)' '(a | c) R b'
      ;;
   esac
 
diff --git a/src/ltlvisit/basicreduce.cc b/src/ltlvisit/basicreduce.cc
index a02386283..adc1126b5 100644
--- a/src/ltlvisit/basicreduce.cc
+++ b/src/ltlvisit/basicreduce.cc
@@ -463,6 +463,8 @@ namespace spot
 			{
 			  // F(a) & (a R b) = a M b
 			  // F(a) & (a M b) = a M b
+			  // F(a) & (b W a) = b U a
+			  // F(a) & (b U a) = b U a
 			  formula* a = uo->child();
 			  bool rewritten = false;
 			  for (multop::vec::iterator j = i;
@@ -484,6 +486,19 @@ namespace spot
 				  *j = 0;
 				  rewritten = true;
 				}
+			      else if (b && (b->op() == binop::W
+					     || b->op() == binop::U)
+				       && b->second() == a)
+				{
+				  binop* r =
+				    binop::instance(binop::U,
+						    b->first()->clone(),
+						    a->clone());
+				  tmpOther->push_back(r);
+				  (*j)->destroy();
+				  *j = 0;
+				  rewritten = true;
+				}
 			    }
 			  if (!rewritten)
 			    tmpOther->push_back(uo->clone());
@@ -508,6 +523,16 @@ namespace spot
 			    {
 			      if (!*j)
 				continue;
+			      // (a U b) & Fb = a U b.
+			      // (a W b) & Fb = a U b.
+			      unop* uo2 = dynamic_cast<unop*>(*j);
+			      if (uo2 && uo2->op() == unop::F
+				  && uo2->child() == ftmp)
+				{
+				  (*j)->destroy();
+				  *j = 0;
+				  weak = false;
+				}
 			      binop* bo2 = dynamic_cast<binop*>(*j);
 			      if (bo2 && (bo2->op() == binop::U
 					  || bo2->op() == binop::W)
@@ -708,6 +733,16 @@ namespace spot
 			    {
 			      if (!*j)
 				continue;
+			      // (a R b) | Gb = a R b.
+			      // (a M b) | Gb = a R b.
+			      unop* uo2 = dynamic_cast<unop*>(*j);
+			      if (uo2 && uo2->op() == unop::G
+				  && uo2->child() == ftmp)
+				{
+				  (*j)->destroy();
+				  *j = 0;
+				  weak = true;
+				}
 			      binop* bo2 = dynamic_cast<binop*>(*j);
 			      if (bo2 && (bo2->op() == binop::R
 					  || bo2->op() == binop::M)