From 60a3b4ed722c6fb38695295e323ddd16073df8e5 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 13 May 2004 09:49:06 +0000 Subject: [PATCH] * src/ltlparse/ltlparse.yy (OP_POST_NEG, OP_POST_POS): New tokens. (subformula): Recognize `ATOMIC_PROP OP_POST_POS' and `ATOMIC_PROP OP_POST_NEG'. * src/ltlparse/ltlscan.ll: Introduce the not_prop start condition, to restrict the set of atomic propositions allowed in places where they are not expected. Make `true' and `false' case insensitive. * src/ltltest/parse.test, src/ltltest/tostring.test: More cases. * src/ltlvisit/tostring.cc (to_string_visitor): Quote atomic propositions equal to "true" or "false". --- ChangeLog | 12 ++++++ src/ltlparse/ltlparse.yy | 41 +++++++++++++++++- src/ltlparse/ltlscan.ll | 88 ++++++++++++++++++++++++++------------- src/ltltest/parse.test | 8 +++- src/ltltest/tostring.test | 6 +++ src/ltlvisit/tostring.cc | 4 +- 6 files changed, 125 insertions(+), 34 deletions(-) diff --git a/ChangeLog b/ChangeLog index 8a83ae92a..8e48788d1 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,15 @@ +2004-05-13 Alexandre Duret-Lutz + + * src/ltlparse/ltlparse.yy (OP_POST_NEG, OP_POST_POS): New tokens. + (subformula): Recognize `ATOMIC_PROP OP_POST_POS' and + `ATOMIC_PROP OP_POST_NEG'. + * src/ltlparse/ltlscan.ll: Introduce the not_prop start condition, + to restrict the set of atomic propositions allowed in places + where they are not expected. Make `true' and `false' case insensitive. + * src/ltltest/parse.test, src/ltltest/tostring.test: More cases. + * src/ltlvisit/tostring.cc (to_string_visitor): Quote atomic + propositions equal to "true" or "false". + 2004-05-11 Alexandre Duret-Lutz * src/ltltest/Makefile.am (TESTS): Run inf.test and reduc.test last. diff --git a/src/ltlparse/ltlparse.yy b/src/ltlparse/ltlparse.yy index 3f0966baf..9a1f89d5a 100644 --- a/src/ltlparse/ltlparse.yy +++ b/src/ltlparse/ltlparse.yy @@ -82,7 +82,7 @@ using namespace spot::ltl; %token ATOMIC_PROP "atomic proposition" OP_NOT "not operator" %token CONST_TRUE "constant true" CONST_FALSE "constant false" %token END_OF_INPUT "end of formula" - +%token OP_POST_NEG "negative suffix" OP_POST_POS "positive suffix" /* Priorities. */ @@ -97,9 +97,11 @@ using namespace spot::ltl; %nonassoc OP_F OP_G %nonassoc OP_X -/* Not has the most important priority. */ +/* Not has the most important priority after Wring's `=0' and `=1'. */ %nonassoc OP_NOT +%nonassoc OP_POST_NEG OP_POST_POS + %type result subformula /* At the time of writing (2004-01-05) there is a bug in CVS Bison: if @@ -152,6 +154,41 @@ subformula: ATOMIC_PROP else delete $1; } + | ATOMIC_PROP OP_POST_POS + { + $$ = parse_environment.require(*$1); + if (! $$) + { + std::string s = "unknown atomic proposition `"; + s += *$1; + s += "' in environment `"; + s += parse_environment.name(); + s += "'"; + error_list.push_back(parse_error(@1, s)); + delete $1; + YYERROR; + } + else + delete $1; + } + | ATOMIC_PROP OP_POST_NEG + { + $$ = parse_environment.require(*$1); + if (! $$) + { + std::string s = "unknown atomic proposition `"; + s += *$1; + s += "' in environment `"; + s += parse_environment.name(); + s += "'"; + error_list.push_back(parse_error(@1, s)); + delete $1; + YYERROR; + } + else + delete $1; + $$ = unop::instance(unop::Not, $$); + } | CONST_TRUE { $$ = constant::true_instance(); } | CONST_FALSE diff --git a/src/ltlparse/ltlscan.ll b/src/ltlparse/ltlscan.ll index 734ff3174..d7f020da5 100644 --- a/src/ltlparse/ltlscan.ll +++ b/src/ltlparse/ltlscan.ll @@ -1,4 +1,4 @@ -/* Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6), +/* 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. ** @@ -51,57 +51,87 @@ flex_set_buffer(const char* buf) %} +%s not_prop + %% %{ yylloc->step(); %} -"(" return PAR_OPEN; -")" return PAR_CLOSE; +"(" BEGIN(0); return PAR_OPEN; +")" BEGIN(not_prop); return PAR_CLOSE; + + /* Must go before the other operators, because the F of FALSE + should not be mistaken with a unary F. */ +"1"|[tT][rR][uU][eE] BEGIN(0); return CONST_TRUE; +"0"|[fF][aA][lL][sS][eE] BEGIN(0); return CONST_FALSE; + + + +"!" BEGIN(0); return OP_NOT; -"!" return OP_NOT; /* & 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; +"||"|"|"|"+"|"\\/" BEGIN(0); return OP_OR; +"&&"|"&"|"."|"*"|"/\\" BEGIN(0); return OP_AND; +"^"|"xor" BEGIN(0); return OP_XOR; +"=>"|"->" BEGIN(0); return OP_IMPLIES; +"<=>"|"<->" BEGIN(0); return OP_EQUIV; /* <>, [], and () are used in Spin. */ -"F"|"<>" return OP_F; -"G"|"[]" return OP_G; -"U" return OP_U; -"R"|"V" return OP_R; -"X"|"()" return OP_X; +"F"|"<>" BEGIN(0); return OP_F; +"G"|"[]" BEGIN(0); return OP_G; +"U" BEGIN(0); return OP_U; +"R"|"V" BEGIN(0); return OP_R; +"X"|"()" BEGIN(0); return OP_X; -"1"|"true" return CONST_TRUE; -"0"|"false" return CONST_FALSE; +"=0" return OP_POST_NEG; +"=1" return OP_POST_POS; -[ \t\n]+ /* discard whitespace */ yylloc->step (); +[ \t\n]+ /* discard whitespace */ yylloc->step (); /* 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, we - don't). */ -[a-zA-EH-WYZ_][a-zA-Z0-9_]* | -[FGX][0-9_][a-zA-Z0-9_]* { - yylval->str = new std::string(yytext); - return ATOMIC_PROP; - } + don't). + */ +[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 + and disallow propositions that start with U, R and V. If you wonder + why we do this, consider the Wring formula `p=0Uq=1'. When p is + parsed, we enter the not_prop start condition, we remain into this + condition when `=0' is processed, and then because we are in this + condition we will not consider `Uq' as an atomic proposition but as + a `U' operator followed by a `q' atomic proposition. + + We also disable atomic proposition that may look a combination + 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_]* { + yylval->str = new std::string(yytext); + BEGIN(not_prop); + return ATOMIC_PROP; + } /* Atomic propositions can also be enclosed in double quotes. */ -\"[^\"]*\" { - yylval->str = new std::string(yytext + 1, yyleng - 2); - return ATOMIC_PROP; - } +\"[^\"]*\" { + yylval->str = new std::string(yytext + 1, + yyleng - 2); + BEGIN(not_prop); + return ATOMIC_PROP; + } -. return *yytext; +. return *yytext; -<> return END_OF_INPUT; +<> return END_OF_INPUT; %{ /* Dummy use of yyunput to shut up a gcc warning. */ diff --git a/src/ltltest/parse.test b/src/ltltest/parse.test index 41cf58988..4550f6448 100755 --- a/src/ltltest/parse.test +++ b/src/ltltest/parse.test @@ -1,5 +1,5 @@ #! /bin/sh -# Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6), +# 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. # @@ -70,7 +70,11 @@ for f in \ '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' \ '((([]<>()p12)) )' \ - 'a R ome V anille' + 'a R ome V anille' \ + 'p=0Uq=1' \ + '((p=1Rq=1)+p=0)UXq=0' \ + '((X(p2=0))U(X(p2=0)))+((Xp1=0)UFALSE)' + do if ./ltl2text "$f"; then : diff --git a/src/ltltest/tostring.test b/src/ltltest/tostring.test index 614c21bac..ed1828808 100755 --- a/src/ltltest/tostring.test +++ b/src/ltltest/tostring.test @@ -45,3 +45,9 @@ run 0 ./tostring 'b & a & a & (c | e |(g U g)| e | c) & b' run 0 ./tostring 'F"F1"&G"G"&X"X"' run 0 ./tostring 'GFfalse' run 0 ./tostring 'GFtrue' +run 0 ./tostring 'p=0Uq=1Ut=1' +run 0 ./tostring 'F"FALSE"' +run 0 ./tostring 'G"TruE"' +run 0 ./tostring 'FFALSE' +run 0 ./tostring 'GTruE' +run 0 ./tostring 'p=0UFXp=1' diff --git a/src/ltlvisit/tostring.cc b/src/ltlvisit/tostring.cc index 67a0f79bb..097733e97 100644 --- a/src/ltlvisit/tostring.cc +++ b/src/ltlvisit/tostring.cc @@ -48,7 +48,9 @@ namespace spot visit(const atomic_prop* ap) { std::string str = ap->name(); - if (str[0] == 'F' || str[0] == 'G' || str[0] == 'X') + if (str[0] == 'F' || str[0] == 'G' || str[0] == 'X' + || !strcasecmp(str.c_str(), "true") + || !strcasecmp(str.c_str(), "false")) { os_ << '"' << str << '"'; }