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

extern FILE	*th;

typedef struct SRC {
	short ln, st;
	struct SRC *nxt;
} SRC;

SRC	*frst = (SRC *) 0;
SRC	*skip = (SRC *) 0;
int	col;

void
putskip(m)	/* states that need not be reached */
{	SRC *tmp;

	for (tmp = skip; tmp; tmp = tmp->nxt)
		if (tmp->st == m)
			return;
	tmp = (SRC *) emalloc(sizeof(SRC));
	tmp->st = (short) m;
	tmp->nxt = skip;
	skip = tmp;
}

void
putsrc(n, m)	/* match states to source lines */
{	SRC *tmp;

	for (tmp = frst; tmp; tmp = tmp->nxt)
		if (tmp->st == m)
		{	if (tmp->ln != n)
				printf("putsrc mismatch %d - %d\n");
			return;
		}
	tmp = (SRC *) emalloc(sizeof(SRC));
	tmp->ln = (short) n;
	tmp->st = (short) m;
	tmp->nxt = frst;
	frst = tmp;
}

void
dumpskip(n, m)
{	SRC *tmp, *lst;
	int j;

	fprintf(th, "uchar reached%d [] = {\n\t", m);
	for (j = 0, col = 0; j <= n; j++)
	{	lst = (SRC *) 0;
		for (tmp = skip; tmp; lst = tmp, tmp = tmp->nxt)
			if (tmp->st == j)
			{	putnr(1);
				if (lst)
					lst->nxt = tmp->nxt;
				else
					skip = tmp->nxt;
				break;
			}
		if (!tmp)
			putnr(0);
	}
	fprintf(th, "};\n");
	skip = (SRC *) 0;
}

void
dumpsrc(n, m)
{	SRC *tmp, *lst;
	int j;

	fprintf(th, "short src_ln%d [] = {\n\t", m);
	for (j = 0, col = 0; j <= n; j++)
	{	lst = (SRC *) 0;
		for (tmp = frst; tmp; lst = tmp, tmp = tmp->nxt)
			if (tmp->st == j)
			{	putnr(tmp->ln);
				if (lst)
					lst->nxt = tmp->nxt;
				else
					frst = tmp->nxt;
				break;
			}
		if (!tmp)
			putnr(0);
	}
	fprintf(th, "};\n");
	frst = (SRC *) 0;
	dumpskip(n, m);
}

void
putnr(n)
{
	if (col++ == 8)
	{	fprintf(th, "\n\t");
		col = 1;
	}
	fprintf(th, "%3d, ", n);
}