Commit a66ad58b authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

* src/ltlparse/ltlscan.ll: Allow /, /, and xor, used in LBTT.

* src/ltltest/parse.test: Test them.
parent 60ef421d
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.
......
......@@ -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);
......
......@@ -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
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment