source: vis_dev/vis-2.3/src/ctlsp/ctlsp.l @ 23

Last change on this file since 23 was 14, checked in by cecile, 13 years ago

vis2.3

File size: 4.8 KB
Line 
1%{
2/**CFile***********************************************************************
3
4  FileName    [ctlsp.l]
5
6  PackageName [ctlsp]
7
8  Synopsis    [Lexical analyzer for CTL* formula parser.]
9
10  Author      [Mohammad Awedh]
11
12  Copyright   [This file was created at the University of Colorado at Boulder.
13  The University of Colorado at Boulder makes no warranty about the suitability
14  of this software for any purpose.  It is presented on an AS IS basis.]
15
16  Revision    [$Id: ctlsp.l,v 1.4 2010/04/09 23:31:37 fabio Exp $]
17
18******************************************************************************/
19
20#include "ctlspRead.h"
21
22/*---------------------------------------------------------------------------*/
23/* Constant declarations                                                     */
24/*---------------------------------------------------------------------------*/
25
26/*---------------------------------------------------------------------------*/
27/* Variable declarations                                                     */
28/*---------------------------------------------------------------------------*/
29
30
31/**AutomaticStart*************************************************************/
32
33/*---------------------------------------------------------------------------*/
34/* Static function prototypes                                                */
35/*---------------------------------------------------------------------------*/
36
37
38/**AutomaticEnd***************************************************************/
39
40
41/*---------------------------------------------------------------------------*/
42/* Definition of internal functions                                          */
43/*---------------------------------------------------------------------------*/
44
45/**Function********************************************************************
46
47  Synopsis    [Initializes global variables for parsing file.]
48
49  SideEffects []
50
51******************************************************************************/
52void
53CtlspFileSetup(
54  FILE * fp)
55{
56  CtlspYyin             = fp;
57  CtlspYylineno         = 1;
58}
59
60/*---------------------------------------------------------------------------*/
61/* Definition of static functions                                            */
62/*---------------------------------------------------------------------------*/
63
64/**Function********************************************************************
65
66  Synopsis    [Prints error message and sets global error flag.]
67
68  SideEffects []
69
70******************************************************************************/
71static void
72CtlspYyerror(
73  char * errmsg)
74{
75  (void) fprintf(vis_stderr, "%s in line %d with token \"%s\"\n", errmsg, CtlspYylineno, yytext);
76  CtlspGlobalError = 1;
77}
78
79%}
80
81/*---------------------------------------------------------------------------*/
82/*      Lexical analyzer rules                                               */
83/*---------------------------------------------------------------------------*/
84
85%option noyywrap
86%option yylineno
87
88/* substitution strings */
89/* alnum is the same set in alnumsymbol in io.l except [ and ] being removed here for the until and release operators */
90/* - , =, and ; are intentionally removed because:
91   - is used for -> and <->
92   = is used for foo = bar
93   ; is used for delimitters */
94/* ( and ) are intentionally removed since they are used as parentheses */
95/* +, *, and ^ have to be used surrounded by spaces since they are symbols.
96   ! can be attached immediately w/o spaces since it is not a symbol */
97
98alnum   [A-Za-z0-9\^\?\|\/\+\*\$\<\>~@\_#\$%\:\"\'\.]
99
100%%
101
102[ \t\n\r]       ;
103
104"#".*   ;   
105
106A       { return(TOK_FORALL); }
107E       { return(TOK_EXISTS); }
108
109AX      { return(TOK_FORALL_NEXT); }
110EX      { return(TOK_EXISTS_NEXT); }
111AF      { return(TOK_FORALL_EVENTUALLY); }
112EF      { return(TOK_EXISTS_EVENTUALLY); }
113AG      { return(TOK_FORALL_GLOBALLY); }
114EG      { return(TOK_EXISTS_GLOBALLY); }
115
116
117X       { return(TOK_NEXT); }
118F       { return(TOK_EVENTUALLY); }
119G       { return(TOK_GLOBALLY); }
120
121X:[0-9]+  { return(TOK_NEXT_MULT); }
122
123AX:[0-9]+  { return(TOK_FORALL_NEXT_MULT); }
124EX:[0-9]+  { return(TOK_EXISTS_NEXT_MULT); }
125
126U       { return(TOK_UNTIL); }
127R       { return(TOK_RELEASE); }
128W       { return(TOK_WEAK_UNTIL); }
129
130
131TRUE    { return(TOK_TRUE); }
132
133FALSE   { return(TOK_FALSE); }
134
135\\DEFINE |
136\\Define |
137\\define  { return(TOK_DEFINE); }
138
139\+      { return(TOK_OR); }
140\|\|    { return(TOK_OR); }
141\*      { return(TOK_AND); }
142\&\&    { return(TOK_AND); }
143!       { return(TOK_NOT); }
144"^"     { return(TOK_XOR); }
145"->"    { return(TOK_THEN); }
146"<->"   { return(TOK_EQ); }
147=       { return(TOK_ASSIGN); }
148==      { return(TOK_EQIV); }
149\,      { return(TOK_COMMA); }
150\\      { return(TOK_MACRO); }
151
152{alnum}+                                   { return(TOK_ID); }
153{alnum}+\[[ ]*[0-9]+[ ]*\]                 { return(TOK_ID2); }
154{alnum}+\[[ ]*[0-9]+[ ]*\:[ ]*[0-9]+[ ]*\] { return(TOK_ID_VECTOR); }
155
156.       { return CtlspYytext[0]; }
157%%
158
159
160
161
162
163
164
165
166
Note: See TracBrowser for help on using the repository browser.