snf: Fix the handling of bounded repetition.

star_normal_form() used to be called under bounded
repetitions like [*0..4], but some of these rewritings
are only correct for [*0..].  For instance
     (a*|1)[*]      can be rewritten to    1[*]
but  (a*|1)[*0..1]  cannot be rewritten to 1[*0..1]
it would be correct to rewrite the latter as (a[+]|1)[*0..1],
canceling the empty word in a*.

Also (a*;b*)[*]     can be rewritten to    (a|b)[*]
but  (a*;b*)[*0..1]  cannot be rewritten to (a|b)[*0..1]
and it cannot either be rewritten to (a[+]|b[+])[*0..1].

This patch introduces a new function to implement
rewritings under bounded repetition.

* src/ltlvisit/snf.hh, src/ltlvisit/snf.cc (star_normal_form_unbounded):
New function.
* src/ltlvisit/simplify.cc: Use it.
* src/ltltest/reduccmp.test: Add tests.
* doc/tl/tl.tex: Document the rewritings implemented.

doc/tl/tl.tex

@@ -1469,27 +1469,53 @@ SERE.
 
 Starred subformul\ae{} are rewritten in Star Normal
 Form~\cite{bruggeman.96.tcs} with:
-\[r\STAR{\mvar{0}..\mvar{j}} \equiv r^\circ\STAR{\mvar{0}..\mvar{j}} \]
+\[r\STAR{} \equiv r^\circ\STAR{} \]
 where $r^\circ$ is recursively defined as follows:
 \begin{align*}
   r^\circ &= r\text{~if~} \varepsilon\not\VDash r \\
   \eword^\circ &= \0 &
   (r_1\CONCAT r_2)^\circ &= r_1^\circ\OR r_2^\circ \text{~if~} \varepsilon\VDash r_1\text{~and~}\varepsilon\VDash r_2\\
-  r\STAR{\mvar{0}..\mvar{j}}^\circ &= r^\circ &
+  r\STAR{\mvar{i}..\mvar{j}}^\circ &= r^\circ \text{~if~} i=0 \text{~or~} \varepsilon\VDash r&
   (r_1\AND r_2)^\circ &= r_1^\circ\OR r_2^\circ \text{~if~} \varepsilon\VDash r_1\text{~and~}\varepsilon\VDash r_2\\
   (r_1\OR r_2)^\circ &= r_1^\circ \OR r_2^\circ &
   (r_1\ANDALT r_2)^\circ &= r_1 \ANDALT r_2
 \end{align*}
 
 Note: the original SNF definition~\cite{bruggeman.96.tcs} does not
-include \samp{$\FUSION$}, \samp{$\AND$}, and \samp{$\ANDALT$}
+include \samp{$\AND$} and \samp{$\ANDALT$} operators, and it
-operators, and it guarantees that $\forall r,\,\varepsilon\not\VDash
+guarantees that $\forall r,\,\varepsilon\not\VDash r^\circ$ because
-r^\circ$ because $r^\circ$ is stripping all the stars and empty words
+$r^\circ$ is stripping all the stars and empty words that occur in
-that occur in $r$.  For instance $\sere{a\STAR{}\CONCAT
+$r$.  For instance $\sere{a\STAR{}\CONCAT
-  b\STAR{}\CONCAT\sere{\1\OR c}}^\circ\STAR{} = \sere{a\OR b\OR
+  b\STAR{}\CONCAT\sere{\eword\OR c}}^\circ\STAR{} = \sere{a\OR b\OR
   c}\STAR{}$.  Our extended definition still respects this property in
-presence of \samp{$\FUSION$} and \samp{$\AND$} operators, but
+presence of \samp{$\AND$} operators, but unfortunately not when the
-unfortunately not when the \samp{$\ANDALT$} operator is used.
+\samp{$\ANDALT$} operator is used.
+
+We extend the above definition to bounded repetitions with:
+\begin{align*}
+  r\STAR{\mvar{i}..\mvar{j}} & \equiv r^\square\STAR{\0..\mvar{j}}\quad\text{if}\quad\varepsilon\VDash r\STAR{\mvar{i}..\mvar{j}}
+\end{align*}
+where $r^\square$ is recursively defined as follows:
+\begin{align*}
+  r^\square &= r\text{~if~} \varepsilon\not\VDash r \\
+  \eword^\square &= \0 &
+  (r_1\CONCAT r_2)^\square &= r_1\CONCAT r_2\\
+  r\STAR{\mvar{i}..\mvar{j}}^\square &= r^\square\STAR{\mvar{\max(1,i)}..\mvar{j}} \text{~if~} i=0 \text{~or~} \varepsilon\VDash r &
+  (r_1\AND r_2)^\square &= r_1^\square\OR r_2^\square \text{~if~} \varepsilon\VDash r_1\text{~and~}\varepsilon\VDash r_2\\
+  (r_1\OR r_2)^\square &= r_1^\square \OR r_2^\square &
+  (r_1\ANDALT r_2)^\square &= r_1 \ANDALT r_2
+\end{align*}
+The differences between $^\square$ and $^\circ$ are in the handling
+of $r\STAR{\mvar{i}..\mvar{j}}$ and in the handling of $r_1\CONCAT r_2$.
+
+% Indeed $(c\STAR{}\OR\1)\STAR{0..1}$ is not equivalent to
+% $(c\STAR{}\OR\1)^\circ\STAR{0..1}\equiv(c\OR\1)\STAR{0..1}\equiv
+% 1\STAR{0..1}$ but to
+% $(c\STAR{}\OR\1)^\square\STAR{0..1}\equiv(c\PLUS{}\OR\1)\STAR{0..1}$.
+
+% Similarly $(a\STAR{}\CONCAT b\STAR{})\STAR{0..1})$ is definitely not
+% equal to $(a\PLUS{}\OR b\PLUS{})\STAR{0..1}).
+
 
 \subsubsection{Basic Simplifications SERE-LTL Binding Operators}
 

