ltlscan.ll 4.5 KB
Newer Older
1
2
3
/* Copyright (C) 2010, Laboratoire de Recherche et Développement de
** l'Epita (LRDE).
** Copyright (C) 2003, 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
** département Systèmes Répartis Coopératifs (SRC), Université Pierre
** et Marie Curie.
**
** This file is part of Spot, a model checking library.
**
** Spot is free software; you can redistribute it and/or modify it
** under the terms of the GNU General Public License as published by
** the Free Software Foundation; either version 2 of the License, or
** (at your option) any later version.
**
** Spot is distributed in the hope that it will be useful, but WITHOUT
** ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
** or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
** License for more details.
**
** You should have received a copy of the GNU General Public License
** along with Spot; see the file COPYING.  If not, write to the Free
** Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
** 02111-1307, USA.
*/
24
%option noyywrap
25
26
%option prefix="ltlyy"
%option outfile="lex.yy.c"
27
28
29

%{
#include <string>
30
#include "ltlparse/parsedecl.hh"
31
32

/* Hack Flex so we read from a string instead of reading from a file.  */
33
#define YY_INPUT(buf, result, max_size)					\
34
35
36
37
38
39
40
41
  do {									\
    result = (max_size < to_parse_size) ? max_size : to_parse_size;	\
    memcpy(buf, to_parse, result);					\
    to_parse_size -= result;						\
    to_parse += result;							\
  } while (0);

#define YY_USER_ACTION \
42
  yylloc->columns(yyleng);
43

44
static const char* to_parse = 0;
45
static size_t to_parse_size = 0;
46

47
48
typedef ltlyy::parser::token token;

49
void
50
flex_set_buffer(const char* buf)
51
52
53
54
55
56
57
{
  to_parse = buf;
  to_parse_size = strlen(to_parse);
}

%}

58
59
%s not_prop

60
61
62
%%

%{
63
  yylloc->step();
64
65
%}

66
67
"("				BEGIN(0); return token::PAR_OPEN;
")"				BEGIN(not_prop); return token::PAR_CLOSE;
68
69
70

  /* Must go before the other operators, because the F of FALSE
     should not be mistaken with a unary F. */
71
72
"1"|[tT][rR][uU][eE]		BEGIN(0); return token::CONST_TRUE;
"0"|[fF][aA][lL][sS][eE]	BEGIN(0); return token::CONST_FALSE;
73
74
75



76
"!"				BEGIN(0); return token::OP_NOT;
77

78
79
  /* & and | come from Spin.  && and || from LTL2BA.
     /\, \/, and xor are from LBTT.
80
  */
81
"||"|"|"|"+"|"\\/"		BEGIN(0); return token::OP_OR;
82
"&&"|"&"|"."|"/\\"		BEGIN(0); return token::OP_AND;
83
84
85
"^"|"xor"			BEGIN(0); return token::OP_XOR;
"=>"|"->"			BEGIN(0); return token::OP_IMPLIES;
"<=>"|"<->"			BEGIN(0); return token::OP_EQUIV;
86
87

  /* <>, [], and () are used in Spin.  */
88
89
90
91
92
"F"|"<>"			BEGIN(0); return token::OP_F;
"G"|"[]"			BEGIN(0); return token::OP_G;
"U"				BEGIN(0); return token::OP_U;
"R"|"V"				BEGIN(0); return token::OP_R;
"X"|"()"			BEGIN(0); return token::OP_X;
93

94
95
"=0"				return token::OP_POST_NEG;
"=1"				return token::OP_POST_POS;
96

97
[ \t\n]+			/* discard whitespace */ yylloc->step ();
98

99
  /* An Atomic proposition cannot start with the letter
100
101
     used by a unary operator (F,G,X), unless this
     letter is followed by a digit in which case we assume
102
     it's an ATOMIC_PROP (even though F0 could be seen as Ffalse, we
103
     don't, because Ffalse is never used in practice).
104
105
  */
<INITIAL>[a-zA-EH-WYZ_][a-zA-Z0-9_]* |
106
<INITIAL>[FGX][0-9][a-zA-Z0-9_]* |
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
  /*
     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)))'.
  */
<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_]* {
123
			  yylval->str = new std::string(yytext, yyleng);
124
			  BEGIN(not_prop);
125
			  return token::ATOMIC_PROP;
126
			}
127

128
  /* Atomic propositions can also be enclosed in double quotes.  */
129
130
131
132
\"[^\"]*\"		{
			  yylval->str = new std::string(yytext + 1,
			                                yyleng - 2);
			  BEGIN(not_prop);
133
			  return token::ATOMIC_PROP;
134
			}
135

136
.			return *yytext;
137

138
<<EOF>>			return token::END_OF_INPUT;
139
140
141
142
143

%{
  /* Dummy use of yyunput to shut up a gcc warning.  */
  (void) &yyunput;
%}