ltlscan.ll 7.1 KB
Newer Older
1
2
/* Copyright (C) 2010, 2011, 2012, Laboratoire de Recherche et
** Développement de l'Epita (LRDE).
3
** Copyright (C) 2003, 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
4
** département Systèmes Répartis Coopératifs (SRC), Université Pierre
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
** 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 warn 8bit batch
25
26
%option prefix="ltlyy"
%option outfile="lex.yy.c"
27
28
29

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

/* Hack Flex so we read from a string instead of reading from a file.  */
34
#define YY_INPUT(buf, result, max_size)					\
35
36
37
38
39
40
41
42
  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 \
43
  yylloc->columns(yyleng);
44

45
static const char* to_parse = 0;
46
static size_t to_parse_size = 0;
47
static int start_token = 0;
48

49
50
typedef ltlyy::parser::token token;

51
void
52
flex_set_buffer(const char* buf, int start_tok)
53
54
55
{
  to_parse = buf;
  to_parse_size = strlen(to_parse);
56
  start_token = start_tok;
57
58
59
60
}

%}

61
%s not_prop
62
%x sqbracket
63

64
65
66
67
68
69
70
71
72
73
74
BOX       "[]"|"□"|"⬜"|"◻"
DIAMOND   "<>"|"◇"|"⋄"|"♢"
ARROWL    "->"|"-->"|"→"|"⟶"
DARROWL   "=>"|"⇒"|"⟹"
ARROWLR   "<->"|"<-->"|"↔"
DARROWLR  "<=>"|"⇔"
CIRCLE    "()"|"○"|"◯"
NOT       "!"|"~"|"¬"
BOXARROW  {BOX}{ARROWL}|"|"{ARROWL}|"↦"
BOXDARROW {BOX}{DARROWL}|"|"{DARROWL}|"⤇"

75
76
77
%%

%{
78
79
80
81
82
83
  if (start_token)
    {
      int t = start_token;
      start_token = 0;
      return t;
    }
84
  yylloc->step();
85
86
%}

87
88
"("				BEGIN(0); return token::PAR_OPEN;
")"				BEGIN(not_prop); return token::PAR_CLOSE;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
89
"{"                             BEGIN(0); return token::BRACE_OPEN;
90
"}"[ \t\n]*"!"			BEGIN(not_prop); return token::BRACE_BANG_CLOSE;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
91
"}"				BEGIN(not_prop); return token::BRACE_CLOSE;
92
93
94

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


99
  /* ~ comes from Goal, ! from everybody else */
100
{NOT}				BEGIN(0); return token::OP_NOT;
101

102
  /* PSL operators */
103
104
105
106
{BOXARROW}			BEGIN(0); return token::OP_UCONCAT;
{DIAMOND}{ARROWL}		BEGIN(0); return token::OP_ECONCAT;
{BOXDARROW}			BEGIN(0); return token::OP_UCONCAT_NONO;
{DIAMOND}{DARROWL}		BEGIN(0); return token::OP_ECONCAT_NONO;
107
108
";"				BEGIN(0); return token::OP_CONCAT;
":"				BEGIN(0); return token::OP_FUSION;
109
"*"|"[*]"			BEGIN(0); return token::OP_STAR;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
110
"[+]"				BEGIN(0); return token::OP_PLUS;
111
112
"[*"				BEGIN(sqbracket); return token::OP_STAR_OPEN;
"[="				BEGIN(sqbracket); return token::OP_EQUAL_OPEN;
113
"["{ARROWL}			BEGIN(sqbracket); return token::OP_GOTO_OPEN;
114
115
<sqbracket>"]"			BEGIN(0); return token::OP_SQBKT_CLOSE;
<sqbracket>[0-9]+		{
116
117
118
119
                                  unsigned num = 0;
                                  try {
                                    num = boost::lexical_cast<unsigned>(yytext);
				    yylval->num = num;
120
				    return token::OP_SQBKT_NUM;
121
122
123
124
125
                                  }
                                  catch (boost::bad_lexical_cast &)
                                  {
                                    error_list.push_back(
				      spot::ltl::parse_error(*yylloc,
126
					"value too large ignored"));
127
128
129
130
				    // Skip this number and read next token
                                    yylloc->step();
				  }
				}
