/***** spin: run.c *****/

/* Copyright (c) 1989-2003 by Lucent Technologies, Bell Laboratories.     */
/* All Rights Reserved.  This software is for educational purposes only.  */
/* No guarantee whatsoever is expressed or implied by the distribution of */
/* this code.  Permission is given to distribute this code provided that  */
/* this introductory message is not removed and no monies are exchanged.  */
/* Software written by Gerard J. Holzmann.  For tool documentation see:   */
/*             http://spinroot.com/                                       */
/* Send all bug-reports and/or questions to: [email protected]            */

#include <stdlib.h>
#include "spin.h"
#include "y.tab.h"

extern RunList	*X, *run;
extern Symbol	*Fname;
extern Element	*LastStep;
extern int	Rvous, lineno, Tval, interactive, MadeChoice;
extern int	TstOnly, verbose, s_trail, xspin, jumpsteps, depth;
extern int	analyze, nproc, nstop, no_print, like_java;

static long	Seed = 1;
static int	E_Check = 0, Escape_Check = 0;

static int	eval_sync(Element *);
static int	pc_enabled(Lextok *n);
extern void	sr_buf(int, int);

void
Srand(unsigned int s)
{	Seed = s;
}

long
Rand(void)
{	/* CACM 31(10), Oct 1988 */
	Seed = 16807*(Seed%127773) - 2836*(Seed/127773);
	if (Seed <= 0) Seed += 2147483647;
	return Seed;
}

Element *
rev_escape(SeqList *e)
{	Element *r;

	if (!e)
		return (Element *) 0;

	if ((r = rev_escape(e->nxt)) != ZE) /* reversed order */
		return r;

	return eval_sub(e->this->frst);		
}

