Implement basic rewriting rules for {r} and !{r}.

* src/ltlvisit/simplify.cc: Here.
* src/ltltest/reduccmp.test: Test them.
* doc/tl/tl.tex: Document them.

doc/tl/tl.tex

@@ -759,16 +759,16 @@ formula $f$ to form another PSL formula.
   existential suffix implication
   & $\sere{r}\Esuffix{} f$
   \\
-  closure
+  weak closure
   & $\sere{r}$
   \\
-  negated closure
+  negated weak closure
   & $\nsere{r}$
   \\
 \end{tabular}
 \end{center}
 
-For technical reasons, the negated closure is actually implemented as
+For technical reasons, the negated weak closure is actually implemented as
 an operator, even if it is syntactically and semantically equal to the
 combination of $\NOT$ and $\sere{r}$.
 
@@ -809,6 +809,8 @@ rewritings are also preformed on output to ease reading.
 $\AsuffixEQ$ and $\AsuffixALTEQ$ are synonyms in the same way as
 $\Asuffix$ and $\AsuffixALT$ are.
 
+The $\seren{r}$ operator is a \emph{strong closure} operator.
+
 \subsection{Trivial Identities (Occur Automatically)}
 
 For any PSL formula $f$, any SERE $r$, and any Boolean
@@ -826,8 +828,8 @@ formula $b$, the following rewritings are systematically performed
 & \nsere{\1} & \equiv \0 \\
   \sere{\eword}\Asuffix f&\equiv \1
 & \sere{\eword}\Esuffix f&\equiv \0
-& \sere{\eword} & \equiv \0
+& \sere{\eword} & \equiv \1
-& \nsere{\eword} & \equiv \1 \\
+& \nsere{\eword} & \equiv \0 \\
   \sere{b}\Asuffix f&\equiv (\NOT{b})\OR f
 & \sere{b}\Esuffix f&\equiv b\AND f
 & \sere{b} &\equiv b
@@ -1205,7 +1207,7 @@ rewriting arrange any PSL formula into negative normal form.
   \NOT(f \M g) & \equiv (\NOT f) \W (\NOT g)&
   \NOT(\sere{r} \Esuffix f) &\equiv \sere{r} \Asuffix \NOT f
 \end{align*}
-\noindent Recall the that negated closure $\nsere{r}$ is actually
+\noindent Recall the that negated weak closure $\nsere{r}$ is actually
 implemented as a specific operator, so it not actually prefixed by the
 $\NOT$ operator.
 \begin{align*}
@@ -1474,6 +1476,22 @@ denoted with $\equiV$ can be disabled by setting the
   \sere{r_1\OR r_2}\Esuffix f &\equiV (\sere{r_1}\Esuffix f)\OR(\sere{r_2}\Esuffix f)
 \end{align*}
 
+Here are basic the rewritings for the weak closure and its negation:
+\begin{align*}
+  \sere{r}&\equiv \1\text{~if~}\varepsilon\VDash r&
+  \nsere{r}&\equiv \0\text{~if~}\varepsilon\VDash r\\
+  \sere{r_1;r_2}&\equiv \sere{r_1}\text{~if~}\varepsilon\VDash r_2&
+  \nsere{r_1;r_2}&\equiv \nsere{r_1}\text{~if~}\varepsilon\VDash r_2\\
+  \sere{b;r}&\equiV b\AND\X\sere{r}&
+  \nsere{b;r}&\equiV (\NOT b)\OR\X\nsere{r}\\
+  \sere{b\STAR{};r}&\equiv b\W\sere{r}&
+  \nsere{b\STAR{};r}&\equiv (\NOT b)\M\nsere{r}\\
+  \sere{b\STAR{\mvar{i}..\mvar{j}};r}&\equiV \underbrace{b\AND \X(b\ldots}_{\mathclap{i\text{~occurences of~}b}}\AND\X\sere{b\STAR{\mvar{0}..\mvar{j-i}}\CONCAT r})&
+  \nsere{b\STAR{\mvar{i}..\mvar{j}};r}&\equiV \underbrace{(\NOT b)\OR \X((\NOT b)\ldots}_{\mathclap{i\text{~occurences of~}\NOT b}}\OR\X\nsere{b\STAR{\mvar{0}..\mvar{j-i}}\CONCAT r}) \\
+  \sere{b\STAR{\mvar{i}..\mvar{j}}}&\equiV \underbrace{b\AND \X(b\AND \X(\ldots b))}_{i\text{~occurences of~}b}&
+  \nsere{b\STAR{\mvar{i}..\mvar{j}}}&\equiV \underbrace{(\NOT b)\OR \X((\NOT b)\OR \X(\ldots(\NOT b)))}_{i\text{~occurences of~}\NOT b}
+\end{align*}
+
 \subsection{Simplifications for Eventual and Universal Formul\ae}
 \label{sec:eventunivrew}
 

