From 473cf77144c0a28528f0a4312fc98214d87316d4 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Sat, 16 Oct 2010 17:24:50 +0200
Subject: [PATCH] Fix trivial identity (0 => Exp) == 1, and add rewritings for
 =>.

The new rewriting are (Exp => Exp) = 1, (Exp <=> Exp) == 1,
and (Exp ^ Exp) == 0.

* src/ltlast/binop.hh: Fix documentation.
* src/ltlast/binop.cc: Fix implementation.
* src/ltltest/equals.test: More tests.
* src/tgbatest/emptchk.test: Remove a useless test.
---
 src/ltlast/binop.cc       | 24 ++++++++++++++++++++++--
 src/ltlast/binop.hh       |  5 ++++-
 src/ltltest/equals.test   |  5 ++++-
 src/tgbatest/emptchk.test |  1 -
 4 files changed, 30 insertions(+), 5 deletions(-)

diff --git a/src/ltlast/binop.cc b/src/ltlast/binop.cc
index edb378b63..1222e8820 100644
--- a/src/ltlast/binop.cc
+++ b/src/ltlast/binop.cc
@@ -158,6 +158,12 @@ namespace spot
 	    return unop::instance(unop::Not, second);
 	  if (first == constant::false_instance())
 	    return second;
+	  if (first == second)
+	    {
+	      first->destroy();
+	      second->destroy();
+	      return constant::false_instance();
+	    }
 	  // We expect constants to appear first, because they are
 	  // instantiated first.
 	  assert(second != constant::false_instance());
@@ -172,10 +178,17 @@ namespace spot
 	  }
 	  //   - (0 <=> Exp) = !Exp
 	  //   - (1 <=> Exp) = Exp
+	  //   - (Exp <=> Exp) = 1
 	  if (first == constant::false_instance())
 	    return unop::instance(unop::Not, second);
 	  if (first == constant::true_instance())
 	    return second;
+	  if (first == second)
+	    {
+	      first->destroy();
+	      second->destroy();
+	      return constant::true_instance();
+	    }
 	  // We expect constants to appear first, because they are
 	  // instantiated first.
 	  assert(second != constant::false_instance());
@@ -183,15 +196,16 @@ namespace spot
 	  break;
 	case Implies:
 	  //   - (1 => Exp) = Exp
-	  //   - (0 => Exp) = 0
+	  //   - (0 => Exp) = 1
 	  //   - (Exp => 1) = 1
 	  //   - (Exp => 0) = !Exp
+	  //   - (Exp => Exp) = 1
 	  if (first == constant::true_instance())
 	    return second;
 	  if (first == constant::false_instance())
 	    {
 	      second->destroy();
-	      return first;
+	      return constant::true_instance();
 	    }
 	  if (second == constant::true_instance())
 	    {
@@ -200,6 +214,12 @@ namespace spot
 	    }
 	  if (second == constant::false_instance())
 	    return unop::instance(unop::Not, first);
+	  if (first == second)
+	    {
+	      first->destroy();
+	      second->destroy();
+	      return constant::true_instance();
+	    }
 	  break;
 	case U:
 	  //   - (Exp U 1) = 1
diff --git a/src/ltlast/binop.hh b/src/ltlast/binop.hh
index d2653ef5b..d9e87a5b3 100644
--- a/src/ltlast/binop.hh
+++ b/src/ltlast/binop.hh
@@ -70,13 +70,16 @@ namespace spot
       /// performed (the left formula is rewritten as the right
       /// formula):
       ///   - (1 => Exp) = Exp
-      ///   - (0 => Exp) = 0
+      ///   - (0 => Exp) = 1
       ///   - (Exp => 1) = 1
       ///   - (Exp => 0) = !Exp
+      ///   - (Exp => Exp) = 1
       ///   - (1 ^ Exp) = !Exp
       ///   - (0 ^ Exp) = Exp
+      ///   - (Exp ^ Exp) = 0
       ///   - (0 <=> Exp) = !Exp
       ///   - (1 <=> Exp) = Exp
+      ///   - (Exp <=> Exp) = Exp
       ///   - (Exp U 1) = 1
       ///   - (Exp U 0) = 0
       ///   - (0 U Exp) = Exp
diff --git a/src/ltltest/equals.test b/src/ltltest/equals.test
index bcc7f3d7b..9e5118241 100755
--- a/src/ltltest/equals.test
+++ b/src/ltltest/equals.test
@@ -88,13 +88,16 @@ run 0 ../equals '!0' '1'
 run 0 ../equals '!!Exp' 'Exp'
 
 run 0 ../equals '(1 => Exp)' 'Exp'
-run 0 ../equals '(0 => Exp)' '0'
+run 0 ../equals '(0 => Exp)' '1'
 run 0 ../equals '(Exp => 1)' '1'
 run 0 ../equals '(Exp => 0)' '!Exp'
+run 0 ../equals '(Exp => Exp)' '1'
 run 0 ../equals '(1 ^ Exp)' '!Exp'
 run 0 ../equals '(0 ^ Exp)' 'Exp'
+run 0 ../equals '(Exp ^ Exp)' '0'
 run 0 ../equals '(0 <=> Exp)' '!Exp'
 run 0 ../equals '(1 <=> Exp)' 'Exp'
+run 0 ../equals '(Exp <=> Exp)' '1'
 run 0 ../equals '(Exp U 1)' '1'
 run 0 ../equals '(Exp U 0)' '0'
 run 0 ../equals '(Exp R 1)' '1'
diff --git a/src/tgbatest/emptchk.test b/src/tgbatest/emptchk.test
index 2f7ea96bd..27263cd44 100755
--- a/src/tgbatest/emptchk.test
+++ b/src/tgbatest/emptchk.test
@@ -96,6 +96,5 @@ expect_ce 'Fa & Xb & GFc & Gd' 1
 expect_ce 'Fa & Xa & GFc & Gc' 2
 expect_ce 'Fc & X(a | Xb) & GF(a | Xb) & Gc' 1
 expect_ce '!((FF a) <=> (F x))' 3
-expect_no '!((FF a) <=> (F a))' 3
 expect_no 'Xa && (!a U b) && !b && X!b' 4
 expect_no '(a U !b) && Gb' 3