Element *
eval_sub(Element *e)
{	Element *f, *g;
	SeqList *z;
	int i, j, k, only_pos;

	if (!e || !e->n)
		return ZE;
#ifdef DEBUG
	printf("\n\teval_sub(%d %s: line %d) ",
		e->Seqno, e->esc?"+esc":"", e->n?e->n->ln:0);
	comment(stdout, e->n, 0);
	printf("\n");
#endif
	if (e->n->ntyp == GOTO)
	{	if (Rvous) return ZE;
		LastStep = e;
		f = get_lab(e->n, 1);
		f = huntele(f, e->status, -1); /* 5.2.3: was missing */
		cross_dsteps(e->n, f->n);
#ifdef DEBUG
		printf("GOTO leads to %d\n", f->seqno);
#endif
		return f;
	}
	if (e->n->ntyp == UNLESS)
	{	/* escapes were distributed into sequence */
		return eval_sub(e->sub->this->frst);
	} else if (e->sub)	/* true for IF, DO, and UNLESS */
	{	Element *has_else = ZE;
		Element *bas_else = ZE;
		int nr_else = 0, nr_choices = 0;
		only_pos = -1;

		if (interactive
		&& !MadeChoice && !E_Check
		&& !Escape_Check
		&& !(e->status&(D_ATOM))
		&& depth >= jumpsteps)
		{	printf("Select stmnt (");
			whoruns(0); printf(")\n");
			if (nproc-nstop > 1)
			{	printf("\tchoice 0: other process\n");
				nr_choices++;
				only_pos = 0;
		}	}
		for (z = e->sub, j=0; z; z = z->nxt)
		{	j++;
			if (interactive
			&& !MadeChoice && !E_Check
			&& !Escape_Check
			&& !(e->status&(D_ATOM))
			&& depth >= jumpsteps
			&& z->this->frst
			&& (xspin || (verbose&32) || Enabled0(z->this->frst)))
			{	if (z->this->frst->n->ntyp == ELSE)
				{	has_else = (Rvous)?ZE:z->this->frst->nxt;
					nr_else = j;
					continue;
				}
				printf("\tchoice %d: ", j);
#if 0
				if (z->this->frst->n)
					printf("line %d, ", z->this->frst->n->ln);
#endif
				if (!Enabled0(z->this->frst))
					printf("unexecutable, ");
				else
				{	nr_choices++;
					only_pos = j;
				}
				comment(stdout, z->this->frst->n, 0);
				printf("\n");
		}	}

		if (nr_choices == 0 && has_else)
		{	printf("\tchoice %d: (else)\n", nr_else);
			only_pos = nr_else;
		}

		if (nr_choices <= 1 && only_pos != -1 && !MadeChoice)
		{	MadeChoice = only_pos;
		}

		if (interactive && depth >= jumpsteps
		&& !Escape_Check
		&& !(e->status&(D_ATOM))
		&& !E_Check)
		{	if (!MadeChoice)
			{	char buf[256];
				if (xspin)
					printf("Make Selection %d\n\n", j);
				else
					printf("Select [0-%d]: ", j);
				fflush(stdout);
				if (scanf("%64s", buf) <= 0)
				{	printf("no input\n");
					return ZE;
				}
				if (isdigit((int)buf[0]))
					k = atoi(buf);
				else
				{	if (buf[0] == 'q')
						alldone(0);
					k = -1;
				}
			} else
			{	k = MadeChoice;
				MadeChoice = 0;
			}
			if (k < 1 || k > j)
			{	if (k != 0) printf("\tchoice outside range\n");
				return ZE;
			}
			k--;
		} else
		{	if (e->n && e->n->indstep >= 0)
				k = 0;	/* select 1st executable guard */
			else
				k = Rand()%j;	/* nondeterminism */
		}

		has_else = ZE;
		bas_else = ZE;
		for (i = 0, z = e->sub; i < j+k; i++)
		{	if (z->this->frst
			&&  z->this->frst->n->ntyp == ELSE)
			{	bas_else = z->this->frst;
				has_else = (Rvous)?ZE:bas_else->nxt;
				if (!interactive || depth < jumpsteps
				|| Escape_Check
				|| (e->status&(D_ATOM)))
				{	z = (z->nxt)?z->nxt:e->sub;
					continue;
				}
			}
			if (z->this->frst
			&&  ((z->this->frst->n->ntyp == ATOMIC
			  ||  z->this->frst->n->ntyp == D_STEP)
			  &&  z->this->frst->n->sl->this->frst->n->ntyp == ELSE))
			{	bas_else = z->this->frst->n->sl->this->frst;
				has_else = (Rvous)?ZE:bas_else->nxt;
				if (!interactive || depth < jumpsteps
				|| Escape_Check
				|| (e->status&(D_ATOM)))
				{	z = (z->nxt)?z->nxt:e->sub;
					continue;
				}
			}
			if (i >= k)
			{	if ((f = eval_sub(z->this->frst)) != ZE)
					return f;
				else if (interactive && depth >= jumpsteps
				&& !(e->status&(D_ATOM)))
				{	if (!E_Check && !Escape_Check)
						printf("\tunexecutable\n");
					return ZE;
			}	}
			z = (z->nxt)?z->nxt:e->sub;
		}
		LastStep = bas_else;
		return has_else;
	} else
	{	if (e->n->ntyp == ATOMIC
		||  e->n->ntyp == D_STEP)
		{	f = e->n->sl->this->frst;
			g = e->n->sl->this->last;
			g->nxt = e->nxt;
			if (!(g = eval_sub(f)))	/* atomic guard */
				return ZE;
			return g;
		} else if (e->n->ntyp == NON_ATOMIC)
		{	f = e->n->sl->this->frst;
			g = e->n->sl->this->last;
			g->nxt = e->nxt;		/* close it */
			return eval_sub(f);
		} else if (e->n->ntyp == '.')
		{	if (!Rvous) return e->nxt;
			return eval_sub(e->nxt);
		} else
		{	SeqList *x;
			if (!(e->status & (D_ATOM))
			&&  e->esc && verbose&32)
			{	printf("Stmnt [");
				comment(stdout, e->n, 0);
				printf("] has escape(s): ");
				for (x = e->esc; x; x = x->nxt)
				{	printf("[");
					g = x->this->frst;
					if (g->n->ntyp == ATOMIC
					||  g->n->ntyp == NON_ATOMIC)
						g = g->n->sl->this->frst;
					comment(stdout, g->n, 0);
					printf("] ");
				}
				printf("\n");
			}
#if 0
			if (!(e->status & D_ATOM))	/* escapes don't reach inside d_steps */
			/* 4.2.4: only the guard of a d_step can have an escape */
#endif
#if 1
			if (!s_trail)	/* trail determines selections, new 5.2.5 */
#endif
			{	Escape_Check++;
				if (like_java)
				{	if ((g = rev_escape(e->esc)) != ZE)
					{	if (verbose&4)
							printf("\tEscape taken\n");
						Escape_Check--;
						return g;
					}
				} else
				{	for (x = e->esc; x; x = x->nxt)
					{	if ((g = eval_sub(x->this->frst)) != ZE)
						{	if (verbose&4)
							{	printf("\tEscape taken ");
								if (g->n && g->n->fn)
									printf("%s:%d", g->n->fn->name, g->n->ln);
								printf("\n");
							}
							Escape_Check--;
							return g;
				}	}	}
				Escape_Check--;
			}
		
			switch (e->n->ntyp) {
			case TIMEOUT: case RUN:
			case PRINT: case PRINTM:
			case C_CODE: case C_EXPR:
			case ASGN: case ASSERT:
			case 's': case 'r': case 'c':
				/* toplevel statements only */
				LastStep = e;
			default:
				break;
			}
			if (Rvous)
			{
				return (eval_sync(e))?e->nxt:ZE;
			}
			return (eval(e->n))?e->nxt:ZE;
		}
	}
	return ZE; /* not reached */
}