src/ltltest/reduccmp.test

@@ -364,6 +364,9 @@ for x in ../reduccmp ../reductaustr; do
      run 0 $x '{(a;c*;d)|(b;c)}' '(a & X(c W d)) | (b & Xc)'
      run 0 $x '!{(a;c*;d)|(b;c)}' '(X(!c M !d) | !a) & (X!c | !b)'
      run 0 $x '(Xc R b) & (Xc W 0)' 'b & XGc'
+     run 0 $x '{{c*|1}[*0..1]}<>-> v' '{{c[+]|1}[*0..1]}<>-> v'
+     run 0 $x '{{b*;c*}[*3..5]}<>-> v' '{{b*;c*}[*0..5]} <>-> v'
+     run 0 $x '{{b*&c*}[*3..5]}<>-> v' '{{b[+]|c[+]}[*0..5]} <>-> v'
 
      # not reduced
      run 0 $x '{a;(b[*2..4];c*;([*0]+{d;e}))*}!' \

src/ltlvisit/simplify.cc

@@ -106,6 +106,16 @@ namespace spot
 	      old->first->destroy();
 	    }
 	}
+	{
+	  snf_cache::iterator i = snfb_cache_.begin();
+	  snf_cache::iterator end = snfb_cache_.end();
+	  while (i != end)
+	    {
+	      snf_cache::iterator old = i++;
+	      old->second->destroy();
+	      old->first->destroy();
+	    }
+	}
 	{
 	  f2f_map::iterator i = bool_isop_.begin();
 	  f2f_map::iterator end = bool_isop_.end();
@@ -387,6 +397,13 @@ namespace spot
 	return ltl::star_normal_form(f, &snf_cache_);
       }
 
+      const formula*
+      star_normal_form_bounded(const formula* f)
+      {
+	return ltl::star_normal_form_bounded(f, &snfb_cache_);
+      }
+
+
       const formula*
       boolean_to_isop(const formula* f)
       {
@@ -406,6 +423,7 @@ namespace spot
       f2f_map nenoform_;
       syntimpl_cache_t syntimpl_;
       snf_cache snf_cache_;
+      snf_cache snfb_cache_;
       f2f_map bool_isop_;
     };
 
@@ -1080,7 +1098,10 @@ namespace spot
 		min = 0;
 	      if (min == 0)
 		{
-		  const formula* s = c_->star_normal_form(h);
+		  const formula* s =
+		    bo->max() == bunop::unbounded ?
+		    c_->star_normal_form(h) :
+		    c_->star_normal_form_bounded(h);
 		  h->destroy();
 		  h = s;
 		}

src/ltlvisit/snf.cc

@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2012 Laboratoire de Recherche et Developpement
+// Copyright (C) 2012, 2014 Laboratoire de Recherche et Developpement
 // de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -31,6 +31,7 @@ namespace spot
       // E°
       class snf_visitor: public visitor
       {
+      protected:
 	const formula* result_;
 	snf_cache* cache_;
       public:
@@ -144,21 +145,50 @@ namespace spot
 	  if (!f->accepts_eword())
 	    return f->clone();
 
-	  if (cache_)
+	  snf_cache::const_iterator i = cache_->find(f);
-	    {
+	  if (i != cache_->end())
-	      snf_cache::const_iterator i = cache_->find(f);
+	    return i->second->clone();
-	      if (i != cache_->end())
-		return i->second->clone();
-	    }
 
 	  f->accept(*this);
 
-	  if (cache_)
+	  (*cache_)[f->clone()] = result_->clone();
-	    (*cache_)[f->clone()] = result_->clone();
 	  return result_;
 	}
       };
 
+      // E^□
+      class snf_visitor_bounded: public snf_visitor
+      {
+      public:
+	snf_visitor_bounded(snf_cache* c): snf_visitor(c)
+	{
+	}
+
+	void
+	visit(const bunop* bo)
+	{
+	  bunop::type op = bo->op();
+	  switch (op)
+	    {
+	    case bunop::Star:
+	      assert(bo->accepts_eword());
+	      result_ = bunop::instance(bunop::Star,
+					recurse(bo->child()),
+					std::max(bo->min(), 1U),
+					bo->max());
+	      break;
+	    }
+	}
+
+	void
+	visit(const multop* mo)
+	{
+	  if (mo->op() == multop::Concat)
+	    result_ = mo->clone();
+	  else
+	    this->snf_visitor::visit(mo);
+	}
+      };
     }
 
 
@@ -169,5 +199,12 @@ namespace spot
       return v.recurse(sere);
     }
 
+    const formula*
+    star_normal_form_bounded(const formula* sere, snf_cache* cache)
+    {
+      snf_visitor_bounded v(cache);
+      return v.recurse(sere);
+    }
+
   }
 }

src/ltlvisit/snf.hh

@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2012, 2013 Laboratoire de Recherche et Developpement
+// Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et
-// de l'Epita (LRDE).
+// Developpement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -52,6 +52,10 @@ namespace spot
     /// \param cache an optional cache
     SPOT_API const formula*
     star_normal_form(const formula* sere, snf_cache* cache = 0);
+
+    /// A variant of star_normal_form() for r[*0..j] where j < ω.
+    SPOT_API const formula*
+    star_normal_form_bounded(const formula* sere, snf_cache* cache = 0);
   }
 }