Implement star-normal-form rewriting.

* src/ltlvisit/snf.cc, src/ltlvisit/snf.hh: New files.
* src/ltlvisit/Makefile.am: Distribute them.
* src/ltlvisit/simplify.cc, src/ltlvisit/simplify.hh: Call snf(f) for
all f[*].
* src/ltltest/reduccmp.test: Test it.
* doc/tl/tl.tex, doc/tl/tl.bib: Document it.

doc/tl/tl.bib

@@ -28,6 +28,15 @@
   month		= jul
 }
 
+@Article{	  bruggeman.96.tcs,
+  author	= {Anne Br{\"u}ggemann-Klein},
+  title		= {Regular Expressions into Finite Automata},
+  journal	= {Theoretical Computer Science},
+  year		= {1996},
+  volume	= {120},
+  pages		= {87--98}
+}
+
 @InProceedings{	  cerna.03.mfcs,
   author	= {Ivana {\v{C}}ern{\'a} and Radek Pel{\'a}nek},
   title		= {Relating Hierarchy of Temporal Properties to Model

doc/tl/tl.tex

@@ -1407,6 +1407,30 @@ SERE.
   \sere{r_1\FUSION b_1}\AND   \sere{r_2\FUSION b_2} &\equiv \sere{r_1\ANDALT r_2}\FUSION\sere{b_1\AND    b_2} \\
 \end{align*}
 
+Stared 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}} \]
+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_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$}
+operators, and it guarantees that $\forall r,\,\varepsilon\not\VDash
+r^\circ$ because $r^\circ$ is stripping all the stars and empty words
+that occur in $r$.  For instance $\sere{a\STAR{}\CONCAT
+  b\STAR{}\CONCAT\sere{\1\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
+unfortunately not when the \samp{$\ANDALT$} operator is used.
+
 \subsection{Simplifications for Eventual and Universal Formul\ae}
 \label{sec:eventunivrew}
 

src/ltltest/reduccmp.test

@@ -291,6 +291,11 @@ for x in ../reduccmp ../reductaustr; do
      run 0 $x '{{a;b*;c}&{d;e*}&{f*;g}&{h*}} <>-> x' \
               '{{f*;g}&{h*}&{{a&&d};{e* & {b*;c}}}} <>-> x'
      run 0 $x '{a&b&c*}|->!Xb' '{(a&&b)|((a&&b):c*)}|-> X!b'
+     run 0 $x '{a;(b*;c*;([*0]+{d;e}))*}!' '{a;{b|c|{d;e}}*}!'
+     # not reduced
+     run 0 $x '{a;(b[*2..4];c*;([*0]+{d;e}))*}!' \
+              '{a;(b[*2..4];c*;([*0]+{d;e}))*}!'
+     run 0 $x '{((a*;b)+[*0])[*4..6]}!' '{((a*;b))[*0..6]}!'
      ;;
   esac
 

src/ltlvisit/Makefile.am

-## Copyright (C) 2010, 2011 Laboratoire de Recherche et Developpement de
-## l'Epita (LRDE).
+## -*- coding: utf-8 -*-
+## Copyright (C) 2010, 2011, 2012 Laboratoire de Recherche et
+## Developpement de l'Epita (LRDE).
 ## Copyright (C) 2004, 2005, 2006  Laboratoire d'Informatique de Paris 6 (LIP6),
-## dpartement Systmes Rpartis Coopratifs (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.
@@ -42,6 +43,7 @@ ltlvisit_HEADERS = \
   reduce.hh \
   simpfg.hh \
   simplify.hh \
+  snf.hh \
   tostring.hh \
   tunabbrev.hh
 
@@ -62,5 +64,6 @@ libltlvisit_la_SOURCES = \
   reduce.cc \
   simpfg.cc \
   simplify.cc \
+  snf.cc \
   tostring.cc \
   tunabbrev.cc

src/ltlvisit/simplify.cc

@@ -32,6 +32,7 @@
 #include "ltlast/visitor.hh"
 #include "ltlvisit/contain.hh"
 #include "ltlvisit/tostring.hh"
+#include "ltlvisit/snf.hh"
 #include <cassert>
 
 namespace spot
@@ -95,6 +96,16 @@ namespace spot
 	      old->first.second->destroy();
 	    }
 	}
+	{
+	  snf_cache::iterator i = snf_cache_.begin();
+	  snf_cache::iterator end = snf_cache_.end();
+	  while (i != end)
+	    {
+	      snf_cache::iterator old = i++;
+	      old->second->destroy();
+	      old->first->destroy();
+	    }
+	}
 
 	dict->unregister_all_my_variables(this);
       }
@@ -184,8 +195,8 @@ namespace spot
 		    break;
 		  }
 		case multop::AndNLM:
