From 2f036493248c35ab9edf6de73435fab284eee4ca Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Mon, 31 Oct 2011 17:47:08 +0100
Subject: [PATCH] Generalize syntactic implication for event. and univ.
 formulae.

* src/ltlvisit/simplify.cc (syntactic_implication_aux): Refine
rules to deal with pure eventualities and purely universal
properties.
* src/ltltest/reduccmp.test: Add tests.
---
 src/ltltest/reduccmp.test |  5 +++++
 src/ltlvisit/simplify.cc  | 29 +++++++++++++----------------
 2 files changed, 18 insertions(+), 16 deletions(-)

diff --git a/src/ltltest/reduccmp.test b/src/ltltest/reduccmp.test
index da10168b0..1567d0c2e 100755
--- a/src/ltltest/reduccmp.test
+++ b/src/ltltest/reduccmp.test
@@ -71,6 +71,11 @@ for x in ../reduccmp ../reductaustr; do
   run 0 $x 'a ^ a' '0'
   run 0 $x 'a ^ !a' '1'
 
+  run 0 $x 'GFa | FGa' 'GFa'
+  run 0 $x 'XXGa | GFa' 'GFa'
+  run 0 $x 'GFa & FGa' 'FGa'
+  run 0 $x 'XXGa & GFa' 'XXGa'
+
   # Basic reductions
   run 0 $x 'X(true)' 'true'
   run 0 $x 'X(false)' 'false'
diff --git a/src/ltlvisit/simplify.cc b/src/ltlvisit/simplify.cc
index 4a4cafcce..f9cee65ca 100644
--- a/src/ltlvisit/simplify.cc
+++ b/src/ltlvisit/simplify.cc
@@ -2235,7 +2235,7 @@ namespace spot
       formula::opkind fk = f->kind();
       formula::opkind gk = g->kind();
 
-      // Deal with all lines except the first one.
+      // Deal with all lines except the first two.
       switch (fk)
 	{
 	case formula::Constant:
@@ -2249,25 +2249,16 @@ namespace spot
 	    const unop* f_ = down_cast<const unop*>(f);
 	    unop::type fo = f_->op();
 
+	    if ((fo == unop::X || fo == unop::F) && g->is_eventual()
+		&& syntactic_implication(f_->child(), g))
+	      return true;
 	    if (gk == formula::UnOp)
 	      {
 		const unop* g_ = down_cast<const unop*>(g);
 		unop::type go = g_->op();
-		if (fo == unop::F)
+		if (fo == unop::X)
 		  {
-		    if ((go == unop::F)
-			&& syntactic_implication(f_->child(), g_->child()))
-		      return true;
-		  }
-		else if (fo == unop::G)
-		  {
-		    if ((go == unop::G || go == unop::X)
-			&& syntactic_implication(f_->child(), g_->child()))
-		      return true;
-		  }
-		else if (fo == unop::X)
-		  {
-		    if ((go == unop::F || go == unop::X)
+		    if (go == unop::X
 			&& syntactic_implication(f_->child(), g_->child()))
 		      return true;
 		  }
@@ -2430,7 +2421,7 @@ namespace spot
 	  }
 	}
 
-      // First line.
+      // First two lines.
       switch (gk)
 	{
 	case formula::Constant:
@@ -2448,6 +2439,12 @@ namespace spot
 		if (syntactic_implication(f, g_->child()))
 		  return true;
 	      }
+	    else if (go == unop::G || go == unop::X)
+	      {
+		if (f->is_universal()
+		    && syntactic_implication(f, g_->child()))
+		  return true;
+	      }
 	    break;
 	  }
 	case formula::BinOp: