Subversion Repositories planix.SVN

Rev

Details | Last modification | View Log | RSS feed

Rev Author Line No. Line
2 - 1 
/***** spin: sched.c *****/
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 
#include <stdlib.h>
13 
#include "spin.h"
14 
#include "y.tab.h"
15 
 
16 
extern int	verbose, s_trail, analyze, no_wrapup;
17 
extern char	*claimproc, *eventmap, Buf[];
18 
extern Ordered	*all_names;
19 
extern Symbol	*Fname, *context;
20 
extern int	lineno, nr_errs, dumptab, xspin, jumpsteps, columns;
21 
extern int	u_sync, Elcnt, interactive, TstOnly, cutoff;
22 
extern short	has_enabled;
23 
extern int	limited_vis, old_scope_rules, product, nclaims;
24 
 
25 
RunList		*X   = (RunList  *) 0;
26 
RunList		*run = (RunList  *) 0;
27 
RunList		*LastX  = (RunList  *) 0; /* previous executing proc */
28 
ProcList	*rdy = (ProcList *) 0;
29 
Element		*LastStep = ZE;
30 
int		nproc=0, nstop=0, Tval=0;
31 
int		Rvous=0, depth=0, nrRdy=0, MadeChoice;
32 
short		Have_claim=0, Skip_claim=0;
33 
 
34 
static int	Priority_Sum = 0;
35 
static void	setlocals(RunList *);
36 
static void	setparams(RunList *, ProcList *, Lextok *);
37 
static void	talk(RunList *);
38 
 
39 
void
40 
runnable(ProcList *p, int weight, int noparams)
41 
{	RunList *r = (RunList *) emalloc(sizeof(RunList));
42 
 
43 
	r->n  = p->n;
44 
	r->tn = p->tn;
45 
	r->b  = p->b;
46 
	r->pid = nproc++ - nstop + Skip_claim;
47 
 
48 
	if (!noparams && ((verbose&4) || (verbose&32)))
49 
		printf("Starting %s with pid %d\n",
50 
			p->n?p->n->name:"--", r->pid);
51 
 
52 
	if (!p->s)
53 
		fatal("parsing error, no sequence %s",
54 
			p->n?p->n->name:"--");
55 
 
56 
	r->pc = huntele(p->s->frst, p->s->frst->status, -1);
57 
	r->ps = p->s;
58 
 
59 
	if (p->s->last)
60 
		p->s->last->status |= ENDSTATE; /* normal end state */
61 
 
62 
	r->nxt = run;
63 
	r->prov = p->prov;
64 
	r->priority = weight;
65 
 
66 
	if (noparams) setlocals(r);
67 
	Priority_Sum += weight;
68 
 
69 
	run = r;
70 
}
71 
 
72 
ProcList *
73 
ready(Symbol *n, Lextok *p, Sequence *s, int det, Lextok *prov, enum btypes b)
74 
	/* n=name, p=formals, s=body det=deterministic prov=provided */
75 
{	ProcList *r = (ProcList *) emalloc(sizeof(ProcList));
76 
	Lextok *fp, *fpt; int j; extern int Npars;
77 
 
78 
	r->n = n;
79 
	r->p = p;
80 
	r->s = s;
81 
	r->b = b;
82 
	r->prov = prov;
83 
	r->tn = nrRdy++;
84 
	if (det != 0 && det != 1)
85 
	{	fprintf(stderr, "spin: bad value for det (cannot happen)\n");
86 
	}
87 
	r->det = (short) det;
88 
	r->nxt = rdy;
89 
	rdy = r;
90 
 
91 
	for (fp  = p, j = 0;  fp;  fp = fp->rgt)
92 
	for (fpt = fp->lft;  fpt; fpt = fpt->rgt)
93 
		j++;	/* count # of parameters */
94 
	Npars = max(Npars, j);
95 
 
96 
	return rdy;
97 
}
98 
 
99 
int
100 
find_maxel(Symbol *s)
101 
{	ProcList *p;
102 
 
103 
	for (p = rdy; p; p = p->nxt)
104 
		if (p->n == s)
105 
			return p->s->maxel++;
106 
	return Elcnt++;
107 
}
108 
 
109 
static void
110 
formdump(void)
111 
{	ProcList *p;
112 
	Lextok *f, *t;
113 
	int cnt;
114 
 
115 
	for (p = rdy; p; p = p->nxt)
116 
	{	if (!p->p) continue;
117 
		cnt = -1;
118 
		for (f = p->p; f; f = f->rgt)	/* types */
119 
		for (t = f->lft; t; t = t->rgt)	/* formals */
120 
		{	if (t->ntyp != ',')
121 
				t->sym->Nid = cnt--;	/* overload Nid */
122 
			else
123 
				t->lft->sym->Nid = cnt--;
124 
		}
125 
	}
126 
}
127 
 
128 
void
129 
announce(char *w)
130 
{
131 
	if (columns)
132 
	{	extern char Buf[];
133 
		extern int firstrow;
134 
		firstrow = 1;
135 
		if (columns == 2)
136 
		{	sprintf(Buf, "%d:%s",
137 
			run->pid - Have_claim, run->n->name);
138 
			pstext(run->pid - Have_claim, Buf);
139 
		} else
140 
			printf("proc %d = %s\n",
141 
			run->pid - Have_claim, run->n->name);
142 
		return;
143 
	}
144 
 
145 
	if (dumptab
146 
	||  analyze
147 
	||  product
148 
	||  s_trail
149 
	|| !(verbose&4))
150 
		return;
151 
 
152 
	if (w)
153 
		printf("  0:	proc  - (%s) ", w);
154 
	else
155 
		whoruns(1);
156 
	printf("creates proc %2d (%s)",
157 
		run->pid - Have_claim,
158 
		run->n->name);
159 
	if (run->priority > 1)
160 
		printf(" priority %d", run->priority);
161 
	printf("\n");
162 
}
163 
 
164 
#ifndef MAXP
165 
#define MAXP	255	/* matches max nr of processes in verifier */
166 
#endif
167 
 
168 
int
169 
enable(Lextok *m)
170 
{	ProcList *p;
171 
	Symbol *s = m->sym;	/* proctype name */
172 
	Lextok *n = m->lft;	/* actual parameters */
173 
 
174 
	if (m->val < 1) m->val = 1;	/* minimum priority */
175 
	for (p = rdy; p; p = p->nxt)
176 
		if (strcmp(s->name, p->n->name) == 0)
177 
		{	if (nproc-nstop >= MAXP)
178 
			{	printf("spin: too many processes (%d max)\n", MAXP);
179 
				break;
180 
			}
181 
			runnable(p, m->val, 0);
182 
			announce((char *) 0);
183 
			setparams(run, p, n);
184 
			setlocals(run); /* after setparams */
185 
			return run->pid - Have_claim + Skip_claim; /* effective simu pid */
186 
		}
187 
	return 0; /* process not found */
188 
}
189 
 
190 
void
191 
check_param_count(int i, Lextok *m)
192 
{	ProcList *p;
193 
	Symbol *s = m->sym;	/* proctype name */
194 
	Lextok *f, *t;		/* formal pars */
195 
	int cnt = 0;
196 
 
197 
	for (p = rdy; p; p = p->nxt)
198 
	{	if (strcmp(s->name, p->n->name) == 0)
199 
		{	if (m->lft)	/* actual param list */
200 
			{	lineno = m->lft->ln;
201 
				Fname  = m->lft->fn;
202 
			}
203 
			for (f = p->p;   f; f = f->rgt) /* one type at a time */
204 
			for (t = f->lft; t; t = t->rgt)	/* count formal params */
205 
			{	cnt++;
206 
			}
207 
			if (i != cnt)
208 
			{	printf("spin: saw %d parameters, expected %d\n", i, cnt);
209 
				non_fatal("wrong number of parameters", "");
210 
			}
211 
			break;
212 
	}	}
213 
}
214 
 
215 
void
216 
start_claim(int n)
217 
{	ProcList *p;
218 
	RunList  *r, *q = (RunList *) 0;
219 
 
220 
	for (p = rdy; p; p = p->nxt)
221 
		if (p->tn == n && p->b == N_CLAIM)
222 
		{	runnable(p, 1, 1);
223 
			goto found;
224 
		}
225 
	printf("spin: couldn't find claim %d (ignored)\n", n);
226 
	if (verbose&32)
227 
	for (p = rdy; p; p = p->nxt)
228 
		printf("\t%d = %s\n", p->tn, p->n->name);
229 
 
230 
	Skip_claim = 1;
231 
	goto done;
232 
found:
233 
	/* move claim to far end of runlist, and reassign it pid 0 */
234 
	if (columns == 2)
235 
	{	extern char Buf[];
236 
		depth = 0;
237 
		sprintf(Buf, "%d:%s", 0, p->n->name);
238 
		pstext(0, Buf);
239 
		for (r = run; r; r = r->nxt)
240 
		{	if (r->b != N_CLAIM)
241 
			{	sprintf(Buf, "%d:%s", r->pid+1, r->n->name);
242 
				pstext(r->pid+1, Buf);
243 
	}	}	}
244 
 
245 
	if (run->pid == 0) return; /* it is the first process started */
246 
 
247 
	q = run; run = run->nxt;
248 
	q->pid = 0; q->nxt = (RunList *) 0;	/* remove */
249 
done:
250 
	Have_claim = 1;
251 
	for (r = run; r; r = r->nxt)
252 
	{	r->pid = r->pid+Have_claim;	/* adjust */
253 
		if (!r->nxt)
254 
		{	r->nxt = q;
255 
			break;
256 
	}	}
257 
}
258 
 
259 
int
260 
f_pid(char *n)
261 
{	RunList *r;
262 
	int rval = -1;
263 
 
264 
	for (r = run; r; r = r->nxt)
265 
		if (strcmp(n, r->n->name) == 0)
266 
		{	if (rval >= 0)
267 
			{	printf("spin: remote ref to proctype %s, ", n);
268 
				printf("has more than one match: %d and %d\n",
269 
					rval, r->pid);
270 
			} else
271 
				rval = r->pid;
272 
		}
273 
	return rval;
274 
}
275 
 
