From a4353d39852b9d9ab51a27d23bca3f3e2cec931e Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Tue, 17 Apr 2012 16:00:22 +0200
Subject: [PATCH] Trivially reduce 'a[*1]' to 'a'.

* src/ltlast/bunop.cc (bunop::instance): Here.
* src/ltlast/bunop.hh, doc/tl/tl.tex: Document it.
* src/ltltest/equals.test: Test it.
---
 doc/tl/tl.tex           | 5 +++--
 src/ltlast/bunop.cc     | 4 ++++
 src/ltlast/bunop.hh     | 1 +
 src/ltltest/equals.test | 8 +++++---
 4 files changed, 13 insertions(+), 5 deletions(-)

diff --git a/doc/tl/tl.tex b/doc/tl/tl.tex
index 31d43fe2e..8da743d3e 100644
--- a/doc/tl/tl.tex
+++ b/doc/tl/tl.tex
@@ -651,7 +651,7 @@ it for output.  $b$ must be a Boolean formula.
   b\EQUAL{\mvar{i}..\mvar{j}} &\equiv \mathtt{\{\{}\NOT b\mathtt{\}}\STAR{0..}\CONCAT b\mathtt{\}}\STAR{\mvar{i}..\mvar{j}}\CONCAT \mathtt{\{}\NOT b\mathtt{\}}\STAR{0..} \\
   b\GOTO{\mvar{i}..} &\equiv \mathtt{\{\{}\NOT b\mathtt{\}}\STAR{0..}\CONCAT b\mathtt{\}}\STAR{\mvar{i}..} &
   b\EQUAL{\mvar{i}..} &\equiv \mathtt{\{\{}\NOT b\mathtt{\}}\STAR{0..}\CONCAT b\mathtt{\}}\STAR{\mvar{i}..}\CONCAT \mathtt{\{}\NOT b\mathtt{\}}\STAR{0..}\text{~if~}i>0 \\
-  && b\EQUAL{0..} &\equiv \mathtt{\{\{}\1\STAR{0..}\mathtt{\}}
+  && b\EQUAL{0..} &\equiv \1\STAR{0..}
 \end{align*}
 \begin{align*}
   f\STARALT &\equiv f\STAR{0..}\\
@@ -687,7 +687,8 @@ $b_1$, $b_2$ are assumed to be Boolean formul\ae.
   \0\STAR{\mvar{i}..\mvar{j}} &\equiv \0 \text{~if~}i>0 \\
   \eword\STAR{\var{i}..\mvar{j}} &\equiv \eword&
   f\STAR{\mvar{i}..\mvar{j}}\STAR{\mvar{k}..\mvar{l}} &\equiv f\STAR{\mvar{ik}..\mvar{jl}}\text{~if~}i(k+1)\le jk+1 \\
-  f\STAR{0}&\equiv \eword
+  f\STAR{0}&\equiv \eword \\
+  f\STAR{1}&\equiv f\\
 \end{align*}
 
 \noindent
diff --git a/src/ltlast/bunop.cc b/src/ltlast/bunop.cc
index 85b9b2e43..d28a5be29 100644
--- a/src/ltlast/bunop.cc
+++ b/src/ltlast/bunop.cc
@@ -211,6 +211,10 @@ namespace spot
 		return constant::empty_word_instance();
 	      }
 
+	    // - Exp[*1] = Exp
+	    if (min == 1 && max == 1)
+	      return child;
+
 	    // - Exp[*i..j][*min..max] = Exp[*i(min)..j(max)]
 	    //                                       if i*(min+1)<=j(min)+1.
 	    if (child->kind() == BUnOp)
diff --git a/src/ltlast/bunop.hh b/src/ltlast/bunop.hh
index 730983702..e89ea1c03 100644
--- a/src/ltlast/bunop.hh
+++ b/src/ltlast/bunop.hh
@@ -51,6 +51,7 @@ namespace spot
       ///   - [*0][*min..max] = [*0]
       ///   - Exp[*0] = [*0]
       ///   - Exp[*i..j][*k..l] = Exp[*ik..jl] if i*(k+1)<=jk+1.
+      ///   - Exp[*1] = Exp
       ///
       /// These rewriting rules imply that it is not possible to build
       /// an LTL formula object that is SYNTACTICALLY equal to one of
diff --git a/src/ltltest/equals.test b/src/ltltest/equals.test
index a2e0a886e..f0090e257 100755
--- a/src/ltltest/equals.test
+++ b/src/ltltest/equals.test
@@ -1,8 +1,9 @@
 #! /bin/sh
-# Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et Développement
-# de l'Epita (LRDE).
+# -*- coding: utf-8 -*-
+# Copyright (C) 2009, 2010, 2011, 2012 Laboratoire de Recherche et
+# Développement de l'Epita (LRDE).
 # Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
-# département Systèmes Répartis Coopératifs (SRC), Université Pierre
+# département Systèmes Répartis Coopératifs (SRC), Université Pierre
 # et Marie Curie.
 #
 # This file is part of Spot, a model checking library.
@@ -160,6 +161,7 @@ run 0 ../equals '{a[*..3][*to2]}' '{a[*:6]}'
 run 0 ../equals '{a[*..3][*2..$]}' '{a[*]}'
 run 0 ../equals '{a[*..3][*2:]}' '{a[*:inf]}'
 run 0 ../equals '{a[*1..]}' '{a[+]}'
+run 0 ../equals '{a[*1]}' '{a}'
 run 0 ../equals '{a[+][*1..3]}' '{a[+]}'
 run 0 ../equals '{a[*1..3][+]}' '{a[+]}'
 run 0 ../equals '{[*2][+]}' '{[*2][+]}'