static int
eval_sync(Element *e)
{	/* allow only synchronous receives
	   and related node types    */
	Lextok *now = (e)?e->n:ZN;

	if (!now
	||  now->ntyp != 'r'
	||  now->val >= 2	/* no rv with a poll */
	||  !q_is_sync(now))
	{
		return 0;
	}

	LastStep = e;
	return eval(now);
}

static int
assign(Lextok *now)
{	int t;

	if (TstOnly) return 1;

	switch (now->rgt->ntyp) {
	case FULL:	case NFULL:
	case EMPTY:	case NEMPTY:
	case RUN:	case LEN:
		t = BYTE;
		break;
	default:
		t = Sym_typ(now->rgt);
		break;
	}
	typ_ck(Sym_typ(now->lft), t, "assignment"); 
	return setval(now->lft, eval(now->rgt));
}

static int
nonprogress(void)	/* np_ */
{	RunList	*r;

	for (r = run; r; r = r->nxt)
	{	if (has_lab(r->pc, 4))	/* 4=progress */
			return 0;
	}
	return 1;
}

int
eval(Lextok *now)
{
	if (now) {
	lineno = now->ln;
	Fname  = now->fn;
#ifdef DEBUG
	printf("eval ");
	comment(stdout, now, 0);
	printf("\n");
#endif
	switch (now->ntyp) {
	case CONST: return now->val;
	case   '!': return !eval(now->lft);
	case  UMIN: return -eval(now->lft);
	case   '~': return ~eval(now->lft);

	case   '/': return (eval(now->lft) / eval(now->rgt));
	case   '*': return (eval(now->lft) * eval(now->rgt));
	case   '-': return (eval(now->lft) - eval(now->rgt));
	case   '+': return (eval(now->lft) + eval(now->rgt));
	case   '%': return (eval(now->lft) % eval(now->rgt));
	case    LT: return (eval(now->lft) <  eval(now->rgt));
	case    GT: return (eval(now->lft) >  eval(now->rgt));
	case   '&': return (eval(now->lft) &  eval(now->rgt));
	case   '^': return (eval(now->lft) ^  eval(now->rgt));
	case   '|': return (eval(now->lft) |  eval(now->rgt));
	case    LE: return (eval(now->lft) <= eval(now->rgt));
	case    GE: return (eval(now->lft) >= eval(now->rgt));
	case    NE: return (eval(now->lft) != eval(now->rgt));
	case    EQ: return (eval(now->lft) == eval(now->rgt));
	case    OR: return (eval(now->lft) || eval(now->rgt));
	case   AND: return (eval(now->lft) && eval(now->rgt));
	case LSHIFT: return (eval(now->lft) << eval(now->rgt));
	case RSHIFT: return (eval(now->lft) >> eval(now->rgt));
	case   '?': return (eval(now->lft) ? eval(now->rgt->lft)
					   : eval(now->rgt->rgt));

	case     'p': return remotevar(now);	/* _p for remote reference */
	case     'q': return remotelab(now);
	case     'R': return qrecv(now, 0);	/* test only    */
	case     LEN: return qlen(now);
	case    FULL: return (qfull(now));
	case   EMPTY: return (qlen(now)==0);
	case   NFULL: return (!qfull(now));
	case  NEMPTY: return (qlen(now)>0);
	case ENABLED: if (s_trail) return 1;
		      return pc_enabled(now->lft);
	case    EVAL: return eval(now->lft);
	case  PC_VAL: return pc_value(now->lft);
	case NONPROGRESS: return nonprogress();
	case    NAME: return getval(now);

	case TIMEOUT: return Tval;
	case     RUN: return TstOnly?1:enable(now);

	case   's': return qsend(now);		/* send         */
	case   'r': return qrecv(now, 1);	/* receive or poll */
	case   'c': return eval(now->lft);	/* condition    */
	case PRINT: return TstOnly?1:interprint(stdout, now);
	case PRINTM: return TstOnly?1:printm(stdout, now);
	case  ASGN: return assign(now);

	case C_CODE: if (!analyze)
		     {	printf("%s:\t", now->sym->name);
		     	plunk_inline(stdout, now->sym->name, 0, 1);
		     }
		     return 1; /* uninterpreted */

	case C_EXPR: if (!analyze)
		     {	printf("%s:\t", now->sym->name);
		     	plunk_expr(stdout, now->sym->name);
		     	printf("\n");
		     }
		     return 1; /* uninterpreted */

	case ASSERT: if (TstOnly || eval(now->lft)) return 1;
		     non_fatal("assertion violated", (char *) 0);
			printf("spin: text of failed assertion: assert(");
			comment(stdout, now->lft, 0);
			printf(")\n");
		     if (s_trail && !xspin) return 1;
		     wrapup(1); /* doesn't return */

	case  IF: case DO: case BREAK: case UNLESS:	/* compound */
	case   '.': return 1;	/* return label for compound */
	case   '@': return 0;	/* stop state */
	case  ELSE: return 1;	/* only hit here in guided trails */
	default   : printf("spin: bad node type %d (run)\n", now->ntyp);
		    if (s_trail) printf("spin: trail file doesn't match spec?\n");
		    fatal("aborting", 0);
	}}
	return 0;
}

