From e7cf7b422d3b893686c55990470729e786472684 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Wed, 25 Apr 2012 15:14:14 +0200
Subject: [PATCH] Trivially reduce f;f to f[*2], f[*1..3];f to f[*2..4], etc.

* src/ltlast/multop.cc (instance): Implement the reduction.
* src/ltlast/multop.hh, doc/tl/tl.tex: Document it.
* src/ltltest/equals.test: Add a test.
---
 doc/tl/tl.tex           | 24 +++++++++-----
 src/ltlast/multop.cc    | 69 +++++++++++++++++++++++++++++++++++++++++
 src/ltlast/multop.hh    |  2 ++
 src/ltltest/equals.test |  1 +
 4 files changed, 88 insertions(+), 8 deletions(-)

diff --git a/doc/tl/tl.tex b/doc/tl/tl.tex
index b3a751029..9b05c77f8 100644
--- a/doc/tl/tl.tex
+++ b/doc/tl/tl.tex
@@ -687,7 +687,7 @@ $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*}
 
@@ -697,9 +697,6 @@ The following rules are all valid with the two arguments swapped.
 %\samp{$\FUSION$}.)
 
 \begin{align*}
-  f\AND f &\equiv f&
-  f\ANDALT f &\equiv f &
-  f\OR f &\equiv f \\
   \0\AND f &\equiv \0 &
   \0\ANDALT f   &\equiv \0 &
   \0\OR f &\equiv f &
@@ -715,22 +712,33 @@ The following rules are all valid with the two arguments swapped.
   \1 \FUSION f & \equiv f\mathrlap{\text{~if~}\varepsilon\nVDash f}\\
   &&
   \STAR{} \AND f &\equiv f &
-  \STAR{} \OR f &\equiv \1\STAR{} &
+  \STAR{} \OR f &\equiv \1\mathrlap{\STAR{}} &
   &&
   \STAR{} \CONCAT f &\equiv \STAR{}\mathrlap{\text{~if~}\varepsilon\VDash f}& \\
   \eword\AND f &\equiv f &
   \eword\ANDALT f &\equiv
   \begin{cases}
-    \eword &\mathrlap{\text{if~} \varepsilon\VDash f} \\
-    \0 &\mathrlap{\text{if~} \varepsilon\nVDash f} \\
+    \mathrlap{\eword\text{~if~} \varepsilon\VDash f} \\
+    \0\mathrlap{\phantom{\STAR{}}\text{~if~} \varepsilon\nVDash f} \\
   \end{cases} &
   &&
   \eword \FUSION f &\equiv \0 &
   \eword \CONCAT f &\equiv f\\
+  f\AND f &\equiv f&
+  f\ANDALT f &\equiv f &
+  f\OR f &\equiv f&
+  &&
+  f\CONCAT f&\equiv f\STAR{2}\\
   b_1 \AND b_2 &\equiv b_1\ANDALT b_2 &
   &&
   &&
-  b_1:b_2 &\equiv b_1\ANDALT b_2\\
+  b_1:b_2 &\equiv b_1\ANDALT b_2 &
+  f\STAR{\mvar{i}..\mvar{j}}\CONCAT f&\equiv f\STAR{\mvar{i+1}..\mvar{j+1}}\\
+  &&
+  &&
+  &&
+  &&
+  \mathllap{f\STAR{\mvar{i}..\mvar{j}}}\CONCAT f\STAR{\mvar{k}..\mvar{l}}&\equiv f\STAR{\mvar{i+k}..\mvar{j+l}}\\
 \end{align*}
 
 \section{SERE-LTL Binding Operators}
diff --git a/src/ltlast/multop.cc b/src/ltlast/multop.cc
index 7464fdd44..00b785dd3 100644
--- a/src/ltlast/multop.cc
+++ b/src/ltlast/multop.cc
@@ -501,6 +501,75 @@ namespace spot
 		v->swap(tmp);
 	      }
 	  }
