From 754ff36b01e480e40f19e2c6d9daddb122d8f2da Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Fri, 15 Oct 2010 16:38:30 +0200
Subject: [PATCH] Accept more syntaxes as range specifications for [*], [=],
 and [->].

* src/ltlparse/ltlscan.ll (OP_SQBKT_SEP): Accept ":" and "to"
in addition to ".." and ",".
(OP_UNBOUNDED): Recognize "$" for the rule below.
* src/ltlparse/ltlparse.yy: Accept [OP1:$] as a synonym
for [OP1:], for people used to SVA's syntax.
* src/ltltest/equals.test: Test these syntaxes.
---
 src/ltlparse/ltlparse.yy | 10 ++++++----
 src/ltlparse/ltlscan.ll  |  9 ++++++++-
 src/ltltest/equals.test  | 16 ++++++++--------
 3 files changed, 22 insertions(+), 13 deletions(-)

diff --git a/src/ltlparse/ltlparse.yy b/src/ltlparse/ltlparse.yy
index a1bd5e6de..45b169f28 100644
--- a/src/ltlparse/ltlparse.yy
+++ b/src/ltlparse/ltlparse.yy
@@ -97,6 +97,7 @@ using namespace spot::ltl;
 %token OP_GOTO_OPEN "opening bracket for goto operator"
 %token OP_SQBKT_CLOSE "closing bracket"
 %token <num> OP_SQBKT_NUM "number for square bracket operator"
+%token OP_UNBOUNDED "unbounded mark"
 %token OP_SQBKT_SEP "separator for square bracket operator"
 %token OP_UCONCAT "universal concat operator"
 %token OP_ECONCAT "existential concat operator"
@@ -190,13 +191,14 @@ enderror: error END_OF_INPUT
 	      }
 
 
-OP_SQBKT_SEP_opt: | OP_SQBKT_SEP
+OP_SQBKT_SEP_unbounded: OP_SQBKT_SEP | OP_SQBKT_SEP OP_UNBOUNDED
+OP_SQBKT_SEP_opt: | OP_SQBKT_SEP_unbounded
 error_opt: | error
 
 /* for [*i..j] and [=i..j] */
 sqbracketargs: OP_SQBKT_NUM OP_SQBKT_SEP OP_SQBKT_NUM OP_SQBKT_CLOSE
               { $$.min = $1; $$.max = $3; }
-	     | OP_SQBKT_NUM OP_SQBKT_SEP OP_SQBKT_CLOSE
+	     | OP_SQBKT_NUM OP_SQBKT_SEP_unbounded OP_SQBKT_CLOSE
               { $$.min = $1; $$.max = bunop::unbounded; }
 	     | OP_SQBKT_SEP OP_SQBKT_NUM OP_SQBKT_CLOSE
               { $$.min = 0U; $$.max = $2; }
@@ -208,11 +210,11 @@ sqbracketargs: OP_SQBKT_NUM OP_SQBKT_SEP OP_SQBKT_NUM OP_SQBKT_CLOSE
 /* [->i..j] has default values that are different than [*] and [=]. */
 gotoargs: OP_GOTO_OPEN OP_SQBKT_NUM OP_SQBKT_SEP OP_SQBKT_NUM OP_SQBKT_CLOSE
            { $$.min = $2; $$.max = $4; }
-	  | OP_GOTO_OPEN OP_SQBKT_NUM OP_SQBKT_SEP OP_SQBKT_CLOSE
+	  | OP_GOTO_OPEN OP_SQBKT_NUM OP_SQBKT_SEP_unbounded OP_SQBKT_CLOSE
            { $$.min = $2; $$.max = bunop::unbounded; }
 	  | OP_GOTO_OPEN OP_SQBKT_SEP OP_SQBKT_NUM OP_SQBKT_CLOSE
            { $$.min = 1U; $$.max = $3; }
-	  | OP_GOTO_OPEN OP_SQBKT_SEP OP_SQBKT_CLOSE
+	  | OP_GOTO_OPEN OP_SQBKT_SEP_unbounded OP_SQBKT_CLOSE
            { $$.min = 1U; $$.max = bunop::unbounded; }
 	  | OP_GOTO_OPEN OP_SQBKT_CLOSE
            { $$.min = $$.max = 1U; }