int
printm(FILE *fd, Lextok *n)
{	extern char Buf[];
	int j;

	Buf[0] = '\0';
	if (!no_print)
	if (!s_trail || depth >= jumpsteps) {
		if (n->lft->ismtyp)
			j = n->lft->val;
		else
			j = eval(n->lft);
		sr_buf(j, 1);
		dotag(fd, Buf);
	}
	return 1;
}

int
interprint(FILE *fd, Lextok *n)
{	Lextok *tmp = n->lft;
	char c, *s = n->sym->name;
	int i, j; char lbuf[512]; /* matches value in sr_buf() */
	extern char Buf[];	/* global, size 4096 */
	char tBuf[4096];	/* match size of global Buf[] */

	Buf[0] = '\0';
	if (!no_print)
	if (!s_trail || depth >= jumpsteps) {
	for (i = 0; i < (int) strlen(s); i++)
		switch (s[i]) {
		case '\"': break; /* ignore */
		case '\\':
			 switch(s[++i]) {
			 case 't': strcat(Buf, "\t"); break;
			 case 'n': strcat(Buf, "\n"); break;
			 default:  goto onechar;
			 }
			 break;
		case  '%':
			 if ((c = s[++i]) == '%')
			 {	strcat(Buf, "%"); /* literal */
				break;
			 }
			 if (!tmp)
			 {	non_fatal("too few print args %s", s);
				break;
			 }
			 j = eval(tmp->lft);
			 tmp = tmp->rgt;
			 switch(c) {
			 case 'c': sprintf(lbuf, "%c", j); break;
			 case 'd': sprintf(lbuf, "%d", j); break;

			 case 'e': strcpy(tBuf, Buf);	/* event name */
				   Buf[0] = '\0';
				   sr_buf(j, 1);
				   strcpy(lbuf, Buf);
				   strcpy(Buf, tBuf);
				   break;

			 case 'o': sprintf(lbuf, "%o", j); break;
			 case 'u': sprintf(lbuf, "%u", (unsigned) j); break;
			 case 'x': sprintf(lbuf, "%x", j); break;
			 default:  non_fatal("bad print cmd: '%s'", &s[i-1]);
				   lbuf[0] = '\0'; break;
			 }
			 goto append;
		default:
onechar:		 lbuf[0] = s[i]; lbuf[1] = '\0';
append:			 strcat(Buf, lbuf);
			 break;
		}
		dotag(fd, Buf);
	}
	if (strlen(Buf) >= 4096) fatal("printf string too long", 0);
	return 1;
}

