/***** spin: mesg.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"

#define MAXQ	2500		/* default max # queues  */

extern	int lineno, verbose;
Queue	*qtab = (Queue *) 0;	/* linked list of queues */
Queue	*ltab[MAXQ];		/* linear list of queues */
int	nqs=0;
int	Mpars=0;	/* max nr of message parameters  */

void
cnt_mpars(n)
	Node *n;
{
	Node *m;
	int i=0;

	for (m=n; m; m = m->rgt)
		i++;
	Mpars = max(Mpars, i);
}

qmake(s)
	Symbol *s;
{
	Node *m;
	Queue *q;
	int i; extern int analyze;

	if (!s->ini)
		return 0;
	if (s->ini->ntyp != CHAN)
		fatal("bad channel initializer for %s\n", s->name);
	if (nqs >= MAXQ)
		fatal("too many queues (%s)", s->name);

	q = (Queue *) emalloc(sizeof(Queue));
	q->qid = ++nqs;
	q->nslots = s->ini->nval;
	for (m = s->ini->rgt; m; m = m->rgt)
		q->nflds++;
	i = max(1, q->nslots);	/* 0-slot qs get 1 slot minimum */

	q->contents  = (int *) emalloc(q->nflds*i*sizeof(int));
	q->fld_width = (short *) emalloc(q->nflds*sizeof(short));
	for (m = s->ini->rgt, i = 0; m; m = m->rgt)
		q->fld_width[i++] = m->ntyp;
	q->nxt = qtab;
	qtab = q;
	ltab[q->qid-1] = q;

	return q->qid;
}

qlen(n)
	Node *n;
{
	int whichq = eval(n->lft)-1;

	if (whichq < MAXQ && whichq >= 0 && ltab[whichq])
		return ltab[whichq]->qlen;
	return 0;
}

q_is_sync(n)
	Node *n;
{
	int whichq = eval(n->lft)-1;

	if (whichq < MAXQ && whichq >= 0 && ltab[whichq])
		return (ltab[whichq]->nslots == 0);
	return 0;
}

qsend(n)
	Node *n;
{
	int whichq = eval(n->lft)-1;

	if (whichq == -1)
	{	printf("Error: sending to an uninitialized chan\n");
		whichq = 0;
	}
	if (whichq < MAXQ && whichq >= 0 && ltab[whichq])
	{	if (ltab[whichq]->nslots > 0)
			return a_snd(ltab[whichq], n);
		else
			return s_snd(ltab[whichq], n);
	}
	return 0;
}

qrecv(n, full)
	Node *n;
{
	int whichq = eval(n->lft)-1;

	if (whichq == -1)
	{	printf("Error: receiving from an uninitialized chan\n");
		whichq = 0;
	}
	if (whichq < MAXQ && whichq >= 0 && ltab[whichq])
		return a_rcv(ltab[whichq], n, full);
	return 0;
}

a_snd(q, n)
	Queue *q;
	Node *n;
{
	Node *m; extern int m_loss;
	int i = q->qlen*q->nflds;	/* q offset */
	int j = 0;			/* q field# */

	if (q->nslots > 0 && q->qlen >= q->nslots)
		return m_loss;	/* q is full */

	for (m = n->rgt; m && j < q->nflds; m = m->rgt, j++)
	{	typex(m->lft, q->fld_width[j]);
		q->contents[i+j] =
			cast_val(q->fld_width[j], eval(m->lft));
		if (verbose&16)
			sr_talk(n, eval(m->lft), "Send", "->", j, 
			  q->nflds, m->lft && m->lft->ntyp == CONST);
	}
	if (verbose&16)
	{	for (i = j; i < q->nflds; i++)
			sr_talk(n, 0, "Send", "->", i, q->nflds, 0);
		if (verbose&32)
		{ if (j < q->nflds)
			printf("\twarning: missing params in send\n");
		  if (m)
			printf("\twarning: too many params in send\n");
	}	}
	q->qlen++;
	return 1;
}