diff --git a/src/ltlparse/ltlscan.ll b/src/ltlparse/ltlscan.ll
index 4fde032b7..39b4b476e 100644
--- a/src/ltlparse/ltlscan.ll
+++ b/src/ltlparse/ltlscan.ll
@@ -116,8 +116,15 @@ flex_set_buffer(const char* buf, int start_tok)
                                     yylloc->step();
 				  }
 				}
-<sqbracket>","|".."		return token::OP_SQBKT_SEP;
+  /* .. is from PSL and EDL
+   : is from Verilog and PSL
+   to is from VHDL
+   , is from Perl */
+<sqbracket>","|".."|":"|"to"	return token::OP_SQBKT_SEP;
 
+  /* In SVA  you use [=1:$] instead of [=1..].  We will also
+     accept [=1..$] and [=1:].  */
+<sqbracket>"$"			return token::OP_UNBOUNDED;
 
   /* & 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 1e0c4055e..bcc7f3d7b 100755
--- a/src/ltltest/equals.test
+++ b/src/ltltest/equals.test
@@ -127,13 +127,13 @@ run 0 ../equals '{a[*0]}' '{[*0]}'
 run 0 ../equals '{a[*..]}' '{a[*]}'
 run 0 ../equals '{a[*2..3][*4..5]}' '{a[*8..15]}'
 run 0 ../equals '{a[*4..5][*2..3]}' '{a[*4..5][*2..3]}'
-run 0 ../equals '{a[*2..3][*]}' '{a[*2..3][*]}'
+run 0 ../equals '{a[*2:3][*]}' '{a[*2 to 3][*]}'
 run 0 ../equals '{a[*1..3][*]}' '{a[*]}'
 run 0 ../equals '{a[*][*2..3]}' '{a[*]}'
 run 0 ../equals '{a[*..3][*2]}' '{a[*..6]}'
-run 0 ../equals '{a[*..3][*..2]}' '{a[*..6]}'
-run 0 ../equals '{a[*..3][*2..]}' '{a[*]}'
-run 0 ../equals '{a[*..3][*2..]}' '{a[*]}'
+run 0 ../equals '{a[*..3][*to2]}' '{a[*:6]}'
+run 0 ../equals '{a[*..3][*2..$]}' '{a[*]}'
+run 0 ../equals '{a[*..3][*2:]}' '{a[*]}'
 run 0 ../equals '{a[*1..]}' '{a[+]}'
 run 0 ../equals '{a[+][*1..3]}' '{a[+]}'
 run 0 ../equals '{a[*1..3][+]}' '{a[+]}'
@@ -147,15 +147,15 @@ run 0 ../equals '{0[=0]}' '{[*]}'
 run 0 ../equals '{0[=0..10]}' '{*}'
 run 0 ../equals '{0[=0..]}' '{*}'
 run 0 ../equals '{1[=0]}' '{[*0]}'
-run 0 ../equals '{1[=1..2]}' '{[*1..2]}'
+run 0 ../equals '{1[=1..2]}' '{[*1,2]}'
 run 0 ../equals '{1[=..4]}' '{1[*..4]}'
 run 0 ../equals '{b[=0]}' '{(!b)[*]}'
-run 0 ../equals '{b[=0..]}' '{*}'
+run 0 ../equals '{b[=0to$]}' '{*}'
 
 run 0 ../equals '{0[->10..100];b}' '0'
 run 0 ../equals '{0[->1..];b}' '0'
-run 0 ../equals '{0[->0..100];b}' '{b}'
-run 0 ../equals '{0[->0..];b}' '{b}'
+run 0 ../equals '{0[->0,100];b}' '{b}'
+run 0 ../equals '{0[->0..$];b}' '{b}'
 run 0 ../equals '{1[->0];b}' '{b}'
 run 0 ../equals '{1[->10,20];b}' '{[*10..20];b}'
 run 0 ../equals '{1[->..];b}' '{[*1..];b}'