source: vis_dev/vis-2.3/src/ctlp/ctlp.y

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

vis2.3
File size: 10.5 KB
Line 
1%{
2/**CFile*****************************************************************
3
4  FileName    [ctlp.y]
5
6  PackageName [ctlp]
7
8  Synopsis    [Yacc for CTL formula parser.]
9
10  SeeAlso     [ctlp.h]
11
12  Author      [Gary York, Ramin Hojati, Tom Shiple, Yuji Kukimoto
13               Jae-Young Jang, In-Ho Moon]
14
15  Copyright   [Copyright (c) 1994-1996 The Regents of the Univ. of California.
16  All rights reserved.
17
18  Permission is hereby granted, without written agreement and without license
19  or royalty fees, to use, copy, modify, and distribute this software and its
20  documentation for any purpose, provided that the above copyright notice and
21  the following two paragraphs appear in all copies of this software.
22
23  IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR
24  DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT
25  OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF
26  CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
27
28  THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES,
29  INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
30  FITNESS FOR A PARTICULAR PURPOSE.  THE SOFTWARE PROVIDED HEREUNDER IS ON AN
31  "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE
32  MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]
33
34******************************************************************************/
35
36#include "ctlpInt.h"
37
38/*
39 * The following is a workaround for a bug in bison, which generates code
40 * that uses alloca().  Their lengthy sequence of #ifdefs for defining
41 * alloca() does the wrong thing for HPUX (it should do what is defined below)
42 */
43#ifdef __hpux
44#  include <alloca.h>
45#endif
46
47static char rcsid[] UNUSED = "$Id: ctlp.y,v 1.20 2010/04/09 23:30:23 fabio Exp $";
48
49/*---------------------------------------------------------------------------*/
50/* Variable declarations                                                     */
51/*---------------------------------------------------------------------------*/
52
53#include "ctlpLex.c"
54
55%}
56
57/*---------------------------------------------------------------------------*/
58/*      Grammar declarations                                                 */
59/*---------------------------------------------------------------------------*/
60
61%union {
62  Ctlp_Formula_t *sf;   /* state formula */
63  char *str;
64}
65
66%type <sf> error stateformula formula
67%type <str> name name_vector name_union name_or macro ax_mult ex_mult
68
69/* %token YYERROR_VERBOSE */
70
71%token TOK_DEFINE
72%token TOK_MACRO
73%token TOK_ID
74%token TOK_ID2
75%token TOK_ID_VECTOR
76%token TOK_ID_UNION
77%token TOK_COMMA
78%token TOK_EQIV
79%token TOK_FORALL
80%token TOK_EXISTS
81%token TOK_UNTIL
82%token TOK_FORALL_NEXT
83%token TOK_FORALL_EVENTUALLY
84%token TOK_FORALL_GLOBALLY
85%token TOK_EXISTS_NEXT
86%token TOK_EXISTS_EVENTUALLY
87%token TOK_EXISTS_GLOBALLY
88%token TOK_FORALL_NEXT_MULT
89%token TOK_EXISTS_NEXT_MULT
90%token TOK_THEN
91%token TOK_EQ
92%token TOK_XOR
93%token TOK_AND
94%token TOK_OR
95%token TOK_NOT
96%token TOK_ASSIGN
97%token TOK_TRUE
98%token TOK_FALSE
99
100/* precedence is specified here from lowest to highest */
101%nonassoc TOK_UNTIL
102%left TOK_THEN
103%left TOK_EQ
104%left TOK_XOR
105%left TOK_OR
106%left TOK_AND
107%nonassoc TOK_FORALL_NEXT TOK_FORALL_EVENTUALLY TOK_FORALL_GLOBALLY TOK_EXISTS_NEXT TOK_EXISTS_EVENTUALLY TOK_EXISTS_GLOBALLY
108%nonassoc TOK_NOT
109
110%%
111
112/*---------------------------------------------------------------------------*/
113/*      Grammar rules                                                        */
114/*---------------------------------------------------------------------------*/
115formulas     : /* nothing */
116             | formulas formula
117             ;
118
119formula : stateformula ';'
120               { CtlpFormulaAddToGlobalArray($1);
121                       $$ = $1;
122           /*
123            * The formula is echoed by the lexical analyzer to stdout.
124            * Here we are just printing the line number after it.
125            */
126           CtlpGlobalFormula = NIL(Ctlp_Formula_t);
127         }
128       | TOK_DEFINE name stateformula
129         { if (!CtlpFormulaAddToTable($2, $3, CtlpMacroTable)){
130             CtlpYyerror("** ctl error : MACRO ERROR");
131                         (void) fprintf(vis_stderr, "Macro \"%s\" is already in table.\n\n",$2);
132             Ctlp_FormulaFree(CtlpGlobalFormula);
133             $$ = NULL;
134           }else{
135             $$ = $3;
136           }
137           CtlpGlobalFormula = NIL(Ctlp_Formula_t);
138         }
139             | error ';'
140               { $$ = NULL;
141           /*
142            * Error was detected reading the formula. Garbage collect
143            * and print error message.
144            */
145                       Ctlp_FormulaFree(CtlpGlobalFormula);
146                       (void) fprintf(vis_stderr, "** ctl error : Invalid CTL formula, line %d\n\n", CtlpYylineno);
147           CtlpGlobalFormula = NIL(Ctlp_Formula_t);
148         }
149             ;
150
151stateformula : '(' stateformula ')'
152       { $$ = $2;
153         CtlpGlobalFormula= $$;}
154     | TOK_EXISTS '(' stateformula TOK_UNTIL stateformula ')'
155       { $$ = Ctlp_FormulaCreate(Ctlp_EU_c, $3, $5);
156         CtlpGlobalFormula= $$; }
157     | TOK_EXISTS_NEXT stateformula
158       { $$ = Ctlp_FormulaCreate(Ctlp_EX_c, $2, NIL(Ctlp_Formula_t));
159         CtlpGlobalFormula= $$;}
160     | ex_mult '(' stateformula ')'
161       { $$ = Ctlp_FormulaCreateEXMult($1, $3);
162         if ($$ == NIL(Ctlp_Formula_t)){
163            CtlpYyerror("** ctl error : MULTIPLE EX ERROR");
164            (void) fprintf(vis_stderr,"Error during parsing line %d.\n\n", CtlpYylineno);
165            Ctlp_FormulaFree(CtlpGlobalFormula);
166         }
167         FREE($1);
168         CtlpGlobalFormula= $$;
169       }
170     | TOK_EXISTS_EVENTUALLY stateformula
171       { $$ = Ctlp_FormulaCreate(Ctlp_EF_c, $2, NIL(Ctlp_Formula_t));
172         CtlpGlobalFormula= $$; }
173     | TOK_EXISTS_GLOBALLY stateformula
174       { $$ = Ctlp_FormulaCreate(Ctlp_EG_c, $2, NIL(Ctlp_Formula_t));
175         CtlpGlobalFormula= $$;}
176     | TOK_FORALL '(' stateformula TOK_UNTIL stateformula ')'
177       { $$ = Ctlp_FormulaCreate(Ctlp_AU_c, $3, $5);
178         CtlpGlobalFormula= $$; }
179     | TOK_FORALL_NEXT stateformula
180       { $$ = Ctlp_FormulaCreate(Ctlp_AX_c, $2, NIL(Ctlp_Formula_t));
181         CtlpGlobalFormula= $$; }
182     | ax_mult '(' stateformula ')'
183       { $$ = Ctlp_FormulaCreateAXMult($1, $3);
184         if ($$ == NIL(Ctlp_Formula_t)){
185            CtlpYyerror("** ctl error : MULTIPLE AX ERROR");
186            (void) fprintf(vis_stderr,"Error during parsing line %d.\n\n", CtlpYylineno);
187            Ctlp_FormulaFree(CtlpGlobalFormula);
188         }
189         FREE($1);
190         CtlpGlobalFormula= $$;
191       }
192     | TOK_FORALL_EVENTUALLY stateformula
193       { $$ = Ctlp_FormulaCreate(Ctlp_AF_c, $2, NIL(Ctlp_Formula_t));
194         CtlpGlobalFormula= $$; }
195     | TOK_FORALL_GLOBALLY stateformula
196       { $$ = Ctlp_FormulaCreate(Ctlp_AG_c, $2, NIL(Ctlp_Formula_t));
197         CtlpGlobalFormula= $$; }
198     | stateformula TOK_AND stateformula
199       { $$ = Ctlp_FormulaCreate(Ctlp_AND_c, $1, $3);
200         CtlpGlobalFormula= $$; }
201     | stateformula TOK_OR stateformula
202       { $$ = Ctlp_FormulaCreate(Ctlp_OR_c, $1, $3);
203         CtlpGlobalFormula= $$; }
204     | TOK_NOT stateformula
205       { $$ = Ctlp_FormulaCreate(Ctlp_NOT_c, $2, NIL(Ctlp_Formula_t));
206         CtlpGlobalFormula= $$; }
207     | stateformula TOK_THEN stateformula
208       { $$ = Ctlp_FormulaCreate(Ctlp_THEN_c, $1, $3);
209         CtlpGlobalFormula= $$; }
210     | stateformula TOK_EQ stateformula
211       { $$ = Ctlp_FormulaCreate(Ctlp_EQ_c, $1, $3);
212         CtlpGlobalFormula= $$; }
213     | stateformula TOK_XOR stateformula
214       { $$ = Ctlp_FormulaCreate(Ctlp_XOR_c, $1, $3);
215         CtlpGlobalFormula= $$; }
216     | name TOK_ASSIGN name
217       { $$ = Ctlp_FormulaCreate(Ctlp_ID_c, $1, $3);
218         CtlpGlobalFormula= $$; }
219     | name TOK_ASSIGN name_union
220       { $$ = Ctlp_FormulaCreateOr($1, $3);
221         FREE($1);
222         FREE($3);
223         CtlpGlobalFormula= $$; }
224     | name_vector TOK_ASSIGN name
225       { $$ = Ctlp_FormulaCreateVectorAnd($1, $3);
226         if ($$ == NIL(Ctlp_Formula_t)){
227            CtlpYyerror("** ctl error : Matching ERROR");
228            (void) fprintf(vis_stderr,"LHS token is not matched to RHS token, line %d.\n\n", CtlpYylineno);
229            Ctlp_FormulaFree(CtlpGlobalFormula);
230         }
231         FREE($1);
232         FREE($3);
233         CtlpGlobalFormula= $$;
234       }
235     | name_vector TOK_ASSIGN name_union
236       { $$ = Ctlp_FormulaCreateVectorOr($1, $3);
237         if ($$ == NIL(Ctlp_Formula_t)){
238            CtlpYyerror("** ctl error : Matching ERROR");
239            (void) fprintf(vis_stderr,"LHS token is not matched to RHS token, line %d\n\n", CtlpYylineno);
240            Ctlp_FormulaFree(CtlpGlobalFormula);
241         }
242         FREE($1);
243         FREE($3);
244         CtlpGlobalFormula= $$; }
245     | name TOK_EQIV name
246       { $$ = Ctlp_FormulaCreateEquiv($1, $3);
247         if ($$ == NIL(Ctlp_Formula_t)){
248            CtlpYyerror("** ctl error : Matching ERROR");
249            (void) fprintf(vis_stderr,"LHS token is not matched to RHS token, line %d.\n\n", CtlpYylineno);
250            Ctlp_FormulaFree(CtlpGlobalFormula);
251         }
252         FREE($1);
253         FREE($3);
254         CtlpGlobalFormula= $$;
255       }
256     | name_vector TOK_EQIV name_vector
257       { $$ = Ctlp_FormulaCreateVectorEquiv($1, $3);
258         FREE($1);
259         FREE($3);
260         CtlpGlobalFormula= $$; }
261     | name TOK_ASSIGN TOK_FORALL
262       { $$ = Ctlp_FormulaCreate(Ctlp_ID_c, $1, util_strsav("A"));
263         CtlpGlobalFormula= $$; }
264     | name TOK_ASSIGN TOK_EXISTS
265       { $$ = Ctlp_FormulaCreate(Ctlp_ID_c, $1, util_strsav("E"));
266         CtlpGlobalFormula= $$; }
267     | name TOK_ASSIGN TOK_UNTIL
268       { $$ = Ctlp_FormulaCreate(Ctlp_ID_c, $1, util_strsav("U"));
269         CtlpGlobalFormula= $$; }
270     | TOK_FORALL TOK_ASSIGN name
271       { $$ = Ctlp_FormulaCreate(Ctlp_ID_c, util_strsav("A"), $3);
272         CtlpGlobalFormula= $$; }
273     | TOK_EXISTS TOK_ASSIGN name
274       { $$ = Ctlp_FormulaCreate(Ctlp_ID_c, util_strsav("E"), $3);
275         CtlpGlobalFormula= $$; }
276     | TOK_UNTIL TOK_ASSIGN name
277       { $$ = Ctlp_FormulaCreate(Ctlp_ID_c, util_strsav("U"), $3);
278         CtlpGlobalFormula= $$; }
279     | TOK_TRUE
280       { $$ = Ctlp_FormulaCreate(Ctlp_TRUE_c, NIL(Ctlp_Formula_t), NIL(Ctlp_Formula_t));
281         CtlpGlobalFormula= $$; }
282     | TOK_FALSE
283       { $$ = Ctlp_FormulaCreate(Ctlp_FALSE_c, NIL(Ctlp_Formula_t), NIL(Ctlp_Formula_t));
284         CtlpGlobalFormula= $$; }
285     | macro
286       { $$ = CtlpFormulaFindInTable($1, CtlpMacroTable);
287         if ($$ == NIL(Ctlp_Formula_t)){
288            CtlpYyerror("** ctl error : Macro Error");
289            (void) fprintf(vis_stderr,"Macro \"%s\" is not defined.\n\n",$1);
290         }
291         FREE($1);
292         CtlpGlobalFormula= $$;
293       };
294
295name:  TOK_ID
296       { $$ = util_strsav(CtlpYytext); }
297     | TOK_ID2
298       { (void) CtlpChangeBracket(CtlpYytext);
299         $$ = util_strsav(CtlpYytext); };
300
301name_vector: TOK_ID_VECTOR
302       { $$ = util_strsav(CtlpYytext); };
303
304name_union: '{' name_or '}'
305       { $$ = $2; };
306
307name_or: name
308       { $$ = $1; }
309      |  name_or TOK_COMMA name
310       { $$ = util_strcat3($1,",",$3);
311         FREE($1);
312         FREE($3);
313       }
314      ;
315
316macro: TOK_MACRO name
317       { $$ = $2; } ;
318
319ax_mult: TOK_FORALL_NEXT_MULT
320       { $$ = util_strsav(CtlpYytext); } ;
321ex_mult: TOK_EXISTS_NEXT_MULT
322       { $$ = util_strsav(CtlpYytext); } ;
323%%
Note: See TracBrowser for help on using the repository browser.