static int
Enabled1(Lextok *n)
{	int i; int v = verbose;

	if (n)
	switch (n->ntyp) {
	case 'c':
		if (has_typ(n->lft, RUN))
			return 1;	/* conservative */
		/* else fall through */
	default:	/* side-effect free */
		verbose = 0;
		E_Check++;
		i = eval(n);
		E_Check--;
		verbose = v;
		return i;

	case C_CODE: case C_EXPR:
	case PRINT: case PRINTM:
	case   ASGN: case ASSERT:
		return 1;

	case 's':
		if (q_is_sync(n))
		{	if (Rvous) return 0;
			TstOnly = 1; verbose = 0;
			E_Check++;
			i = eval(n);
			E_Check--;
			TstOnly = 0; verbose = v;
			return i;
		}
		return (!qfull(n));
	case 'r':
		if (q_is_sync(n))
			return 0;	/* it's never a user-choice */
		n->ntyp = 'R'; verbose = 0;
		E_Check++;
		i = eval(n);
		E_Check--;
		n->ntyp = 'r'; verbose = v;
		return i;
	}
	return 0;
}

int
Enabled0(Element *e)
{	SeqList *z;

	if (!e || !e->n)
		return 0;

	switch (e->n->ntyp) {
	case '@':
		return X->pid == (nproc-nstop-1);
	case '.':
		return 1;
	case GOTO:
		if (Rvous) return 0;
		return 1;
	case UNLESS:
		return Enabled0(e->sub->this->frst);
	case ATOMIC:
	case D_STEP:
	case NON_ATOMIC:
		return Enabled0(e->n->sl->this->frst);
	}
	if (e->sub)	/* true for IF, DO, and UNLESS */
	{	for (z = e->sub; z; z = z->nxt)
			if (Enabled0(z->this->frst))
				return 1;
		return 0;
	}
	for (z = e->esc; z; z = z->nxt)
	{	if (Enabled0(z->this->frst))
			return 1;
	}
#if 0
	printf("enabled1 ");
	comment(stdout, e->n, 0);
	printf(" ==> %s\n", Enabled1(e->n)?"yes":"nope");
#endif
	return Enabled1(e->n);
}

int
pc_enabled(Lextok *n)
{	int i = nproc - nstop;
	int pid = eval(n);
	int result = 0;
	RunList *Y, *oX;

	if (pid == X->pid)
		fatal("used: enabled(pid=thisproc) [%s]", X->n->name);

	for (Y = run; Y; Y = Y->nxt)
		if (--i == pid)
		{	oX = X; X = Y;
			result = Enabled0(Y->pc);
			X = oX;
			break;
		}
	return result;
}