Fix translation of !{r}.

We need a marked version of !{r} to perform breakpoint unroling.

* src/ltlast/unop.cc, src/ltlast/unop.hh: Declare a NegClosureMarked
operator.
* src/ltlvisit/mark.hh, src/ltlvisit/mark.cc,
src/tgbaalgos/ltl2tgba_fm.cc: Adjust to deal with NegClosureMarked
and NegClosure as apropriate.
* src/ltlvisit/simplify.cc, src/ltlvisit/tostring.cc,
src/ltlvisit/tunabbrev.cc, src/tgbaalgos/eltl2tgba_lacim.cc,
src/tgbaalgos/ltl2taa.cc, src/tgbaalgos/ltl2tgba_lacim.cc,
src/tgba/formula2bdd.cc: Deal with NegClosureMarked in the same way as
we deal with NegClosure.
* src/tgbatest/ltl2tgba.test: More tests.
* src/ltltest/kind.test: Adjust.
* doc/tl/tl.tex: Mention the marked negated closure.

NEWS

@@ -3,6 +3,8 @@ New in spot 0.9a:
   * Bug fixes:
     - The random SERE generator was using the wrong operators
       for "and" and "or", mistaking And/Or with AndRat/OrRat.
+    - The translation of !{r} was incorrect when this subformula
+      was recurring (e.g. in G!{r}) and r had loops.
 
 New in spot 0.9 (2012-05-09):
 

doc/tl/tl.tex

