From 210723e30c37d71081508b3fe99c6a17fc62474a Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Sat, 14 Apr 2012 23:18:37 +0200
Subject: [PATCH] Implement [->i..j] and [=i..j] as sugar with [*i..j].

* src/ltlast/bunop.hh, src/ltlast/bunop.cc (sugar_goto, sugar_equal):
New functions..
* src/ltlparse/ltlparse.yy: Use them.
---
 src/ltlast/bunop.cc      | 38 ++++++++++++++++++++++++++++++++++++--
 src/ltlast/bunop.hh      | 23 +++++++++++++++++++++++
 src/ltlparse/ltlparse.yy |  8 ++++----
 3 files changed, 63 insertions(+), 6 deletions(-)

diff --git a/src/ltlast/bunop.cc b/src/ltlast/bunop.cc
index a99d86d63..b50bab04e 100644
--- a/src/ltlast/bunop.cc
+++ b/src/ltlast/bunop.cc
@@ -1,5 +1,5 @@
-// Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et Développement
-// de l'Epita (LRDE).
+// Copyright (C) 2009, 2010, 2011, 2012 Laboratoire de Recherche et
+// Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -25,6 +25,7 @@
 #include <sstream>
 #include "constant.hh"
 #include "unop.hh"
+#include "multop.hh"
 
 namespace spot
 {
@@ -389,6 +390,39 @@ namespace spot
       return static_cast<bunop*>(ap->clone());
     }
 
+    formula*
+    bunop::sugar_goto(formula* b, unsigned min, unsigned max)
+    {
+      assert(b->is_boolean());
+      // b[->min..max] is implemented as ((!b)[*];b)[*min..max]
+      formula* s = bunop::instance(bunop::Star,
+				   unop::instance(unop::Not, b->clone()));
+      return bunop::instance(bunop::Star,
+			     multop::instance(multop::Concat, s, b),
+			     min, max);
+    }
+
+    formula*
+    bunop::sugar_equal(formula* b, unsigned min, unsigned max)
+    {
+      assert(b->is_boolean());
+      // b[=0..] = 1[*]
+      if (min == 0 && max == unbounded)
+	{
+	  b->destroy();
+	  return instance(Star, constant::true_instance());
+	}
+
+      // b[=min..max] is implemented as ((!b)[*];b)[*min..max];(!b)[*]
+      formula* s = bunop::instance(bunop::Star,
+				   unop::instance(unop::Not, b->clone()));
+      formula* t = bunop::instance(bunop::Star,
+				   multop::instance(multop::Concat,
+						    s->clone(), b),
+				   min, max);
+      return multop::instance(multop::Concat, t, s);
+    }
+
     unsigned
     bunop::instance_count()
     {
diff --git a/src/ltlast/bunop.hh b/src/ltlast/bunop.hh
index 6a85ef1a9..3069ecd94 100644
--- a/src/ltlast/bunop.hh
+++ b/src/ltlast/bunop.hh
@@ -71,6 +71,29 @@ namespace spot
 			       unsigned min = 0,
 			       unsigned max = unbounded);
 
+      /// \brief Implement <code>b[->i..j]</code> using the Kleen star.
+      ///
+      /// <code>b[->i..j]</code> is implemented as
+      /// <code>((!b)[*];b)[*i..j]</code>.
+      ///
+      /// Note that \a min defaults to 1, not 0, because [->] means
+      /// [->1..].
+      ///
+      /// \pre \a child must be a Boolean formula.
+      static formula* sugar_goto(formula* child,
+				 unsigned min = 1,
+				 unsigned max = unbounded);
+
+      /// \brief Implement b[=i..j] using the Kleen star.
+      ///
+      /// <code>b[=i..j]</code> is implemented as
+      /// <code>((!b)[*];b)[*i..j];(!b)[*]</code>.
+      ///
+      /// \pre \a child must be a Boolean formula.
+      static formula* sugar_equal(formula* child,
+				  unsigned min = 0,
+				  unsigned max = unbounded);
+
       virtual void accept(visitor& v);
       virtual void accept(const_visitor& v) const;
 
diff --git a/src/ltlparse/ltlparse.yy b/src/ltlparse/ltlparse.yy
index 9119cfa3e..4bd6aa64a 100644
--- a/src/ltlparse/ltlparse.yy
+++ b/src/ltlparse/ltlparse.yy
@@ -1,5 +1,5 @@
-/* Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et Développement
-** de l'Epita (LRDE).
+/* Copyright (C) 2009, 2010, 2011, 2012 Laboratoire de Recherche et
+** Développement de l'Epita (LRDE).
 ** Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de
 ** Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
 ** Université Pierre et Marie Curie.
@@ -403,7 +403,7 @@ sere: booleanatom
 		  }
 		if ($1->is_boolean())
 		  {
-		    $$ = bunop::instance(bunop::Equal, $1, $2.min, $2.max);
+		    $$ = bunop::sugar_equal($1, $2.min, $2.max);
 		  }
 		else
 		  {
@@ -425,7 +425,7 @@ sere: booleanatom
 		  }
 		if ($1->is_boolean())
 		  {
-		    $$ = bunop::instance(bunop::Goto, $1, $2.min, $2.max);
+		    $$ = bunop::sugar_goto($1, $2.min, $2.max);
 		  }
 		else
 		  {