276 
void
277 
wrapup(int fini)
278 
{
279 
	limited_vis = 0;
280 
	if (columns)
281 
	{	extern void putpostlude(void);
282 
		if (columns == 2) putpostlude();
283 
		if (!no_wrapup)
284 
		printf("-------------\nfinal state:\n-------------\n");
285 
	}
286 
	if (no_wrapup)
287 
		goto short_cut;
288 
	if (nproc != nstop)
289 
	{	int ov = verbose;
290 
		printf("#processes: %d\n", nproc-nstop - Have_claim + Skip_claim);
291 
		verbose &= ~4;
292 
		dumpglobals();
293 
		verbose = ov;
294 
		verbose &= ~1;	/* no more globals */
295 
		verbose |= 32;	/* add process states */
296 
		for (X = run; X; X = X->nxt)
297 
			talk(X);
298 
		verbose = ov;	/* restore */
299 
	}
300 
	printf("%d process%s created\n",
301 
		nproc - Have_claim + Skip_claim,
302 
		(xspin || nproc!=1)?"es":"");
303 
short_cut:
304 
	if (xspin) alldone(0);	/* avoid an abort from xspin */
305 
	if (fini)  alldone(1);
306 
}
307 
 
308 
static char is_blocked[256];
309 
 
310 
static int
311 
p_blocked(int p)
312 
{	int i, j;
313 
 
314 
	is_blocked[p%256] = 1;
315 
	for (i = j = 0; i < nproc - nstop; i++)
316 
		j += is_blocked[i];
317 
	if (j >= nproc - nstop)
318 
	{	memset(is_blocked, 0, 256);
319 
		return 1;
320 
	}
321 
	return 0;
322 
}
323 
 
324 
static Element *
325 
silent_moves(Element *e)
326 
{	Element *f;
327 
 
328 
	if (e->n)
329 
	switch (e->n->ntyp) {
330 
	case GOTO:
331 
		if (Rvous) break;
332 
		f = get_lab(e->n, 1);
333 
		cross_dsteps(e->n, f->n);
334 
		return f; /* guard against goto cycles */
335 
	case UNLESS:
336 
		return silent_moves(e->sub->this->frst);
337 
	case NON_ATOMIC:
338 
	case ATOMIC:
339 
	case D_STEP:
340 
		e->n->sl->this->last->nxt = e->nxt;
341 
		return silent_moves(e->n->sl->this->frst);
342 
	case '.':
343 
		return silent_moves(e->nxt);
344 
	}
345 
	return e;
346 
}
347 
 
