From ca686cb07e3f8b67d384e7cc75c4caf2d90b6b06 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Mon, 22 Aug 2011 22:14:36 +0200
Subject: [PATCH] Fix a case caught by the random formula generator.

* src/ltlvisit/simplify.cc (ltl_simplifier): Since we are processing
the formula bottom-up, don't assume all trivial simplification have
been done.
* src/ltltest/reduccmp.test: More tests.
---
 src/ltltest/reduccmp.test |  7 ++++++-
 src/ltlvisit/simplify.cc  | 36 +++++++++++++++++++++++++++++-------
 2 files changed, 35 insertions(+), 8 deletions(-)

diff --git a/src/ltltest/reduccmp.test b/src/ltltest/reduccmp.test
index 8db8b2bec..aa99ec3e2 100755
--- a/src/ltltest/reduccmp.test
+++ b/src/ltltest/reduccmp.test
@@ -66,7 +66,7 @@ for x in ../reduccmp ../reductaustr; do
   run 0 $x 'a | (b U a) | a' '(b U a)'
   run 0 $x 'a U (b U a)' '(b U a)'
 
-  # Basics reduction
+  # Basic reductions
   run 0 $x 'X(true)' 'true'
   run 0 $x 'X(false)' 'false'
   run 0 $x 'F(true)' 'true'
@@ -147,6 +147,11 @@ for x in ../reduccmp ../reductaustr; do
      run 0 $x 'b R Ga' 'Ga'
      run 0 $x 'b R FGa' 'FGa'
 
+     run 0 $x 'G(!a M a) M 1' '0'
+     run 0 $x 'G(!a M a) U 1' '1'
+     run 0 $x 'a R (!a M a)' '0'
+     run 0 $x 'a W (!a M a)' 'Ga'
+
      # 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 5d68ad0a2..4c5afa273 100644
--- a/src/ltlvisit/simplify.cc
+++ b/src/ltlvisit/simplify.cc
@@ -540,6 +540,14 @@ namespace spot
       formula*
       simplify_recursively(const formula* f, ltl_simplifier_cache* c);
 
+      constant*
+      is_constant(formula* f)
+      {
+	if (f->kind() != formula::Constant)
+	  return 0;
+	return static_cast<constant*>(f);
+      }
+
       unop*
       is_unop(formula* f, unop::type op)
       {
@@ -868,8 +876,11 @@ namespace spot
 	      break;
 
 	    case unop::X:
-	      // X(constant) = constant is a trivial identity
-	      assert(result_->kind() != formula::Constant);
+	      // X(constant) = constant is a trivial identity, but if
+	      // the constant has been constructed by recurse() this
+	      // identity has not been applied.
+	      if (is_constant(result_))
+		  return;
 
 	      // XGF(f) = GF(f) and XFG(f)=FG(f)
 	      if (is_GF(result_) || is_FG(result_))
@@ -885,8 +896,11 @@ namespace spot
 	      break;
 
 	    case unop::F:
-	      // F(constant) = constant is a trivial identity.
-	      assert(result_->kind() != formula::Constant);
+	      // F(constant) = constant is a trivial identity, but if
+	      // the constant has been constructed by recurse() this
+	      // identity has not been applied.
+	      if (is_constant(result_))
+		  return;
 
 	      // If f is a pure eventuality formula then F(f)=f.
 	      if (opt_.event_univ && result_->is_eventual())
@@ -940,8 +954,11 @@ namespace spot
 	      break;
 
 	    case unop::G:
-	      // G(constant) = constant is a trivial identity
-	      assert(result_->kind() != formula::Constant);
+	      // G(constant) = constant is a trivial identity, but if
+	      // the constant has been constructed by recurse() this
+	      // identity has not been applied.
+	      if (is_constant(result_))
+		  return;
 
 	      // If f is a pure universality formula then G(f)=f.
 	      if (opt_.event_univ && result_->is_universal())
@@ -1263,7 +1280,12 @@ namespace spot
 		// a R true = true
 		// a W true = true
 		// a M false = false
-		assert(f2->kind() != formula::Constant);
+		if (is_constant(f2))
+		  {
+		    result_ = f2;
+		    f1->destroy();
+		    return;
+		  }
 
 		// Same effect as dynamic_cast<unop*>, only faster.
 		unop* fu1 =