ltlscan.ll 1.66 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
%option noyywrap

%{
#include <string>
#include "parsedecl.hh"

/* Hack Flex so we read from a string instead of reading from a file.  */
# define YY_INPUT(buf, result, max_size)				\
  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 \
    yylloc->columns (yyleng);

static const char *to_parse = 0;
static int to_parse_size = 0;
  
void
flex_set_buffer(const char *buf)
{
  to_parse = buf;
  to_parse_size = strlen(to_parse);
}

%}

%%

%{
  yylloc->step ();
%}

37
38
"("			return PAR_OPEN;
")"			return PAR_CLOSE;
39

40
41
42
43
44
45
46
"!"			return OP_NOT;
  /* & and | come from Spin.  && and || from LTL2BA.  */
"||"|"|"|"+"		return OP_OR;
"&&"|"&"|"."|"*"	return OP_AND;
"^"			return OP_XOR;
"=>"|"->"		return OP_IMPLIES;
"<=>"|"<->"		return OP_EQUIV;
47
48

  /* <>, [], and () are used in Spin.  */
49
50
51
52
53
"F"|"<>"		return OP_F;
"G"|"[]"		return OP_G;
"U"			return OP_U;
"R"|"V"			return OP_R;
"X"|"()"		return OP_X;
54

55
56
"1"|"true"		return CONST_TRUE;
"0"|"false"		return CONST_FALSE;
57

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

60
  /* An Atomic proposition cannot start with the letter
61
62
63
64
65
66
67
68
69
70
71
72
     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).  */
[a-zA-EH-WYZ_][a-zA-Z0-9_]* | 
[FGX][0-9_][a-zA-Z0-9_]* { 
		  yylval->str = new std::string(yytext); 
	          return ATOMIC_PROP;
		}

.		return *yytext;

<<EOF>>		return END_OF_INPUT;
73
74
75
76
77

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