ltlscan.ll 2.86 KB
Newer Older
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
/* Copyright (C) 2003  Laboratoire d'Informatique de Paris 6 (LIP6),
** 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.
*/
22
%option noyywrap
23
24
%option prefix="ltlyy"
%option outfile="lex.yy.c"
25
26
27

%{
#include <string>
28
#include "ltlparse/parsedecl.hh"
29
30

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

42
static const char* to_parse = 0;
43
static size_t to_parse_size = 0;
44

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

%}

%%

%{
57
  yylloc->step();
58
59
%}

60
61
"("			return PAR_OPEN;
")"			return PAR_CLOSE;
62

63
"!"			return OP_NOT;
64
65
  /* & and | come from Spin.  && and || from LTL2BA.
     /\, \/, and xor are from LBTT.
66
67
68
69
  */
"||"|"|"|"+"|"\\/"	return OP_OR;
"&&"|"&"|"."|"*"|"/\\"	return OP_AND;
"^"|"xor"		return OP_XOR;
70
71
"=>"|"->"		return OP_IMPLIES;
"<=>"|"<->"		return OP_EQUIV;
72
73

  /* <>, [], and () are used in Spin.  */
74
75
76
77
78
"F"|"<>"		return OP_F;
"G"|"[]"		return OP_G;
"U"			return OP_U;
"R"|"V"			return OP_R;
"X"|"()"		return OP_X;
79

80
81
"1"|"true"		return CONST_TRUE;
"0"|"false"		return CONST_FALSE;
82

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

85
  /* An Atomic proposition cannot start with the letter
86
87
     used by a unary operator (F,G,X), unless this
     letter is followed by a digit in which case we assume
88
89
     it's an ATOMIC_PROP (even though F0 could be seen as Ffalse, we
     don't).  */
90
91
92
93
94
95
[a-zA-EH-WYZ_][a-zA-Z0-9_]* |
[FGX][0-9_][a-zA-Z0-9_]* {
		  yylval->str = new std::string(yytext);
	          return ATOMIC_PROP;
		}

96
  /* Atomic propositions can also be enclosed in double quotes.  */
97
98
\"[^\"]*\"	{
		  yylval->str = new std::string(yytext + 1, yyleng - 2);
99
100
101
102
103
104
	          return ATOMIC_PROP;
		}

.		return *yytext;

<<EOF>>		return END_OF_INPUT;
105
106
107
108
109

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