From 1ecc6984d31b0348586fcb37a61493606ec859c1 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Tue, 9 Mar 2010 16:26:27 +0100
Subject: [PATCH] Accept "{E}|->ltl" and "{E}(ltl)" as synonym for
 "{E}[]->ltl".

* src/ltlparse/ltlparse.yy (parenthesedsubformula): Extract these
rules from...
(subformula): ... here, and use it to recognize "{SERE}(formula)".
* src/ltlparse/ltlscan.ll: Recognize "|->" as "[]->".
* src/ltltest/equals.test: Test these two new syntaxes.
---
 src/ltlparse/ltlparse.yy | 15 ++++++++++-----
 src/ltlparse/ltlscan.ll  |  6 ++++++
 src/ltltest/equals.test  |  2 ++
 3 files changed, 18 insertions(+), 5 deletions(-)

diff --git a/src/ltlparse/ltlparse.yy b/src/ltlparse/ltlparse.yy
index 194457f35..27fd40305 100644
--- a/src/ltlparse/ltlparse.yy
+++ b/src/ltlparse/ltlparse.yy
@@ -118,7 +118,8 @@ using namespace spot::ltl;
 
 %nonassoc OP_POST_NEG OP_POST_POS
 
-%type <ltl> subformula booleanatom rationalexp bracedrationalexp
+%type <ltl> subformula booleanatom rationalexp
+%type <ltl> bracedrationalexp parenthesedsubformula
 
 %destructor { delete $$; } <str>
 %destructor { $$->destroy(); } <ltl>
@@ -232,10 +233,9 @@ booleanatom: ATOMIC_PROP
 	      { $$ = constant::false_instance(); }
 
 rationalexp: booleanatom
+            | bracedrationalexp
 	    | CONST_EMPTYWORD
 	      { $$ = constant::empty_word_instance(); }
-            | bracedrationalexp
-	      { $$ = $1; }
 	    | PAR_OPEN rationalexp PAR_CLOSE
 	      { $$ = $2; }
 	    | PAR_OPEN error PAR_CLOSE
@@ -292,8 +292,7 @@ bracedrationalexp: BRACE_OPEN rationalexp BRACE_CLOSE
 		$$ = constant::false_instance();
 	      }
 
-subformula: booleanatom
-	    | PAR_OPEN subformula PAR_CLOSE
+parenthesedsubformula: PAR_OPEN subformula PAR_CLOSE
 	      { $$ = $2; }
 	    | PAR_OPEN error PAR_CLOSE
 	      { error_list.push_back(parse_error(@$,
@@ -311,6 +310,10 @@ subformula: booleanatom
 		    "treating this parenthetical block as false"));
 		$$ = constant::false_instance();
 	      }
+
+
+subformula: booleanatom
+            | parenthesedsubformula
 	    | subformula OP_AND subformula
 	      { $$ = multop::instance(multop::And, $1, $3); }
 	    | subformula OP_AND error
@@ -367,6 +370,8 @@ subformula: booleanatom
 	      { $$ = unop::instance(unop::Closure, $1); }
             | bracedrationalexp OP_UCONCAT subformula
 	      { $$ = binop::instance(binop::UConcat, $1, $3); }
+            | bracedrationalexp parenthesedsubformula
+	      { $$ = binop::instance(binop::UConcat, $1, $2); }
             | bracedrationalexp OP_UCONCAT error
 	      { missing_right_binop($$, $1, @2, "universal concat operator"); }
             | bracedrationalexp OP_ECONCAT subformula
diff --git a/src/ltlparse/ltlscan.ll b/src/ltlparse/ltlscan.ll
index 0e90862bc..36049f001 100644
--- a/src/ltlparse/ltlscan.ll
+++ b/src/ltlparse/ltlscan.ll
@@ -85,7 +85,13 @@ flex_set_buffer(const char* buf, int start_tok)
   /* ~ comes from Goal, ! from everybody else */
 "!"|"~"				BEGIN(0); return token::OP_NOT;
 
+  /* PSL operators */
 "[*0]"				BEGIN(0); return token::CONST_EMPTYWORD;
+"[]->"|"|->"			BEGIN(0); return token::OP_UCONCAT;
+"<>->"				BEGIN(0); return token::OP_ECONCAT;
+"*"|"[*]"			BEGIN(0); return token::OP_STAR;
+";"				BEGIN(0); return token::OP_CONCAT;
+":"				BEGIN(0); return token::OP_FUSION;
 
   /* & and | come from Spin.  && and || from LTL2BA.
      /\, \/, and xor are from LBTT.
diff --git a/src/ltltest/equals.test b/src/ltltest/equals.test
index 53d6dcd31..ce4f68811 100755
--- a/src/ltltest/equals.test
+++ b/src/ltltest/equals.test
@@ -120,3 +120,5 @@ run 0 ../equals '{x;x}<>->FF(0)' '0'
 run 0 ../equals '{x;x}<>->GX(1)' '{x;x}<>->1'
 run 0 ../equals '{x;x}[]->GX(1)' '1'
 run 0 ../equals '{x;x}[]->FF(0)' '{x;x}[]->0'
+run 0 ../equals '{x;x}[]->y' '{x;x}|->y'
+run 0 ../equals '{x;x}[]->y' '{x;x}(y)'