From f2732dd8cc3f96754d0d47e319ea2be9ec2fe50e Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 15 Oct 2010 17:46:47 +0200 Subject: [PATCH] Read p=0Wq=1 and p=0Mq=1 correctly. * src/ltlparse/ltlscan.ll: Handle p=0Wq=1 and p=0Mq=1 in the same way as we did for * src/ltltest/parse.test: More tests. --- src/ltlparse/ltlscan.ll | 21 +++++++++++---------- src/ltltest/parse.test | 2 ++ 2 files changed, 13 insertions(+), 10 deletions(-) diff --git a/src/ltlparse/ltlscan.ll b/src/ltlparse/ltlscan.ll index 39b4b476e..0c006262c 100644 --- a/src/ltlparse/ltlscan.ll +++ b/src/ltlparse/ltlscan.ll @@ -164,21 +164,22 @@ flex_set_buffer(const char* buf, int start_tok) [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. + 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 M, U, R, V, and W. 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 like 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_.]* { +[a-zA-EH-LN-QSTYZ_.][a-zA-EH-WYZ0-9_.]* | +[a-zA-EH-LN-QSTYZ_.][a-zA-EH-WYZ0-9_.][a-zA-Z0-9_.]* { yylval->str = new std::string(yytext, yyleng); BEGIN(not_prop); return token::ATOMIC_PROP; diff --git a/src/ltltest/parse.test b/src/ltltest/parse.test index d8ec2aaf6..0f4351218 100755 --- a/src/ltltest/parse.test +++ b/src/ltltest/parse.test @@ -73,6 +73,8 @@ for f in \ 'a R ome V anille' \ 'p=0Uq=1' \ '((p=1Rq=1)+p=0)UXq=0' \ + '((p=1Mq=1)Wx+p=0)RXq=0' \ + '((p=1Vq=1)Rx+p=0)WXq=0' \ '((X(p2=0))U(X(p2=0)))+((Xp1=0)UFALSE)' do