From a66ad58b5da79dedd278256f9cd5900a60f591e3 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Tue, 29 Jul 2003 16:28:38 +0000
Subject: [PATCH] * src/ltlparse/ltlscan.ll: Allow /, /, and xor, used in LBTT.
 * src/ltltest/parse.test: Test them.

---
 ChangeLog               |  3 +++
 src/ltlparse/ltlscan.ll | 13 ++++++++-----
 src/ltltest/parse.test  |  5 ++++-
 3 files changed, 15 insertions(+), 6 deletions(-)

diff --git a/ChangeLog b/ChangeLog
index 0cf4eb01c..5749daac5 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,5 +1,8 @@
 2003-07-29  Alexandre Duret-Lutz  <aduret@src.lip6.fr>
 
+	* src/ltlparse/ltlscan.ll: Allow /\, \/, and xor, used in LBTT.
+	* src/ltltest/parse.test: Test them.
+
 	* src/tgbaalgos/lbtt.cc: Typos.
 
 	* lbtt/: Upgrade to lbtt 1.0.2.
diff --git a/src/ltlparse/ltlscan.ll b/src/ltlparse/ltlscan.ll
index 051b04f89..2c058006b 100644
--- a/src/ltlparse/ltlscan.ll
+++ b/src/ltlparse/ltlscan.ll
@@ -40,10 +40,12 @@ flex_set_buffer(const char *buf)
 ")"			return PAR_CLOSE;
 
 "!"			return OP_NOT;
-  /* & and | come from Spin.  && and || from LTL2BA.  */
-"||"|"|"|"+"		return OP_OR;
-"&&"|"&"|"."|"*"	return OP_AND;
-"^"			return OP_XOR;
+  /* & and | come from Spin.  && and || from LTL2BA.  
+     /\, \/, and xor are from LBTT. 
+  */
+"||"|"|"|"+"|"\\/"	return OP_OR;
+"&&"|"&"|"."|"*"|"/\\"	return OP_AND;
+"^"|"xor"		return OP_XOR;
 "=>"|"->"		return OP_IMPLIES;
 "<=>"|"<->"		return OP_EQUIV;
 
@@ -62,7 +64,8 @@ flex_set_buffer(const char *buf)
   /* 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).  */
+     it's an ATOMIC_PROP (even though F0 could be seen as Ffalse, we
+     don't).  */
 [a-zA-EH-WYZ_][a-zA-Z0-9_]* | 
 [FGX][0-9_][a-zA-Z0-9_]* { 
 		  yylval->str = new std::string(yytext); 
diff --git a/src/ltltest/parse.test b/src/ltltest/parse.test
index 01a8845f3..a06d5e4a1 100755
--- a/src/ltltest/parse.test
+++ b/src/ltltest/parse.test
@@ -21,13 +21,16 @@ for f in \
   'a3214 | b' \
   'a & b' \
   'a && b' \
+  'a /\ b' \
   'a || b' \
+  'a \/ b' \
   'a | b' \
   '_a_ U b' \
   'a R b' \
   'a <=> b' \
   'a <-> b' \
   'a ^ b' \
+  'a xor b' \
   'a => b' \
   'a -> b' \
   'F b' \
@@ -44,7 +47,7 @@ for f in \
   '((b * a) + a) & d' \
   '(ab & ac | ad ) <=> af ' \
   'a U b U c U d U e U f U g U h U i U j U k U l U m' \
-  '(ab * !Xad + ad U ab) & FG p12 & GF p13' \
+  '(ab * !Xad + ad U ab) & FG p12 /\ GF p13' \
   '((([]<>()p12))   )' \
   'a R ome V anille'
 do