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

/* Copyright (c) 1991 by AT&T Bell Telephone Laboratories, Inc.
 * All Rights Reserved. This software is for educational purposes only.
 * No part of this source code may be reproduced in any form
 * without explicit written permission from the copyright owner.
 * This software was written by Gerard J. Holzmann, as part of the book
 * ``Design and Validation of Computer Protocols,'' ISBN 0-13-539925-4,
 * Prentice Hall, Englewood Cliffs, NJ, 07632.
 * Send bug-reports to: gerard@research.att.com
 */

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

Element *
eval_sub(e)
	Element *e;
{
	Element *f, *g;
	SeqList *z;
	int i, j, k;
	extern int Rvous, lineno;
	extern Symbol *Fname;

	if (!e->n)
		return (Element *)0;
	if (e->n->ntyp == GOTO)
		return (!Rvous)?get_lab(e->n->nsym):(Element *)0;
	if (e->sub)
	{	for (z = e->sub, j=0; z; z = z->nxt)
			j++;
		k = rand()%j;	/* nondeterminism */
		for (i = 0, z = e->sub; i < j+k; i++)
		{	if (i >= k && (f = eval_sub(z->this->frst)))
				return f;
			z = (z->nxt)?z->nxt:e->sub;
		}
	} else
	{	if (e->n->ntyp == ATOMIC)
		{	f = e->n->seql->this->frst;
			g = e->n->seql->this->last;
			g->nxt = e->nxt;
			if (!(g = eval_sub(f)))	/* atomic guard */
				return (Element *)0;
			Rvous=0;
			while (g && (g->status & (ATOM|L_ATOM))
			&& !(f->status & L_ATOM))
			{	f = g;
				g = eval_sub(f);
			}
			if (!g)
			{	wrapup();
				lineno = f->n->nval;
				fatal("atomic seq blocks", (char *)0);
			}
			return g;
		} else if (Rvous)
		{	if (eval_sync(e->n))
				return e->nxt;
		} else
			return (eval(e->n))?e->nxt:(Element *)0;
	}
	return (Element *)0;
}

eval_sync(now)
	Node *now;
{	/* allow only synchronous receives
	/* and related node types    */

	if (now)
	switch (now->ntyp) {
	case TIMEOUT:	case PRINT:	case ASSERT:
	case RUN:	case LEN:	case 's':
	case 'c':	case ASGN:	case BREAK:
	case IF:	case DO:	case '.':
		return 0;
	case 'R':
	case 'r':
		if (!q_is_sync(now))
			return 0;
	}
	return eval(now);
}

eval(now)
	Node *now;
{
	extern int Tval, lineno;
	extern Symbol *Fname;
	if (now)
	switch (now->ntyp) {
	case CONST: return now->nval;
	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   '<': 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 TIMEOUT: return Tval;

	case   RUN: return enable(now->nsym, now->lft);
	case   LEN: return qlen(now);
	case   's': return qsend(now);		/* send         */
	case   'r': return qrecv(now, 1);	/* full-receive */
	case   'R': return qrecv(now, 0);	/* test only    */
	case   'c': return eval(now->lft);	/* condition    */
	case   'p': return remotevar(now);
	case   'q': return remotelab(now);
	case PRINT: return interprint(now);
	case  ASGN: return setval(now->lft, eval(now->rgt));
	case  NAME: return getval(now->nsym, eval(now->lft));
	case ASSERT: if (eval(now->lft)) return 1;
		     yyerror("assertion violated", (char *) 0);
		     wrapup(); exit(1);
	case  IF: case DO: case BREAK:	/* compound structure */
	case   '.': return 1;	/* return label for compound */
	case   '@': return 0;	/* stop state */
	default   : printf("spin: bad node type %d (run)\n", now->ntyp);
		    fflush(stdout);
		    exit(1);
	}
	return 0;
}

interprint(n)
	Node *n;
{
	Node *tmp = n->lft;
	char c, *s = n->nsym->name;
	int i, j;
	
	for (i = 0; i < strlen(s); i++)
		switch (s[i]) {
		default:   putchar(s[i]); break;
		case '\"': break; /* ignore */
		case '\\':
			 switch(s[++i]) {
			 case 't': putchar('\t'); break;
			 case 'n': putchar('\n'); break;
			 default:  putchar(s[i]); break;
			 }
			 break;
		case  '%':
			 if ((c = s[++i]) == '%')
			 {	putchar('%'); /* literal */
				break;
			 }
			 if (!tmp)
			 {	yyerror("too few print args %s", s);
				break;
			 }
			 j = eval(tmp->lft);
			 tmp = tmp->rgt;
			 switch(c) {
			 case 'c': printf("%c", j); break;
			 case 'd': printf("%d", j); break;
			 case 'o': printf("%o", j); break;
			 case 'u': printf("%u", j); break;
			 case 'x': printf("%x", j); break;
			 default:  yyerror("unrecognized print cmd %%'%c'", c);
				   break;
			 }
			 break;
		}
	fflush(stdout);
	return 1;
}