From fdd73d51238ac506ff6d1ba92928fb19b31a4506 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Thu, 17 Feb 2011 18:47:21 +0100
Subject: [PATCH] Add support for the {SERE}! PSL operator.

* src/ltlparse/ltlscan.ll: Recognize }!.  Also remove
five duplicate rules.
* src/ltlparse/ltlparse.yy: Build {r}<>->1 when parsing {r}!.
* src/ltlvisit/tostring.cc: Print {r}! instead of {r}<>->1.
* src/ltltest/tostring.test, src/ltltest/equals.test:
Add more tests.
---
 src/ltlparse/ltlparse.yy  |  5 +++++
 src/ltlparse/ltlscan.ll   |  6 +-----
 src/ltltest/equals.test   |  5 +++++
 src/ltltest/tostring.test |  5 ++++-
 src/ltlvisit/tostring.cc  | 13 ++++++++++++-
 5 files changed, 27 insertions(+), 7 deletions(-)

diff --git a/src/ltlparse/ltlparse.yy b/src/ltlparse/ltlparse.yy
index 9cb47b334..15000e7eb 100644
--- a/src/ltlparse/ltlparse.yy
+++ b/src/ltlparse/ltlparse.yy
@@ -83,6 +83,7 @@ using namespace spot::ltl;
 %token START_RATEXP "RATEXP start marker"
 %token PAR_OPEN "opening parenthesis" PAR_CLOSE "closing parenthesis"
 %token BRACE_OPEN "opening brace" BRACE_CLOSE "closing brace"
+%token BRACE_BANG_CLOSE "closing brace-bang"
 %token OP_OR "or operator" OP_XOR "xor operator"
 %token OP_AND "and operator" OP_SHORT_AND "short and operator"
 %token OP_IMPLIES "implication operator" OP_EQUIV "equivalent operator"
@@ -627,6 +628,10 @@ subformula: booleanatom
 	      { missing_right_binop($$, $1, @2,
 				"existential non-overlapping concat operator");
 	      }
+            | BRACE_OPEN rationalexp BRACE_BANG_CLOSE
+	      /* {SERE}! = {SERE} <>-> 1 */
+	      { $$ = binop::instance(binop::EConcat, $2,
+				     constant::true_instance()); }
 ;
 
 %%
diff --git a/src/ltlparse/ltlscan.ll b/src/ltlparse/ltlscan.ll
index 0c006262c..063021cfc 100644
--- a/src/ltlparse/ltlscan.ll
+++ b/src/ltlparse/ltlscan.ll
@@ -76,6 +76,7 @@ flex_set_buffer(const char* buf, int start_tok)
 "("				BEGIN(0); return token::PAR_OPEN;
 ")"				BEGIN(not_prop); return token::PAR_CLOSE;
 "{"                             BEGIN(0); return token::BRACE_OPEN;
+"}"[ \t\n]*"!"			BEGIN(not_prop); return token::BRACE_BANG_CLOSE;
 "}"				BEGIN(not_prop); return token::BRACE_CLOSE;
 
   /* Must go before the other operators, because the F of FALSE
@@ -135,11 +136,6 @@ flex_set_buffer(const char* buf, int start_tok)
 "^"|"xor"			BEGIN(0); return token::OP_XOR;
 "=>"|"->"|"-->"			BEGIN(0); return token::OP_IMPLIES;
 "<=>"|"<->"|"<-->"		BEGIN(0); return token::OP_EQUIV;
-"*"|"[*]"			BEGIN(0); return token::OP_STAR;
-";"				BEGIN(0); return token::OP_CONCAT;
-":"				BEGIN(0); return token::OP_FUSION;
-"[]->"				BEGIN(0); return token::OP_UCONCAT;
-"<>->"				BEGIN(0); return token::OP_ECONCAT;
 
   /* <>, [], and () are used in Spin.  */
 "F"|"<>"			BEGIN(0); return token::OP_F;
diff --git a/src/ltltest/equals.test b/src/ltltest/equals.test
index 006df3f4b..25a740257 100755
--- a/src/ltltest/equals.test
+++ b/src/ltltest/equals.test
@@ -50,6 +50,7 @@ run 0 ../equals 'a & a & true' 'a'
 run 0 ../equals 'a & false & a' 'false'
 run 0 ../equals 'a | false | a' 'a'
 run 0 ../equals 'true | a | a' 'true'
+run 0 ../equals '{a*}!' '{a*}<>->1'
 
 # other formulae which are not
 run 1 ../equals 'a' 'b'
@@ -62,6 +63,10 @@ run 1 ../equals 'a & b & c' 'c & a'
 run 1 ../equals 'b & c' 'c & a & b'
 run 1 ../equals 'a & b & (c |(f U g)| e)' \
                 'b & a & a & (c | e |(g U g)| e | c) & b'
+run 1 ../equals '{a*}' '{a*}<>->1'
+run 1 ../equals '!{a*}' '{a*}<>->1'
+run 1 ../equals '{a*}' '{a*}!'
+run 1 ../equals '!{a*}' '{a*}!'
 
 # Precedence
 run 0 ../equals 'a & b ^ c | d' 'd | c ^ b & a'
diff --git a/src/ltltest/tostring.test b/src/ltltest/tostring.test
index fa3e1c252..2fd5ba8e4 100755
--- a/src/ltltest/tostring.test
+++ b/src/ltltest/tostring.test
@@ -1,5 +1,5 @@
 #! /bin/sh
-# Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement
+# Copyright (C) 2009, 2010, 2011 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
@@ -69,3 +69,6 @@ run 0 ../tostring '{a[*1..]}'
 run 0 ../tostring '{a[+]}'
 run 0 ../tostring '{[+]}'
 run 0 ../tostring '{a[*2..3][*4..5]}'
+
+run 0 ../tostring '{a**}<>->1' > out
+test "`sed 1q < out `" = '{a[*]}!'
diff --git a/src/ltlvisit/tostring.cc b/src/ltlvisit/tostring.cc
index 91a04e15a..d0d1e8bdb 100644
--- a/src/ltlvisit/tostring.cc
+++ b/src/ltlvisit/tostring.cc
@@ -165,6 +165,12 @@ namespace spot
 	      top_level_ = top_level;
 	      break;
 	    case binop::EConcat:
+	      if (bo->second() == constant::true_instance())
+		{
+		  os_ << "}!";
+		  in_ratexp_ = false;
+		  goto second_done;
+		}
 	      os_ << "} <>-> ";
 	      in_ratexp_ = false;
 	      top_level_ = false;
@@ -177,6 +183,7 @@ namespace spot
 	    }
 
 	  bo->second()->accept(*this);
+	second_done:
 	  if (!top_level)
 	    closep();
 	}
@@ -255,7 +262,6 @@ namespace spot
 	      break;
 	    }
 
-	  top_level_ = false;
 	  if (need_parent || full_parent_)
 	    openp();
 	  uo->child()->accept(*this);
@@ -416,6 +422,11 @@ namespace spot
 	      top_level_ = true;
 	      os_ << "{";
 	      bo->first()->accept(*this);
+	      if (bo->second() == constant::true_instance())
+		{
+		  os_ << "}!";
+		  break;
+		}
 	      os_ << "} <>-> ";
 	      top_level_ = false;
 	      bo->second()->accept(*this);