348 
static RunList *
349 
pickproc(RunList *Y)
350 
{	SeqList *z; Element *has_else;
351 
	short Choices[256];
352 
	int j, k, nr_else = 0;
353 
 
354 
	if (nproc <= nstop+1)
355 
	{	X = run;
356 
		return NULL;
357 
	}
358 
	if (!interactive || depth < jumpsteps)
359 
	{	/* was: j = (int) Rand()%(nproc-nstop); */
360 
		if (Priority_Sum < nproc-nstop)
361 
			fatal("cannot happen - weights", (char *)0);
362 
		j = (int) Rand()%Priority_Sum;
363 
 
364 
		while (j - X->priority >= 0)
365 
		{	j -= X->priority;
366 
			Y = X;
367 
			X = X->nxt;
368 
			if (!X) { Y = NULL; X = run; }
369 
		}
370 
	} else
371 
	{	int only_choice = -1;
372 
		int no_choice = 0, proc_no_ch, proc_k;
373 
 
374 
		Tval = 0;	/* new 4.2.6 */
375 
try_again:	printf("Select a statement\n");
376 
try_more:	for (X = run, k = 1; X; X = X->nxt)
377 
		{	if (X->pid > 255) break;
378 
 
379 
			Choices[X->pid] = (short) k;
380 
 
381 
			if (!X->pc
382 
			||  (X->prov && !eval(X->prov)))
383 
			{	if (X == run)
384 
					Choices[X->pid] = 0;
385 
				continue;
386 
			}
387 
			X->pc = silent_moves(X->pc);
388 
			if (!X->pc->sub && X->pc->n)
389 
			{	int unex;
390 
				unex = !Enabled0(X->pc);
391 
				if (unex)
392 
					no_choice++;
393 
				else
394 
					only_choice = k;
395 
				if (!xspin && unex && !(verbose&32))
396 
				{	k++;
397 
					continue;
398 
				}
399 
				printf("\tchoice %d: ", k++);
400 
				p_talk(X->pc, 0);
401 
				if (unex)
402 
					printf(" unexecutable,");
403 
				printf(" [");
404 
				comment(stdout, X->pc->n, 0);
405 
				if (X->pc->esc) printf(" + Escape");
406 
				printf("]\n");
407 
			} else {
408 
			has_else = ZE;
409 
			proc_no_ch = no_choice;
410 
			proc_k = k;
411 
			for (z = X->pc->sub, j=0; z; z = z->nxt)
412 
			{	Element *y = silent_moves(z->this->frst);
413 
				int unex;
414 
				if (!y) continue;
415 
 
416 
				if (y->n->ntyp == ELSE)
417 
				{	has_else = (Rvous)?ZE:y;
418 
					nr_else = k++;
419 
					continue;
420 
				}
421 
 
422 
				unex = !Enabled0(y);
423 
				if (unex)
424 
					no_choice++;
425 
				else
426 
					only_choice = k;
427 
				if (!xspin && unex && !(verbose&32))
428 
				{	k++;
429 
					continue;
430 
				}
431 
				printf("\tchoice %d: ", k++);
432 
				p_talk(X->pc, 0);
433 
				if (unex)
434 
					printf(" unexecutable,");
435 
				printf(" [");
436 
				comment(stdout, y->n, 0);
437 
				printf("]\n");
438 
			}
439 
			if (has_else)
440 
			{	if (no_choice-proc_no_ch >= (k-proc_k)-1)
441 
				{	only_choice = nr_else;
442 
					printf("\tchoice %d: ", nr_else);
443 
					p_talk(X->pc, 0);
444 
					printf(" [else]\n");
445 
				} else
446 
				{	no_choice++;
447 
					printf("\tchoice %d: ", nr_else);
448 
					p_talk(X->pc, 0);
449 
					printf(" unexecutable, [else]\n");
450 
			}	}
451 
		}	}
452 
		X = run;
453 
		if (k - no_choice < 2 && Tval == 0)
454 
		{	Tval = 1;
455 
			no_choice = 0; only_choice = -1;
456 
			goto try_more;
457 
		}
458 
		if (xspin)
459 
			printf("Make Selection %d\n\n", k-1);
460 
		else
461 
		{	if (k - no_choice < 2)
462 
			{	printf("no executable choices\n");
463 
				alldone(0);
464 
			}
465 
			printf("Select [1-%d]: ", k-1);
466 
		}
467 
		if (!xspin && k - no_choice == 2)
468 
		{	printf("%d\n", only_choice);
469 
			j = only_choice;
470 
		} else
471 
		{	char buf[256];
472 
			fflush(stdout);
473 
			if (scanf("%64s", buf) == 0)
474 
			{	printf("\tno input\n");
475 
				goto try_again;
476 
			}
477 
			j = -1;
478 
			if (isdigit((int) buf[0]))
479 
				j = atoi(buf);
480 
			else
481 
			{	if (buf[0] == 'q')
482 
					alldone(0);
483 
			}
484 
			if (j < 1 || j >= k)
485 
			{	printf("\tchoice is outside range\n");
486 
				goto try_again;
487 
		}	}
488 
		MadeChoice = 0;
489 
		Y = NULL;
490 
		for (X = run; X; Y = X, X = X->nxt)
491 
		{	if (!X->nxt
492 
			||   X->nxt->pid > 255
493 
			||   j < Choices[X->nxt->pid])
494 
			{
495 
				MadeChoice = 1+j-Choices[X->pid];
496 
				break;
497 
		}	}
498 
	}
499 
	return Y;
500 
}
501 
 
502 
void
503 
multi_claims(void)
504 
{	ProcList *p, *q = NULL;
505 
 
506 
	if (nclaims > 1)
507 
	{	printf("  the model contains %d never claims:", nclaims);
508 
		for (p = rdy; p; p = p->nxt)
509 
		{	if (p->b == N_CLAIM)
510 
			{	printf("%s%s", q?", ":" ", p->n->name);
511 
				q = p;
512 
		}	}
513 
		printf("\n");
514 
		printf("  only one claim is used in a verification run\n");
515 
		printf("  choose which one with ./pan -N name (defaults to -N %s)\n",
516 
			q?q->n->name:"--");
517 
	}
518 
}
519 
 