a_rcv(q, n, full)
	Queue *q;
	Node *n;
{
	Node *m;
	int j, k;
	if (q->qlen == 0)
		return 0;	/* q is empty */

	for (m = n->rgt, j=0; m && j < q->nflds; m = m->rgt, j++)
	{	if (m->lft->ntyp == CONST)
		{	if (q->contents[j] != m->lft->nval)
				return 0;	/* no match */
		} else if (m->lft->ntyp != NAME)
			fatal("bad arg in receive", (char *)0);
	}
	if (verbose&8 && verbose&32)
	{	if (j < q->nflds)
		  printf("\twarning: missing params in next recv\n");
		else if (m)
		  printf("\twarning: too many params in next recv\n");
	}
	for (m = n->rgt, j=0; j<q->nflds; m = (m)?m->rgt:m, j++)
	{	if (verbose&8)
			sr_talk(n, q->contents[j], "Recv", "<-", j,
				q->nflds, m && m->lft->ntyp == CONST);
		if (m && m->lft->ntyp == NAME)
		{	typex(m->lft, q->fld_width[j]);
			setval(m->lft, q->contents[j]);
		}
		for (k = 0; full && k < q->qlen-1; k++)
			q->contents[k*q->nflds+j] =
			  q->contents[(k+1)*q->nflds+j];
	}
	if (full) q->qlen--;
	return 1;
}

s_snd(q, n)
	Queue *q;
	Node *n;
{
	Node *m;
	int i, j = 0;	/* q field# */

	for (m = n->rgt; m && j < q->nflds; m = m->rgt, j++)
		q->contents[j] = cast_val(q->fld_width[j], eval(m->lft));

	q->qlen = 1;
	if (!complete_rendez())
	{	q->qlen = 0;
		return 0;
	}
	if (verbose&16)
	{	m = n->rgt;
		for (j = 0; m && j < q->nflds; m = m->rgt, j++)
		{	typex(m->lft, q->fld_width[j]);
			sr_talk(n, eval(m->lft), "Sent", "->", j,
			  q->nflds, m->lft && m->lft->ntyp == CONST);
		}
		for (i = j; i < q->nflds; i++)
			sr_talk(n, 0, "Sent", "->", i, q->nflds, 0);
		if (verbose&32)
		{	if (j < q->nflds)
			  printf("\twarning: missing params in send\n");
			if (m)
			  printf("\twarning: too many params in send\n");
	}	}
	return 1;
}

void
sr_talk(n, v, s, a, j, mx, named)
	Node *n;
	char *s, *a;
{
	if (j == 0)
	{	whoruns();
		printf("line %3d, %s ", n->nval, s);
	} else
		printf(",");
	sr_mesg(v, named);

	if (j == mx-1)
	{	printf("\t%s queue %d", a, eval(n->lft));
		if (n->nsym->type == CHAN)
			printf(" (%s", n->nsym->name);
		else
			printf(" (%s", lookup(n->nsym->name)->name);
		if (n->lft->lft)
			printf("[%d]", eval(n->lft->lft));
		printf(")\n");
	}
	fflush(stdout);
}

void
sr_mesg(v, j)
{	extern Node *Mtype;
	int cnt = 1;
	Node *n;
	for (n = Mtype; n && j; n = n->rgt, cnt++)
		if (cnt == v)
		{	printf("%s", n->lft->nsym->name);
			return;
		}
	printf("%d", v);
}

void
doq(s, n)
	Symbol *s;
{
	Queue *q;
	int j, k;
	if (!s->val)	/* uninitialized queue */
		return;
	for (q = qtab; q; q = q->nxt)
	if (q->qid == s->val[n])
	{	if (s->nel != 1)
		  printf("\t\tqueue %d (%s[%d]): ", q->qid, s->name, n);
		else
		  printf("\t\tqueue %d (%s): ", q->qid, s->name);
		for (k = 0; k < q->qlen; k++)
		{	printf("[");
			for (j = 0; j < q->nflds; j++)
			{	if (j > 0) printf(",");
				sr_mesg(q->contents[k*q->nflds+j], j==0);
			}
			printf("]");
		}
		printf("\n");
		break;
	}
}