alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

* src/ltlparse/ltlscan.ll: Allow doubly quoted atomic propositions.

Browse source
This commit is contained in:
Alexandre Duret-Lutz 2003-10-02 15:58:57 +00:00
parent 694ce34bc5
commit d06e09b951
2 changed files with 17 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

4
ChangeLog
View file

@ -1,3 +1,7 @@
2003-10-02 Alexandre Duret-Lutz <adl@src.lip6.fr>
* src/ltlparse/ltlscan.ll: Allow doubly quoted atomic propositions.
2003-10-01 Alexandre Duret-Lutz <aduret@src.lip6.fr> 2003-10-01 Alexandre Duret-Lutz <aduret@src.lip6.fr>
* iface/gspn/udcsltl.test, iface/gspn/udcseltl.test, * iface/gspn/udcsltl.test, iface/gspn/udcseltl.test,

20
src/ltlparse/ltlscan.ll
View file

@ -20,7 +20,7 @@
static const char *to_parse = 0; static const char *to_parse = 0;
static size_t to_parse_size = 0; static size_t to_parse_size = 0;
void void
flex_set_buffer(const char *buf) flex_set_buffer(const char *buf)
{ {
@ -40,8 +40,8 @@ flex_set_buffer(const char *buf)
")" return PAR_CLOSE; ")" return PAR_CLOSE;
"!" return OP_NOT; "!" return OP_NOT;
/* & and | come from Spin. && and || from LTL2BA. /* & and | come from Spin. && and || from LTL2BA.
/\, \/, and xor are from LBTT. /\, \/, and xor are from LBTT.
*/ */
"||"|"|"|"+"|"\\/" return OP_OR; "||"|"|"|"+"|"\\/" return OP_OR;
"&&"|"&"|"."|"*"|"/\\" return OP_AND; "&&"|"&"|"."|"*"|"/\\" return OP_AND;
@ -59,16 +59,22 @@ flex_set_buffer(const char *buf)
"1"|"true" return CONST_TRUE; "1"|"true" return CONST_TRUE;
"0"|"false" return CONST_FALSE; "0"|"false" return CONST_FALSE;
[ \t\n]+ /* discard whitespace */ yylloc->step (); [ \t\n]+ /* discard whitespace */ yylloc->step ();
/* An Atomic proposition cannot start with the letter /* An Atomic proposition cannot start with the letter
used by a unary operator (F,G,X), unless this used by a unary operator (F,G,X), unless this
letter is followed by a digit in which case we assume letter is followed by a digit in which case we assume
it's an ATOMIC_PROP (even though F0 could be seen as Ffalse, we it's an ATOMIC_PROP (even though F0 could be seen as Ffalse, we
don't). */ don't). */
[a-zA-EH-WYZ_][a-zA-Z0-9_]* | [a-zA-EH-WYZ_][a-zA-Z0-9_]* |
[FGX][0-9_][a-zA-Z0-9_]* { [FGX][0-9_][a-zA-Z0-9_]* {
yylval->str = new std::string(yytext); yylval->str = new std::string(yytext);
return ATOMIC_PROP;
}
/* Atomic propositions can also be inclosed in double quotes. */
\"[^\"]*\" {
yylval->str = new std::string(yytext + 1, yyleng - 2);
return ATOMIC_PROP; return ATOMIC_PROP;
} }