Context Navigation

← Previous Revision
Latest Revision
Next Revision →
Blame
Revision Log

ctlsp.y @ 44

Last change on this file since 44 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	/---------------------------------------------------------------------------/
109	formulas : /* nothing */
110	\| formulas formula
111	;
112
113	formula : 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
155	CTLsFormula : 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
447	propformula: '(' 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
587	name: TOK_ID
588	{ $$ = util_strsav(CtlspYytext); }
589	\| TOK_ID2
590	{ (void) CtlspChangeBracket(CtlspYytext);
591	$$ = util_strsav(CtlspYytext); };
592	name_vector: TOK_ID_VECTOR
593	{ $$ = util_strsav(CtlspYytext); };
594
595	name_union: '{' name_or '}'
596	{ $$ = $2; };
597	name_or: name
598	{ $$ = $1; }
599	\| name_or TOK_COMMA name
600	{ $$ = util_strcat3($1,",",$3);
601	FREE($1);
602	FREE($3);
603	}
604	;
605
606	macro: TOK_MACRO name
607	{ $$ = $2; } ;
608
609	x_mult: TOK_NEXT_MULT
610	{ $$ = util_strsav(CtlspYytext); } ;
611
612	ax_mult: TOK_FORALL_NEXT_MULT
613	{ $$ = util_strsav(CtlspYytext); } ;
614
615	ex_mult: TOK_EXISTS_NEXT_MULT
616	{ $$ = util_strsav(CtlspYytext); } ;
617	%%

Note: See TracBrowser for help on using the repository browser.

Download in other formats:

Original Format