From d9cd704bcb502f28472f73d3cd01eed43f65c08d Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Fri, 18 Apr 2003 09:12:26 +0000
Subject: [PATCH] * src/ltlparse/ltlscan.ll: Recognize && and ||. *
 src/ltltest/parse.test, src/ltltest/parseerr.test, src/ltltest/equals.test:
 Use these operators..

---
 ChangeLog                 |  6 ++++++
 src/ltlparse/ltlscan.ll   | 35 ++++++++++++++++++-----------------
 src/ltltest/equals.test   |  6 +++---
 src/ltltest/parse.test    |  3 +++
 src/ltltest/parseerr.test |  1 +
 5 files changed, 31 insertions(+), 20 deletions(-)

diff --git a/ChangeLog b/ChangeLog
index 265d9f81f..754c322f3 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,3 +1,9 @@
+2003-04-18  Alexandre DURET-LUTZ  <aduret@src.lip6.fr>
+
+	* src/ltlparse/ltlscan.ll: Recognize && and ||.
+	* src/ltltest/parse.test, src/ltltest/parseerr.test, 
+	src/ltltest/equals.test: Use these operators..
+
 2003-04-17  Alexandre DURET-LUTZ  <aduret@src.lip6.fr>
 
 	* src/ltltest/readltl.cc, src/ltltest/equals.cc: Cosmetics.
diff --git a/src/ltlparse/ltlscan.ll b/src/ltlparse/ltlscan.ll
index 248173a8c..9fe78ae2d 100644
--- a/src/ltlparse/ltlscan.ll
+++ b/src/ltlparse/ltlscan.ll
@@ -34,29 +34,30 @@ flex_set_buffer(const char *buf)
   yylloc->step ();
 %}
 
-"("		return PAR_OPEN;
-")"		return PAR_CLOSE;
+"("			return PAR_OPEN;
+")"			return PAR_CLOSE;
 
-"!"		return OP_NOT;
-"|"|"+"		return OP_OR;
-"&"|"."|"*"	return OP_AND;
-"^"		return OP_XOR;
-"=>"|"->"	return OP_IMPLIES;
-"<=>"|"<->"	return OP_EQUIV;
+"!"			return OP_NOT;
+  /* & and | come from Spin.  && and || from LTL2BA.  */
+"||"|"|"|"+"		return OP_OR;
+"&&"|"&"|"."|"*"	return OP_AND;
+"^"			return OP_XOR;
+"=>"|"->"		return OP_IMPLIES;
+"<=>"|"<->"		return OP_EQUIV;
 
   /* <>, [], and () are used in Spin.  */
-"F"|"<>"	return OP_F;
-"G"|"[]"	return OP_G;
-"U"		return OP_U;
-"R"|"V"		return OP_R;
-"X"|"()"	return OP_X;
+"F"|"<>"		return OP_F;
+"G"|"[]"		return OP_G;
+"U"			return OP_U;
+"R"|"V"			return OP_R;
+"X"|"()"		return OP_X;
 
-"1"|"true"	return CONST_TRUE;
-"0"|"false"	return CONST_FALSE;
+"1"|"true"		return CONST_TRUE;
+"0"|"false"		return CONST_FALSE;
 
-[ \t\n]+	yylloc->step (); /* discard whitespace */
+[ \t\n]+		/* discard whitespace */ yylloc->step (); 
 
-  /* An Atomic propisition cannot start with the letter
+  /* An Atomic proposition cannot start with the letter
      used by a unary operator (F,G,X), unless this
      letter is followed by a digit in which case we assume
      it's an ATOMIC_PROP (even though F0 could be seen as Ffalse).  */
diff --git a/src/ltltest/equals.test b/src/ltltest/equals.test
index feed0296c..3101afa4f 100755
--- a/src/ltltest/equals.test
+++ b/src/ltltest/equals.test
@@ -19,12 +19,12 @@ check 0 'G a ' ' G a'
 check 0 'a U b' 'a U b'
 check 0 'a & b' 'a & b'
 check 0 'a & b' 'b & a'
-check 0 'a & b & c' 'c & a & b'
+check 0 'a & b & c' 'c & a && b'
 check 0 'a & b & c' 'b & c & a'
-check 0 'a & b & a' 'b & a & b'
+check 0 'a && b & a' 'b & a & b'
 check 0 'a & b' 'b & a & b'
 check 0 'a & b' 'b & a & a'
-check 0 'a & b & (c |(f U g)| e)' 'b & a & a & (c | e |(f U g)| e | c) & b'
+check 0 'a & b & (c |(f U g)|| e)' 'b & a & a & (c | e |(f U g)| e | c) & b'
 
 # other formulae which are not
 check 1 'a' 'b'
diff --git a/src/ltltest/parse.test b/src/ltltest/parse.test
index 6ba29c911..cd2f7f26b 100755
--- a/src/ltltest/parse.test
+++ b/src/ltltest/parse.test
@@ -20,6 +20,9 @@ for f in \
   'a + b' \
   'a3214 | b' \
   'a & b' \
+  'a && b' \
+  'a || b' \
+  'a | b' \
   '_a_ U b' \
   'a R b' \
   'a <=> b' \
diff --git a/src/ltltest/parseerr.test b/src/ltltest/parseerr.test
index f439c8069..ed7e7a5f6 100755
--- a/src/ltltest/parseerr.test
+++ b/src/ltltest/parseerr.test
@@ -39,6 +39,7 @@ check 'a U b V c R' ''
 # leading and trailing garbage are skipped
 check '/2/3/4/5 a + b /6/7/8/' 'multop(Or, AP(a), AP(b))'
 check 'a U b c' 'binop(U, AP(a), AP(b))'
+check 'a &&& b' 'AP(b)'
 # (check multop merging while we are at it)
 check 'a & b & c & d e' 'multop(And, AP(a), AP(b), AP(c), AP(d))'
 check 'a & (b | c) & d should work' 'multop(And, AP(a), multop(Or, AP(b), AP(c)), AP(d))'