131
132
133
134
135
136
  /* .. is from PSL and EDL
   : is from Verilog and PSL
   to is from VHDL
   , is from Perl */
<sqbracket>","|".."|":"|"to"	return token::OP_SQBKT_SEP;

137
138
139
140
  /* In SVA you use [=1:$] instead of [=1..].  We will also accept
     [=1..$] and [=1:].  The PSL LRM shows examples like [=1:inf]
     instead, so will accept this too.  */
<sqbracket>"$"|"inf"		return token::OP_UNBOUNDED;
141

142
143
  /* & and | come from Spin.  && and || from LTL2BA.
     /\, \/, and xor are from LBTT.
144
     --> and <--> come from Goal.  */
145
146
"||"|"|"|"+"|"\\/"|"∨"|"∪"	BEGIN(0); return token::OP_OR;
"&&"|"/\\"|"∧"|"∩"		BEGIN(0); return token::OP_AND;
147
"&"				BEGIN(0); return token::OP_SHORT_AND;
148
149
150
"^"|"xor"|"⊕"			BEGIN(0); return token::OP_XOR;
{ARROWL}|{DARROWL}		BEGIN(0); return token::OP_IMPLIES;
{ARROWLR}|{DARROWLR}		BEGIN(0); return token::OP_EQUIV;
151
152

  /* <>, [], and () are used in Spin.  */
153
154
"F"|{DIAMOND}			BEGIN(0); return token::OP_F;
"G"|{BOX}			BEGIN(0); return token::OP_G;
155
156
"U"				BEGIN(0); return token::OP_U;
"R"|"V"				BEGIN(0); return token::OP_R;
157
"X"|{CIRCLE}			BEGIN(0); return token::OP_X;
158
159
"W"				BEGIN(0); return token::OP_W;
"M"				BEGIN(0); return token::OP_M;
160

161
162
"=0"				return token::OP_POST_NEG;
"=1"				return token::OP_POST_POS;
163

164
<*>[ \t\n]+			/* discard whitespace */ yylloc->step ();
165

166
  /* An Atomic proposition cannot start with the letter
167
168
     used by a unary operator (F,G,X), unless this
     letter is followed by a digit in which case we assume
169
     it's an ATOMIC_PROP (even though F0 could be seen as Ffalse, we
170
     don't, because Ffalse is never used in practice).
171
  */
172
173
<INITIAL>[a-zA-EH-WYZ_.][a-zA-Z0-9_.]* |
<INITIAL>[FGX][0-9][a-zA-Z0-9_.]* |
174
  /*
175
176
177
178
179
180
181
182
183
     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.
184

185
     We also disable atomic proposition that may look like a combination
186
187
188
     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)))'.
  */
189
190
<not_prop>[a-zA-EH-LN-QSTYZ_.][a-zA-EH-WYZ0-9_.]* |
<not_prop>[a-zA-EH-LN-QSTYZ_.][a-zA-EH-WYZ0-9_.][a-zA-Z0-9_.]* {
191
			  yylval->str = new std::string(yytext, yyleng);
192
			  BEGIN(not_prop);
193
			  return token::ATOMIC_PROP;
194
			}
195

196
  /* Atomic propositions can also be enclosed in double quotes.  */
197
198
\"[^\"]*\"		{
			  yylval->str = new std::string(yytext + 1,
199
							yyleng - 2);
200
			  BEGIN(not_prop);
201
			  return token::ATOMIC_PROP;
202
			}
203

204
<*>.			return *yytext;
205

206
<<EOF>>			return token::END_OF_INPUT;
207
208
209
210
211

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