520 
void
521 
sched(void)
522 
{	Element *e;
523 
	RunList *Y = NULL;	/* previous process in run queue */
524 
	RunList *oX;
525 
	int go, notbeyond = 0;
526 
#ifdef PC
527 
	int bufmax = 100;
528 
#endif
529 
	if (dumptab)
530 
	{	formdump();
531 
		symdump();
532 
		dumplabels();
533 
		return;
534 
	}
535 
 
536 
	if (has_enabled && u_sync > 0)
537 
	{	printf("spin: error, cannot use 'enabled()' in ");
538 
		printf("models with synchronous channels.\n");
539 
		nr_errs++;
540 
	}
541 
	if (product)
542 
	{	sync_product();
543 
		alldone(0);
544 
	}
545 
	if (analyze)
546 
	{	gensrc();
547 
		multi_claims();
548 
		return;
549 
	}
550 
	if (s_trail)
551 
	{	match_trail();
552 
		return;
553 
	}
554 
	if (claimproc)
555 
	printf("warning: never claim not used in random simulation\n");
556 
	if (eventmap)
557 
	printf("warning: trace assertion not used in random simulation\n");
558 
 
559 
	X = run;
560 
	Y = pickproc(Y);
561 
 
562 
	while (X)
563 
	{	context = X->n;
564 
		if (X->pc && X->pc->n)
565 
		{	lineno = X->pc->n->ln;
566 
			Fname  = X->pc->n->fn;
567 
		}
568 
		if (cutoff > 0 && depth >= cutoff)
569 
		{	printf("-------------\n");
570 
			printf("depth-limit (-u%d steps) reached\n", cutoff);
571 
			break;
572 
		}
573 
#ifdef PC
574 
		if (xspin && !interactive && --bufmax <= 0)
575 
		{	int c; /* avoid buffer overflow on pc's */
576 
			printf("spin: type return to proceed\n");
577 
			fflush(stdout);
578 
			c = getc(stdin);
579 
			if (c == 'q') wrapup(0);
580 
			bufmax = 100;
581 
		}
582 
#endif
583 
		depth++; LastStep = ZE;
584 
		oX = X;	/* a rendezvous could change it */
585 
		go = 1;
586 
		if (X->prov && X->pc
587 
		&& !(X->pc->status & D_ATOM)
588 
		&& !eval(X->prov))
589 
		{	if (!xspin && ((verbose&32) || (verbose&4)))
590 
			{	p_talk(X->pc, 1);
591 
				printf("\t<<Not Enabled>>\n");
592 
			}
593 
			go = 0;
594 
		}
595 
		if (go && (e = eval_sub(X->pc)))
596 
		{	if (depth >= jumpsteps
597 
			&& ((verbose&32) || (verbose&4)))
598 
			{	if (X == oX)
599 
				if (!(e->status & D_ATOM) || (verbose&32)) /* no talking in d_steps */
600 
				{	p_talk(X->pc, 1);
601 
					printf("	[");
602 
					if (!LastStep) LastStep = X->pc;
603 
					comment(stdout, LastStep->n, 0);
604 
					printf("]\n");
605 
				}
606 
				if (verbose&1) dumpglobals();
607 
				if (verbose&2) dumplocal(X);
608 
 
609 
				if (!(e->status & D_ATOM))
610 
				if (xspin)
611 
					printf("\n");
612 
			}
613 
			if (oX != X
614 
			||  (X->pc->status & (ATOM|D_ATOM)))		/* new 5.0 */
615 
			{	e = silent_moves(e);
616 
				notbeyond = 0;
617 
			}
618 
			oX->pc = e; LastX = X;
619 
 
620 
			if (!interactive) Tval = 0;
621 
			memset(is_blocked, 0, 256);
622 
 
623 
			if (X->pc && (X->pc->status & (ATOM|L_ATOM))
624 
			&&  (notbeyond == 0 || oX != X))
625 
			{	if ((X->pc->status & L_ATOM))
626 
					notbeyond = 1;
627 
				continue; /* no process switch */
628 
			}
629 
		} else
630 
		{	depth--;
631 
			if (oX->pc && (oX->pc->status & D_ATOM))
632 
			{	non_fatal("stmnt in d_step blocks", (char *)0);
633 
			}
634 
			if (X->pc
635 
			&&  X->pc->n
636 
			&&  X->pc->n->ntyp == '@'
637 
			&&  X->pid == (nproc-nstop-1))
638 
			{	if (X != run && Y != NULL)
639 
					Y->nxt = X->nxt;
640 
				else
641 
					run = X->nxt;
642 
				nstop++;
643 
				Priority_Sum -= X->priority;
644 
				if (verbose&4)
645 
				{	whoruns(1);
646 
					dotag(stdout, "terminates\n");
647 
				}
648 
				LastX = X;
649 
				if (!interactive) Tval = 0;
650 
				if (nproc == nstop) break;
651 
				memset(is_blocked, 0, 256);
652 
				/* proc X is no longer in runlist */
653 
				X = (X->nxt) ? X->nxt : run;
654 
			} else
655 
			{	if (p_blocked(X->pid))
656 
				{	if (Tval) break;
657 
					Tval = 1;
658 
					if (depth >= jumpsteps)
659 
					{	oX = X;
660 
						X = (RunList *) 0; /* to suppress indent */
661 
						dotag(stdout, "timeout\n");
662 
						X = oX;
663 
		}	}	}	}
664 
 
665 
		if (!run || !X) break;	/* new 5.0 */
666 
 
667 
		Y = pickproc(X);
668 
		notbeyond = 0;
669 
	}
670 
	context = ZS;
671 
	wrapup(0);
672 
}
673 
 
