1 /***** spin: run.c *****/
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 */
16 extern RunList
*X
, *run
;
18 extern Element
*LastStep
;
19 extern int Rvous
, lineno
, Tval
, interactive
, MadeChoice
;
20 extern int TstOnly
, verbose
, s_trail
, xspin
, jumpsteps
, depth
;
21 extern int nproc
, nstop
, no_print
, like_java
;
24 static int E_Check
= 0, Escape_Check
= 0;
26 static int eval_sync(Element
*);
27 static int pc_enabled(Lextok
*n
);
28 extern void sr_buf(int, int);
37 { /* CACM 31(10), Oct 1988 */
38 Seed
= 16807*(Seed
%127773) - 2836*(Seed
/127773);
39 if (Seed
<= 0) Seed
+= 2147483647;
44 rev_escape(SeqList
*e
)
50 if ((r
= rev_escape(e
->nxt
)) != ZE
) /* reversed order */
53 return eval_sub(e
->this->frst
);
65 printf("\n\teval_sub(%d %s: line %d) ",
66 e
->Seqno
, e
->esc
?"+esc":"", e
->n
?e
->n
->ln
:0);
67 comment(stdout
, e
->n
, 0);
70 if (e
->n
->ntyp
== GOTO
)
71 { if (Rvous
) return ZE
;
74 cross_dsteps(e
->n
, f
->n
);
77 if (e
->n
->ntyp
== UNLESS
)
78 { /* escapes were distributed into sequence */
79 return eval_sub(e
->sub
->this->frst
);
80 } else if (e
->sub
) /* true for IF, DO, and UNLESS */
81 { Element
*has_else
= ZE
;
82 Element
*bas_else
= ZE
;
83 int nr_else
= 0, nr_choices
= 0;
86 && !MadeChoice
&& !E_Check
88 && !(e
->status
&(D_ATOM
))
89 && depth
>= jumpsteps
)
90 { printf("Select stmnt (");
91 whoruns(0); printf(")\n");
93 printf("\tchoice 0: other process\n");
95 for (z
= e
->sub
, j
=0; z
; z
= z
->nxt
)
98 && !MadeChoice
&& !E_Check
100 && !(e
->status
&(D_ATOM
))
101 && depth
>= jumpsteps
103 && (xspin
|| (verbose
&32) || Enabled0(z
->this->frst
)))
104 { if (z
->this->frst
->n
->ntyp
== ELSE
)
105 { has_else
= (Rvous
)?ZE
:z
->this->frst
->nxt
;
109 printf("\tchoice %d: ", j
);
111 if (z
->this->frst
->n
)
112 printf("line %d, ", z
->this->frst
->n
->ln
);
114 if (!Enabled0(z
->this->frst
))
115 printf("unexecutable, ");
118 comment(stdout
, z
->this->frst
->n
, 0);
122 if (nr_choices
== 0 && has_else
)
123 printf("\tchoice %d: (else)\n", nr_else
);
125 if (interactive
&& depth
>= jumpsteps
127 && !(e
->status
&(D_ATOM
))
132 printf("Make Selection %d\n\n", j
);
134 printf("Select [0-%d]: ", j
);
149 { if (k
!= 0) printf("\tchoice outside range\n");
154 { if (e
->n
&& e
->n
->indstep
>= 0)
155 k
= 0; /* select 1st executable guard */
157 k
= Rand()%j
; /* nondeterminism */
161 for (i
= 0, z
= e
->sub
; i
< j
+k
; i
++)
163 && z
->this->frst
->n
->ntyp
== ELSE
)
164 { bas_else
= z
->this->frst
;
165 has_else
= (Rvous
)?ZE
:bas_else
->nxt
;
166 if (!interactive
|| depth
< jumpsteps
168 || (e
->status
&(D_ATOM
)))
169 { z
= (z
->nxt
)?z
->nxt
:e
->sub
;
174 && ((z
->this->frst
->n
->ntyp
== ATOMIC
175 || z
->this->frst
->n
->ntyp
== D_STEP
)
176 && z
->this->frst
->n
->sl
->this->frst
->n
->ntyp
== ELSE
))
177 { bas_else
= z
->this->frst
->n
->sl
->this->frst
;
178 has_else
= (Rvous
)?ZE
:bas_else
->nxt
;
179 if (!interactive
|| depth
< jumpsteps
181 || (e
->status
&(D_ATOM
)))
182 { z
= (z
->nxt
)?z
->nxt
:e
->sub
;
187 { if ((f
= eval_sub(z
->this->frst
)) != ZE
)
189 else if (interactive
&& depth
>= jumpsteps
190 && !(e
->status
&(D_ATOM
)))
191 { if (!E_Check
&& !Escape_Check
)
192 printf("\tunexecutable\n");
195 z
= (z
->nxt
)?z
->nxt
:e
->sub
;
200 { if (e
->n
->ntyp
== ATOMIC
201 || e
->n
->ntyp
== D_STEP
)
202 { f
= e
->n
->sl
->this->frst
;
203 g
= e
->n
->sl
->this->last
;
205 if (!(g
= eval_sub(f
))) /* atomic guard */
208 } else if (e
->n
->ntyp
== NON_ATOMIC
)
209 { f
= e
->n
->sl
->this->frst
;
210 g
= e
->n
->sl
->this->last
;
211 g
->nxt
= e
->nxt
; /* close it */
213 } else if (e
->n
->ntyp
== '.')
214 { if (!Rvous
) return e
->nxt
;
215 return eval_sub(e
->nxt
);
218 if (!(e
->status
& (D_ATOM
))
219 && e
->esc
&& verbose
&32)
221 comment(stdout
, e
->n
, 0);
222 printf("] has escape(s): ");
223 for (x
= e
->esc
; x
; x
= x
->nxt
)
226 if (g
->n
->ntyp
== ATOMIC
227 || g
->n
->ntyp
== NON_ATOMIC
)
228 g
= g
->n
->sl
->this->frst
;
229 comment(stdout
, g
->n
, 0);
235 if (!(e
->status
& D_ATOM
)) /* escapes don't reach inside d_steps */
236 /* 4.2.4: only the guard of a d_step can have an escape */
240 { if ((g
= rev_escape(e
->esc
)) != ZE
)
242 printf("\tEscape taken\n");
247 { for (x
= e
->esc
; x
; x
= x
->nxt
)
248 { if ((g
= eval_sub(x
->this->frst
)) != ZE
)
250 printf("\tEscape taken\n");
257 switch (e
->n
->ntyp
) {
258 case TIMEOUT
: case RUN
:
259 case PRINT
: case PRINTM
:
260 case C_CODE
: case C_EXPR
:
261 case ASGN
: case ASSERT
:
262 case 's': case 'r': case 'c':
263 /* toplevel statements only */
270 return (eval_sync(e
))?e
->nxt
:ZE
;
272 return (eval(e
->n
))?e
->nxt
:ZE
;
275 return ZE
; /* not reached */
279 eval_sync(Element
*e
)
280 { /* allow only synchronous receives
281 and related node types */
282 Lextok
*now
= (e
)?e
->n
:ZN
;
286 || now
->val
>= 2 /* no rv with a poll */
300 if (TstOnly
) return 1;
302 switch (now
->rgt
->ntyp
) {
303 case FULL
: case NFULL
:
304 case EMPTY
: case NEMPTY
:
309 t
= Sym_typ(now
->rgt
);
312 typ_ck(Sym_typ(now
->lft
), t
, "assignment");
313 return setval(now
->lft
, eval(now
->rgt
));
317 nonprogress(void) /* np_ */
320 for (r
= run
; r
; r
= r
->nxt
)
321 { if (has_lab(r
->pc
, 4)) /* 4=progress */
335 comment(stdout
, now
, 0);
339 case CONST
: return now
->val
;
340 case '!': return !eval(now
->lft
);
341 case UMIN
: return -eval(now
->lft
);
342 case '~': return ~eval(now
->lft
);
344 case '/': return (eval(now
->lft
) / eval(now
->rgt
));
345 case '*': return (eval(now
->lft
) * eval(now
->rgt
));
346 case '-': return (eval(now
->lft
) - eval(now
->rgt
));
347 case '+': return (eval(now
->lft
) + eval(now
->rgt
));
348 case '%': return (eval(now
->lft
) % eval(now
->rgt
));
349 case LT
: return (eval(now
->lft
) < eval(now
->rgt
));
350 case GT
: return (eval(now
->lft
) > eval(now
->rgt
));
351 case '&': return (eval(now
->lft
) & eval(now
->rgt
));
352 case '^': return (eval(now
->lft
) ^ eval(now
->rgt
));
353 case '|': return (eval(now
->lft
) | eval(now
->rgt
));
354 case LE
: return (eval(now
->lft
) <= eval(now
->rgt
));
355 case GE
: return (eval(now
->lft
) >= eval(now
->rgt
));
356 case NE
: return (eval(now
->lft
) != eval(now
->rgt
));
357 case EQ
: return (eval(now
->lft
) == eval(now
->rgt
));
358 case OR
: return (eval(now
->lft
) || eval(now
->rgt
));
359 case AND
: return (eval(now
->lft
) && eval(now
->rgt
));
360 case LSHIFT
: return (eval(now
->lft
) << eval(now
->rgt
));
361 case RSHIFT
: return (eval(now
->lft
) >> eval(now
->rgt
));
362 case '?': return (eval(now
->lft
) ? eval(now
->rgt
->lft
)
363 : eval(now
->rgt
->rgt
));
365 case 'p': return remotevar(now
); /* _p for remote reference */
366 case 'q': return remotelab(now
);
367 case 'R': return qrecv(now
, 0); /* test only */
368 case LEN
: return qlen(now
);
369 case FULL
: return (qfull(now
));
370 case EMPTY
: return (qlen(now
)==0);
371 case NFULL
: return (!qfull(now
));
372 case NEMPTY
: return (qlen(now
)>0);
373 case ENABLED
: if (s_trail
) return 1;
374 return pc_enabled(now
->lft
);
375 case EVAL
: return eval(now
->lft
);
376 case PC_VAL
: return pc_value(now
->lft
);
377 case NONPROGRESS
: return nonprogress();
378 case NAME
: return getval(now
);
380 case TIMEOUT
: return Tval
;
381 case RUN
: return TstOnly
?1:enable(now
);
383 case 's': return qsend(now
); /* send */
384 case 'r': return qrecv(now
, 1); /* receive or poll */
385 case 'c': return eval(now
->lft
); /* condition */
386 case PRINT
: return TstOnly
?1:interprint(stdout
, now
);
387 case PRINTM
: return TstOnly
?1:printm(stdout
, now
);
388 case ASGN
: return assign(now
);
390 case C_CODE
: printf("%s:\t", now
->sym
->name
);
391 plunk_inline(stdout
, now
->sym
->name
, 0);
392 return 1; /* uninterpreted */
394 case C_EXPR
: printf("%s:\t", now
->sym
->name
);
395 plunk_expr(stdout
, now
->sym
->name
);
397 return 1; /* uninterpreted */
399 case ASSERT
: if (TstOnly
|| eval(now
->lft
)) return 1;
400 non_fatal("assertion violated", (char *) 0);
401 printf("spin: text of failed assertion: assert(");
402 comment(stdout
, now
->lft
, 0);
404 if (s_trail
&& !xspin
) return 1;
405 wrapup(1); /* doesn't return */
407 case IF
: case DO
: case BREAK
: case UNLESS
: /* compound */
408 case '.': return 1; /* return label for compound */
409 case '@': return 0; /* stop state */
410 case ELSE
: return 1; /* only hit here in guided trails */
411 default : printf("spin: bad node type %d (run)\n", now
->ntyp
);
412 if (s_trail
) printf("spin: trail file doesn't match spec?\n");
413 fatal("aborting", 0);
419 printm(FILE *fd
, Lextok
*n
)
425 if (!s_trail
|| depth
>= jumpsteps
) {
437 interprint(FILE *fd
, Lextok
*n
)
438 { Lextok
*tmp
= n
->lft
;
439 char c
, *s
= n
->sym
->name
;
440 int i
, j
; char lbuf
[512]; /* matches value in sr_buf() */
441 extern char Buf
[]; /* global, size 4096 */
442 char tBuf
[4096]; /* match size of global Buf[] */
446 if (!s_trail
|| depth
>= jumpsteps
) {
447 for (i
= 0; i
< (int) strlen(s
); i
++)
449 case '\"': break; /* ignore */
452 case 't': strcat(Buf
, "\t"); break;
453 case 'n': strcat(Buf
, "\n"); break;
454 default: goto onechar
;
458 if ((c
= s
[++i
]) == '%')
459 { strcat(Buf
, "%"); /* literal */
463 { non_fatal("too few print args %s", s
);
469 case 'c': sprintf(lbuf
, "%c", j
); break;
470 case 'd': sprintf(lbuf
, "%d", j
); break;
472 case 'e': strcpy(tBuf
, Buf
); /* event name */
479 case 'o': sprintf(lbuf
, "%o", j
); break;
480 case 'u': sprintf(lbuf
, "%u", (unsigned) j
); break;
481 case 'x': sprintf(lbuf
, "%x", j
); break;
482 default: non_fatal("bad print cmd: '%s'", &s
[i
-1]);
483 lbuf
[0] = '\0'; break;
487 onechar
: lbuf
[0] = s
[i
]; lbuf
[1] = '\0';
488 append
: strcat(Buf
, lbuf
);
493 if (strlen(Buf
) >= 4096) fatal("printf string too long", 0);
499 { int i
; int v
= verbose
;
504 if (has_typ(n
->lft
, RUN
))
505 return 1; /* conservative */
506 /* else fall through */
507 default: /* side-effect free */
515 case C_CODE
: case C_EXPR
:
516 case PRINT
: case PRINTM
:
517 case ASGN
: case ASSERT
:
522 { if (Rvous
) return 0;
523 TstOnly
= 1; verbose
= 0;
527 TstOnly
= 0; verbose
= v
;
533 return 0; /* it's never a user-choice */
534 n
->ntyp
= 'R'; verbose
= 0;
538 n
->ntyp
= 'r'; verbose
= v
;
551 switch (e
->n
->ntyp
) {
553 return X
->pid
== (nproc
-nstop
-1);
560 return Enabled0(e
->sub
->this->frst
);
564 return Enabled0(e
->n
->sl
->this->frst
);
566 if (e
->sub
) /* true for IF, DO, and UNLESS */
567 { for (z
= e
->sub
; z
; z
= z
->nxt
)
568 if (Enabled0(z
->this->frst
))
572 for (z
= e
->esc
; z
; z
= z
->nxt
)
573 { if (Enabled0(z
->this->frst
))
578 comment(stdout
, e
->n
, 0);
579 printf(" ==> %s\n", Enabled1(e
->n
)?"yes":"nope");
581 return Enabled1(e
->n
);
585 pc_enabled(Lextok
*n
)
586 { int i
= nproc
- nstop
;
592 fatal("used: enabled(pid=thisproc) [%s]", X
->n
->name
);
594 for (Y
= run
; Y
; Y
= Y
->nxt
)
597 result
= Enabled0(Y
->pc
);
This page took 0.115438 seconds and 4 git commands to generate.