From 2c31e541b5b553f7ebf8314fcb3f5f028acf8bd7 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Thu, 14 Oct 2010 19:14:42 +0200
Subject: [PATCH] Rewrite Exp[=0..] as [*].

* src/ltlast/bunop.cc: Implement this rewriting.
* src/ltlast/bunop.hh: Document it.
* src/ltltest/equals.test: Test it.
---
 src/ltlast/bunop.cc     | 11 ++++++++++-
 src/ltlast/bunop.hh     |  1 +
 src/ltltest/equals.test |  1 +
 3 files changed, 12 insertions(+), 1 deletion(-)

diff --git a/src/ltlast/bunop.cc b/src/ltlast/bunop.cc
index 3f4476ffd..02a49c9bc 100644
--- a/src/ltlast/bunop.cc
+++ b/src/ltlast/bunop.cc
@@ -167,13 +167,22 @@ namespace spot
 	{
 	case Equal:
 	  {
+	    //   - Exp[=0..] = [*]
+	    if (min == 0 && max == unbounded)
+	      {
+		op = Star;
+		child->destroy();
+		child = constant::true_instance();
+		break;
+	      }
+
 	    //   - 0[=0..max] = [*]
 	    //   - 0[=min..max] = 0 if min > 0
 	    if (child == constant::false_instance())
 	      {
 		if (min == 0)
 		  {
-		    max = -1U;
+		    max = unbounded;
 		    op = Star;
 		    child = constant::true_instance();
 		    break;
diff --git a/src/ltlast/bunop.hh b/src/ltlast/bunop.hh
index e1bbd6ddc..84038bff9 100644
--- a/src/ltlast/bunop.hh
+++ b/src/ltlast/bunop.hh
@@ -55,6 +55,7 @@ namespace spot
       ///   - 0[=min..max] = 0 if min > 0
       ///   - 1[=0] = [*0]
       ///   - 1[=min..max] = 1[*min..max] if max > 0
+      ///   - Exp[=0..] = [*]
       ///   - Exp[=0] = (!Exp)[*]
       ///
       /// These rewriting rules imply that it is not possible to build
diff --git a/src/ltltest/equals.test b/src/ltltest/equals.test
index 439a27daf..883d832fc 100755
--- a/src/ltltest/equals.test
+++ b/src/ltltest/equals.test
@@ -150,3 +150,4 @@ run 0 ../equals '{1[=0]}' '{[*0]}'
 run 0 ../equals '{1[=1..2]}' '{[*1..2]}'
 run 0 ../equals '{1[=..4]}' '{1[*..4]}'
 run 0 ../equals '{b[=0]}' '{(!b)[*]}'
+run 0 ../equals '{b[=0..]}' '{*}'