source: vis_dev/vis-2.3/src/ctlsp/ctlsp.y @ 17

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

vis2.3
File size: 19.9 KB
Line 
1%{
2/**CFile*****************************************************************
3
4  FileName    [ctlsp.y]
5
6  PackageName [ctlsp]
7
8  Synopsis    [Yacc for CTL* formula parser.]
9
10  SeeAlso     [ctlsp.h]
11
12  Author      [Mohammad Awedh]
13
14  Copyright   [This file was created at the University of Colorado at Boulder.
15  The University of Colorado at Boulder makes no warranty about the suitability
16  of this software for any purpose.  It is presented on an AS IS basis.]
17
18******************************************************************************/
19
20#include "ctlspInt.h"
21
22/*
23 * The following is a workaround for a bug in bison, which generates code
24 * that uses alloca().  Their lengthy sequence of #ifdefs for defining
25 * alloca() does the wrong thing for HPUX (it should do what is defined below)
26 */
27#ifdef __hpux
28#  include <alloca.h>
29#endif
30
31/*---------------------------------------------------------------------------*/
32/* Variable declarations                                                     */
33/*---------------------------------------------------------------------------*/
34
35#include "ctlspLex.c"
36
37/*---------------------------------------------------------------------------*/
38/* Macro declarations                                                        */
39/*---------------------------------------------------------------------------*/
40
41%}
42
43/*---------------------------------------------------------------------------*/
44/*      Grammar declarations                                                 */
45/*---------------------------------------------------------------------------*/
46
47%union {
48  Ctlsp_Formula_t *sf;  /* state formula */
49  char *str;
50}
51
52%type <sf> error formula propformula CTLsFormula
53%type <str> name name_vector name_union name_or macro x_mult ax_mult ex_mult
54
55/* %token YYERROR_VERBOSE */
56
57%token TOK_DEFINE
58%token TOK_MACRO
59%token TOK_ID
60%token TOK_ID2
61%token TOK_ID_VECTOR
62%token TOK_ID_UNION
63%token TOK_COMMA
64%token TOK_EQIV
65%token TOK_FORALL
66%token TOK_EXISTS
67%token TOK_UNTIL
68%token TOK_RELEASE
69%token TOK_WEAK_UNTIL
70%token TOK_NEXT
71%token TOK_EVENTUALLY
72%token TOK_GLOBALLY
73%token TOK_FORALL_NEXT
74%token TOK_FORALL_EVENTUALLY
75%token TOK_FORALL_GLOBALLY
76%token TOK_EXISTS_NEXT
77%token TOK_EXISTS_EVENTUALLY
78%token TOK_EXISTS_GLOBALLY
79%token TOK_NEXT_MULT
80%token TOK_FORALL_NEXT_MULT
81%token TOK_EXISTS_NEXT_MULT
82%token TOK_THEN
83%token TOK_EQ
84%token TOK_XOR
85%token TOK_AND
86%token TOK_OR
87%token TOK_NOT
88%token TOK_ASSIGN
89%token TOK_TRUE
90%token TOK_FALSE
91
92/* precedence is specified here from lowest to highest */
93
94%nonassoc TOK_UNTIL TOK_RELEASE TOK_WEAK_UNTIL
95%left TOK_THEN
96%left TOK_EQ
97%left TOK_XOR
98%left TOK_OR
99%left TOK_AND
100%nonassoc TOK_NEXT TOK_EVENTUALLY TOK_GLOBALLY
101%nonassoc  TOK_FORALL TOK_EXISTS TOK_FORALL_EVENTUALLY TOK_FORALL_GLOBALLY TOK_EXISTS_NEXT TOK_EXISTS_EVENTUALLY TOK_EXISTS_GLOBALLY
102%nonassoc TOK_NOT
103
104%%
105
106/*---------------------------------------------------------------------------*/
107/*      Grammar rules                                                        */
108/*---------------------------------------------------------------------------*/
109formulas     : /* nothing */
110             | formulas formula
111             ;
112
113formula : CTLsFormula ';'
114        {
115          if  (Ctlsp_FormulaReadClass($1) == Ctlsp_pathformula_c )
116            {
117             Ctlsp_FormulaFree(CtlspGlobalFormula);
118             (void) fprintf(vis_stderr, "** CTL * error : Invalid CTL* formula (it is path formula) , line %d\n\n", CtlspYylineno);
119             CtlspGlobalFormula = NIL(Ctlsp_Formula_t);
120            }
121          else
122            {
123             CtlspFormulaAddToGlobalArray($1);
124             $$ = $1;
125             /*
126              * The formula is echoed by the lexical analyzer to stdout.
127              * Here we are just printing the line number after it.
128              */
129              CtlspGlobalFormula = NIL(Ctlsp_Formula_t);
130            }
131         }
132        | TOK_DEFINE name CTLsFormula
133          { if (!CtlspFormulaAddToTable($2, $3, CtlspMacroTable)){
134             CtlspYyerror("** CTL* error : MACRO ERROR");
135             (void) fprintf(vis_stderr, "Macro \"%s\" is already in table.\n\n",$2);
136             Ctlsp_FormulaFree(CtlspGlobalFormula);
137             $$ = NULL;
138           }else{
139             $$ = $3;
140          }
141           CtlspGlobalFormula = NIL(Ctlsp_Formula_t);
142         }
143        | error ';'
144          { $$ = NULL;
145           /*
146            * Error was detected reading the formula. Garbage collect
147            * and print error message.
148            */
149            Ctlsp_FormulaFree(CtlspGlobalFormula);
150            (void) fprintf(vis_stderr, "** ctl* error : Invalid CTL* formula, line %d\n\n", CtlspYylineno);
151            CtlspGlobalFormula = NIL(Ctlsp_Formula_t);
152         }
153         ;
154
155CTLsFormula : propformula
156             {
157                Ctlsp_FormulaSetClass($1, Ctlsp_propformula_c);
158                Ctlsp_FormulaSetClassOfCTL($1, Ctlsp_CTL_c);
159                $$ = $1;
160                CtlspGlobalFormula= $$;
161              }
162             | '(' CTLsFormula ')'
163              {
164                /*Ctlsp_FormulaSetClass($2,  Ctlsp_FormulaReadClass($2));
165                  do nothing, and the formula keeps its old class
166                */
167                $$ = $2;
168                CtlspGlobalFormula= $$;
169              }
170             | TOK_NOT CTLsFormula
171               { $$ = Ctlsp_FormulaCreate(Ctlsp_NOT_c, $2, NIL(Ctlsp_Formula_t));
172                 Ctlsp_FormulaSetClass($$, Ctlsp_FormulaReadClass($2));
173                 Ctlsp_FormulaSetClassOfCTL($$, Ctlsp_FormulaReadClassOfCTL($2));
174                 CtlspGlobalFormula= $$;
175               }
176             |  CTLsFormula TOK_AND CTLsFormula
177               { $$ = Ctlsp_FormulaCreate(Ctlsp_AND_c, $1, $3);
178                 Ctlsp_FormulaSetClass($$, table1(Ctlsp_FormulaReadClass($1),Ctlsp_FormulaReadClass($3)) );
179                 if ((Ctlsp_FormulaReadClassOfCTL($1) ==  Ctlsp_CTL_c) && (Ctlsp_FormulaReadClassOfCTL($3) == Ctlsp_CTL_c))
180                   {
181                     Ctlsp_FormulaSetClassOfCTL($$, Ctlsp_CTL_c);
182                   }
183                 else
184                     Ctlsp_FormulaSetClassOfCTL($$, Ctlsp_NotCTL_c);
185
186                 CtlspGlobalFormula= $$;
187               }
188             | CTLsFormula TOK_OR CTLsFormula
189               { $$ = Ctlsp_FormulaCreate(Ctlsp_OR_c, $1, $3);
190                 Ctlsp_FormulaSetClass($$, table1(Ctlsp_FormulaReadClass($1),Ctlsp_FormulaReadClass($3)) );
191
192                 if ((Ctlsp_FormulaReadClassOfCTL($1) ==  Ctlsp_CTL_c) && (Ctlsp_FormulaReadClassOfCTL($3) == Ctlsp_CTL_c))
193                   {
194                     Ctlsp_FormulaSetClassOfCTL($$, Ctlsp_CTL_c);
195                   }
196                 else
197                     Ctlsp_FormulaSetClassOfCTL($$, Ctlsp_NotCTL_c);
198
199                 CtlspGlobalFormula= $$;
200               }
201             | CTLsFormula TOK_THEN CTLsFormula
202               { $$ = Ctlsp_FormulaCreate(Ctlsp_THEN_c, $1, $3);
203                 Ctlsp_FormulaSetClass($$, table1(Ctlsp_FormulaReadClass($1),Ctlsp_FormulaReadClass($3)) );
204
205                 if ((Ctlsp_FormulaReadClassOfCTL($1) ==  Ctlsp_CTL_c) && (Ctlsp_FormulaReadClassOfCTL($3) == Ctlsp_CTL_c))
206                   {
207                     Ctlsp_FormulaSetClassOfCTL($$, Ctlsp_CTL_c);
208                   }
209                 else
210                     Ctlsp_FormulaSetClassOfCTL($$, Ctlsp_NotCTL_c);
211
212                 CtlspGlobalFormula= $$;
213               }
214             | CTLsFormula TOK_EQ CTLsFormula
215               { $$ = Ctlsp_FormulaCreate(Ctlsp_EQ_c, $1, $3);
216                 Ctlsp_FormulaSetClass($$, table1(Ctlsp_FormulaReadClass($1),Ctlsp_FormulaReadClass($3)) );
217
218                 if ((Ctlsp_FormulaReadClassOfCTL($1) ==  Ctlsp_CTL_c) && (Ctlsp_FormulaReadClassOfCTL($3) == Ctlsp_CTL_c))
219                   {
220                     Ctlsp_FormulaSetClassOfCTL($$, Ctlsp_CTL_c);
221                   }
222                 else
223                     Ctlsp_FormulaSetClassOfCTL($$, Ctlsp_NotCTL_c);
224
225                 CtlspGlobalFormula= $$;
226               }
227             | CTLsFormula TOK_XOR CTLsFormula
228               { $$ = Ctlsp_FormulaCreate(Ctlsp_XOR_c, $1, $3);
229                 Ctlsp_FormulaSetClass($$, table1(Ctlsp_FormulaReadClass($1),Ctlsp_FormulaReadClass($3)) );
230                 if ((Ctlsp_FormulaReadClassOfCTL($1) ==  Ctlsp_CTL_c) && (Ctlsp_FormulaReadClassOfCTL($3) == Ctlsp_CTL_c))
231                   {
232                     Ctlsp_FormulaSetClassOfCTL($$, Ctlsp_CTL_c);
233                   }
234                 else
235                     Ctlsp_FormulaSetClassOfCTL($$, Ctlsp_NotCTL_c);
236                 CtlspGlobalFormula= $$;
237               }
238
239             | TOK_NEXT CTLsFormula
240               { $$ = Ctlsp_FormulaCreate(Ctlsp_X_c, $2, NIL(Ctlsp_Formula_t));
241                 Ctlsp_FormulaSetClass($$, table2(Ctlsp_FormulaReadClass($2)));
242                 if (Ctlsp_FormulaReadClassOfCTL($2) ==  Ctlsp_CTL_c)
243                   {
244                     Ctlsp_FormulaSetClassOfCTL($$, Ctlsp_PathCTL_c);
245                   }
246                 else
247                     Ctlsp_FormulaSetClassOfCTL($$, Ctlsp_NotCTL_c);
248                 CtlspGlobalFormula= $$;
249               }
250             | TOK_EVENTUALLY CTLsFormula
251               { $$ = Ctlsp_FormulaCreate(Ctlsp_F_c, $2, NIL(Ctlsp_Formula_t));
252                 Ctlsp_FormulaSetClass($$, table2(Ctlsp_FormulaReadClass($2)));
253                 if (Ctlsp_FormulaReadClassOfCTL($2) ==  Ctlsp_CTL_c)
254                   {
255                     Ctlsp_FormulaSetClassOfCTL($$, Ctlsp_PathCTL_c);
256                   }
257                 else
258                     Ctlsp_FormulaSetClassOfCTL($$, Ctlsp_NotCTL_c);
259                 CtlspGlobalFormula= $$;
260               }
261             | TOK_GLOBALLY CTLsFormula
262               { $$ = Ctlsp_FormulaCreate(Ctlsp_G_c, $2, NIL(Ctlsp_Formula_t));
263                 Ctlsp_FormulaSetClass($$, table2(Ctlsp_FormulaReadClass($2)) );
264                 if (Ctlsp_FormulaReadClassOfCTL($2) ==  Ctlsp_CTL_c)
265                   {
266                     Ctlsp_FormulaSetClassOfCTL($$, Ctlsp_PathCTL_c);
267                   }
268                 else
269                     Ctlsp_FormulaSetClassOfCTL($$, Ctlsp_NotCTL_c);
270                 CtlspGlobalFormula= $$;
271               }
272             | CTLsFormula TOK_UNTIL CTLsFormula
273               { $$ = Ctlsp_FormulaCreate(Ctlsp_U_c, $1, $3);
274                 Ctlsp_FormulaSetClass($$, table3(Ctlsp_FormulaReadClass($1),Ctlsp_FormulaReadClass($3)) );
275                 if ((Ctlsp_FormulaReadClassOfCTL($1) ==  Ctlsp_CTL_c) && (Ctlsp_FormulaReadClassOfCTL($3) == Ctlsp_CTL_c))
276                   {
277                     Ctlsp_FormulaSetClassOfCTL($$, Ctlsp_PathCTL_c);
278                   }
279                 else
280                   {
281                     Ctlsp_FormulaSetClassOfCTL($$, Ctlsp_NotCTL_c);
282                   }
283                 CtlspGlobalFormula= $$;
284               }
285             | CTLsFormula TOK_RELEASE CTLsFormula
286               { $$ = Ctlsp_FormulaCreate(Ctlsp_R_c, $1, $3);
287                 Ctlsp_FormulaSetClass($$, table3(Ctlsp_FormulaReadClass($1),Ctlsp_FormulaReadClass($3)) );
288                 if ((Ctlsp_FormulaReadClassOfCTL($1) ==  Ctlsp_CTL_c) && (Ctlsp_FormulaReadClassOfCTL($3) == Ctlsp_CTL_c))
289                   {
290                     Ctlsp_FormulaSetClassOfCTL($$, Ctlsp_PathCTL_c);
291                   }
292                 else
293                   {
294                     Ctlsp_FormulaSetClassOfCTL($$, Ctlsp_NotCTL_c);
295                   }
296                 CtlspGlobalFormula= $$;
297               }
298             | CTLsFormula TOK_WEAK_UNTIL CTLsFormula
299               { $$ = Ctlsp_FormulaCreate(Ctlsp_W_c, $1, $3);
300                 Ctlsp_FormulaSetClass($$, table3(Ctlsp_FormulaReadClass($1),Ctlsp_FormulaReadClass($3)) );
301                 if ((Ctlsp_FormulaReadClassOfCTL($1) ==  Ctlsp_CTL_c) && (Ctlsp_FormulaReadClassOfCTL($3) == Ctlsp_CTL_c))
302                   {
303                     Ctlsp_FormulaSetClassOfCTL($$, Ctlsp_PathCTL_c);
304                   }
305                 else
306                   {
307                     Ctlsp_FormulaSetClassOfCTL($$, Ctlsp_NotCTL_c);
308                   }
309                 CtlspGlobalFormula= $$;
310               }
311             | TOK_EXISTS CTLsFormula
312               { $$ = Ctlsp_FormulaCreate(Ctlsp_E_c, $2, NIL(Ctlsp_Formula_t));
313                 Ctlsp_FormulaSetClass($$, Ctlsp_stateformula_c);
314                 if (Ctlsp_FormulaReadClassOfCTL($2) ==  Ctlsp_PathCTL_c)
315                   {
316                     Ctlsp_FormulaSetClassOfCTL($$, Ctlsp_CTL_c);
317                   }
318                 else
319                   {
320                     Ctlsp_FormulaSetClassOfCTL($$, Ctlsp_NotCTL_c);
321                   }
322                 CtlspGlobalFormula= $$;
323               }
324             |  TOK_EXISTS_NEXT CTLsFormula
325               { $$ = Ctlsp_FormulaCreate(Ctlsp_X_c, $2, NIL(Ctlsp_Formula_t));
326                 Ctlsp_FormulaSetClass($$, table2(Ctlsp_FormulaReadClass($2)));
327                 $$ = Ctlsp_FormulaCreate(Ctlsp_E_c, $$, NIL(Ctlsp_Formula_t));
328                 Ctlsp_FormulaSetClass($$, Ctlsp_stateformula_c);
329                 if (Ctlsp_FormulaReadClassOfCTL($2) ==  Ctlsp_CTL_c)
330                 {
331                   Ctlsp_FormulaSetClassOfCTL($$, Ctlsp_CTL_c);
332                 }
333                 else
334                 {
335                     Ctlsp_FormulaSetClassOfCTL($$, Ctlsp_NotCTL_c);
336                 }
337                 CtlspGlobalFormula= $$;
338               }
339              | ex_mult '(' CTLsFormula ')'
340                 { $$ = Ctlsp_FormulaCreateEXMult($1, $3);
341                   if ($$ == NIL(Ctlsp_Formula_t)){
342                   CtlspYyerror("** ctl* error : MULTIPLE EX ERROR");
343                   (void) fprintf(vis_stderr,"Error during parsing line %d.\n\n", CtlspYylineno);
344                   Ctlsp_FormulaFree(CtlspGlobalFormula);
345                   }
346                   FREE($1);
347                   CtlspGlobalFormula= $$;
348               }
349             | TOK_EXISTS_EVENTUALLY CTLsFormula
350               { $$ = Ctlsp_FormulaCreate(Ctlsp_F_c, $2, NIL(Ctlsp_Formula_t));
351                 Ctlsp_FormulaSetClass($$, table2(Ctlsp_FormulaReadClass($2)));
352                 $$ = Ctlsp_FormulaCreate(Ctlsp_E_c, $$, NIL(Ctlsp_Formula_t));
353                 Ctlsp_FormulaSetClass($$, Ctlsp_stateformula_c);
354                 if (Ctlsp_FormulaReadClassOfCTL($2) ==  Ctlsp_CTL_c)
355                   {
356                     Ctlsp_FormulaSetClassOfCTL($$, Ctlsp_CTL_c);
357                   }
358                 else
359                     Ctlsp_FormulaSetClassOfCTL($$, Ctlsp_NotCTL_c);
360                 CtlspGlobalFormula= $$;
361               }
362             | TOK_EXISTS_GLOBALLY CTLsFormula
363               { $$ = Ctlsp_FormulaCreate(Ctlsp_G_c, $2, NIL(Ctlsp_Formula_t));
364                 Ctlsp_FormulaSetClass($$, table2(Ctlsp_FormulaReadClass($2)));
365                 $$ = Ctlsp_FormulaCreate(Ctlsp_E_c, $$, NIL(Ctlsp_Formula_t));
366                 Ctlsp_FormulaSetClass($$, Ctlsp_stateformula_c);
367                 if (Ctlsp_FormulaReadClassOfCTL($2) ==  Ctlsp_CTL_c)
368                   {
369                     Ctlsp_FormulaSetClassOfCTL($$, Ctlsp_CTL_c);
370                   }
371                 else
372                     Ctlsp_FormulaSetClassOfCTL($$, Ctlsp_NotCTL_c);
373                 CtlspGlobalFormula= $$;
374               }
375             | TOK_FORALL CTLsFormula
376               { $$ = Ctlsp_FormulaCreate(Ctlsp_A_c, $2, NIL(Ctlsp_Formula_t));
377                 Ctlsp_FormulaSetClass($$, Ctlsp_stateformula_c);
378                 if (Ctlsp_FormulaReadClassOfCTL($2) ==  Ctlsp_PathCTL_c)
379                   {
380                     Ctlsp_FormulaSetClassOfCTL($$, Ctlsp_CTL_c);
381                   }
382                 else
383                     Ctlsp_FormulaSetClassOfCTL($$, Ctlsp_NotCTL_c);
384                 CtlspGlobalFormula= $$;
385               }
386             | TOK_FORALL_GLOBALLY CTLsFormula
387               { $$ = Ctlsp_FormulaCreate(Ctlsp_G_c, $2, NIL(Ctlsp_Formula_t));
388                 Ctlsp_FormulaSetClass($$, table2(Ctlsp_FormulaReadClass($2)));
389                 $$ = Ctlsp_FormulaCreate(Ctlsp_A_c, $$, NIL(Ctlsp_Formula_t));
390                 Ctlsp_FormulaSetClass($$, Ctlsp_stateformula_c);
391                 if (Ctlsp_FormulaReadClassOfCTL($2) ==  Ctlsp_CTL_c)
392                   {
393                     Ctlsp_FormulaSetClassOfCTL($$, Ctlsp_CTL_c);
394                   }
395                 else
396                     Ctlsp_FormulaSetClassOfCTL($$, Ctlsp_NotCTL_c);
397                 CtlspGlobalFormula= $$;
398               }
399             | TOK_FORALL_NEXT CTLsFormula
400               { $$ = Ctlsp_FormulaCreate(Ctlsp_X_c, $2, NIL(Ctlsp_Formula_t));
401                 Ctlsp_FormulaSetClass($$, table2(Ctlsp_FormulaReadClass($2)));
402                 $$ = Ctlsp_FormulaCreate(Ctlsp_A_c, $$, NIL(Ctlsp_Formula_t));
403                 Ctlsp_FormulaSetClass($$, Ctlsp_stateformula_c);
404                 if (Ctlsp_FormulaReadClassOfCTL($2) ==  Ctlsp_CTL_c)
405                   {
406                     Ctlsp_FormulaSetClassOfCTL($$, Ctlsp_CTL_c);
407                   }
408                 else
409                     Ctlsp_FormulaSetClassOfCTL($$, Ctlsp_NotCTL_c);
410                 CtlspGlobalFormula= $$;
411               }
412              | ax_mult '(' CTLsFormula ')'
413                 { $$ = Ctlsp_FormulaCreateAXMult($1, $3);
414                   if ($$ == NIL(Ctlsp_Formula_t)){
415                   CtlspYyerror("** ctl* error : MULTIPLE AX ERROR");
416                   (void) fprintf(vis_stderr,"Error during parsing line %d.\n\n", CtlspYylineno);
417                   Ctlsp_FormulaFree(CtlspGlobalFormula);
418                   }
419                   FREE($1);
420                   CtlspGlobalFormula= $$;
421               }
422             | TOK_FORALL_EVENTUALLY CTLsFormula
423               { $$ = Ctlsp_FormulaCreate(Ctlsp_F_c, $2, NIL(Ctlsp_Formula_t));
424                 Ctlsp_FormulaSetClass($$, table2(Ctlsp_FormulaReadClass($2)));
425                 $$ = Ctlsp_FormulaCreate(Ctlsp_A_c, $$, NIL(Ctlsp_Formula_t));
426                 Ctlsp_FormulaSetClass($$, Ctlsp_stateformula_c);
427                 if (Ctlsp_FormulaReadClassOfCTL($2) ==  Ctlsp_CTL_c)
428                   {
429                     Ctlsp_FormulaSetClassOfCTL($$, Ctlsp_CTL_c);
430                   }
431                 else
432                     Ctlsp_FormulaSetClassOfCTL($$, Ctlsp_NotCTL_c);
433                 CtlspGlobalFormula= $$;
434               }
435              | x_mult '(' CTLsFormula ')'
436                 { $$ = Ctlsp_FormulaCreateXMult($1, $3);
437                   if ($$ == NIL(Ctlsp_Formula_t)){
438                   CtlspYyerror("** ctl* error : MULTIPLE X ERROR");
439                   (void) fprintf(vis_stderr,"Error during parsing line %d.\n\n", CtlspYylineno);
440                   Ctlsp_FormulaFree(CtlspGlobalFormula);
441                   }
442                   FREE($1);
443                   CtlspGlobalFormula= $$;
444               }
445         ;
446
447propformula: '(' propformula ')'
448               { $$ = $2;
449                 CtlspGlobalFormula= $$;
450               }
451             | name TOK_ASSIGN name
452             { $$ = Ctlsp_FormulaCreate(Ctlsp_ID_c, $1, $3);
453               CtlspGlobalFormula= $$;
454             }
455             | name TOK_ASSIGN name_union
456             { $$ = Ctlsp_FormulaCreateOr($1, $3);
457               FREE($1);
458               FREE($3);
459               CtlspGlobalFormula= $$;
460             }
461             | name_vector TOK_ASSIGN name
462               { $$ = Ctlsp_FormulaCreateVectorAnd($1, $3);
463                 if ($$ == NIL(Ctlsp_Formula_t))
464                 {
465                  CtlspYyerror("** ctl error : Matching ERROR");
466                  (void) fprintf(vis_stderr,"LHS token is not matched to RHS token, line %d.\n\n", CtlspYylineno);
467                  Ctlsp_FormulaFree(CtlspGlobalFormula);
468                 }
469                 FREE($1);
470                 FREE($3);
471                 CtlspGlobalFormula= $$;
472               }
473             | name_vector TOK_ASSIGN name_union
474               { $$ = Ctlsp_FormulaCreateVectorOr($1, $3);
475                if ($$ == NIL(Ctlsp_Formula_t)){
476                   CtlspYyerror("** ctl error : Matching ERROR");
477                   (void) fprintf(vis_stderr,"LHS token is not matched to RHS token, line %d\n\n", CtlspYylineno);
478                   Ctlsp_FormulaFree(CtlspGlobalFormula);
479                }
480                FREE($1);
481                FREE($3);
482                CtlspGlobalFormula= $$;
483               }
484             | name TOK_EQIV name
485               { $$ = Ctlsp_FormulaCreateEquiv($1, $3);
486                 if ($$ == NIL(Ctlsp_Formula_t)){
487                   CtlspYyerror("** ctl error : Matching ERROR");
488                   (void) fprintf(vis_stderr,"LHS token is not matched to RHS token, line %d.\n\n", CtlspYylineno);
489                   Ctlsp_FormulaFree(CtlspGlobalFormula);
490                 }
491                 FREE($1);
492                 FREE($3);
493                 CtlspGlobalFormula= $$;
494               }
495             | name_vector TOK_EQIV name_vector
496               { $$ = Ctlsp_FormulaCreateVectorEquiv($1, $3);
497                 FREE($1);
498                 FREE($3);
499                 CtlspGlobalFormula= $$;
500               }
501             | name TOK_ASSIGN TOK_FORALL
502               { $$ = Ctlsp_FormulaCreate(Ctlsp_ID_c, $1, util_strsav("A"));
503                 CtlspGlobalFormula= $$;
504               }
505             | name TOK_ASSIGN TOK_EXISTS
506               { $$ = Ctlsp_FormulaCreate(Ctlsp_ID_c, $1, util_strsav("E"));
507                 CtlspGlobalFormula= $$;
508               }
509             | name TOK_ASSIGN TOK_EVENTUALLY
510               { $$ = Ctlsp_FormulaCreate(Ctlsp_ID_c, $1, util_strsav("F"));
511                 CtlspGlobalFormula= $$;
512               }
513             | name TOK_ASSIGN TOK_GLOBALLY
514               { $$ = Ctlsp_FormulaCreate(Ctlsp_ID_c, $1, util_strsav("G"));
515                 CtlspGlobalFormula= $$;
516               }
517             | name TOK_ASSIGN TOK_NEXT
518               { $$ = Ctlsp_FormulaCreate(Ctlsp_ID_c, $1, util_strsav("X"));
519                 CtlspGlobalFormula= $$;
520               }
521             | name TOK_ASSIGN TOK_UNTIL
522               { $$ = Ctlsp_FormulaCreate(Ctlsp_ID_c, $1, util_strsav("U"));
523                 CtlspGlobalFormula= $$;
524               }
525             | name TOK_ASSIGN TOK_WEAK_UNTIL
526               { $$ = Ctlsp_FormulaCreate(Ctlsp_ID_c, $1, util_strsav("W"));
527                 CtlspGlobalFormula= $$;
528               }
529             | name TOK_ASSIGN TOK_RELEASE
530               { $$ = Ctlsp_FormulaCreate(Ctlsp_ID_c, $1, util_strsav("R"));
531                 CtlspGlobalFormula= $$;
532               }
533             | TOK_FORALL TOK_ASSIGN name
534               { $$ = Ctlsp_FormulaCreate(Ctlsp_ID_c, util_strsav("A"), $3);
535                 CtlspGlobalFormula= $$;
536               }
537             | TOK_EXISTS TOK_ASSIGN name
538               { $$ = Ctlsp_FormulaCreate(Ctlsp_ID_c, util_strsav("E"), $3);
539                 CtlspGlobalFormula= $$;
540               }
541             | TOK_EVENTUALLY TOK_ASSIGN name
542               { $$ = Ctlsp_FormulaCreate(Ctlsp_ID_c, util_strsav("F"), $3);
543                 CtlspGlobalFormula= $$;
544               }
545             | TOK_GLOBALLY TOK_ASSIGN name
546               { $$ = Ctlsp_FormulaCreate(Ctlsp_ID_c, util_strsav("G"), $3);
547                 CtlspGlobalFormula= $$;
548               }
549             | TOK_NEXT TOK_ASSIGN name
550               { $$ = Ctlsp_FormulaCreate(Ctlsp_ID_c, util_strsav("X"), $3);
551                 CtlspGlobalFormula= $$;
552               }
553             | TOK_UNTIL TOK_ASSIGN name
554               { $$ = Ctlsp_FormulaCreate(Ctlsp_ID_c, util_strsav("U"), $3);
555                 CtlspGlobalFormula= $$;
556               }
557             | TOK_WEAK_UNTIL TOK_ASSIGN name
558               { $$ = Ctlsp_FormulaCreate(Ctlsp_ID_c, util_strsav("W"), $3);
559                 CtlspGlobalFormula= $$;
560               }
561             | TOK_RELEASE TOK_ASSIGN name
562               { $$ = Ctlsp_FormulaCreate(Ctlsp_ID_c, util_strsav("R"), $3);
563                 CtlspGlobalFormula= $$;
564               }
565             | TOK_TRUE
566               { $$ = Ctlsp_FormulaCreate(Ctlsp_TRUE_c, NIL(Ctlsp_Formula_t), NIL(Ctlsp_Formula_t));
567                 CtlspGlobalFormula= $$;
568               }
569             | TOK_FALSE
570               { $$ = Ctlsp_FormulaCreate(Ctlsp_FALSE_c, NIL(Ctlsp_Formula_t), NIL(Ctlsp_Formula_t));
571                 CtlspGlobalFormula= $$;
572               }
573             | macro
574               { $$ = CtlspFormulaFindInTable($1, CtlspMacroTable);
575                 if ($$ == NIL(Ctlsp_Formula_t)){
576                    CtlspYyerror("** ctl* error : Macro Error");
577                    (void) fprintf(vis_stderr,"Macro \"%s\" is not defined.\n\n",$1);
578                    FREE($1);
579                    CtlspGlobalFormula= $$;
580                    YYERROR;
581                 }
582                 FREE($1);
583                 CtlspGlobalFormula= $$;
584
585               };
586
587name:  TOK_ID
588       { $$ = util_strsav(CtlspYytext); }
589     | TOK_ID2
590       { (void) CtlspChangeBracket(CtlspYytext);
591         $$ = util_strsav(CtlspYytext); };
592name_vector: TOK_ID_VECTOR
593       { $$ = util_strsav(CtlspYytext); };
594
595name_union: '{' name_or '}'
596       { $$ = $2; };
597name_or: name
598       { $$ = $1; }
599      |  name_or TOK_COMMA name
600       { $$ = util_strcat3($1,",",$3);
601         FREE($1);
602         FREE($3);
603       }
604      ;
605
606macro: TOK_MACRO name
607       { $$ = $2; } ;
608
609x_mult: TOK_NEXT_MULT
610       { $$ = util_strsav(CtlspYytext); } ;
611
612ax_mult: TOK_FORALL_NEXT_MULT
613       { $$ = util_strsav(CtlspYytext); } ;
614
615ex_mult: TOK_EXISTS_NEXT_MULT
616       { $$ = util_strsav(CtlspYytext); } ;
617%%
Note: See TracBrowser for help on using the repository browser.