-	        case multop::AndRat:
-	        case multop::OrRat:
+		case multop::AndRat:
+		case multop::OrRat:
 		case multop::Concat:
 		case multop::Fusion:
 		  assert(!"Unsupported operator");
@@ -327,11 +338,18 @@ namespace spot
 	simplified_[orig->clone()] = simplified->clone();
       }
 
+      const formula*
+      star_normal_form(const formula* f)
+      {
+	return ltl::star_normal_form(f, &snf_cache_);
+      }
+
     private:
       f2b_map as_bdd_;
       f2f_map simplified_;
       f2f_map nenoform_;
       syntimpl_cache_t syntimpl_;
+      snf_cache snf_cache_;
     };
 
 
@@ -437,11 +455,10 @@ namespace spot
 	void
 	visit(bunop* bo)
 	{
-	  // !(a*) is not simplified, whatever that means
+	  // !(a*) should never occur.
+	  assert(!negated_);
 	  result_ = bunop::instance(bo->op(), recurse_(bo->child(), false),
 				    bo->min(), bo->max());
-	  if (negated_)
-	    result_ = unop::instance(unop::Not, result_);
 	}
 
 	formula* equiv_or_xor(bool equiv, formula* f1, formula* f2)
@@ -1002,8 +1019,23 @@ namespace spot
 	void
 	visit(bunop* bo)
 	{
-	  result_ = bunop::instance(bo->op(), recurse(bo->child()),
-				    bo->min(), bo->max());
+	  bunop::type op = bo->op();
+	  unsigned min = bo->min();
+	  formula* h = recurse(bo->child());
+	  switch (op)
+	    {
+	    case bunop::Star:
+	      if (h->accepts_eword())
+		min = 0;
+	      if (min == 0)
+		{
+		  const formula* s = c_->star_normal_form(h);
+		  h->destroy();
+		  h = const_cast<formula*>(s);
+		}
+	      result_ = bunop::instance(op, h, min, bo->max());
+	      break;
+	    }
 	}
 
 	void
@@ -3724,6 +3756,12 @@ namespace spot
       return cache_->as_bdd(f);
     }
 