@@ -98,6 +98,7 @@
 
 \newcommand{\sere}[1]{\texttt{\{}#1\texttt{\}}}
 \newcommand{\nsere}[1]{\texttt{!\{}#1\texttt{\}}}
+\newcommand{\nsereMarked}[1]{\texttt{!+\{}#1\texttt{\}}}
 \newcommand{\seren}[1]{\texttt{\{}#1\texttt{\}!}}
 
 % rewriting rules that enlarge the formula
@@ -974,15 +975,16 @@ instance using the following methods:
 \\\texttt{is\_syntactic\_persistence()}& Whether the formula is a syntactic
   persistence property.
 \\\texttt{is\_marked()}& Whether the formula contains a special
-  ``marked'' version of the $\Esuffix$ operator.\footnotemark
+  ``marked'' version of the $\Esuffix$ or $\nsere{r}$ operators.\footnotemark
 \\\texttt{accepts\_eword()}& Whether the formula accepts
   $\eword$. (This can only be true for a SERE formula.)
 \end{tabulary}
 
-\footnotetext{This special operator is used when translating recurring
+\footnotetext{These ``marked'' operators are used when
-  $\Esuffix$, it is rendered as $\EsuffixMarked$ and it obeys the same
+  translating recurring $\Esuffix$ or $\nsere{r}$ operators.  They are
-  simplification rules and properties as $\Esuffix$ (except for the
+  rendered as $\EsuffixMarked$ and $\nsereMarked{r}$ and obey the
-  \texttt{is\_marked()} property).}
+  same simplification rules and properties as their unmarked
+  counterpart (except for the \texttt{is\_marked()} property).}
 
 \section{Pure Eventualities and Purely Universal Formul\ae{}}
 \label{sec:eventuniv}

src/ltlast/unop.cc

@@ -112,7 +112,8 @@ namespace spot
 	  is.accepting_eword = false;
 	  break;
 	case NegClosure:
-	  is.not_marked = false;
+	case NegClosureMarked:
+	  is.not_marked = (op == NegClosure);
 	  is.boolean = false;
 	  is.ltl_formula = false;
 	  is.eltl_formula = false;
@@ -198,6 +199,8 @@ namespace spot
 	  return "Closure";
 	case NegClosure:
 	  return "NegClosure";
+	case NegClosureMarked:
+	  return "NegClosureMarked";
 	}
       // Unreachable code.
       assert(0);
@@ -297,6 +300,7 @@ namespace spot
 	  break;
 
 	case NegClosure:
+	case NegClosureMarked:
 	  // {1} = 0,  {[*0]} = 0
 	  if (child == constant::true_instance()
 	      || child == constant::empty_word_instance())

src/ltlast/unop.hh

@@ -47,7 +47,7 @@ namespace spot
 	// ELTL
 	Finish,
 	// Closure
-	Closure, NegClosure,
+	Closure, NegClosure, NegClosureMarked
 	};
 
       /// \brief Build an unary operator with operation \a op and

src/ltltest/kind.test

@@ -115,7 +115,7 @@ check '{a;b*;c}' '&!xfPsopr'
 check '{a;b*;c}!' '&!xfPgopr'
 check '!{a;b*;c}!' '&xfPsopr'  # The negative normal form is {a;b*;c}[]->0
 check '{a;b*;c}[]->0' '&!xfPsopr'
-check '!{a;b*;c}' '&!xfPgopr+'
+check '!{a;b*;c}' '&!xfPgopr'
 
 run 0 ../consterm '1'
 run 0 ../consterm '0'

src/ltlvisit/mark.cc

@@ -22,6 +22,8 @@
 #include "ltlast/allnodes.hh"
 #include <cassert>
 #include <algorithm>
+#include <set>
+#include <vector>
 #include "ltlvisit/tostring.hh"
 #include "misc/casts.hh"
 
@@ -103,21 +105,25 @@ namespace spot
 	      {
 		typedef std::set<std::pair<const formula*,
 					   const formula*> > pset;
-		pset Epairs, EMpairs;
+		pset empairs;
+		typedef std::set<const formula*> sset;
+		sset nmset;
+		typedef std::vector<const binop*> unbinop;
+		unbinop elist;
+		typedef std::vector<const unop*> ununop;
+		ununop nlist;
 
 		for (unsigned i = 0; i < mos; ++i)
 		  {
 		    const formula* f = mo->nth(i);
-
+		    if (const binop* bo = is_binop(f))
-		    if (f->kind() != formula::BinOp)
 		      {
-			res->push_back(recurse(f));
-		      }
-		    else
-		      {
-			const binop* bo = static_cast<const binop*>(f);
 			switch (bo->op())
 			  {
+			  case binop::EConcatMarked:
+			    empairs.insert(std::make_pair(bo->first(),
+							  bo->second()));
+			    // fall through
 			  case binop::Xor:
 			  case binop::Implies:
 			  case binop::Equiv:
@@ -129,29 +135,49 @@ namespace spot
 			    res->push_back(recurse(f));
 			    break;
 			  case binop::EConcat:
-			    assert(mo->op() == multop::And);
+			    elist.push_back(bo);
-			    Epairs.insert(std::make_pair(bo->first(),
-							 bo->second()));
-			    break;
-			  case binop::EConcatMarked:
-			    assert(mo->op() == multop::And);
-			    EMpairs.insert(std::make_pair(bo->first(),
-							  bo->second()));
 			    break;
 			  }
 		      }
+		    if (const unop* uo = is_unop(f))
+		      {
+			switch (uo->op())
+			  {
+			  case unop::NegClosureMarked:
+			    nmset.insert(uo->child());
+			    // fall through
+			  case unop::Not:
+			  case unop::X:
+			  case unop::F:
+			  case unop::G:
+			  case unop::Finish:
+			  case unop::Closure:
+			    res->push_back(recurse(f));
+			    break;
+			  case unop::NegClosure:
+			    nlist.push_back(uo);
+			    break;
+			  }
+		      }
+		    else
+		      {
+			res->push_back(recurse(f));
+		      }
 		  }
-		for (pset::const_iterator i = EMpairs.begin();
+		// Keep only the non-marked EConcat for which we
-		     i != EMpairs.end(); ++i)
+		// have not seen a similar EConcatMarked.
-		  res->push_back(binop::instance(binop::EConcatMarked,
+		for (unbinop::const_iterator i = elist.begin();
-						 i->first->clone(),
+		     i != elist.end(); ++i)
-						 i->second->clone()));
+		  if (empairs.find(std::make_pair((*i)->first(),
-		for (pset::const_iterator i = Epairs.begin();
+						  (*i)->second()))
-		     i != Epairs.end(); ++i)
+		      == empairs.end())
-		  if (EMpairs.find(*i) == EMpairs.end())
+		    res->push_back((*i)->clone());
-		    res->push_back(binop::instance(binop::EConcat,
+		// Keep only the non-marked NegClosure for which we
-						   i->first->clone(),
+		// have not seen a similar NegClosureMarked.
-						   i->second->clone()));
+		for (ununop::const_iterator i = nlist.begin();
+		     i != nlist.end(); ++i)
+		  if (nmset.find((*i)->child()) == nmset.end())
+		    res->push_back((*i)->clone());
 	      }
 	    }
 	  result_ = multop::instance(mo->op(), res);
@@ -212,7 +238,24 @@ namespace spot
 	void
 	visit(const unop* uo)
 	{
-	  result_ = uo->clone();
+	  switch (uo->op())
+	    {
+	    case unop::Not:
+	    case unop::X:
+	    case unop::F:
+	    case unop::G:
+	    case unop::Finish:
+	    case unop::Closure:
+	    case unop::NegClosureMarked:
+	      result_ = uo->clone();
+	      return;
+	    case unop::NegClosure:
+	      result_ = unop::instance(unop::NegClosureMarked,
+				       uo->child()->clone());
+	      return;
+	    }
+	  /* Unreachable code. */
+	  assert(0);
 	}
 
 	void
@@ -245,13 +288,13 @@ namespace spot
 	    case binop::M:
 	    case binop::R:
 	    case binop::UConcat:
+	    case binop::EConcatMarked:
 	      result_ = bo->clone();
 	      return;
-	    case binop::EConcatMarked:
 	    case binop::EConcat:
 	      {
 		const formula* f1 = bo->first()->clone();
-		const formula* f2 = recurse(bo->second());
+		const formula* f2 = bo->second()->clone();
 		result_ = binop::instance(binop::EConcatMarked, f1, f2);
 		return;
 	      }

src/ltlvisit/mark.hh

@@ -32,7 +32,7 @@ namespace spot
     class mark_tools
     {
     public:
-      /// \brief Mark operators UConcat and EConcat.
+      /// \brief Mark operators NegClosure and EConcat.
       /// \ingroup ltl_rewriting
       ///
       /// \param f The formula to rewrite.

src/ltlvisit/simplify.cc

@@ -418,7 +418,8 @@ namespace spot
 	visit(const unop* uo)
 	{
 	  const formula* f = uo->child();
-	  switch (uo->op())
+	  unop::type op = uo->op();
+	  switch (op)
 	    {
 	    case unop::Not:
 	      // "Not"s should be caught by nenoform_recursively().
@@ -445,8 +446,9 @@ namespace spot
 				       recurse_(f, false));
 	      return;
 	    case unop::NegClosure:
+	    case unop::NegClosureMarked:
 	      result_ = unop::instance(negated_ ?
-				       unop::Closure : uo->op(),
+				       unop::Closure : op,
 				       recurse_(f, false));
 	      return;
 	      /* !Finish(x), is not simplified */
@@ -1273,6 +1275,7 @@ namespace spot
 	      break;
 	    case unop::Closure:
 	    case unop::NegClosure:
+	    case unop::NegClosureMarked:
 	      // {e} = 1 if e accepts [*0]
 	      // !{e} = 0 if e accepts [*0]
 	      if (result_->accepts_eword())
@@ -1332,7 +1335,7 @@ namespace spot
 			multop::instance(multop::Concat, v);
 		      tail = unop::instance(op, tail);
 
-		      bool doneg = op == unop::NegClosure;
+		      bool doneg = op != unop::Closure;
 		      for (unsigned n = start; n > 0;)
 			{
 			  --n;
@@ -1398,7 +1401,7 @@ namespace spot
 			    tail = // {b[*0..j-i]} or !{b[*0..j-i]}
 			      unop::instance(op, tail);
 			    tail =
-			      dup_b_x_tail(op == unop::NegClosure,
+			      dup_b_x_tail(op != unop::Closure,
 					   c, tail, min);
 			    mo->destroy();
 			    result_ = recurse_destroy(tail);
@@ -1417,14 +1420,14 @@ namespace spot
 			unsigned min = s->min();
 			assert(min > 0);
 			const formula* tail;
-			if (op == unop::NegClosure)
+			if (op == unop::Closure)
-			  tail =
-			    dup_b_x_tail(true,
-					 c, constant::false_instance(), min);
-			else
 			  tail =
 			    dup_b_x_tail(false,
 					 c, constant::true_instance(), min);
+			else
+			  tail =
+			    dup_b_x_tail(true,
+					 c, constant::false_instance(), min);
 			result_->destroy();
 			result_ = recurse_destroy(tail);
 			return;

src/ltlvisit/tostring.cc

@@ -539,6 +539,12 @@ namespace spot
 	      in_ratexp_ = true;
 	      top_level_ = true;
 	      break;
+	    case unop::NegClosureMarked:
+	      emit(KNot);
+	      os_ << (kw_ == utf8_kw ? "̃{": "+{");
+	      in_ratexp_ = true;
+	      top_level_ = true;
+	      break;
 	    }
 
 	  if (need_parent || full_parent_)

src/ltlvisit/tunabbrev.cc

@@ -46,6 +46,7 @@ namespace spot
 	case unop::Not:
 	case unop::Closure:
 	case unop::NegClosure:
+	case unop::NegClosureMarked:
 	  this->super::visit(uo);
 	  return;
 	case unop::F:

src/tgba/formula2bdd.cc

@@ -88,6 +88,7 @@ namespace spot
 	  case unop::X:
 	  case unop::Closure:
 	  case unop::NegClosure:
+	  case unop::NegClosureMarked:
 	    assert(!"unsupported operator");
 	  case unop::Not:
 	    {

src/tgbaalgos/eltl2tgba_lacim.cc

@@ -103,6 +103,7 @@ namespace spot
           case unop::G:
 	  case unop::Closure:
 	  case unop::NegClosure:
+	  case unop::NegClosureMarked:
 	    assert(!"unsupported operator");
 	  }
 	/* Unreachable code.  */

src/tgbaalgos/ltl2taa.cc

@@ -143,6 +143,7 @@ namespace spot
 	  case unop::Finish:
 	  case unop::Closure:
 	  case unop::NegClosure:
+	  case unop::NegClosureMarked:
 	    assert(!"unsupported operator");
 	    return;
 	}

src/tgbaalgos/ltl2tgba_fm.cc

@@ -508,6 +508,7 @@ namespace spot
 	  case unop::Finish:
 	  case unop::Closure:
 	  case unop::NegClosure:
+	  case unop::NegClosureMarked:
 	    assert(!"not a rational operator");
 	    return;
 	  case unop::Not:
@@ -1178,7 +1179,7 @@ namespace spot
 	    }
 	  case unop::Closure:
 	    {
-	      rat_seen_ = true;
+	      // rat_seen_ = true;
 	      const formula* f = node->child();
 	      if (f->accepts_eword())
 		{
@@ -1217,18 +1218,23 @@ namespace spot
 	    }
 	    break;
 
+	  case unop::NegClosureMarked:
+	    has_marked_ = true;
 	  case unop::NegClosure:
+	    rat_seen_ = true;
 	    {
-	      rat_seen_ = true;
+	      const formula* c = node->child();
-	      has_marked_ = true;
+	      if (c->accepts_eword())
-
-	      if (node->child()->accepts_eword())
 		{
 		  res_ = bddfalse;
 		  return;
 		}
-
+	      if (mark_all_)
-	      bdd f1 = translate_ratexp(node->child(), dict_);
+		{
+		  op = unop::NegClosureMarked;
+		  has_marked_ = true;
+		}
+	      bdd f1 = translate_ratexp(c, dict_);
 
 	      // trace_ltl_bdd(dict_, f1);
 

src/tgbaalgos/ltl2tgba_lacim.cc

@@ -153,6 +153,7 @@ namespace spot
 	  case unop::Finish:
 	  case unop::Closure:
 	  case unop::NegClosure:
+	  case unop::NegClosureMarked:
 	    assert(!"unsupported operator");
 	  }
 	/* Unreachable code.  */

src/tgbatest/ltl2tgba.test

@@ -1,8 +1,9 @@
 #!/bin/sh
-# Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et Développement
+# -*- coding: utf-8 -*-
-# de l'Epita (LRDE).
+# 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.
@@ -108,6 +109,16 @@ check_psl '{((a&!b);((!a&!b)*))&&(!b*;(!a&b))}'
 # other side.
 check_psl '{c;a;(f&!f)[=2];c}|{b;a;(!f&f)[=2];c}'
 
+
+# these were mis-translated in Spot 0.9
+check_psl 'G!{(b;1)*;a}'
+check_psl '(G!{(b;1)*;a} && ({1;1[*3]*}[]->{(b&!a)[*2];!b&!a}))'
+# In particular, Spot 0.9 would incorrectly reject the sequence:
+# (a̅b;a̅b;a̅b̅);(a̅b;a̅b;a̅b̅);(a̅b;a̅b;a̅b̅);... in 'G!{(b;1)*;a}'
+# This means the following automaton was incorrectly empty in Spot 0.9.
+run 0 ../ltl2tgba -e -R3 '(G!{(b;1)*;a} && ({1;1[*3]*}[]->{(b&!a)[*2];!b&!a}))'
+
+
 # Make sure 'a U (b U c)' has 3 states and 6 transitions,
 # before and after degeneralization.
 for opt in '' -D -DS; do