674 
int
675 
complete_rendez(void)
676 
{	RunList *orun = X, *tmp;
677 
	Element  *s_was = LastStep;
678 
	Element *e;
679 
	int j, ointer = interactive;
680 
 
681 
	if (s_trail)
682 
		return 1;
683 
	if (orun->pc->status & D_ATOM)
684 
		fatal("rv-attempt in d_step sequence", (char *)0);
685 
	Rvous = 1;
686 
	interactive = 0;
687 
 
688 
	j = (int) Rand()%Priority_Sum;	/* randomize start point */
689 
	X = run;
690 
	while (j - X->priority >= 0)
691 
	{	j -= X->priority;
692 
		X = X->nxt;
693 
		if (!X) X = run;
694 
	}
695 
	for (j = nproc - nstop; j > 0; j--)
696 
	{	if (X != orun
697 
		&& (!X->prov || eval(X->prov))
698 
		&& (e = eval_sub(X->pc)))
699 
		{	if (TstOnly)
700 
			{	X = orun;
701 
				Rvous = 0;
702 
				goto out;
703 
			}
704 
			if ((verbose&32) || (verbose&4))
705 
			{	tmp = orun; orun = X; X = tmp;
706 
				if (!s_was) s_was = X->pc;
707 
				p_talk(s_was, 1);
708 
				printf("	[");
709 
				comment(stdout, s_was->n, 0);
710 
				printf("]\n");
711 
				tmp = orun; orun = X; X = tmp;
712 
				if (!LastStep) LastStep = X->pc;
713 
				p_talk(LastStep, 1);
714 
				printf("	[");
715 
				comment(stdout, LastStep->n, 0);
716 
				printf("]\n");
717 
			}
718 
			Rvous = 0; /* before silent_moves */
719 
			X->pc = silent_moves(e);
720 
out:				interactive = ointer;
721 
			return 1;
722 
		}
723 
 
724 
		X = X->nxt;
725 
		if (!X) X = run;
726 
	}
727 
	Rvous = 0;
728 
	X = orun;
729 
	interactive = ointer;
730 
	return 0;
731 
}
732 
 
733 
/***** Runtime - Local Variables *****/
734 
 
735 
static void
736 
addsymbol(RunList *r, Symbol  *s)
737 
{	Symbol *t;
738 
	int i;
739 
 
740 
	for (t = r->symtab; t; t = t->next)
741 
		if (strcmp(t->name, s->name) == 0
742 
		&& (old_scope_rules
743 
		 || strcmp((const char *)t->bscp, (const char *)s->bscp) == 0))
744 
			return;		/* it's already there */
745 
 
746 
	t = (Symbol *) emalloc(sizeof(Symbol));
747 
	t->name = s->name;
748 
	t->type = s->type;
749 
	t->hidden = s->hidden;
750 
	t->nbits  = s->nbits;
751 
	t->nel  = s->nel;
752 
	t->ini  = s->ini;
753 
	t->setat = depth;
754 
	t->context = r->n;
755 
 
756 
	t->bscp  = (unsigned char *) emalloc(strlen((const char *)s->bscp)+1);
757 
	strcpy((char *)t->bscp, (const char *)s->bscp);
758 
 
759 
	if (s->type != STRUCT)
760 
	{	if (s->val)	/* if already initialized, copy info */
761 
		{	t->val = (int *) emalloc(s->nel*sizeof(int));
762 
			for (i = 0; i < s->nel; i++)
763 
				t->val[i] = s->val[i];
764 
		} else
765 
		{	(void) checkvar(t, 0);	/* initialize it */
766 
		}
767 
	} else
768 
	{	if (s->Sval)
769 
			fatal("saw preinitialized struct %s", s->name);
770 
		t->Slst = s->Slst;
771 
		t->Snm  = s->Snm;
772 
		t->owner = s->owner;
773 
	/*	t->context = r->n; */
774 
	}
775 
	t->next = r->symtab;	/* add it */
776 
	r->symtab = t;
777 
}
778 
 
779 
static void
780 
setlocals(RunList *r)
781 
{	Ordered	*walk;
782 
	Symbol	*sp;
783 
	RunList	*oX = X;
784 
 
785 
	X = r;
786 
	for (walk = all_names; walk; walk = walk->next)
787 
	{	sp = walk->entry;
788 
		if (sp
789 
		&&  sp->context
790 
		&&  strcmp(sp->context->name, r->n->name) == 0
791 
		&&  sp->Nid >= 0
792 
		&& (sp->type == UNSIGNED
793 
		||  sp->type == BIT
794 
		||  sp->type == MTYPE
795 
		||  sp->type == BYTE
796 
		||  sp->type == CHAN
797 
		||  sp->type == SHORT
798 
		||  sp->type == INT
799 
		||  sp->type == STRUCT))
800 
		{	if (!findloc(sp))
801 
			non_fatal("setlocals: cannot happen '%s'",
802 
				sp->name);
803 
		}
804 
	}
805 
	X = oX;
806 
}
807 
 
