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

Allow atomic propositions and identifiers like `X.Y'.

Browse source 
* src/ltlparse/ltlscan.ll: Do not recognize `.' as an AND.  Allow
it in atomic propositions.
* src/evtgbaparse/evtgbascan.ll, src/tgbaparse/tgbascan.ll: Accept
`.' in identifiers.
* src/misc/bareword.cc (is_bareword): Accept `.' inside
barewords, so that there is no need to quote `X.Y'.
* src/ltltest/parse.test: Do not use `.' as and operator..
This commit is contained in:
Alexandre Duret-Lutz 2011-03-06 19:12:24 +01:00
parent 8ce39e09b2
commit 4a62224932
6 changed files with 36 additions and 18 deletions
Download patch file Download diff file Expand all files Collapse all files

12
ChangeLog
View file

@ -1,3 +1,15 @@
2011-03-06 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Allow atomic propositions and identifiers like `X.Y'.
* src/ltlparse/ltlscan.ll: Do not recognize `.' as an AND. Allow
it in atomic propositions.
* src/evtgbaparse/evtgbascan.ll, src/tgbaparse/tgbascan.ll: Accept
`.' in identifiers.
* src/misc/bareword.cc (is_bareword): Accept `.' inside
barewords, so that there is no need to quote `X.Y'.
* src/ltltest/parse.test: Do not use `.' as and operator..
2011-03-06 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Augment dve2check to perform LTL model checking.

10
src/evtgbaparse/evtgbascan.ll
View file

@ -1,4 +1,6 @@
/* Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
/* Copyright (C) 2011, Laboratoire de Recherche et Développement de
** l'Epita (LRDE).
** Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
** département Systèmes Répartis Coopératifs (SRC), Université Pierre
** et Marie Curie.
**
@ -47,10 +49,10 @@ eol \n|\r|\n\r|\r\n
acc[ \t]*= return token::ACC_DEF;
init[ \t]*= return token::INIT_DEF;
[a-zA-Z][a-zA-Z0-9_]* {
[a-zA-Z_.][a-zA-Z0-9_.]* {
yylval->str = new std::string(yytext);
return token::IDENT;
}
return token::IDENT;
}
/* discard whitespace */
{eol} yylloc->lines(yyleng); yylloc->step();

12
src/ltlparse/ltlscan.ll
View file

@ -79,7 +79,7 @@ flex_set_buffer(const char* buf)
/\, \/, and xor are from LBTT.
--> and <--> come from Goal. */
"||"|"|"|"+"|"\\/" BEGIN(0); return token::OP_OR;
"&&"|"&"|"."|"/\\" BEGIN(0); return token::OP_AND;
"&&"|"&"|"/\\" BEGIN(0); return token::OP_AND;
"^"|"xor" BEGIN(0); return token::OP_XOR;
"=>"|"->"|"-->" BEGIN(0); return token::OP_IMPLIES;
"<=>"|"<->"|"<-->" BEGIN(0); return token::OP_EQUIV;
@ -104,8 +104,8 @@ flex_set_buffer(const char* buf)
it's an ATOMIC_PROP (even though F0 could be seen as Ffalse, we
don't, because Ffalse is never used in practice).
*/
<INITIAL>[a-zA-EH-WYZ_][a-zA-Z0-9_]* |
<INITIAL>[FGX][0-9][a-zA-Z0-9_]* |
<INITIAL>[a-zA-EH-WYZ_.][a-zA-Z0-9_.]* |
<INITIAL>[FGX][0-9][a-zA-Z0-9_.]* |
/*
However if we have just parsed an atomic proposition, then we
are not expecting another atomic proposition, so we can be stricter
@ -120,8 +120,8 @@ flex_set_buffer(const char* buf)
of a binary operator followed by several unary operators.
E.g. UFXp. This way, `p=0UFXp=1' will be parsed as `(p=0)U(F(X(p=1)))'.
*/
<not_prop>[a-zA-EH-QSTWYZ_][a-zA-EH-WYZ0-9_]* |
<not_prop>[a-zA-EH-QSTWYZ_][a-zA-EH-WYZ0-9_][a-zA-Z0-9_]* {
<not_prop>[a-zA-EH-QSTWYZ_.][a-zA-EH-WYZ0-9_.]* |
<not_prop>[a-zA-EH-QSTWYZ_.][a-zA-EH-WYZ0-9_.][a-zA-Z0-9_.]* {
yylval->str = new std::string(yytext, yyleng);
BEGIN(not_prop);
return token::ATOMIC_PROP;
@ -130,7 +130,7 @@ flex_set_buffer(const char* buf)
/* Atomic propositions can also be enclosed in double quotes. */
\"[^\"]*\" {
yylval->str = new std::string(yytext + 1,
yyleng - 2);
yyleng - 2);
BEGIN(not_prop);
return token::ATOMIC_PROP;
}

4
src/ltltest/parse.test
View file

@ -1,5 +1,5 @@
#! /bin/sh
# Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement
# Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et Developpement
# de l'Epita (LRDE).
# Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
# département Systèmes Répartis Coopératifs (SRC), Université Pierre
@ -39,7 +39,7 @@ for f in \
'(p11011)' \
'a & b' \
'a & _b12' \
'a . b' \
'a && .b.' \
'a + b' \
'a3214 | b' \
'a & b' \

6
src/misc/bareword.cc
View file

@ -1,3 +1,5 @@
// Copyright (C) 2011 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie.
@ -30,11 +32,11 @@ namespace spot
{
// Bare words cannot be empty and should start with a letter.
if (!*str
|| !(isalpha(*str) || *str == '_'))
|| !(isalpha(*str) || *str == '_' || *str == '.'))
return false;
// The remaining of the word must be alphanumeric.
while (*++str)
if (!(isalnum(*str) || *str == '_'))
if (!(isalnum(*str) || *str == '_' || *str == '.'))
return false;
return true;
}

10
src/tgbaparse/tgbascan.ll
View file

@ -1,4 +1,6 @@
/* Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
/* Copyright (C) 2011, Laboratoire de Recherche et Développement de
** l'Epita (LRDE).
** Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
** département Systèmes Répartis Coopératifs (SRC), Université Pierre
** et Marie Curie.
**
@ -47,10 +49,10 @@ eol \n|\r|\n\r|\r\n
acc[ \t]*= return token::ACC_DEF;
[a-zA-Z][a-zA-Z0-9_]* {
[a-zA-Z_.][a-zA-Z0-9_.]* {
yylval->str = new std::string(yytext, yyleng);
return token::IDENT;
}
return token::IDENT;
}
/* discard whitespace */
{eol} yylloc->lines(yyleng); yylloc->step();