1 /***** spin: spin.y *****/
4 * This file is part of the public release of Spin. It is subject to the
5 * terms in the LICENSE file that is included in this source directory.
6 * Tool documentation is available at http://spinroot.com
11 #include <sys/types.h>
17 #define YYMAXDEPTH 20000 /* default is 10000 */
19 #define Stop nn(ZN,'@',ZN,ZN)
20 #define PART0 "place initialized declaration of "
21 #define PART1 "place initialized chan decl of "
22 #define PART2 " at start of proctype "
24 static Lextok *ltl_to_string(Lextok *);
26 extern Symbol *context, *owner;
27 extern Lextok *for_body(Lextok *, int);
28 extern void for_setup(Lextok *, Lextok *, Lextok *);
29 extern Lextok *for_index(Lextok *, Lextok *);
30 extern Lextok *sel_index(Lextok *, Lextok *, Lextok *);
31 extern void keep_track_off(Lextok *);
32 extern void safe_break(void);
33 extern void restore_break(void);
34 extern int u_sync, u_async, dumptab, scope_level;
35 extern int initialization_ok;
36 extern short has_sorted, has_random, has_enabled, has_pcvalue, has_np, has_priority;
37 extern short has_code, has_state, has_ltl, has_io;
38 extern void count_runs(Lextok *);
39 extern void no_internals(Lextok *);
40 extern void any_runs(Lextok *);
41 extern void explain(int);
42 extern void ltl_list(char *, char *);
43 extern void validref(Lextok *, Lextok *);
44 extern void sanity_check(Lextok *);
47 int Mpars = 0; /* max nr of message parameters */
48 int nclaims = 0; /* nr of never claims */
49 int ltl_mode = 0; /* set when parsing an ltl formula */
50 int Expand_Ok = 0, realread = 1, IArgs = 0, NamesNotAdded = 0;
51 int in_for = 0, in_seq = 0, par_cnt = 0;
52 int dont_simplify = 0;
53 char *claimproc = (char *) 0;
54 char *eventmap = (char *) 0;
56 static char *ltl_name;
57 static int Embedded = 0, inEventMap = 0, has_ini = 0;
61 %token ASSERT PRINT PRINTM PREPROC
62 %token C_CODE C_DECL C_EXPR C_STATE C_TRACK
63 %token RUN LEN ENABLED SET_P GET_P EVAL PC_VAL
64 %token TYPEDEF MTYPE INLINE RETURN LABEL OF
65 %token GOTO BREAK ELSE SEMI ARROW
66 %token IF FI DO OD FOR SELECT IN SEP DOTDOT
67 %token ATOMIC NON_ATOMIC D_STEP UNLESS
68 %token TIMEOUT NONPROGRESS
69 %token ACTIVE PROCTYPE D_PROCTYPE
70 %token HIDDEN SHOW ISLOCAL
71 %token PRIORITY PROVIDED
72 %token FULL EMPTY NFULL NEMPTY
73 %token CONST TYPE XU /* val */
74 %token NAME UNAME PNAME INAME /* sym */
75 %token STRING CLAIM TRACE INIT LTL /* sym */
78 %left SND O_SND RCV R_RCV /* SND doubles as boolean negation */
79 %left IMPLIES EQUIV /* ltl */
82 %left ALWAYS EVENTUALLY /* ltl */
83 %left UNTIL WEAK_UNTIL RELEASE /* ltl */
98 /** PROMELA Grammar Rules **/
100 program : units { yytext[0] = '\0'; }
107 unit : proc /* proctype { } */
108 | init /* init { } */
109 | claim /* never claim */
110 | ltl /* ltl formula */
111 | events /* event assertions */
112 | one_decl /* variables, chans */
113 | utype /* user defined types */
114 | c_fcts /* c functions etc. */
115 | ns /* named sequence */
116 | semi /* optional separator */
120 l_par : '(' { par_cnt++; }
123 r_par : ')' { par_cnt--; }
127 proc : inst /* optional instantiator */
129 setptype($3, PROCTYPE, ZN);
132 context->ini = $2; /* linenr and file */
133 Expand_Ok++; /* expand struct names in decl */
136 l_par decl r_par { Expand_Ok--;
138 fatal("initializer in parameter list", (char *) 0);
143 if ($1 != ZN && $1->val > 0)
145 rl = ready($3->sym, $6, $11->sq, $2->val, $10, A_PROC);
146 for (j = 0; j < $1->val; j++)
147 { runnable(rl, $9?$9->val:1, 1);
150 if (dumptab) $3->sym->ini = $1;
152 { rl = ready($3->sym, $6, $11->sq, $2->val, $10, P_PROC);
154 if (rl && has_ini == 1) /* global initializations, unsafe */
155 { /* printf("proctype %s has initialized data\n",
164 proctype: PROCTYPE { $$ = nn(ZN,CONST,ZN,ZN); $$->val = 0; }
165 | D_PROCTYPE { $$ = nn(ZN,CONST,ZN,ZN); $$->val = 1; }
168 inst : /* empty */ { $$ = ZN; }
169 | ACTIVE { $$ = nn(ZN,CONST,ZN,ZN); $$->val = 1; }
170 | ACTIVE '[' const_expr ']' {
171 $$ = nn(ZN,CONST,ZN,ZN); $$->val = $3->val;
173 non_fatal("max nr of processes is 255\n", "");
175 | ACTIVE '[' NAME ']' {
176 $$ = nn(ZN,CONST,ZN,ZN);
179 fatal("undeclared variable %s",
181 else if ($3->sym->ini->ntyp != CONST)
182 fatal("need constant initializer for %s\n",
185 $$->val = $3->sym->ini->val;
189 init : INIT { context = $1->sym; }
192 rl = ready(context, ZN, $4->sq, 0, ZN, I_PROC);
193 runnable(rl, $3?$3->val:1, 1);
199 ltl : LTL optname2 { ltl_mode = 1; ltl_name = $2->sym->name; }
200 ltl_body { if ($4) ltl_list($2->sym->name, $4->sym->name);
201 ltl_mode = 0; has_ltl = 1;
205 ltl_body: '{' full_expr OS '}' { $$ = ltl_to_string($2); }
206 | error { $$ = NULL; }
209 claim : CLAIM optname { if ($2 != ZN)
210 { $1->sym = $2->sym; /* new 5.3.0 */
214 if (claimproc && !strcmp(claimproc, $1->sym->name))
215 { fatal("claim %s redefined", claimproc);
217 claimproc = $1->sym->name;
219 body { (void) ready($1->sym, ZN, $4->sq, 0, ZN, N_CLAIM);
224 optname : /* empty */ { char tb[32];
226 sprintf(tb, "never_%d", nclaims);
227 $$ = nn(ZN, NAME, ZN, ZN);
228 $$->sym = lookup(tb);
233 optname2 : /* empty */ { char tb[32]; static int nltl = 0;
235 sprintf(tb, "ltl_%d", nltl++);
236 $$ = nn(ZN, NAME, ZN, ZN);
237 $$->sym = lookup(tb);
242 events : TRACE { context = $1->sym;
244 non_fatal("trace %s redefined", eventmap);
245 eventmap = $1->sym->name;
249 if (strcmp($1->sym->name, ":trace:") == 0)
250 { (void) ready($1->sym, ZN, $3->sq, 0, ZN, E_TRACE);
252 { (void) ready($1->sym, ZN, $3->sq, 0, ZN, N_TRACE);
259 utype : TYPEDEF NAME '{' { if (context)
260 { fatal("typedef %s must be global",
266 decl_lst '}' { setuname($5);
272 nm : NAME { $$ = $1; }
275 fatal("invalid use of '%s'", $1->sym->name);
279 ns : INLINE nm l_par { NamesNotAdded++; }
280 args r_par { prep_inline($2->sym, $5);
285 c_fcts : ccode { /* leaves pseudo-inlines with sym of
286 * type CODE_FRAG or CODE_DECL in global context
292 cstate : C_STATE STRING STRING {
293 c_state($2->sym, $3->sym, ZS);
294 has_code = has_state = 1;
296 | C_TRACK STRING STRING {
297 c_track($2->sym, $3->sym, ZS);
298 has_code = has_state = 1;
300 | C_STATE STRING STRING STRING {
301 c_state($2->sym, $3->sym, $4->sym);
302 has_code = has_state = 1;
304 | C_TRACK STRING STRING STRING {
305 c_track($2->sym, $3->sym, $4->sym);
306 has_code = has_state = 1;
310 ccode : C_CODE { Symbol *s;
312 s = prep_inline(ZS, ZN);
314 $$ = nn(ZN, C_CODE, ZN, ZN);
320 | C_DECL { Symbol *s;
322 s = prep_inline(ZS, ZN);
325 $$ = nn(ZN, C_CODE, ZN, ZN);
332 cexpr : C_EXPR { Symbol *s;
334 s = prep_inline(ZS, ZN);
335 /* if context is 0 this was inside an ltl formula
336 mark the last inline added to seqnames */
341 $$ = nn(ZN, C_EXPR, ZN, ZN);
345 no_side_effects(s->name);
350 body : '{' { open_seq(1); in_seq = $1->ln; }
351 sequence OS { add_seq(Stop); }
352 '}' { $$->sq = close_seq(0); in_seq = 0;
353 if (scope_level != 0)
354 { non_fatal("missing '}' ?", 0);
360 sequence: step { if ($1) add_seq($1); }
361 | sequence MS step { if ($3) add_seq($3); }
364 step : one_decl { $$ = ZN; }
365 | XU vref_lst { setxus($2, $1->val); $$ = ZN; }
366 | NAME ':' one_decl { fatal("label preceding declaration,", (char *)0); }
367 | NAME ':' XU { fatal("label predecing xr/xs claim,", 0); }
369 | stmnt UNLESS { if ($1->ntyp == DO) { safe_break(); } }
370 stmnt { if ($1->ntyp == DO) { restore_break(); }
371 $$ = do_unless($1, $4);
373 | error { printf("Not a Step\n"); }
376 vis : /* empty */ { $$ = ZN; }
377 | HIDDEN { $$ = $1; }
379 | ISLOCAL { $$ = $1; }
386 one_decl: vis TYPE var_list { setptype($3, $2->val, $1);
389 | vis UNAME var_list { setutype($3, $2->sym, $1);
390 $$ = expand($3, Expand_Ok);
392 | vis TYPE asgn '{' nlst '}' {
393 if ($2->val != MTYPE)
394 fatal("malformed declaration", 0);
397 non_fatal("cannot %s mtype (ignored)",
400 fatal("mtype declaration must be global", 0);
404 decl_lst: one_decl { $$ = nn(ZN, ',', $1, ZN); }
406 decl_lst { $$ = nn(ZN, ',', $1, $3); }
409 decl : /* empty */ { $$ = ZN; }
410 | decl_lst { $$ = $1; }
413 vref_lst: varref { $$ = nn($1, XU, $1, ZN); }
414 | varref ',' vref_lst { $$ = nn($1, XU, $1, $3); }
417 var_list: ivar { $$ = nn($1, TYPE, ZN, ZN); }
418 | ivar ',' var_list { $$ = nn($1, TYPE, ZN, $3); }
421 c_list : CONST { $1->ntyp = CONST; $$ = $1; }
422 | CONST ',' c_list { $1->ntyp = CONST; $$ = nn($1, ',', $1, $3); }
425 ivar : vardcl { $$ = $1;
426 $1->sym->ini = nn(ZN,CONST,ZN,ZN);
427 $1->sym->ini->val = 0;
428 if (!initialization_ok)
430 zx = nn(ZN, NAME, ZN, ZN);
432 xz = nn(zx, ASGN, zx, $1->sym->ini);
434 /* make sure zx doesnt turn out to be a STRUCT later */
438 | vardcl ASGN '{' c_list '}' {
439 if (!$1->sym->isarray)
440 fatal("%s must be an array", $1->sym->name);
444 $1->sym->hidden |= (4|8); /* conservative */
445 if (!initialization_ok)
446 { Lextok *zx = nn(ZN, NAME, ZN, ZN);
448 add_seq(nn(zx, ASGN, zx, $4));
451 | vardcl ASGN expr { $$ = $1;
453 if ($3->ntyp == CONST
454 || ($3->ntyp == NAME && $3->sym->context))
455 { has_ini = 2; /* local init */
457 { has_ini = 1; /* possibly global */
460 if (any_oper($3, RUN))
461 { fatal("cannot use 'run' in var init, saw", (char *) 0);
463 nochan_manip($1, $3, 0);
465 if (!initialization_ok)
466 { Lextok *zx = nn(ZN, NAME, ZN, ZN);
468 add_seq(nn(zx, ASGN, zx, $3));
471 | vardcl ASGN ch_init { $1->sym->ini = $3;
472 $$ = $1; has_ini = 1;
473 if (!initialization_ok)
474 { non_fatal(PART1 "'%s'" PART2, $1->sym->name);
479 ch_init : '[' const_expr ']' OF
480 '{' typ_list '}' { if ($2->val)
484 { int i = cnt_mpars($6);
485 Mpars = max(Mpars, i);
487 $$ = nn(ZN, CHAN, ZN, $6);
494 vardcl : NAME { $1->sym->nel = 1; $$ = $1; }
495 | NAME ':' CONST { $1->sym->nbits = $3->val;
496 if ($3->val >= 8*sizeof(long))
497 { non_fatal("width-field %s too large",
499 $3->val = 8*sizeof(long)-1;
501 $1->sym->nel = 1; $$ = $1;
503 | NAME '[' const_expr ']' { $1->sym->nel = $3->val; $1->sym->isarray = 1; $$ = $1; }
504 | NAME '[' NAME ']' { /* make an exception for an initialized scalars */
505 $$ = nn(ZN, CONST, ZN, ZN);
506 fprintf(stderr, "spin: %s:%d, warning: '%s' in array bound ",
507 $1->fn->name, $1->ln, $3->sym->name);
508 if ($3->sym->ini->val > 0)
509 { fprintf(stderr, "evaluated as %d\n", $3->sym->ini->val);
510 $$->val = $3->sym->ini->val;
512 { fprintf(stderr, "evaluated as 8 by default (to avoid zero)\n");
515 $1->sym->nel = $$->val;
516 $1->sym->isarray = 1;
521 varref : cmpnd { $$ = mk_explicit($1, Expand_Ok, NAME); }
524 pfld : NAME { $$ = nn($1, NAME, ZN, ZN);
525 if ($1->sym->isarray && !in_for)
526 { non_fatal("missing array index for '%s'",
530 | NAME { owner = ZS; }
531 '[' expr ']' { $$ = nn($1, NAME, $4, ZN); }
534 cmpnd : pfld { Embedded++;
535 if ($1->sym->type == STRUCT)
536 owner = $1->sym->Snm;
538 sfld { $$ = $1; $$->rgt = $3;
539 if ($3 && $1->sym->type != STRUCT)
540 $1->sym->type = STRUCT;
542 if (!Embedded && !NamesNotAdded
544 fatal("undeclared variable: %s",
546 if ($3) validref($1, $3->lft);
551 sfld : /* empty */ { $$ = ZN; }
552 | '.' cmpnd %prec DOT { $$ = nn(ZN, '.', $2, ZN); }
555 stmnt : Special { $$ = $1; initialization_ok = 0; }
556 | Stmnt { $$ = $1; initialization_ok = 0;
557 if (inEventMap) non_fatal("not an event", (char *)0);
561 for_pre : FOR l_par { in_for = 1; }
562 varref { trapwonly($4 /*, "for" */);
563 pushbreak(); /* moved up */
568 for_post: '{' sequence OS '}' ;
570 Special : varref RCV { Expand_Ok++; }
571 rargs { Expand_Ok--; has_io++;
572 $$ = nn($1, 'r', $1, $4);
573 trackchanuse($4, ZN, 'R');
575 | varref SND { Expand_Ok++; }
576 margs { Expand_Ok--; has_io++;
577 $$ = nn($1, 's', $1, $4);
578 $$->val=0; trackchanuse($4, ZN, 'S');
581 | for_pre ':' expr DOTDOT expr r_par {
582 for_setup($1, $3, $5); in_for = 0;
584 for_post { $$ = for_body($1, 1);
586 | for_pre IN varref r_par { $$ = for_index($1, $3); in_for = 0;
588 for_post { $$ = for_body($5, 1);
590 | SELECT l_par varref ':' expr DOTDOT expr r_par {
591 trapwonly($3 /*, "select" */);
592 $$ = sel_index($3, $5, $7);
594 | IF options FI { $$ = nn($1, IF, ZN, ZN);
600 | DO { pushbreak(); }
601 options OD { $$ = nn($1, DO, ZN, ZN);
607 | BREAK { $$ = nn(ZN, GOTO, ZN, ZN);
608 $$->sym = break_dest();
610 | GOTO NAME { $$ = nn($2, GOTO, ZN, ZN);
611 if ($2->sym->type != 0
612 && $2->sym->type != LABEL) {
613 non_fatal("bad label-name %s",
616 $2->sym->type = LABEL;
618 | NAME ':' stmnt { $$ = nn($1, ':',$3, ZN);
619 if ($1->sym->type != 0
620 && $1->sym->type != LABEL) {
621 non_fatal("bad label-name %s",
624 $1->sym->type = LABEL;
626 | NAME ':' { $$ = nn($1, ':',ZN,ZN);
627 if ($1->sym->type != 0
628 && $1->sym->type != LABEL) {
629 non_fatal("bad label-name %s",
632 $$->lft = nn(ZN, 'c', nn(ZN,CONST,ZN,ZN), ZN);
633 $$->lft->lft->val = 1; /* skip */
634 $1->sym->type = LABEL;
636 | error { $$ = nn(ZN, 'c', nn(ZN,CONST,ZN,ZN), ZN);
637 $$->lft->val = 1; /* skip */
641 Stmnt : varref ASGN full_expr { $$ = nn($1, ASGN, $1, $3);
643 nochan_manip($1, $3, 0);
646 | varref INCR { $$ = nn(ZN,CONST, ZN, ZN); $$->val = 1;
647 $$ = nn(ZN, '+', $1, $$);
648 $$ = nn($1, ASGN, $1, $$);
651 if ($1->sym->type == CHAN)
652 fatal("arithmetic on chan", (char *)0);
654 | varref DECR { $$ = nn(ZN,CONST, ZN, ZN); $$->val = 1;
655 $$ = nn(ZN, '-', $1, $$);
656 $$ = nn($1, ASGN, $1, $$);
659 if ($1->sym->type == CHAN)
660 fatal("arithmetic on chan id's", (char *)0);
662 | SET_P l_par two_args r_par { $$ = nn(ZN, SET_P, $3, ZN); has_priority++; }
663 | PRINT l_par STRING { realread = 0; }
664 prargs r_par { $$ = nn($3, PRINT, $5, ZN); realread = 1; }
665 | PRINTM l_par varref r_par { $$ = nn(ZN, PRINTM, $3, ZN); }
666 | PRINTM l_par CONST r_par { $$ = nn(ZN, PRINTM, $3, ZN); }
667 | ASSERT full_expr { $$ = nn(ZN, ASSERT, $2, ZN); AST_track($2, 0); }
669 | varref R_RCV { Expand_Ok++; }
670 rargs { Expand_Ok--; has_io++;
671 $$ = nn($1, 'r', $1, $4);
672 $$->val = has_random = 1;
673 trackchanuse($4, ZN, 'R');
675 | varref RCV { Expand_Ok++; }
676 LT rargs GT { Expand_Ok--; has_io++;
677 $$ = nn($1, 'r', $1, $5);
678 $$->val = 2; /* fifo poll */
679 trackchanuse($5, ZN, 'R');
681 | varref R_RCV { Expand_Ok++; }
682 LT rargs GT { Expand_Ok--; has_io++; /* rrcv poll */
683 $$ = nn($1, 'r', $1, $5);
684 $$->val = 3; has_random = 1;
685 trackchanuse($5, ZN, 'R');
687 | varref O_SND { Expand_Ok++; }
688 margs { Expand_Ok--; has_io++;
689 $$ = nn($1, 's', $1, $4);
690 $$->val = has_sorted = 1;
691 trackchanuse($4, ZN, 'S');
694 | full_expr { $$ = nn(ZN, 'c', $1, ZN); count_runs($$); }
695 | ELSE { $$ = nn(ZN,ELSE,ZN,ZN);
697 | ATOMIC '{' { open_seq(0); }
698 sequence OS '}' { $$ = nn($1, ATOMIC, ZN, ZN);
699 $$->sl = seqlist(close_seq(3), 0);
702 make_atomic($$->sl->this, 0);
704 | D_STEP '{' { open_seq(0);
707 sequence OS '}' { $$ = nn($1, D_STEP, ZN, ZN);
708 $$->sl = seqlist(close_seq(4), 0);
711 make_atomic($$->sl->this, D_ATOM);
714 | '{' { open_seq(0); }
715 sequence OS '}' { $$ = nn(ZN, NON_ATOMIC, ZN, ZN);
716 $$->sl = seqlist(close_seq(5), 0);
721 l_par args r_par { initialization_ok = 0;
722 pickup_inline($1->sym, $4, ZN);
727 | varref ASGN INAME { IArgs++; }
728 l_par args r_par { initialization_ok = 0;
729 pickup_inline($3->sym, $6, $1);
733 | RETURN full_expr { $$ = return_statement($2); }
736 options : option { $$->sl = seqlist($1->sq, 0); }
737 | option options { $$->sl = seqlist($1->sq, $2->sl); }
740 option : SEP { open_seq(0); }
741 sequence OS { $$ = nn(ZN,0,ZN,ZN);
742 $$->sq = close_seq(6);
749 | semi { /* redundant semi at end of sequence */ }
756 MS : semi { /* at least one semi-colon */ }
757 | MS semi { /* but more are okay too */ }
760 aname : NAME { $$ = $1; }
764 const_expr: CONST { $$ = $1; }
765 | '-' const_expr %prec UMIN { $$ = $2; $$->val = -($2->val); }
766 | l_par const_expr r_par { $$ = $2; }
767 | const_expr '+' const_expr { $$ = $1; $$->val = $1->val + $3->val; }
768 | const_expr '-' const_expr { $$ = $1; $$->val = $1->val - $3->val; }
769 | const_expr '*' const_expr { $$ = $1; $$->val = $1->val * $3->val; }
770 | const_expr '/' const_expr { $$ = $1; $$->val = $1->val / $3->val; }
771 | const_expr '%' const_expr { $$ = $1; $$->val = $1->val % $3->val; }
774 expr : l_par expr r_par { $$ = $2; }
775 | expr '+' expr { $$ = nn(ZN, '+', $1, $3); }
776 | expr '-' expr { $$ = nn(ZN, '-', $1, $3); }
777 | expr '*' expr { $$ = nn(ZN, '*', $1, $3); }
778 | expr '/' expr { $$ = nn(ZN, '/', $1, $3); }
779 | expr '%' expr { $$ = nn(ZN, '%', $1, $3); }
780 | expr '&' expr { $$ = nn(ZN, '&', $1, $3); }
781 | expr '^' expr { $$ = nn(ZN, '^', $1, $3); }
782 | expr '|' expr { $$ = nn(ZN, '|', $1, $3); }
783 | expr GT expr { $$ = nn(ZN, GT, $1, $3); }
784 | expr LT expr { $$ = nn(ZN, LT, $1, $3); }
785 | expr GE expr { $$ = nn(ZN, GE, $1, $3); }
786 | expr LE expr { $$ = nn(ZN, LE, $1, $3); }
787 | expr EQ expr { $$ = nn(ZN, EQ, $1, $3); }
788 | expr NE expr { $$ = nn(ZN, NE, $1, $3); }
789 | expr AND expr { $$ = nn(ZN, AND, $1, $3); }
790 | expr OR expr { $$ = nn(ZN, OR, $1, $3); }
791 | expr LSHIFT expr { $$ = nn(ZN, LSHIFT,$1, $3); }
792 | expr RSHIFT expr { $$ = nn(ZN, RSHIFT,$1, $3); }
793 | '~' expr { $$ = nn(ZN, '~', $2, ZN); }
794 | '-' expr %prec UMIN { $$ = nn(ZN, UMIN, $2, ZN); }
795 | SND expr %prec NEG { $$ = nn(ZN, '!', $2, ZN); }
797 | l_par expr ARROW expr ':' expr r_par {
798 $$ = nn(ZN, OR, $4, $6);
799 $$ = nn(ZN, '?', $2, $$);
802 | RUN aname { Expand_Ok++;
804 fatal("used 'run' outside proctype",
808 Opt_priority { Expand_Ok--;
809 $$ = nn($2, RUN, $5, ZN);
810 $$->val = ($7) ? $7->val : 0;
811 trackchanuse($5, $2, 'A'); trackrun($$);
813 | LEN l_par varref r_par { $$ = nn($3, LEN, $3, ZN); }
814 | ENABLED l_par expr r_par { $$ = nn(ZN, ENABLED, $3, ZN); has_enabled++; }
815 | GET_P l_par expr r_par { $$ = nn(ZN, GET_P, $3, ZN); has_priority++; }
816 | varref RCV { Expand_Ok++; }
817 '[' rargs ']' { Expand_Ok--; has_io++;
818 $$ = nn($1, 'R', $1, $5);
820 | varref R_RCV { Expand_Ok++; }
821 '[' rargs ']' { Expand_Ok--; has_io++;
822 $$ = nn($1, 'R', $1, $5);
823 $$->val = has_random = 1;
825 | varref { $$ = $1; trapwonly($1 /*, "varref" */); }
827 | CONST { $$ = nn(ZN,CONST,ZN,ZN);
828 $$->ismtyp = $1->ismtyp;
831 | TIMEOUT { $$ = nn(ZN,TIMEOUT, ZN, ZN); }
832 | NONPROGRESS { $$ = nn(ZN,NONPROGRESS, ZN, ZN);
835 | PC_VAL l_par expr r_par { $$ = nn(ZN, PC_VAL, $3, ZN);
838 | PNAME '[' expr ']' '@' NAME
839 { $$ = rem_lab($1->sym, $3, $6->sym); }
840 | PNAME '[' expr ']' ':' pfld
841 { $$ = rem_var($1->sym, $3, $6->sym, $6->lft); }
842 | PNAME '@' NAME { $$ = rem_lab($1->sym, ZN, $3->sym); }
843 | PNAME ':' pfld { $$ = rem_var($1->sym, ZN, $3->sym, $3->lft); }
844 | ltl_expr { $$ = $1; /* sanity_check($1); */ }
847 Opt_priority: /* none */ { $$ = ZN; }
848 | PRIORITY CONST { $$ = $2; has_priority++; }
851 full_expr: expr { $$ = $1; }
855 ltl_expr: expr UNTIL expr { $$ = nn(ZN, UNTIL, $1, $3); }
856 | expr RELEASE expr { $$ = nn(ZN, RELEASE, $1, $3); }
857 | expr WEAK_UNTIL expr { $$ = nn(ZN, ALWAYS, $1, ZN);
858 $$ = nn(ZN, OR, $$, nn(ZN, UNTIL, $1, $3));
860 | expr IMPLIES expr {
861 $$ = nn(ZN, '!', $1, ZN);
862 $$ = nn(ZN, OR, $$, $3);
864 | expr EQUIV expr { $$ = nn(ZN, EQUIV, $1, $3); }
865 | NEXT expr %prec NEG { $$ = nn(ZN, NEXT, $2, ZN); }
866 | ALWAYS expr %prec NEG { $$ = nn(ZN, ALWAYS,$2, ZN); }
867 | EVENTUALLY expr %prec NEG { $$ = nn(ZN, EVENTUALLY, $2, ZN); }
870 /* an Expr cannot be negated - to protect Probe expressions */
871 Expr : Probe { $$ = $1; }
872 | l_par Expr r_par { $$ = $2; }
873 | Expr AND Expr { $$ = nn(ZN, AND, $1, $3); }
874 | Expr AND expr { $$ = nn(ZN, AND, $1, $3); }
875 | expr AND Expr { $$ = nn(ZN, AND, $1, $3); }
876 | Expr OR Expr { $$ = nn(ZN, OR, $1, $3); }
877 | Expr OR expr { $$ = nn(ZN, OR, $1, $3); }
878 | expr OR Expr { $$ = nn(ZN, OR, $1, $3); }
881 Probe : FULL l_par varref r_par { $$ = nn($3, FULL, $3, ZN); }
882 | NFULL l_par varref r_par { $$ = nn($3, NFULL, $3, ZN); }
883 | EMPTY l_par varref r_par { $$ = nn($3, EMPTY, $3, ZN); }
884 | NEMPTY l_par varref r_par { $$ = nn($3,NEMPTY, $3, ZN); }
887 Opt_enabler: /* none */ { $$ = ZN; }
888 | PROVIDED l_par full_expr r_par { if (!proper_enabler($3))
889 { non_fatal("invalid PROVIDED clause",
895 | PROVIDED error { $$ = ZN;
896 non_fatal("usage: provided ( ..expr.. )",
901 basetype: TYPE { $$->sym = ZS;
903 if ($$->val == UNSIGNED)
904 fatal("unsigned cannot be used as mesg type", 0);
906 | UNAME { $$->sym = $1->sym;
909 | error /* e.g., unsigned ':' const */
912 typ_list: basetype { $$ = nn($1, $1->val, ZN, ZN); }
913 | basetype ',' typ_list { $$ = nn($1, $1->val, ZN, $3); }
916 two_args: expr ',' expr { $$ = nn(ZN, ',', $1, $3); }
919 args : /* empty */ { $$ = ZN; }
923 prargs : /* empty */ { $$ = ZN; }
924 | ',' arg { $$ = $2; }
927 margs : arg { $$ = $1; }
928 | expr l_par arg r_par { if ($1->ntyp == ',')
929 $$ = tail_add($1, $3);
931 $$ = nn(ZN, ',', $1, $3);
935 arg : expr { if ($1->ntyp == ',')
938 $$ = nn(ZN, ',', $1, ZN);
940 | expr ',' arg { if ($1->ntyp == ',')
941 $$ = tail_add($1, $3);
943 $$ = nn(ZN, ',', $1, $3);
947 rarg : varref { $$ = $1; trackvar($1, $1);
948 trapwonly($1 /*, "rarg" */); }
949 | EVAL l_par expr r_par { $$ = nn(ZN,EVAL,$3,ZN);
950 trapwonly($1 /*, "eval rarg" */); }
951 | CONST { $$ = nn(ZN,CONST,ZN,ZN);
952 $$->ismtyp = $1->ismtyp;
955 | '-' CONST %prec UMIN { $$ = nn(ZN,CONST,ZN,ZN);
956 $$->val = - ($2->val);
960 rargs : rarg { if ($1->ntyp == ',')
963 $$ = nn(ZN, ',', $1, ZN);
965 | rarg ',' rargs { if ($1->ntyp == ',')
966 $$ = tail_add($1, $3);
968 $$ = nn(ZN, ',', $1, $3);
970 | rarg l_par rargs r_par { if ($1->ntyp == ',')
971 $$ = tail_add($1, $3);
973 $$ = nn(ZN, ',', $1, $3);
975 | l_par rargs r_par { $$ = $2; }
978 nlst : NAME { $$ = nn($1, NAME, ZN, ZN);
979 $$ = nn(ZN, ',', $$, ZN); }
980 | nlst NAME { $$ = nn($2, NAME, ZN, ZN);
981 $$ = nn(ZN, ',', $$, $1);
983 | nlst ',' { $$ = $1; /* commas optional */ }
987 #define binop(n, sop) fprintf(fd, "("); recursive(fd, n->lft); \
988 fprintf(fd, ") %s (", sop); recursive(fd, n->rgt); \
990 #define unop(n, sop) fprintf(fd, "%s (", sop); recursive(fd, n->lft); \
994 recursive(FILE *fd, Lextok *n)
1016 case RELEASE: /* see http://en.wikipedia.org/wiki/Linear_temporal_logic */
1032 fprintf(fd, "c_expr { %s }", put_inline(fd, n->sym->name));
1041 ltl_to_string(Lextok *n)
1042 { Lextok *m = nn(ZN, 0, ZN, ZN);
1044 char ltl_formula[2048];
1045 FILE *tf = fopen(TMP_FILE1, "w+"); /* tmpfile() fails on Windows 7 */
1047 /* convert the parsed ltl to a string
1048 by writing into a file, using existing functions,
1049 and then passing it to the existing interface for
1050 conversion into a never claim
1051 (this means parsing everything twice, which is
1052 a little redundant, but adds only miniscule overhead)
1056 { fatal("cannot create temporary file", (char *) 0);
1061 (void) fseek(tf, 0L, SEEK_SET);
1063 memset(ltl_formula, 0, sizeof(ltl_formula));
1064 retval = fgets(ltl_formula, sizeof(ltl_formula), tf);
1067 (void) unlink(TMP_FILE1);
1070 { printf("%p\n", retval);
1071 fatal("could not translate ltl ltl_formula", 0);
1074 if (1) printf("ltl %s: %s\n", ltl_name, ltl_formula);
1076 m->sym = lookup(ltl_formula);
1084 return (t == EVENTUALLY || t == ALWAYS || t == UNTIL
1085 || t == WEAK_UNTIL || t == RELEASE);
1091 return (t == AND || t == OR || t == IMPLIES || t == EQUIV);
1095 /* flags correct formula like: ltl { true U (true U true) } */
1097 sanity_check(Lextok *t) /* check proper embedding of ltl_expr */
1100 sanity_check(t->lft);
1101 sanity_check(t->rgt);
1103 if (t->lft && t->rgt)
1104 { if (!is_boolean(t->ntyp)
1105 && (is_temporal(t->lft->ntyp)
1106 || is_temporal(t->rgt->ntyp)))
1107 { printf("spin: attempt to apply '");
1110 explain(t->lft->ntyp);
1112 explain(t->rgt->ntyp);
1114 /* non_fatal("missing parentheses?", (char *)0); */
1120 yyerror(char *fmt, ...)
1122 non_fatal(fmt, (char *) 0);