808 
static void
809 
oneparam(RunList *r, Lextok *t, Lextok *a, ProcList *p)
810 
{	int k; int at, ft;
811 
	RunList *oX = X;
812 
 
813 
	if (!a)
814 
		fatal("missing actual parameters: '%s'", p->n->name);
815 
	if (t->sym->nel > 1 || t->sym->isarray)
816 
		fatal("array in parameter list, %s", t->sym->name);
817 
	k = eval(a->lft);
818 
 
819 
	at = Sym_typ(a->lft);
820 
	X = r;	/* switch context */
821 
	ft = Sym_typ(t);
822 
 
823 
	if (at != ft && (at == CHAN || ft == CHAN))
824 
	{	char buf[256], tag1[64], tag2[64];
825 
		(void) sputtype(tag1, ft);
826 
		(void) sputtype(tag2, at);
827 
		sprintf(buf, "type-clash in params of %s(..), (%s<-> %s)",
828 
			p->n->name, tag1, tag2);
829 
		non_fatal("%s", buf);
830 
	}
831 
	t->ntyp = NAME;
832 
	addsymbol(r, t->sym);
833 
	(void) setval(t, k);
834 
 
835 
	X = oX;
836 
}
837 
 
838 
static void
839 
setparams(RunList *r, ProcList *p, Lextok *q)
840 
{	Lextok *f, *a;	/* formal and actual pars */
841 
	Lextok *t;	/* list of pars of 1 type */
842 
 
843 
	if (q)
844 
	{	lineno = q->ln;
845 
		Fname  = q->fn;
846 
	}
847 
	for (f = p->p, a = q; f; f = f->rgt) /* one type at a time */
848 
	for (t = f->lft; t; t = t->rgt, a = (a)?a->rgt:a)
849 
	{	if (t->ntyp != ',')
850 
			oneparam(r, t, a, p);	/* plain var */
851 
		else
852 
			oneparam(r, t->lft, a, p); /* expanded struct */
853 
	}
854 
}
855 
 
856 
Symbol *
857 
findloc(Symbol *s)
858 
{	Symbol *r;
859 
 
860 
	if (!X)
861 
	{	/* fatal("error, cannot eval '%s' (no proc)", s->name); */
862 
		return ZS;
863 
	}
864 
	for (r = X->symtab; r; r = r->next)
865 
		if (strcmp(r->name, s->name) == 0
866 
		&& (old_scope_rules || strcmp((const char *)r->bscp, (const char *)s->bscp) == 0))
867 
			break;
868 
	if (!r)
869 
	{	addsymbol(X, s);
870 
		r = X->symtab;
871 
	}
872 
	return r;
873 
}
874 
 
875 
int
876 
in_bound(Symbol *r, int n)
877 
{
878 
	if (!r)	return 0;
879 
 
880 
	if (n >= r->nel || n < 0)
881 
	{	printf("spin: indexing %s[%d] - size is %d\n",
882 
			r->name, n, r->nel);
883 
		non_fatal("indexing array \'%s\'", r->name);
884 
		return 0;
885 
	}
886 
	return 1;
887 
}
888 
 
889 
int
890 
getlocal(Lextok *sn)
891 
{	Symbol *r, *s = sn->sym;
892 
	int n = eval(sn->lft);
893 
 
894 
	r = findloc(s);
895 
	if (r && r->type == STRUCT)
896 
		return Rval_struct(sn, r, 1); /* 1 = check init */
897 
	if (in_bound(r, n))
898 
		return cast_val(r->type, r->val[n], r->nbits);
899 
	return 0;
900 
}
901 
 
902 
int
903 
setlocal(Lextok *p, int m)
904 
{	Symbol *r = findloc(p->sym);
905 
	int n = eval(p->lft);
906 
 
907 
	if (in_bound(r, n))
908 
	{	if (r->type == STRUCT)
909 
			(void) Lval_struct(p, r, 1, m); /* 1 = check init */
910 
		else
911 
		{
912 
#if 0
913 
			if (r->nbits > 0)
914 
				m = (m & ((1<<r->nbits)-1));
915 
			r->val[n] = m;
916 
#else
917 
			r->val[n] = cast_val(r->type, m, r->nbits);
918 
#endif
919 
			r->setat = depth;
920 
	}	}
921 
 
922 
	return 1;
923 
}
924 
 
925 
void
926 
whoruns(int lnr)
927 
{	if (!X) return;
928 
 
929 
	if (lnr) printf("%3d:	", depth);
930 
	printf("proc ");
931 
	if (Have_claim && X->pid == 0)
932 
		printf(" -");
933 
	else
934 
		printf("%2d", X->pid - Have_claim);
935 
	printf(" (%s) ", X->n->name);
936 
}
937 
 
938 
static void
939 
talk(RunList *r)
940 
{
941 
	if ((verbose&32) || (verbose&4))
942 
	{	p_talk(r->pc, 1);
943 
		printf("\n");
944 
		if (verbose&1) dumpglobals();
945 
		if (verbose&2) dumplocal(r);
946 
	}
947 
}
948 
 
