| 2 |
- |
1 |
/***** spin: spin.y *****/
|
|
|
2 |
|
|
|
3 |
/* Copyright (c) 1989-2003 by Lucent Technologies, Bell Laboratories. */
|
|
|
4 |
/* All Rights Reserved. This software is for educational purposes only. */
|
|
|
5 |
/* No guarantee whatsoever is expressed or implied by the distribution of */
|
|
|
6 |
/* this code. Permission is given to distribute this code provided that */
|
|
|
7 |
/* this introductory message is not removed and no monies are exchanged. */
|
|
|
8 |
/* Software written by Gerard J. Holzmann. For tool documentation see: */
|
|
|
9 |
/* http://spinroot.com/ */
|
|
|
10 |
/* Send all bug-reports and/or questions to: bugs@spinroot.com */
|
|
|
11 |
|
|
|
12 |
%{
|
|
|
13 |
#include "spin.h"
|
|
|
14 |
#include <sys/types.h>
|
|
|
15 |
#ifndef PC
|
|
|
16 |
#include <unistd.h>
|
|
|
17 |
#endif
|
|
|
18 |
#include <stdarg.h>
|
|
|
19 |
|
|
|
20 |
#define YYDEBUG 0
|
|
|
21 |
#define Stop nn(ZN,'@',ZN,ZN)
|
|
|
22 |
#define PART0 "place initialized var decl of "
|
|
|
23 |
#define PART1 "place initialized chan decl of "
|
|
|
24 |
#define PART2 " at start of proctype "
|
|
|
25 |
|
|
|
26 |
static Lextok *ltl_to_string(Lextok *);
|
|
|
27 |
|
|
|
28 |
extern Symbol *context, *owner;
|
|
|
29 |
extern Lextok *for_body(Lextok *, int);
|
|
|
30 |
extern void for_setup(Lextok *, Lextok *, Lextok *);
|
|
|
31 |
extern Lextok *for_index(Lextok *, Lextok *);
|
|
|
32 |
extern Lextok *sel_index(Lextok *, Lextok *, Lextok *);
|
|
|
33 |
extern int u_sync, u_async, dumptab, scope_level;
|
|
|
34 |
extern int initialization_ok, split_decl;
|
|
|
35 |
extern short has_sorted, has_random, has_enabled, has_pcvalue, has_np;
|
|
|
36 |
extern short has_code, has_state, has_io;
|
|
|
37 |
extern void count_runs(Lextok *);
|
|
|
38 |
extern void no_internals(Lextok *);
|
|
|
39 |
extern void any_runs(Lextok *);
|
|
|
40 |
extern void ltl_list(char *, char *);
|
|
|
41 |
extern void validref(Lextok *, Lextok *);
|
|
|
42 |
extern char yytext[];
|
|
|
43 |
|
|
|
44 |
int Mpars = 0; /* max nr of message parameters */
|
|
|
45 |
int nclaims = 0; /* nr of never claims */
|
|
|
46 |
int ltl_mode = 0; /* set when parsing an ltl formula */
|
|
|
47 |
int Expand_Ok = 0, realread = 1, IArgs = 0, NamesNotAdded = 0;
|
|
|
48 |
int in_for = 0;
|
|
|
49 |
char *claimproc = (char *) 0;
|
|
|
50 |
char *eventmap = (char *) 0;
|
|
|
51 |
static char *ltl_name;
|
|
|
52 |
|
|
|
53 |
static int Embedded = 0, inEventMap = 0, has_ini = 0;
|
|
|
54 |
|
|
|
55 |
%}
|
|
|
56 |
|
|
|
57 |
%token ASSERT PRINT PRINTM
|
|
|
58 |
%token C_CODE C_DECL C_EXPR C_STATE C_TRACK
|
|
|
59 |
%token RUN LEN ENABLED EVAL PC_VAL
|
|
|
60 |
%token TYPEDEF MTYPE INLINE LABEL OF
|
|
|
61 |
%token GOTO BREAK ELSE SEMI
|
|
|
62 |
%token IF FI DO OD FOR SELECT IN SEP DOTDOT
|
|
|
63 |
%token ATOMIC NON_ATOMIC D_STEP UNLESS
|
|
|
64 |
%token TIMEOUT NONPROGRESS
|
|
|
65 |
%token ACTIVE PROCTYPE D_PROCTYPE
|
|
|
66 |
%token HIDDEN SHOW ISLOCAL
|
|
|
67 |
%token PRIORITY PROVIDED
|
|
|
68 |
%token FULL EMPTY NFULL NEMPTY
|
|
|
69 |
%token CONST TYPE XU /* val */
|
|
|
70 |
%token NAME UNAME PNAME INAME /* sym */
|
|
|
71 |
%token STRING CLAIM TRACE INIT LTL /* sym */
|
|
|
72 |
|
|
|
73 |
%right ASGN
|
|
|
74 |
%left SND O_SND RCV R_RCV /* SND doubles as boolean negation */
|
|
|
75 |
%left IMPLIES EQUIV /* ltl */
|
|
|
76 |
%left OR
|
|
|
77 |
%left AND
|
|
|
78 |
%left ALWAYS EVENTUALLY /* ltl */
|
|
|
79 |
%left UNTIL WEAK_UNTIL RELEASE /* ltl */
|
|
|
80 |
%right NEXT /* ltl */
|
|
|
81 |
%left '|'
|
|
|
82 |
%left '^'
|
|
|
83 |
%left '&'
|
|
|
84 |
%left EQ NE
|
|
|
85 |
%left GT LT GE LE
|
|
|
86 |
%left LSHIFT RSHIFT
|
|
|
87 |
%left '+' '-'
|
|
|
88 |
%left '*' '/' '%'
|
|
|
89 |
%left INCR DECR
|
|
|
90 |
%right '~' UMIN NEG
|
|
|
91 |
%left DOT
|
|
|
92 |
%%
|
|
|
93 |
|
|
|
94 |
/** PROMELA Grammar Rules **/
|
|
|
95 |
|
|
|
96 |
program : units { yytext[0] = '\0'; }
|
|
|
97 |
;
|
|
|
98 |
|
|
|
99 |
units : unit
|
|
|
100 |
| units unit
|
|
|
101 |
;
|
|
|
102 |
|
|
|
103 |
unit : proc /* proctype { } */
|
|
|
104 |
| init /* init { } */
|
|
|
105 |
| claim /* never claim */
|
|
|
106 |
| ltl /* ltl formula */
|
|
|
107 |
| events /* event assertions */
|
|
|
108 |
| one_decl /* variables, chans */
|
|
|
109 |
| utype /* user defined types */
|
|
|
110 |
| c_fcts /* c functions etc. */
|
|
|
111 |
| ns /* named sequence */
|
|
|
112 |
| SEMI /* optional separator */
|
|
|
113 |
| error
|
|
|
114 |
;
|
|
|
115 |
|
|
|
116 |
proc : inst /* optional instantiator */
|
|
|
117 |
proctype NAME {
|
|
|
118 |
setptype($3, PROCTYPE, ZN);
|
|
|
119 |
setpname($3);
|
|
|
120 |
context = $3->sym;
|
|
|
121 |
context->ini = $2; /* linenr and file */
|
|
|
122 |
Expand_Ok++; /* expand struct names in decl */
|
|
|
123 |
has_ini = 0;
|
|
|
124 |
}
|
|
|
125 |
'(' decl ')' { Expand_Ok--;
|
|
|
126 |
if (has_ini)
|
|
|
127 |
fatal("initializer in parameter list", (char *) 0);
|
|
|
128 |
}
|
|
|
129 |
Opt_priority
|
|
|
130 |
Opt_enabler
|
|
|
131 |
body { ProcList *rl;
|
|
|
132 |
if ($1 != ZN && $1->val > 0)
|
|
|
133 |
{ int j;
|
|
|
134 |
rl = ready($3->sym, $6, $11->sq, $2->val, $10, A_PROC);
|
|
|
135 |
for (j = 0; j < $1->val; j++)
|
|
|
136 |
{ runnable(rl, $9?$9->val:1, 1);
|
|
|
137 |
}
|
|
|
138 |
announce(":root:");
|
|
|
139 |
if (dumptab) $3->sym->ini = $1;
|
|
|
140 |
} else
|
|
|
141 |
{ rl = ready($3->sym, $6, $11->sq, $2->val, $10, P_PROC);
|
|
|
142 |
}
|
|
|
143 |
if (rl && has_ini == 1) /* global initializations, unsafe */
|
|
|
144 |
{ /* printf("proctype %s has initialized data\n",
|
|
|
145 |
$3->sym->name);
|
|
|
146 |
*/
|
|
|
147 |
rl->unsafe = 1;
|
|
|
148 |
}
|
|
|
149 |
context = ZS;
|
|
|
150 |
}
|
|
|
151 |
;
|
|
|
152 |
|
|
|
153 |
proctype: PROCTYPE { $$ = nn(ZN,CONST,ZN,ZN); $$->val = 0; }
|
|
|
154 |
| D_PROCTYPE { $$ = nn(ZN,CONST,ZN,ZN); $$->val = 1; }
|
|
|
155 |
;
|
|
|
156 |
|
|
|
157 |
inst : /* empty */ { $$ = ZN; }
|
|
|
158 |
| ACTIVE { $$ = nn(ZN,CONST,ZN,ZN); $$->val = 1; }
|
|
|
159 |
| ACTIVE '[' CONST ']' {
|
|
|
160 |
$$ = nn(ZN,CONST,ZN,ZN); $$->val = $3->val;
|
|
|
161 |
if ($3->val > 255)
|
|
|
162 |
non_fatal("max nr of processes is 255\n", "");
|
|
|
163 |
}
|
|
|
164 |
| ACTIVE '[' NAME ']' {
|
|
|
165 |
$$ = nn(ZN,CONST,ZN,ZN);
|
|
|
166 |
$$->val = 0;
|
|
|
167 |
if (!$3->sym->type)
|
|
|
168 |
fatal("undeclared variable %s",
|
|
|
169 |
$3->sym->name);
|
|
|
170 |
else if ($3->sym->ini->ntyp != CONST)
|
|
|
171 |
fatal("need constant initializer for %s\n",
|
|
|
172 |
$3->sym->name);
|
|
|
173 |
else
|
|
|
174 |
$$->val = $3->sym->ini->val;
|
|
|
175 |
}
|
|
|
176 |
;
|
|
|
177 |
|
|
|
178 |
init : INIT { context = $1->sym; }
|
|
|
179 |
Opt_priority
|
|
|
180 |
body { ProcList *rl;
|
|
|
181 |
rl = ready(context, ZN, $4->sq, 0, ZN, I_PROC);
|
|
|
182 |
runnable(rl, $3?$3->val:1, 1);
|
|
|
183 |
announce(":root:");
|
|
|
184 |
context = ZS;
|
|
|
185 |
}
|
|
|
186 |
;
|
|
|
187 |
|
|
|
188 |
ltl : LTL optname2 { ltl_mode = 1; ltl_name = $2->sym->name; }
|
|
|
189 |
ltl_body { if ($4) ltl_list($2->sym->name, $4->sym->name);
|
|
|
190 |
ltl_mode = 0;
|
|
|
191 |
}
|
|
|
192 |
;
|
|
|
193 |
|
|
|
194 |
ltl_body: '{' full_expr OS '}' { $$ = ltl_to_string($2); }
|
|
|
195 |
| error { $$ = NULL; }
|
|
|
196 |
;
|
|
|
197 |
|
|
|
198 |
claim : CLAIM optname { if ($2 != ZN)
|
|
|
199 |
{ $1->sym = $2->sym; /* new 5.3.0 */
|
|
|
200 |
}
|
|
|
201 |
nclaims++;
|
|
|
202 |
context = $1->sym;
|
|
|
203 |
if (claimproc && !strcmp(claimproc, $1->sym->name))
|
|
|
204 |
{ fatal("claim %s redefined", claimproc);
|
|
|
205 |
}
|
|
|
206 |
claimproc = $1->sym->name;
|
|
|
207 |
}
|
|
|
208 |
body { (void) ready($1->sym, ZN, $4->sq, 0, ZN, N_CLAIM);
|
|
|
209 |
context = ZS;
|
|
|
210 |
}
|
|
|
211 |
;
|
|
|
212 |
|
|
|
213 |
optname : /* empty */ { char tb[32];
|
|
|
214 |
memset(tb, 0, 32);
|
|
|
215 |
sprintf(tb, "never_%d", nclaims);
|
|
|
216 |
$$ = nn(ZN, NAME, ZN, ZN);
|
|
|
217 |
$$->sym = lookup(tb);
|
|
|
218 |
}
|
|
|
219 |
| NAME { $$ = $1; }
|
|
|
220 |
;
|
|
|
221 |
|
|
|
222 |
optname2 : /* empty */ { char tb[32]; static int nltl = 0;
|
|
|
223 |
memset(tb, 0, 32);
|
|
|
224 |
sprintf(tb, "ltl_%d", nltl++);
|
|
|
225 |
$$ = nn(ZN, NAME, ZN, ZN);
|
|
|
226 |
$$->sym = lookup(tb);
|
|
|
227 |
}
|
|
|
228 |
| NAME { $$ = $1; }
|
|
|
229 |
;
|
|
|
230 |
|
|
|
231 |
events : TRACE { context = $1->sym;
|
|
|
232 |
if (eventmap)
|
|
|
233 |
non_fatal("trace %s redefined", eventmap);
|
|
|
234 |
eventmap = $1->sym->name;
|
|
|
235 |
inEventMap++;
|
|
|
236 |
}
|
|
|
237 |
body {
|
|
|
238 |
if (strcmp($1->sym->name, ":trace:") == 0)
|
|
|
239 |
{ (void) ready($1->sym, ZN, $3->sq, 0, ZN, E_TRACE);
|
|
|
240 |
} else
|
|
|
241 |
{ (void) ready($1->sym, ZN, $3->sq, 0, ZN, N_TRACE);
|
|
|
242 |
}
|
|
|
243 |
context = ZS;
|
|
|
244 |
inEventMap--;
|
|
|
245 |
}
|
|
|
246 |
;
|
|
|
247 |
|
|
|
248 |
utype : TYPEDEF NAME { if (context)
|
|
|
249 |
fatal("typedef %s must be global",
|
|
|
250 |
$2->sym->name);
|
|
|
251 |
owner = $2->sym;
|
|
|
252 |
}
|
|
|
253 |
'{' decl_lst '}' { setuname($5); owner = ZS; }
|
|
|
254 |
;
|
|
|
255 |
|
|
|
256 |
nm : NAME { $$ = $1; }
|
|
|
257 |
| INAME { $$ = $1;
|
|
|
258 |
if (IArgs)
|
|
|
259 |
fatal("invalid use of '%s'", $1->sym->name);
|
|
|
260 |
}
|
|
|
261 |
;
|
|
|
262 |
|
|
|
263 |
ns : INLINE nm '(' { NamesNotAdded++; }
|
|
|
264 |
args ')' { prep_inline($2->sym, $5);
|
|
|
265 |
NamesNotAdded--;
|
|
|
266 |
}
|
|
|
267 |
;
|
|
|
268 |
|
|
|
269 |
c_fcts : ccode { /* leaves pseudo-inlines with sym of
|
|
|
270 |
* type CODE_FRAG or CODE_DECL in global context
|
|
|
271 |
*/
|
|
|
272 |
}
|
|
|
273 |
| cstate
|
|
|
274 |
;
|
|
|
275 |
|
|
|
276 |
cstate : C_STATE STRING STRING {
|
|
|
277 |
c_state($2->sym, $3->sym, ZS);
|
|
|
278 |
has_code = has_state = 1;
|
|
|
279 |
}
|
|
|
280 |
| C_TRACK STRING STRING {
|
|
|
281 |
c_track($2->sym, $3->sym, ZS);
|
|
|
282 |
has_code = has_state = 1;
|
|
|
283 |
}
|
|
|
284 |
| C_STATE STRING STRING STRING {
|
|
|
285 |
c_state($2->sym, $3->sym, $4->sym);
|
|
|
286 |
has_code = has_state = 1;
|
|
|
287 |
}
|
|
|
288 |
| C_TRACK STRING STRING STRING {
|
|
|
289 |
c_track($2->sym, $3->sym, $4->sym);
|
|
|
290 |
has_code = has_state = 1;
|
|
|
291 |
}
|
|
|
292 |
;
|
|
|
293 |
|
|
|
294 |
ccode : C_CODE { Symbol *s;
|
|
|
295 |
NamesNotAdded++;
|
|
|
296 |
s = prep_inline(ZS, ZN);
|
|
|
297 |
NamesNotAdded--;
|
|
|
298 |
$$ = nn(ZN, C_CODE, ZN, ZN);
|
|
|
299 |
$$->sym = s;
|
|
|
300 |
has_code = 1;
|
|
|
301 |
}
|
|
|
302 |
| C_DECL { Symbol *s;
|
|
|
303 |
NamesNotAdded++;
|
|
|
304 |
s = prep_inline(ZS, ZN);
|
|
|
305 |
NamesNotAdded--;
|
|
|
306 |
s->type = CODE_DECL;
|
|
|
307 |
$$ = nn(ZN, C_CODE, ZN, ZN);
|
|
|
308 |
$$->sym = s;
|
|
|
309 |
has_code = 1;
|
|
|
310 |
}
|
|
|
311 |
;
|
|
|
312 |
cexpr : C_EXPR { Symbol *s;
|
|
|
313 |
NamesNotAdded++;
|
|
|
314 |
s = prep_inline(ZS, ZN);
|
|
|
315 |
NamesNotAdded--;
|
|
|
316 |
$$ = nn(ZN, C_EXPR, ZN, ZN);
|
|
|
317 |
$$->sym = s;
|
|
|
318 |
no_side_effects(s->name);
|
|
|
319 |
has_code = 1;
|
|
|
320 |
}
|
|
|
321 |
;
|
|
|
322 |
|
|
|
323 |
body : '{' { open_seq(1); }
|
|
|
324 |
sequence OS { add_seq(Stop); }
|
|
|
325 |
'}' { $$->sq = close_seq(0);
|
|
|
326 |
if (scope_level != 0)
|
|
|
327 |
{ non_fatal("missing '}' ?", 0);
|
|
|
328 |
scope_level = 0;
|
|
|
329 |
}
|
|
|
330 |
}
|
|
|
331 |
;
|
|
|
332 |
|
|
|
333 |
sequence: step { if ($1) add_seq($1); }
|
|
|
334 |
| sequence MS step { if ($3) add_seq($3); }
|
|
|
335 |
;
|
|
|
336 |
|
|
|
337 |
step : one_decl { $$ = ZN; }
|
|
|
338 |
| XU vref_lst { setxus($2, $1->val); $$ = ZN; }
|
|
|
339 |
| NAME ':' one_decl { fatal("label preceding declaration,", (char *)0); }
|
|
|
340 |
| NAME ':' XU { fatal("label predecing xr/xs claim,", 0); }
|
|
|
341 |
| stmnt { $$ = $1; }
|
|
|
342 |
| stmnt UNLESS stmnt { $$ = do_unless($1, $3); }
|
|
|
343 |
;
|
|
|
344 |
|
|
|
345 |
vis : /* empty */ { $$ = ZN; }
|
|
|
346 |
| HIDDEN { $$ = $1; }
|
|
|
347 |
| SHOW { $$ = $1; }
|
|
|
348 |
| ISLOCAL { $$ = $1; }
|
|
|
349 |
;
|
|
|
350 |
|
|
|
351 |
asgn: /* empty */
|
|
|
352 |
| ASGN
|
|
|
353 |
;
|
|
|
354 |
|
|
|
355 |
one_decl: vis TYPE var_list { setptype($3, $2->val, $1);
|
|
|
356 |
$$ = $3;
|
|
|
357 |
}
|
|
|
358 |
| vis UNAME var_list { setutype($3, $2->sym, $1);
|
|
|
359 |
$$ = expand($3, Expand_Ok);
|
|
|
360 |
}
|
|
|
361 |
| vis TYPE asgn '{' nlst '}' {
|
|
|
362 |
if ($2->val != MTYPE)
|
|
|
363 |
fatal("malformed declaration", 0);
|
|
|
364 |
setmtype($5);
|
|
|
365 |
if ($1)
|
|
|
366 |
non_fatal("cannot %s mtype (ignored)",
|
|
|
367 |
$1->sym->name);
|
|
|
368 |
if (context != ZS)
|
|
|
369 |
fatal("mtype declaration must be global", 0);
|
|
|
370 |
}
|
|
|
371 |
;
|
|
|
372 |
|
|
|
373 |
decl_lst: one_decl { $$ = nn(ZN, ',', $1, ZN); }
|
|
|
374 |
| one_decl SEMI
|
|
|
375 |
decl_lst { $$ = nn(ZN, ',', $1, $3); }
|
|
|
376 |
;
|
|
|
377 |
|
|
|
378 |
decl : /* empty */ { $$ = ZN; }
|
|
|
379 |
| decl_lst { $$ = $1; }
|
|
|
380 |
;
|
|
|
381 |
|
|
|
382 |
vref_lst: varref { $$ = nn($1, XU, $1, ZN); }
|
|
|
383 |
| varref ',' vref_lst { $$ = nn($1, XU, $1, $3); }
|
|
|
384 |
;
|
|
|
385 |
|
|
|
386 |
var_list: ivar { $$ = nn($1, TYPE, ZN, ZN); }
|
|
|
387 |
| ivar ',' var_list { $$ = nn($1, TYPE, ZN, $3); }
|
|
|
388 |
;
|
|
|
389 |
|
|
|
390 |
ivar : vardcl { $$ = $1;
|
|
|
391 |
$1->sym->ini = nn(ZN,CONST,ZN,ZN);
|
|
|
392 |
$1->sym->ini->val = 0;
|
|
|
393 |
}
|
|
|
394 |
| vardcl ASGN expr { $$ = $1;
|
|
|
395 |
$1->sym->ini = $3;
|
|
|
396 |
trackvar($1,$3);
|
|
|
397 |
if ($3->ntyp == CONST
|
|
|
398 |
|| ($3->ntyp == NAME && $3->sym->context))
|
|
|
399 |
{ has_ini = 2; /* local init */
|
|
|
400 |
} else
|
|
|
401 |
{ has_ini = 1; /* possibly global */
|
|
|
402 |
}
|
|
|
403 |
if (!initialization_ok && split_decl)
|
|
|
404 |
{ nochan_manip($1, $3, 0);
|
|
|
405 |
no_internals($1);
|
|
|
406 |
non_fatal(PART0 "'%s'" PART2, $1->sym->name);
|
|
|
407 |
}
|
|
|
408 |
}
|
|
|
409 |
| vardcl ASGN ch_init { $1->sym->ini = $3;
|
|
|
410 |
$$ = $1; has_ini = 1;
|
|
|
411 |
if (!initialization_ok && split_decl)
|
|
|
412 |
{ non_fatal(PART1 "'%s'" PART2, $1->sym->name);
|
|
|
413 |
}
|
|
|
414 |
}
|
|
|
415 |
;
|
|
|
416 |
|
|
|
417 |
ch_init : '[' CONST ']' OF
|
|
|
418 |
'{' typ_list '}' { if ($2->val)
|
|
|
419 |
u_async++;
|
|
|
420 |
else
|
|
|
421 |
u_sync++;
|
|
|
422 |
{ int i = cnt_mpars($6);
|
|
|
423 |
Mpars = max(Mpars, i);
|
|
|
424 |
}
|
|
|
425 |
$$ = nn(ZN, CHAN, ZN, $6);
|
|
|
426 |
$$->val = $2->val;
|
|
|
427 |
}
|
|
|
428 |
;
|
|
|
429 |
|
|
|
430 |
vardcl : NAME { $1->sym->nel = 1; $$ = $1; }
|
|
|
431 |
| NAME ':' CONST { $1->sym->nbits = $3->val;
|
|
|
432 |
if ($3->val >= 8*sizeof(long))
|
|
|
433 |
{ non_fatal("width-field %s too large",
|
|
|
434 |
$1->sym->name);
|
|
|
435 |
$3->val = 8*sizeof(long)-1;
|
|
|
436 |
}
|
|
|
437 |
$1->sym->nel = 1; $$ = $1;
|
|
|
438 |
}
|
|
|
439 |
| NAME '[' CONST ']' { $1->sym->nel = $3->val; $1->sym->isarray = 1; $$ = $1; }
|
|
|
440 |
;
|
|
|
441 |
|
|
|
442 |
varref : cmpnd { $$ = mk_explicit($1, Expand_Ok, NAME); }
|
|
|
443 |
;
|
|
|
444 |
|
|
|
445 |
pfld : NAME { $$ = nn($1, NAME, ZN, ZN);
|
|
|
446 |
if ($1->sym->isarray && !in_for)
|
|
|
447 |
{ non_fatal("missing array index for '%s'",
|
|
|
448 |
$1->sym->name);
|
|
|
449 |
}
|
|
|
450 |
}
|
|
|
451 |
| NAME { owner = ZS; }
|
|
|
452 |
'[' expr ']' { $$ = nn($1, NAME, $4, ZN); }
|
|
|
453 |
;
|
|
|
454 |
|
|
|
455 |
cmpnd : pfld { Embedded++;
|
|
|
456 |
if ($1->sym->type == STRUCT)
|
|
|
457 |
owner = $1->sym->Snm;
|
|
|
458 |
}
|
|
|
459 |
sfld { $$ = $1; $$->rgt = $3;
|
|
|
460 |
if ($3 && $1->sym->type != STRUCT)
|
|
|
461 |
$1->sym->type = STRUCT;
|
|
|
462 |
Embedded--;
|
|
|
463 |
if (!Embedded && !NamesNotAdded
|
|
|
464 |
&& !$1->sym->type)
|
|
|
465 |
fatal("undeclared variable: %s",
|
|
|
466 |
$1->sym->name);
|
|
|
467 |
if ($3) validref($1, $3->lft);
|
|
|
468 |
owner = ZS;
|
|
|
469 |
}
|
|
|
470 |
;
|
|
|
471 |
|
|
|
472 |
sfld : /* empty */ { $$ = ZN; }
|
|
|
473 |
| '.' cmpnd %prec DOT { $$ = nn(ZN, '.', $2, ZN); }
|
|
|
474 |
;
|
|
|
475 |
|
|
|
476 |
stmnt : Special { $$ = $1; initialization_ok = 0; }
|
|
|
477 |
| Stmnt { $$ = $1; initialization_ok = 0;
|
|
|
478 |
if (inEventMap)
|
|
|
479 |
non_fatal("not an event", (char *)0);
|
|
|
480 |
}
|
|
|
481 |
;
|
|
|
482 |
|
|
|
483 |
for_pre : FOR '(' { in_for = 1; }
|
|
|
484 |
varref { $$ = $4; }
|
|
|
485 |
;
|
|
|
486 |
|
|
|
487 |
for_post: '{' sequence OS '}' ;
|
|
|
488 |
|
|
|
489 |
Special : varref RCV { Expand_Ok++; }
|
|
|
490 |
rargs { Expand_Ok--; has_io++;
|
|
|
491 |
$$ = nn($1, 'r', $1, $4);
|
|
|
492 |
trackchanuse($4, ZN, 'R');
|
|
|
493 |
}
|
|
|
494 |
| varref SND { Expand_Ok++; }
|
|
|
495 |
margs { Expand_Ok--; has_io++;
|
|
|
496 |
$$ = nn($1, 's', $1, $4);
|
|
|
497 |
$$->val=0; trackchanuse($4, ZN, 'S');
|
|
|
498 |
any_runs($4);
|
|
|
499 |
}
|
|
|
500 |
| for_pre ':' expr DOTDOT expr ')' {
|
|
|
501 |
for_setup($1, $3, $5); in_for = 0;
|
|
|
502 |
}
|
|
|
503 |
for_post { $$ = for_body($1, 1);
|
|
|
504 |
}
|
|
|
505 |
| for_pre IN varref ')' { $$ = for_index($1, $3); in_for = 0;
|
|
|
506 |
}
|
|
|
507 |
for_post { $$ = for_body($5, 1);
|
|
|
508 |
}
|
|
|
509 |
| SELECT '(' varref ':' expr DOTDOT expr ')' {
|
|
|
510 |
$$ = sel_index($3, $5, $7);
|
|
|
511 |
}
|
|
|
512 |
| IF options FI { $$ = nn($1, IF, ZN, ZN);
|
|
|
513 |
$$->sl = $2->sl;
|
|
|
514 |
prune_opts($$);
|
|
|
515 |
}
|
|
|
516 |
| DO { pushbreak(); }
|
|
|
517 |
options OD { $$ = nn($1, DO, ZN, ZN);
|
|
|
518 |
$$->sl = $3->sl;
|
|
|
519 |
prune_opts($$);
|
|
|
520 |
}
|
|
|
521 |
| BREAK { $$ = nn(ZN, GOTO, ZN, ZN);
|
|
|
522 |
$$->sym = break_dest();
|
|
|
523 |
}
|
|
|
524 |
| GOTO NAME { $$ = nn($2, GOTO, ZN, ZN);
|
|
|
525 |
if ($2->sym->type != 0
|
|
|
526 |
&& $2->sym->type != LABEL) {
|
|
|
527 |
non_fatal("bad label-name %s",
|
|
|
528 |
$2->sym->name);
|
|
|
529 |
}
|
|
|
530 |
$2->sym->type = LABEL;
|
|
|
531 |
}
|
|
|
532 |
| NAME ':' stmnt { $$ = nn($1, ':',$3, ZN);
|
|
|
533 |
if ($1->sym->type != 0
|
|
|
534 |
&& $1->sym->type != LABEL) {
|
|
|
535 |
non_fatal("bad label-name %s",
|
|
|
536 |
$1->sym->name);
|
|
|
537 |
}
|
|
|
538 |
$1->sym->type = LABEL;
|
|
|
539 |
}
|
|
|
540 |
;
|
|
|
541 |
|
|
|
542 |
Stmnt : varref ASGN full_expr { $$ = nn($1, ASGN, $1, $3);
|
|
|
543 |
trackvar($1, $3);
|
|
|
544 |
nochan_manip($1, $3, 0);
|
|
|
545 |
no_internals($1);
|
|
|
546 |
}
|
|
|
547 |
| varref INCR { $$ = nn(ZN,CONST, ZN, ZN); $$->val = 1;
|
|
|
548 |
$$ = nn(ZN, '+', $1, $$);
|
|
|
549 |
$$ = nn($1, ASGN, $1, $$);
|
|
|
550 |
trackvar($1, $1);
|
|
|
551 |
no_internals($1);
|
|
|
552 |
if ($1->sym->type == CHAN)
|
|
|
553 |
fatal("arithmetic on chan", (char *)0);
|
|
|
554 |
}
|
|
|
555 |
| varref DECR { $$ = nn(ZN,CONST, ZN, ZN); $$->val = 1;
|
|
|
556 |
$$ = nn(ZN, '-', $1, $$);
|
|
|
557 |
$$ = nn($1, ASGN, $1, $$);
|
|
|
558 |
trackvar($1, $1);
|
|
|
559 |
no_internals($1);
|
|
|
560 |
if ($1->sym->type == CHAN)
|
|
|
561 |
fatal("arithmetic on chan id's", (char *)0);
|
|
|
562 |
}
|
|
|
563 |
| PRINT '(' STRING { realread = 0; }
|
|
|
564 |
prargs ')' { $$ = nn($3, PRINT, $5, ZN); realread = 1; }
|
|
|
565 |
| PRINTM '(' varref ')' { $$ = nn(ZN, PRINTM, $3, ZN); }
|
|
|
566 |
| PRINTM '(' CONST ')' { $$ = nn(ZN, PRINTM, $3, ZN); }
|
|
|
567 |
| ASSERT full_expr { $$ = nn(ZN, ASSERT, $2, ZN); AST_track($2, 0); }
|
|
|
568 |
| ccode { $$ = $1; }
|
|
|
569 |
| varref R_RCV { Expand_Ok++; }
|
|
|
570 |
rargs { Expand_Ok--; has_io++;
|
|
|
571 |
$$ = nn($1, 'r', $1, $4);
|
|
|
572 |
$$->val = has_random = 1;
|
|
|
573 |
trackchanuse($4, ZN, 'R');
|
|
|
574 |
}
|
|
|
575 |
| varref RCV { Expand_Ok++; }
|
|
|
576 |
LT rargs GT { Expand_Ok--; has_io++;
|
|
|
577 |
$$ = nn($1, 'r', $1, $5);
|
|
|
578 |
$$->val = 2; /* fifo poll */
|
|
|
579 |
trackchanuse($5, ZN, 'R');
|
|
|
580 |
}
|
|
|
581 |
| varref R_RCV { Expand_Ok++; }
|
|
|
582 |
LT rargs GT { Expand_Ok--; has_io++; /* rrcv poll */
|
|
|
583 |
$$ = nn($1, 'r', $1, $5);
|
|
|
584 |
$$->val = 3; has_random = 1;
|
|
|
585 |
trackchanuse($5, ZN, 'R');
|
|
|
586 |
}
|
|
|
587 |
| varref O_SND { Expand_Ok++; }
|
|
|
588 |
margs { Expand_Ok--; has_io++;
|
|
|
589 |
$$ = nn($1, 's', $1, $4);
|
|
|
590 |
$$->val = has_sorted = 1;
|
|
|
591 |
trackchanuse($4, ZN, 'S');
|
|
|
592 |
any_runs($4);
|
|
|
593 |
}
|
|
|
594 |
| full_expr { $$ = nn(ZN, 'c', $1, ZN); count_runs($$); }
|
|
|
595 |
| ELSE { $$ = nn(ZN,ELSE,ZN,ZN);
|
|
|
596 |
}
|
|
|
597 |
| ATOMIC '{' { open_seq(0); }
|
|
|
598 |
sequence OS '}' { $$ = nn($1, ATOMIC, ZN, ZN);
|
|
|
599 |
$$->sl = seqlist(close_seq(3), 0);
|
|
|
600 |
make_atomic($$->sl->this, 0);
|
|
|
601 |
}
|
|
|
602 |
| D_STEP '{' { open_seq(0);
|
|
|
603 |
rem_Seq();
|
|
|
604 |
}
|
|
|
605 |
sequence OS '}' { $$ = nn($1, D_STEP, ZN, ZN);
|
|
|
606 |
$$->sl = seqlist(close_seq(4), 0);
|
|
|
607 |
make_atomic($$->sl->this, D_ATOM);
|
|
|
608 |
unrem_Seq();
|
|
|
609 |
}
|
|
|
610 |
| '{' { open_seq(0); }
|
|
|
611 |
sequence OS '}' { $$ = nn(ZN, NON_ATOMIC, ZN, ZN);
|
|
|
612 |
$$->sl = seqlist(close_seq(5), 0);
|
|
|
613 |
}
|
|
|
614 |
| INAME { IArgs++; }
|
|
|
615 |
'(' args ')' { pickup_inline($1->sym, $4); IArgs--; }
|
|
|
616 |
Stmnt { $$ = $7; }
|
|
|
617 |
;
|
|
|
618 |
|
|
|
619 |
options : option { $$->sl = seqlist($1->sq, 0); }
|
|
|
620 |
| option options { $$->sl = seqlist($1->sq, $2->sl); }
|
|
|
621 |
;
|
|
|
622 |
|
|
|
623 |
option : SEP { open_seq(0); }
|
|
|
624 |
sequence OS { $$ = nn(ZN,0,ZN,ZN);
|
|
|
625 |
$$->sq = close_seq(6); }
|
|
|
626 |
;
|
|
|
627 |
|
|
|
628 |
OS : /* empty */
|
|
|
629 |
| SEMI { /* redundant semi at end of sequence */ }
|
|
|
630 |
;
|
|
|
631 |
|
|
|
632 |
MS : SEMI { /* at least one semi-colon */ }
|
|
|
633 |
| MS SEMI { /* but more are okay too */ }
|
|
|
634 |
;
|
|
|
635 |
|
|
|
636 |
aname : NAME { $$ = $1; }
|
|
|
637 |
| PNAME { $$ = $1; }
|
|
|
638 |
;
|
|
|
639 |
|
|
|
640 |
expr : '(' expr ')' { $$ = $2; }
|
|
|
641 |
| expr '+' expr { $$ = nn(ZN, '+', $1, $3); }
|
|
|
642 |
| expr '-' expr { $$ = nn(ZN, '-', $1, $3); }
|
|
|
643 |
| expr '*' expr { $$ = nn(ZN, '*', $1, $3); }
|
|
|
644 |
| expr '/' expr { $$ = nn(ZN, '/', $1, $3); }
|
|
|
645 |
| expr '%' expr { $$ = nn(ZN, '%', $1, $3); }
|
|
|
646 |
| expr '&' expr { $$ = nn(ZN, '&', $1, $3); }
|
|
|
647 |
| expr '^' expr { $$ = nn(ZN, '^', $1, $3); }
|
|
|
648 |
| expr '|' expr { $$ = nn(ZN, '|', $1, $3); }
|
|
|
649 |
| expr GT expr { $$ = nn(ZN, GT, $1, $3); }
|
|
|
650 |
| expr LT expr { $$ = nn(ZN, LT, $1, $3); }
|
|
|
651 |
| expr GE expr { $$ = nn(ZN, GE, $1, $3); }
|
|
|
652 |
| expr LE expr { $$ = nn(ZN, LE, $1, $3); }
|
|
|
653 |
| expr EQ expr { $$ = nn(ZN, EQ, $1, $3); }
|
|
|
654 |
| expr NE expr { $$ = nn(ZN, NE, $1, $3); }
|
|
|
655 |
| expr AND expr { $$ = nn(ZN, AND, $1, $3); }
|
|
|
656 |
| expr OR expr { $$ = nn(ZN, OR, $1, $3); }
|
|
|
657 |
| expr LSHIFT expr { $$ = nn(ZN, LSHIFT,$1, $3); }
|
|
|
658 |
| expr RSHIFT expr { $$ = nn(ZN, RSHIFT,$1, $3); }
|
|
|
659 |
| '~' expr { $$ = nn(ZN, '~', $2, ZN); }
|
|
|
660 |
| '-' expr %prec UMIN { $$ = nn(ZN, UMIN, $2, ZN); }
|
|
|
661 |
| SND expr %prec NEG { $$ = nn(ZN, '!', $2, ZN); }
|
|
|
662 |
|
|
|
663 |
| '(' expr SEMI expr ':' expr ')' {
|
|
|
664 |
$$ = nn(ZN, OR, $4, $6);
|
|
|
665 |
$$ = nn(ZN, '?', $2, $$);
|
|
|
666 |
}
|
|
|
667 |
|
|
|
668 |
| RUN aname { Expand_Ok++;
|
|
|
669 |
if (!context)
|
|
|
670 |
fatal("used 'run' outside proctype",
|
|
|
671 |
(char *) 0);
|
|
|
672 |
}
|
|
|
673 |
'(' args ')'
|
|
|
674 |
Opt_priority { Expand_Ok--;
|
|
|
675 |
$$ = nn($2, RUN, $5, ZN);
|
|
|
676 |
$$->val = ($7) ? $7->val : 1;
|
|
|
677 |
trackchanuse($5, $2, 'A'); trackrun($$);
|
|
|
678 |
}
|
|
|
679 |
| LEN '(' varref ')' { $$ = nn($3, LEN, $3, ZN); }
|
|
|
680 |
| ENABLED '(' expr ')' { $$ = nn(ZN, ENABLED, $3, ZN);
|
|
|
681 |
has_enabled++;
|
|
|
682 |
}
|
|
|
683 |
| varref RCV { Expand_Ok++; }
|
|
|
684 |
'[' rargs ']' { Expand_Ok--; has_io++;
|
|
|
685 |
$$ = nn($1, 'R', $1, $5);
|
|
|
686 |
}
|
|
|
687 |
| varref R_RCV { Expand_Ok++; }
|
|
|
688 |
'[' rargs ']' { Expand_Ok--; has_io++;
|
|
|
689 |
$$ = nn($1, 'R', $1, $5);
|
|
|
690 |
$$->val = has_random = 1;
|
|
|
691 |
}
|
|
|
692 |
| varref { $$ = $1; trapwonly($1 /*, "varref" */); }
|
|
|
693 |
| cexpr { $$ = $1; }
|
|
|
694 |
| CONST { $$ = nn(ZN,CONST,ZN,ZN);
|
|
|
695 |
$$->ismtyp = $1->ismtyp;
|
|
|
696 |
$$->val = $1->val;
|
|
|
697 |
}
|
|
|
698 |
| TIMEOUT { $$ = nn(ZN,TIMEOUT, ZN, ZN); }
|
|
|
699 |
| NONPROGRESS { $$ = nn(ZN,NONPROGRESS, ZN, ZN);
|
|
|
700 |
has_np++;
|
|
|
701 |
}
|
|
|
702 |
| PC_VAL '(' expr ')' { $$ = nn(ZN, PC_VAL, $3, ZN);
|
|
|
703 |
has_pcvalue++;
|
|
|
704 |
}
|
|
|
705 |
| PNAME '[' expr ']' '@' NAME
|
|
|
706 |
{ $$ = rem_lab($1->sym, $3, $6->sym); }
|
|
|
707 |
| PNAME '[' expr ']' ':' pfld
|
|
|
708 |
{ $$ = rem_var($1->sym, $3, $6->sym, $6->lft); }
|
|
|
709 |
| PNAME '@' NAME { $$ = rem_lab($1->sym, ZN, $3->sym); }
|
|
|
710 |
| PNAME ':' pfld { $$ = rem_var($1->sym, ZN, $3->sym, $3->lft); }
|
|
|
711 |
| ltl_expr { $$ = $1; }
|
|
|
712 |
;
|
|
|
713 |
|
|
|
714 |
Opt_priority: /* none */ { $$ = ZN; }
|
|
|
715 |
| PRIORITY CONST { $$ = $2; }
|
|
|
716 |
;
|
|
|
717 |
|
|
|
718 |
full_expr: expr { $$ = $1; }
|
|
|
719 |
| Expr { $$ = $1; }
|
|
|
720 |
;
|
|
|
721 |
|
|
|
722 |
ltl_expr: expr UNTIL expr { $$ = nn(ZN, UNTIL, $1, $3); }
|
|
|
723 |
| expr RELEASE expr { $$ = nn(ZN, RELEASE, $1, $3); }
|
|
|
724 |
| expr WEAK_UNTIL expr { $$ = nn(ZN, ALWAYS, $1, ZN);
|
|
|
725 |
$$ = nn(ZN, OR, $$, nn(ZN, UNTIL, $1, $3));
|
|
|
726 |
}
|
|
|
727 |
| expr IMPLIES expr {
|
|
|
728 |
$$ = nn(ZN, '!', $1, ZN);
|
|
|
729 |
$$ = nn(ZN, OR, $$, $3);
|
|
|
730 |
}
|
|
|
731 |
| expr EQUIV expr { $$ = nn(ZN, EQUIV, $1, $3); }
|
|
|
732 |
| NEXT expr %prec NEG { $$ = nn(ZN, NEXT, $2, ZN); }
|
|
|
733 |
| ALWAYS expr %prec NEG { $$ = nn(ZN, ALWAYS,$2, ZN); }
|
|
|
734 |
| EVENTUALLY expr %prec NEG { $$ = nn(ZN, EVENTUALLY, $2, ZN); }
|
|
|
735 |
;
|
|
|
736 |
|
|
|
737 |
/* an Expr cannot be negated - to protect Probe expressions */
|
|
|
738 |
Expr : Probe { $$ = $1; }
|
|
|
739 |
| '(' Expr ')' { $$ = $2; }
|
|
|
740 |
| Expr AND Expr { $$ = nn(ZN, AND, $1, $3); }
|
|
|
741 |
| Expr AND expr { $$ = nn(ZN, AND, $1, $3); }
|
|
|
742 |
| expr AND Expr { $$ = nn(ZN, AND, $1, $3); }
|
|
|
743 |
| Expr OR Expr { $$ = nn(ZN, OR, $1, $3); }
|
|
|
744 |
| Expr OR expr { $$ = nn(ZN, OR, $1, $3); }
|
|
|
745 |
| expr OR Expr { $$ = nn(ZN, OR, $1, $3); }
|
|
|
746 |
;
|
|
|
747 |
|
|
|
748 |
Probe : FULL '(' varref ')' { $$ = nn($3, FULL, $3, ZN); }
|
|
|
749 |
| NFULL '(' varref ')' { $$ = nn($3, NFULL, $3, ZN); }
|
|
|
750 |
| EMPTY '(' varref ')' { $$ = nn($3, EMPTY, $3, ZN); }
|
|
|
751 |
| NEMPTY '(' varref ')' { $$ = nn($3,NEMPTY, $3, ZN); }
|
|
|
752 |
;
|
|
|
753 |
|
|
|
754 |
Opt_enabler: /* none */ { $$ = ZN; }
|
|
|
755 |
| PROVIDED '(' full_expr ')' { if (!proper_enabler($3))
|
|
|
756 |
{ non_fatal("invalid PROVIDED clause",
|
|
|
757 |
(char *)0);
|
|
|
758 |
$$ = ZN;
|
|
|
759 |
} else
|
|
|
760 |
$$ = $3;
|
|
|
761 |
}
|
|
|
762 |
| PROVIDED error { $$ = ZN;
|
|
|
763 |
non_fatal("usage: provided ( ..expr.. )",
|
|
|
764 |
(char *)0);
|
|
|
765 |
}
|
|
|
766 |
;
|
|
|
767 |
|
|
|
768 |
basetype: TYPE { $$->sym = ZS;
|
|
|
769 |
$$->val = $1->val;
|
|
|
770 |
if ($$->val == UNSIGNED)
|
|
|
771 |
fatal("unsigned cannot be used as mesg type", 0);
|
|
|
772 |
}
|
|
|
773 |
| UNAME { $$->sym = $1->sym;
|
|
|
774 |
$$->val = STRUCT;
|
|
|
775 |
}
|
|
|
776 |
| error /* e.g., unsigned ':' const */
|
|
|
777 |
;
|
|
|
778 |
|
|
|
779 |
typ_list: basetype { $$ = nn($1, $1->val, ZN, ZN); }
|
|
|
780 |
| basetype ',' typ_list { $$ = nn($1, $1->val, ZN, $3); }
|
|
|
781 |
;
|
|
|
782 |
|
|
|
783 |
args : /* empty */ { $$ = ZN; }
|
|
|
784 |
| arg { $$ = $1; }
|
|
|
785 |
;
|
|
|
786 |
|
|
|
787 |
prargs : /* empty */ { $$ = ZN; }
|
|
|
788 |
| ',' arg { $$ = $2; }
|
|
|
789 |
;
|
|
|
790 |
|
|
|
791 |
margs : arg { $$ = $1; }
|
|
|
792 |
| expr '(' arg ')' { if ($1->ntyp == ',')
|
|
|
793 |
$$ = tail_add($1, $3);
|
|
|
794 |
else
|
|
|
795 |
$$ = nn(ZN, ',', $1, $3);
|
|
|
796 |
}
|
|
|
797 |
;
|
|
|
798 |
|
|
|
799 |
arg : expr { if ($1->ntyp == ',')
|
|
|
800 |
$$ = $1;
|
|
|
801 |
else
|
|
|
802 |
$$ = nn(ZN, ',', $1, ZN);
|
|
|
803 |
}
|
|
|
804 |
| expr ',' arg { if ($1->ntyp == ',')
|
|
|
805 |
$$ = tail_add($1, $3);
|
|
|
806 |
else
|
|
|
807 |
$$ = nn(ZN, ',', $1, $3);
|
|
|
808 |
}
|
|
|
809 |
;
|
|
|
810 |
|
|
|
811 |
rarg : varref { $$ = $1; trackvar($1, $1);
|
|
|
812 |
trapwonly($1 /*, "rarg" */); }
|
|
|
813 |
| EVAL '(' expr ')' { $$ = nn(ZN,EVAL,$3,ZN);
|
|
|
814 |
trapwonly($1 /*, "eval rarg" */); }
|
|
|
815 |
| CONST { $$ = nn(ZN,CONST,ZN,ZN);
|
|
|
816 |
$$->ismtyp = $1->ismtyp;
|
|
|
817 |
$$->val = $1->val;
|
|
|
818 |
}
|
|
|
819 |
| '-' CONST %prec UMIN { $$ = nn(ZN,CONST,ZN,ZN);
|
|
|
820 |
$$->val = - ($2->val);
|
|
|
821 |
}
|
|
|
822 |
;
|
|
|
823 |
|
|
|
824 |
rargs : rarg { if ($1->ntyp == ',')
|
|
|
825 |
$$ = $1;
|
|
|
826 |
else
|
|
|
827 |
$$ = nn(ZN, ',', $1, ZN);
|
|
|
828 |
}
|
|
|
829 |
| rarg ',' rargs { if ($1->ntyp == ',')
|
|
|
830 |
$$ = tail_add($1, $3);
|
|
|
831 |
else
|
|
|
832 |
$$ = nn(ZN, ',', $1, $3);
|
|
|
833 |
}
|
|
|
834 |
| rarg '(' rargs ')' { if ($1->ntyp == ',')
|
|
|
835 |
$$ = tail_add($1, $3);
|
|
|
836 |
else
|
|
|
837 |
$$ = nn(ZN, ',', $1, $3);
|
|
|
838 |
}
|
|
|
839 |
| '(' rargs ')' { $$ = $2; }
|
|
|
840 |
;
|
|
|
841 |
|
|
|
842 |
nlst : NAME { $$ = nn($1, NAME, ZN, ZN);
|
|
|
843 |
$$ = nn(ZN, ',', $$, ZN); }
|
|
|
844 |
| nlst NAME { $$ = nn($2, NAME, ZN, ZN);
|
|
|
845 |
$$ = nn(ZN, ',', $$, $1);
|
|
|
846 |
}
|
|
|
847 |
| nlst ',' { $$ = $1; /* commas optional */ }
|
|
|
848 |
;
|
|
|
849 |
%%
|
|
|
850 |
|
|
|
851 |
#define binop(n, sop) fprintf(fd, "("); recursive(fd, n->lft); \
|
|
|
852 |
fprintf(fd, ") %s (", sop); recursive(fd, n->rgt); \
|
|
|
853 |
fprintf(fd, ")");
|
|
|
854 |
#define unop(n, sop) fprintf(fd, "%s (", sop); recursive(fd, n->lft); \
|
|
|
855 |
fprintf(fd, ")");
|
|
|
856 |
|
|
|
857 |
static void
|
|
|
858 |
recursive(FILE *fd, Lextok *n)
|
|
|
859 |
{
|
|
|
860 |
if (n)
|
|
|
861 |
switch (n->ntyp) {
|
|
|
862 |
case NEXT:
|
|
|
863 |
unop(n, "X");
|
|
|
864 |
break;
|
|
|
865 |
case ALWAYS:
|
|
|
866 |
unop(n, "[]");
|
|
|
867 |
break;
|
|
|
868 |
case EVENTUALLY:
|
|
|
869 |
unop(n, "<>");
|
|
|
870 |
break;
|
|
|
871 |
case '!':
|
|
|
872 |
unop(n, "!");
|
|
|
873 |
break;
|
|
|
874 |
case UNTIL:
|
|
|
875 |
binop(n, "U");
|
|
|
876 |
break;
|
|
|
877 |
case WEAK_UNTIL:
|
|
|
878 |
binop(n, "W");
|
|
|
879 |
break;
|
|
|
880 |
case RELEASE: /* see http://en.wikipedia.org/wiki/Linear_temporal_logic */
|
|
|
881 |
binop(n, "V");
|
|
|
882 |
break;
|
|
|
883 |
case OR:
|
|
|
884 |
binop(n, "||");
|
|
|
885 |
break;
|
|
|
886 |
case AND:
|
|
|
887 |
binop(n, "&&");
|
|
|
888 |
break;
|
|
|
889 |
case IMPLIES:
|
|
|
890 |
binop(n, "->");
|
|
|
891 |
break;
|
|
|
892 |
case EQUIV:
|
|
|
893 |
binop(n, "<->");
|
|
|
894 |
break;
|
|
|
895 |
default:
|
|
|
896 |
comment(fd, n, 0);
|
|
|
897 |
break;
|
|
|
898 |
}
|
|
|
899 |
}
|
|
|
900 |
|
|
|
901 |
#define TMP_FILE "_S_p_I_n_.tmp"
|
|
|
902 |
|
|
|
903 |
extern int unlink(const char *);
|
|
|
904 |
|
|
|
905 |
static Lextok *
|
|
|
906 |
ltl_to_string(Lextok *n)
|
|
|
907 |
{ Lextok *m = nn(ZN, 0, ZN, ZN);
|
|
|
908 |
char *retval;
|
|
|
909 |
char formula[1024];
|
|
|
910 |
FILE *tf = fopen(TMP_FILE, "w+"); /* tmpfile() fails on Windows 7 */
|
|
|
911 |
|
|
|
912 |
/* convert the parsed ltl to a string
|
|
|
913 |
by writing into a file, using existing functions,
|
|
|
914 |
and then passing it to the existing interface for
|
|
|
915 |
conversion into a never claim
|
|
|
916 |
(this means parsing everything twice, which is
|
|
|
917 |
a little redundant, but adds only miniscule overhead)
|
|
|
918 |
*/
|
|
|
919 |
|
|
|
920 |
if (!tf)
|
|
|
921 |
{ fatal("cannot create temporary file", (char *) 0);
|
|
|
922 |
}
|
|
|
923 |
recursive(tf, n);
|
|
|
924 |
(void) fseek(tf, 0L, SEEK_SET);
|
|
|
925 |
|
|
|
926 |
memset(formula, 0, sizeof(formula));
|
|
|
927 |
retval = fgets(formula, sizeof(formula), tf);
|
|
|
928 |
fclose(tf);
|
|
|
929 |
(void) unlink(TMP_FILE);
|
|
|
930 |
|
|
|
931 |
if (!retval)
|
|
|
932 |
{ printf("%p\n", retval);
|
|
|
933 |
fatal("could not translate ltl formula", 0);
|
|
|
934 |
}
|
|
|
935 |
|
|
|
936 |
if (1) printf("ltl %s: %s\n", ltl_name, formula);
|
|
|
937 |
|
|
|
938 |
m->sym = lookup(formula);
|
|
|
939 |
|
|
|
940 |
return m;
|
|
|
941 |
}
|
|
|
942 |
|
|
|
943 |
void
|
|
|
944 |
yyerror(char *fmt, ...)
|
|
|
945 |
{
|
|
|
946 |
non_fatal(fmt, (char *) 0);
|
|
|
947 |
}
|