From 4a62224932c8cd9894b23dfd060fc4b1b7ddf874 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sun, 6 Mar 2011 19:12:24 +0100 Subject: [PATCH] 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.. --- ChangeLog | 12 ++++++++++++ src/evtgbaparse/evtgbascan.ll | 10 ++++++---- src/ltlparse/ltlscan.ll | 12 ++++++------ src/ltltest/parse.test | 4 ++-- src/misc/bareword.cc | 6 ++++-- src/tgbaparse/tgbascan.ll | 10 ++++++---- 6 files changed, 36 insertions(+), 18 deletions(-) diff --git a/ChangeLog b/ChangeLog index 36d2c33e8..cdb7ad456 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,15 @@ +2011-03-06 Alexandre Duret-Lutz + + 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 Augment dve2check to perform LTL model checking. diff --git a/src/evtgbaparse/evtgbascan.ll b/src/evtgbaparse/evtgbascan.ll index 5151de8e4..c8f38d0cf 100644 --- a/src/evtgbaparse/evtgbascan.ll +++ b/src/evtgbaparse/evtgbascan.ll @@ -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(); diff --git a/src/ltlparse/ltlscan.ll b/src/ltlparse/ltlscan.ll index 215a054bb..a93bef7e4 100644 --- a/src/ltlparse/ltlscan.ll +++ b/src/ltlparse/ltlscan.ll @@ -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). */ -[a-zA-EH-WYZ_][a-zA-Z0-9_]* | -[FGX][0-9][a-zA-Z0-9_]* | +[a-zA-EH-WYZ_.][a-zA-Z0-9_.]* | +[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)))'. */ -[a-zA-EH-QSTWYZ_][a-zA-EH-WYZ0-9_]* | -[a-zA-EH-QSTWYZ_][a-zA-EH-WYZ0-9_][a-zA-Z0-9_]* { +[a-zA-EH-QSTWYZ_.][a-zA-EH-WYZ0-9_.]* | +[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; } diff --git a/src/ltltest/parse.test b/src/ltltest/parse.test index 43e42c4f1..1c0a59c19 100755 --- a/src/ltltest/parse.test +++ b/src/ltltest/parse.test @@ -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' \ diff --git a/src/misc/bareword.cc b/src/misc/bareword.cc index 3d548d797..c1628edd7 100644 --- a/src/misc/bareword.cc +++ b/src/misc/bareword.cc @@ -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; } diff --git a/src/tgbaparse/tgbascan.ll b/src/tgbaparse/tgbascan.ll index 0f46e7eff..cda637ebc 100644 --- a/src/tgbaparse/tgbascan.ll +++ b/src/tgbaparse/tgbascan.ll @@ -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();