949 
void
950 
p_talk(Element *e, int lnr)
951 
{	static int lastnever = -1;
952 
	static char nbuf[128];
953 
	int newnever = -1;
954 
 
955 
	if (e && e->n)
956 
		newnever = e->n->ln;
957 
 
958 
	if (Have_claim && X && X->pid == 0
959 
	&&  lastnever != newnever && e)
960 
	{	if (xspin)
961 
		{	printf("MSC: ~G line %d\n", newnever);
962 
#if 0
963 
			printf("%3d:	proc  - (NEVER) line   %d \"never\" ",
964 
				depth, newnever);
965 
			printf("(state 0)\t[printf('MSC: never\\\\n')]\n");
966 
		} else
967 
		{	printf("%3d:	proc  - (NEVER) line   %d \"never\"\n",
968 
				depth, newnever);
969 
#endif
970 
		}
971 
		lastnever = newnever;
972 
	}
973 
 
974 
	whoruns(lnr);
975 
	if (e)
976 
	{	if (e->n)
977 
		{	char *ptr = e->n->fn->name;
978 
			char *qtr = nbuf;
979 
			while (*ptr != '\0')
980 
			{	if (*ptr != '"')
981 
				{	*qtr++ = *ptr;
982 
				}
983 
				ptr++;
984 
			}
985 
			*qtr = '\0';
986 
		} else
987 
		{	strcpy(nbuf, "-");
988 
		}
989 
		printf("%s:%d (state %d)",
990 
			nbuf,
991 
			e->n?e->n->ln:-1,
992 
			e->seqno);
993 
		if (!xspin
994 
		&&  ((e->status&ENDSTATE) || has_lab(e, 2)))	/* 2=end */
995 
		{	printf(" <valid end state>");
996 
		}
997 
	}
998 
}
999 
 
1000 
int
1001 
remotelab(Lextok *n)
1002 
{	int i;
1003 
 
1004 
	lineno = n->ln;
1005 
	Fname  = n->fn;
1006 
	if (n->sym->type != 0 && n->sym->type != LABEL)
1007 
	{	printf("spin: error, type: %d\n", n->sym->type);
1008 
		fatal("not a labelname: '%s'", n->sym->name);
1009 
	}
1010 
	if (n->indstep >= 0)
1011 
	{	fatal("remote ref to label '%s' inside d_step",
1012 
			n->sym->name);
1013 
	}
1014 
	if ((i = find_lab(n->sym, n->lft->sym, 1)) == 0)
1015 
		fatal("unknown labelname: %s", n->sym->name);
1016 
	return i;
1017 
}
1018 
 
1019 
int
1020 
remotevar(Lextok *n)
1021 
{	int prno, i, added=0;
1022 
	RunList *Y, *oX;
1023 
	Lextok *onl;
1024 
	Symbol *os;
1025 
 
1026 
	lineno = n->ln;
1027 
	Fname  = n->fn;
1028 
 
1029 
	if (!n->lft->lft)
1030 
		prno = f_pid(n->lft->sym->name);
1031 
	else
1032 
	{	prno = eval(n->lft->lft); /* pid - can cause recursive call */
1033 
#if 0
1034 
		if (n->lft->lft->ntyp == CONST)	/* user-guessed pid */
1035 
#endif
1036 
		{	prno += Have_claim;
1037 
			added = Have_claim;
1038 
	}	}
1039 
 
1040 
	if (prno < 0)
1041 
		return 0;	/* non-existing process */
1042 
#if 0
1043 
	i = nproc - nstop;
1044 
	for (Y = run; Y; Y = Y->nxt)
1045 
	{	--i;
1046 
		printf("	%s: i=%d, prno=%d, ->pid=%d\n", Y->n->name, i, prno, Y->pid);
1047 
	}
1048 
#endif
1049 
	i = nproc - nstop + Skip_claim;	/* 6.0: added Skip_claim */
1050 
	for (Y = run; Y; Y = Y->nxt)
1051 
	if (--i == prno)
1052 
	{	if (strcmp(Y->n->name, n->lft->sym->name) != 0)
1053 
		{	printf("spin: remote reference error on '%s[%d]'\n",
1054 
				n->lft->sym->name, prno-added);
1055 
			non_fatal("refers to wrong proctype '%s'", Y->n->name);
1056 
		}
1057 
		if (strcmp(n->sym->name, "_p") == 0)
1058 
		{	if (Y->pc)
1059 
				return Y->pc->seqno;
1060 
			/* harmless, can only happen with -t */
1061 
			return 0;
1062 
		}
1063 
#if 1
1064 
		/* new 4.0 allow remote variables */
1065 
		oX = X;
1066 
		X = Y;
1067 
 
1068 
		onl = n->lft;
1069 
		n->lft = n->rgt;
1070 
 
1071 
		os = n->sym;
1072 
		n->sym = findloc(n->sym);
1073 
 
1074 
		i = getval(n);
1075 
 
1076 
		n->sym = os;
1077 
		n->lft = onl;
1078 
		X = oX;
1079 
		return i;
1080 
#else
1081 
		break;
1082 
#endif
1083 
	}
1084 
	printf("remote ref: %s[%d] ", n->lft->sym->name, prno-added);
1085 
	non_fatal("%s not found", n->sym->name);
1086 
	printf("have only:\n");
1087 
	i = nproc - nstop - 1;
1088 
	for (Y = run; Y; Y = Y->nxt, i--)
1089 
		if (!strcmp(Y->n->name, n->lft->sym->name))
1090 
		printf("\t%d\t%s\n", i, Y->n->name);
1091 
 
1092 
	return 0;
1093 
}