src/ltltest/reduccmp.test

@@ -270,13 +270,13 @@ for x in ../reduccmp ../reductaustr; do
      run 0 $x '{a && {b*;c:e}} <>-> d' 'a & c & d & e'
      run 0 $x '{a && {b;c*}} <>-> d' 'a & b & d'
      run 0 $x '{a && {b;c*:e}} <>-> d' 'a & b & d & e'
-     run 0 $x '{{b1;r1*}&&{b2;r2*}}' '{{b1&&b2};{r1*&&r2*}}'
+     run 0 $x '{{{b1;r1*}&&{b2;r2*}};c}' 'b1&b2&X{{r1*&&r2*};c}'
      run 0 $x '{{b1:r1*}&&{b2:r2*}}' '{{b1&&b2}:{r1*&&r2*}}'
      run 0 $x '{{r1*;b1}&&{r2*;b2}}' '{{r1*&&r2*};{b1&&b2}}'
      run 0 $x '{{r1*:b1}&&{r2*:b2}}' '{{r1*&&r2*}:{b1&&b2}}'
      run 0 $x '{{a;b*;c}&&{d;e*}&&{f*;g}&&{h*}}' \
               '{{f*;g}&&{h*}&&{{a&&d};{e* && {b*;c}}}}'
-     run 0 $x '{{b1;r1*}&{b2;r2*}}' '{{b1&&b2};{r1*&r2*}}'
+     run 0 $x '{{{b1;r1*}&{b2;r2*}};c}' 'b1&b2&X{{r1*&r2*};c}'
      run 0 $x '{{b1:r1*}&{b2:r2*}}' '{{b1&&b2}:{r1*&r2*}}'
      run 0 $x '{{r1*;b1}&{r2*;b2}}' '{{r1*&r2*};{b1&&b2}}'
      run 0 $x '{{r1*:b1}&{r2*:b2}}' '{{r1*&r2*}:{b1&&b2}}'
@@ -312,6 +312,12 @@ for x in ../reduccmp ../reductaustr; do
      run 0 $x '{a|b*|c|d*}<>->e' '((a | c) & e) | (e M b) | (e M d)'
      run 0 $x '{{[*0] | a};b;{[*0] | a};c;e[*]} <>-> f' \
 	      '{{[*0] | a};b;{[*0] | a}} <>-> X(c & (f | X(f M e)))'
+     run 0 $x '{a;b[*];c[*];e;f*}' 'a & X(b W (c W e))'
+     run 0 $x '{a;b*;(a* && (b;c));c*}' 'a & X(b W {a[*] && {b;c}})'
+     run 0 $x '{a;a;b[*2..];b}' 'a & X(a & X(b & X(b & Xb)))'
+     run 0 $x '!{a;a;b[*2..];b}' '!a | X(!a | X(!b | X(!b | X!b)))'
+     run 0 $x '!{a;b[*];c[*];e;f*}' '!a | X(!b M (!c M !e))'
+     run 0 $x '!{a;b*;(a* && (b;c));c*}' '!a | X(!b M !{a[*] && {b;c}})'
 
      # not reduced
      run 0 $x '{a;(b[*2..4];c*;([*0]+{d;e}))*}!' \

src/ltlvisit/simplify.cc

@@ -1038,6 +1038,32 @@ namespace spot
 	    }
 	}
 
+	// if !neg build c&X(c&X(...&X(tail))) with n occurences of c
+	// if neg build !c|X(!c|X(...|X(tail))).
+	formula*
+	dup_b_x_tail(bool neg, formula* c, formula* tail, unsigned n)
+	{
+	  c->clone();
+	  multop::type mop;
+	  if (neg)
+	    {
+	      c = unop::instance(unop::Not, c);
+	      mop = multop::Or;
+	    }
+	  else
+	    {
+	      mop = multop::And;
+	    }
+	  while (n--)
+	    {
+	      tail = unop::instance(unop::X, tail);
+	      tail = // b&X(tail) or !b|X(tail)
+		multop::instance(mop, c->clone(), tail);
+	    }
+	  c->destroy();
+	  return tail;
+	}
+
 	void
 	visit(unop* uo)
 	{
@@ -1256,9 +1282,150 @@ namespace spot
 		  && c_->lcc.contained(result_, uo))
 		return;
 	      break;
-	    case unop::Finish:
 	    case unop::Closure:
 	    case unop::NegClosure:
+	      // {e} = 1 if e accepts [*0]
+	      // !{e} = 0 if e accepts [*0]
+	      if (result_->accepts_eword())
+		{
+		  result_->destroy();
+		  result_ = ((op == unop::Closure)
+			     ? constant::true_instance()
+			     : constant::false_instance());
+		  return;
+		}
+	      if (multop* mo = is_Concat(result_))
+		{
+		  unsigned end = mo->size() - 1;
+		  // {b₁;b₂;b₃*;e₁;f₁;e₂;f₂;e₂;e₃;e₄}
+		  //    = b₁&X(b₂&X(b₃ W {e₁;f₁;e₂;f₂}))
+		  // !{b₁;b₂;b₃*;e₁;f₁;e₂;f₂;e₂;e₃;e₄}
+		  //    = !b₁|X(!b₂|X(!b₃ M !{e₁;f₁;e₂;f₂}))
+		  // if e denotes a term that accepts [*0]
+		  // and b denotes a Boolean formula.
+		  while (mo->nth(end)->accepts_eword())
+		    --end;
+		  unsigned start = 0;
+		  while (start <= end)
+		    {
+		      formula* r = mo->nth(start);
+		      bunop* es = is_KleenStar(r);
+		      if ((r->is_boolean() && !opt_.reduce_size_strictly)
+			  || (es && es->child()->is_boolean()))
+			++start;
+		      else
+			break;
+		    }
+		  unsigned s = end + 1 - start;
+		  if (s != mo->size())
+		    {
+		      multop::vec* v = new multop::vec;
+		      v->reserve(s);
+		      for (unsigned n = start; n <= end; ++n)
+			v->push_back(mo->nth(n)->clone());
+		      formula* tail = multop::instance(multop::Concat, v);
+		      tail = unop::instance(op, tail);
+
+		      bool doneg = op == unop::NegClosure;
+		      for (unsigned n = start; n > 0;)
+			{
+			  --n;
+			  formula* e = mo->nth(n);
+			  // {b;f} = b & X{f}
+			  // !{b;f} = !b | X!{f}
+			  if (e->is_boolean())
+			    {
+			      tail = unop::instance(unop::X, tail);
+			      e->clone();
+			      if (doneg)
+				tail =
+				  multop::instance(multop::Or,
+						   unop::instance(unop::Not, e),
+						   tail);
+			      else
+				tail =
+				  multop::instance(multop::And, e, tail);
+			    }
+			  // {b*;f} = b W {f}
+			  // !{b*;f} = !b M !{f}
+			  else
+			    {
+			      bunop* es = is_KleenStar(e);
+			      assert(es);
+			      formula* c = es->child()->clone();
+			      if (doneg)
+				tail =
+				  binop::instance(binop::M,
+						  unop::instance(unop::Not, c),
+						  tail);
+			      else
+				tail = binop::instance(binop::W, c, tail);
+			    }
+			}
+		      mo->destroy();
+		      result_ = recurse_destroy(tail);
+		      return;
+		    }
+
+		  // {b[*i..j];c} = b&X(b&X(... b&X{b[*0..j-i];c}))
+		  // !{b[*i..j];c} = !b&X(!b&X(... !b&X!{b[*0..j-i];c}))
+		  if (!opt_.reduce_size_strictly)
+		    if (bunop* s = is_Star(mo->nth(0)))
+		      {
+			formula* c = s->child();
+			unsigned min = s->min();
+			if (c->is_boolean() && min > 0)
+			  {
+			    unsigned max = s->max();
+			    if (max != bunop::unbounded)
+			      max -= min;
+			    unsigned ss = mo->size();
+			    multop::vec* v = new multop::vec;
+			    v->reserve(ss);
+			    v->push_back(bunop::instance(bunop::Star,
+							 c->clone(),
+							 0, max));
+			    for (unsigned n = 1; n < ss; ++n)
+			      v->push_back(mo->nth(n)->clone());
+			    formula* tail =
+			      multop::instance(multop::Concat, v);
+			    tail = // {b[*0..j-i]} or !{b[*0..j-i]}
+			      unop::instance(op, tail);
+			    tail =
+			      dup_b_x_tail(op == unop::NegClosure,
+					   c, tail, min);
+			    mo->destroy();
+			    result_ = recurse_destroy(tail);
+			    return;
+			  }
+			}
+		}
+	      // {b[*i..j]} = b&X(b&X(... b))  with i occurences of b
+	      // !{b[*i..j]} = !b&X(!b&X(... !b))
+	      if (!opt_.reduce_size_strictly)
+		if (bunop* s = is_Star(result_))
+		  {
+		    formula* c = s->child();
+		    if (c->is_boolean())
+		      {
+			unsigned min = s->min();
+			assert(min > 0);
+			formula* tail;
+			if (op == unop::NegClosure)
+			  tail =
+			    dup_b_x_tail(true,
+					 c, constant::false_instance(), min);
+			else
+			  tail =
+			    dup_b_x_tail(false,
+					 c, constant::true_instance(), min);
+			result_->destroy();
+			result_ = recurse_destroy(tail);
+			return;
+		      }
+		  }
+	      break;
+	    case unop::Finish:
 	      // No simplification
 	      break;
 	    }