+	else if (op == Concat)
+	  {
+	    // Perform an extra loop to merge starable items.
+	    //   f;f -> f[*2]
+	    //   f;f[*i..j] -> f[*i+1..j+1]
+	    //   f[*i..j];f -> f[*i+1..j+1]
+	    //   f[*i..j];f[*k..l] -> f[*i+k..j+l]
+	    i = v->begin();
+	    while (i != v->end())
+	      {
+		vec::iterator fpos = i;
+		formula* f;
+		unsigned min;
+		unsigned max;
+		bool changed = false;
+		if (bunop* is = is_Star(*i))
+		  {
+		    f = is->child();
+		    min = is->min();
+		    max = is->max();
+		  }
+		else
+		  {
+		    f = *i;
+		    min = max = 1;
+		  }
+
+		++i;
+		while (i != v->end())
+		  {
+		    formula* f2;
+		    unsigned min2;
+		    unsigned max2;
+		    if (bunop* is = is_Star(*i))
+		      {
+			f2 = is->child();
+			if (f2 != f)
+			  break;
+			min2 = is->min();
+			max2 = is->max();
+		      }
+		    else
+		      {
+			f2 = *i;
+			if (f2 != f)
+			  break;
+			min2 = max2 = 1;
+		      }
+		    if (min2 == bunop::unbounded)
+		      min = bunop::unbounded;
+		    else if (min != bunop::unbounded)
+		      min += min2;
+		    if (max2 == bunop::unbounded)
+		      max = bunop::unbounded;
+		    else if (max != bunop::unbounded)
+		      max += max2;
+		    (*i)->destroy();
+		    i = v->erase(i);
+		    changed = true;
+		  }
+		if (changed)
+		  {
+		    formula* newfs = bunop::instance(bunop::Star, f->clone(),
+						     min, max);
+		    (*fpos)->destroy();
+		    *fpos = newfs;
+		  }
+	      }
+	  }
       }
 
       vec::size_type s = v->size();
diff --git a/src/ltlast/multop.hh b/src/ltlast/multop.hh
index 3b7878474..26ac02426 100644
--- a/src/ltlast/multop.hh
+++ b/src/ltlast/multop.hh
@@ -111,6 +111,8 @@ namespace spot
       /// - Concat(Exps1...,FExps2...,1[*],FExps3...,Exps4) =
       ///     Concat(Exps1...,1[*],Exps4) if FExps2...FExps3... all accept [*0]
       /// - Concat(Exp) = Exp
+      /// - Concat(Exps1...,E,E[*i..j],E[*k..l],Exps2...) =
+      ///     Concat(Exps1...,E[*1+i+k..j+l],Exps2...)  and similar forms
       /// - Fusion(Exps1...1,Exps2...) = Fusion(Exps1...,Exps2...)
       ///     if at least one exp reject [*0]
       /// - Fusion(Exps1...,0,Exps2...) = 0
diff --git a/src/ltltest/equals.test b/src/ltltest/equals.test
index c4b2d51db..2293f6cad 100755
--- a/src/ltltest/equals.test
+++ b/src/ltltest/equals.test
@@ -164,6 +164,7 @@ run 1 ../equals '{(a;!a)*:(a;!a)*:b}!' '{(a;!a)*:b}!'
 run 1 ../equals '{(1:a*);b}!' '{a*;b}!'
 run 0 ../equals '{z;a*;b*;*;c;d;*;b*;e;a*;*;b*}' '{z;[*];c;d;[*];e;[*]}'
 run 0 ../equals '{((a;b)|[*0]);[*];c}!' '{[*];c}!'
+run 0 ../equals '{a;a;a*;a;b;b[*];c[*2:3];c[*4:5]}' '{a[*3..];b[+];c[*6..8]}'
 
 run 0 ../equals '{a[*0]}' '{[*0]}'
 run 0 ../equals '{a[*..]}' '{a[*]}'