+    const formula*
+    ltl_simplifier::star_normal_form(const formula* f)
+    {
+      return cache_->star_normal_form(f);
+    }
+
     bdd_dict*
     ltl_simplifier::get_dict() const
     {

src/ltlvisit/simplify.hh

@@ -132,6 +132,9 @@ namespace spot
       /// Return the bdd_dict used.
       bdd_dict* get_dict() const;
 
+      /// Cached version of spot::ltl::star_normal_form().
+      const formula* star_normal_form(const formula* f);
+
     private:
       ltl_simplifier_cache* cache_;
       // Copy disallowed.

src/ltlvisit/snf.cc

+// -*- coding: utf-8 -*-
+// Copyright (C) 2012 Laboratoire de Recherche et Developpement
+// de l'Epita (LRDE).
+//
+// This file is part of Spot, a model checking library.
+//
+// Spot is free software; you can redistribute it and/or modify it
+// under the terms of the GNU General Public License as published by
+// the Free Software Foundation; either version 3 of the License, or
+// (at your option) any later version.
+//
+// Spot is distributed in the hope that it will be useful, but WITHOUT
+// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+// License for more details.
+//
+// You should have received a copy of the GNU General Public License
+// along with Spot; see the file COPYING.  If not, write to the Free
+// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+// 02111-1307, USA.
+
+#include "snf.hh"
+#include "ltlast/allnodes.hh"
+#include "ltlast/visitor.hh"
+#include "ltlvisit/tostring.hh"
+
+namespace spot
+{
+  namespace ltl
+  {
+    namespace
+    {
+      // E°
+      class snf_visitor: public visitor
+      {
+	formula* result_;
+	snf_cache* cache_;
+      public:
+
+	snf_visitor(snf_cache* c): cache_(c)
+	{
+	}
+
+	formula*
+	result() const
+	{
+	  return result_;
+	}
+
+	void
+	visit(atomic_prop*)
+	{
+	  assert(!"unexpected operator");
+	}
+
+	void
+	visit(constant* c)
+	{
+	  assert(c == constant::empty_word_instance());
+	  result_ = constant::false_instance();
+	}
+
+	void
+	visit(bunop* bo)
+	{
+	  bunop::type op = bo->op();
+	  switch (op)
+	    {
+	    case bunop::Star:
+	      assert(bo->accepts_eword());
+	      // Strip the star.
+	      result_ = recurse(bo->child());
+	      break;
+	    }
+	}
+
+	void
+	visit(unop*)
+	{
+	  assert(!"unexpected operator");
+	}
+
+	void
+	visit(binop*)
+	{
+	  assert(!"unexpected operator");
+	}
+
+	void
+	visit(automatop*)
+	{
+	  assert(!"unexpected operator");
+	}
+
+	void
+	visit(multop* mo)
+	{
+	  multop::type op = mo->op();
+	  switch (op)
+	    {
+	    case multop::And:
+	    case multop::Or:
+	    case multop::Fusion:
+	      assert(!"unexpected operator");
+	      break;
+	    case multop::Concat:
+	    case multop::AndNLM:
+	      // Let F designate expressions that accept [*0],
+	      // and G designate expressions that do not.
+
+	      // (G₁;G₂;G₃)° = G₁;G₂;G₃
+	      // (G₁;F₂;G₃)° = (G₁°);F₂;(G₃°) = G₁;F₂;G₃
+	      // because there is nothing to do recursively on a G.
+	      //
+	      // AndNLM can be dealt with similarly.
+	      //
+	      // This case is already handled in recurse().
+	      // if we reach this switch, we only have to
+	      // deal with...
+	      //
+	      // (F₁;F₂;F₃)° = (F₁°)|(F₂°)|(F₃°)
+	      // (F₁&F₂&F₃)° = (F₁°)|(F₂°)|(F₃°)
+	      // so we fall through to the OrRat case...
+	    case multop::OrRat:
+	      assert(mo->accepts_eword());
+	      {
+		unsigned s = mo->size();
+		multop::vec* v = new multop::vec;
+		v->reserve(s);
+		for (unsigned pos = 0; pos < s; ++pos)
+		  v->push_back(recurse(mo->nth(pos)));
+		result_ = multop::instance(multop::OrRat, v);
+	      }
+	      break;
+	    case multop::AndRat:
+	      // FIXME: Can we deal with AndRat in a better way
+	      // when it accepts [*0].
+	      result_ = mo->clone();
+	      break;
+	    }
+	}
+
+	formula*
+	recurse(formula* f)
+	{
+	  if (!f->accepts_eword())
+	    return f->clone();
+
+	  if (cache_)
+	    {
+	      snf_cache::const_iterator i = cache_->find(f);
+	      if (i != cache_->end())
+		return i->second->clone();
+	    }
+
+	  f->accept(*this);
+
+	  if (cache_)
+	    (*cache_)[f->clone()] = result_->clone();
+	  return result_;
+	}
+      };
+
+    }
+
+
+    formula*
+    star_normal_form(const formula* sere, snf_cache* cache)
+    {
+      snf_visitor v(cache);
+      return v.recurse(const_cast<formula*>(sere));
+    }
+
+  }
+}

src/ltlvisit/snf.hh

+// -*- coding: utf-8 -*-
+// Copyright (C) 2012 Laboratoire de Recherche et Developpement
+// de l'Epita (LRDE).
+//
+// This file is part of Spot, a model checking library.
+//
+// Spot is free software; you can redistribute it and/or modify it
+// under the terms of the GNU General Public License as published by
+// the Free Software Foundation; either version 3 of the License, or
+// (at your option) any later version.
+//
+// Spot is distributed in the hope that it will be useful, but WITHOUT
+// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+// License for more details.
+//
+// You should have received a copy of the GNU General Public License
+// along with Spot; see the file COPYING.  If not, write to the Free
+// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+// 02111-1307, USA.
+
+#ifndef SPOT_LTLVISIT_SNF_HH
+#define SPOT_LTLVISIT_SNF_HH
+
+#include "ltlast/formula.hh"
+#include "misc/hash.hh"
+
+namespace spot
+{
+  namespace ltl
+  {
+
+    typedef Sgi::hash_map<const formula*, const formula*,
+			  ptr_hash<formula> > snf_cache;
+
+    /// Helper to rewrite a sere in Star Normal Form.
+    ///
+    /// This should only be called on children of a Star operator.  It
+    /// corresponds to the E° operation defined in the following
+    /// paper.
+    ///
+    /// \verbatim
+    /// @Article{	  bruggeman.96.tcs,
+    ///   author	= {Anne Br{\"u}ggemann-Klein},
+    ///   title		= {Regular Expressions into Finite Automata},
+    ///   journal	= {Theoretical Computer Science},
+    ///   year		= {1996},
+    ///   volume	= {120},
+    ///   pages		= {87--98}
+    /// }
+    /// \endverbatim
+    ///
+    /// \param sere the SERE to rewrite
+    /// \param cache an optional cache
+    formula* star_normal_form(const formula* sere,
+			      snf_cache* cache = 0);
+  }
+}
+
+#endif // SPOT_LTLVISIT_SNF_HH