/***** spin: guided.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: bugs@spinroot.com            */

#include "spin.h"
#include <sys/types.h>
#include <sys/stat.h>
#include <limits.h>
#include "y.tab.h"

extern RunList	*run, *X;
extern Element	*Al_El;
extern Symbol	*Fname, *oFname;
extern int	verbose, lineno, xspin, jumpsteps, depth, merger, cutoff;
extern int	nproc, nstop, Tval, ntrail, columns;
extern short	Have_claim, Skip_claim, has_code;
extern void ana_src(int, int);
extern char	**trailfilename;

int	TstOnly = 0, pno;

static int	lastclaim = -1;
static FILE	*fd;
static void	lost_trail(void);

static void
whichproc(int p)
{	RunList *oX;

	for (oX = run; oX; oX = oX->nxt)
		if (oX->pid == p)
		{	printf("(%s) ", oX->n->name);
			break;
		}
}

static int
newer(char *f1, char *f2)
{
#if defined(WIN32) || defined(WIN64)
	struct _stat x, y;
#else
	struct stat x, y;
#endif

	if (stat(f1, (struct stat *)&x) < 0) return 0;
	if (stat(f2, (struct stat *)&y) < 0) return 1;
	if (x.st_mtime < y.st_mtime) return 0;
	
	return 1;
}

void
hookup(void)
{	Element *e;

	for (e = Al_El; e; e = e->Nxt)
		if (e->n
		&& (e->n->ntyp == ATOMIC
		||  e->n->ntyp == NON_ATOMIC
		||  e->n->ntyp == D_STEP))
			(void) huntstart(e);
}

int
not_claim(void)
{
	return (!Have_claim || !X || X->pid != 0);
}

int globmin = INT_MAX;
int globmax = 0;

int
find_min(Sequence *s)
{	SeqList *l;
	Element *e;

	if (s->minel < 0)
	{	s->minel = INT_MAX;
		for (e = s->frst; e; e = e->nxt)
		{	if (e->status & 512)
			{	continue;
			}
			e->status |= 512;

			if (e->n->ntyp == ATOMIC
			||  e->n->ntyp == NON_ATOMIC
			||  e->n->ntyp == D_STEP)
			{	int n = find_min(e->n->sl->this);
				if (n < s->minel)
				{	s->minel = n;
				}
			} else if (e->Seqno < s->minel)
			{	s->minel = e->Seqno;
			}
			for (l = e->sub; l; l = l->nxt)
			{	int n = find_min(l->this);
				if (n < s->minel)
				{	s->minel = n;
		}	}	}
	}
	if (s->minel < globmin)
	{	globmin = s->minel;
	}
	return s->minel;
}

int
find_max(Sequence *s)
{
	if (s->last->Seqno > globmax)
	{	globmax = s->last->Seqno;
	}
	return s->last->Seqno;
}

void
match_trail(void)
{	int i, a, nst;
	Element *dothis;
	char snap[512], *q;

	if (has_code)
	{	printf("spin: important:\n");
		printf("  =======================================warning====\n");
		printf("  this model contains embedded c code statements\n");
		printf("  these statements will not be executed when the trail\n");
		printf("  is replayed in this way -- they are just printed,\n");
		printf("  which will likely lead to inaccurate variable values.\n");
		printf("  for an accurate replay use: ./pan -r\n");
		printf("  =======================================warning====\n\n");
	}

	/*
	 * if source model name is leader.pml
	 * look for the trail file under these names:
	 *	leader.pml.trail
	 *	leader.pml.tra
	 *	leader.trail
	 *	leader.tra
	 */

	if (trailfilename)
	{	if (strlen(*trailfilename) < sizeof(snap))
		{	strcpy(snap, (const char *) *trailfilename);
		} else
		{	fatal("filename %s too long", *trailfilename);
		}
	} else
	{	if (ntrail)
			sprintf(snap, "%s%d.trail", oFname->name, ntrail);
		else
			sprintf(snap, "%s.trail", oFname->name);
	}

	if ((fd = fopen(snap, "r")) == NULL)
	{	snap[strlen(snap)-2] = '\0';	/* .tra */
		if ((fd = fopen(snap, "r")) == NULL)
		{	if ((q = strchr(oFname->name, '.')) != NULL)
			{	*q = '\0';
				if (ntrail)
					sprintf(snap, "%s%d.trail",
						oFname->name, ntrail);
				else
					sprintf(snap, "%s.trail",
						oFname->name);
				*q = '.';

				if ((fd = fopen(snap, "r")) != NULL)
					goto okay;

				snap[strlen(snap)-2] = '\0';	/* last try */
				if ((fd = fopen(snap, "r")) != NULL)
					goto okay;
			}
			printf("spin: cannot find trail file\n");
			alldone(1);
	}	}
okay:		
	if (xspin == 0 && newer(oFname->name, snap))
	printf("spin: warning, \"%s\" is newer than %s\n",
		oFname->name, snap);

	Tval = 1;

	/*
	 * sets Tval because timeouts may be part of trail
	 * this used to also set m_loss to 1, but that is
	 * better handled with the runtime -m flag
	 */

	hookup();

	while (fscanf(fd, "%d:%d:%d\n", &depth, &pno, &nst) == 3)
	{	if (depth == -2)
		{	if (verbose)
			{	printf("starting claim %d\n", pno);
			}
			start_claim(pno);
			continue;
		}
		if (depth == -4)
		{	if (verbose)
			{	printf("using statement merging\n");
			}
			merger = 1;
			ana_src(0, 1);
			continue;
		}
		if (depth == -1)
		{	if (1 || verbose)
			{	if (columns == 2)
				dotag(stdout, " CYCLE>\n");
				else
				dotag(stdout, "<<<<<START OF CYCLE>>>>>\n");
			}
			continue;
		}

		if (cutoff > 0 && depth >= cutoff)
		{	printf("-------------\n");
			printf("depth-limit (-u%d steps) reached\n", cutoff);
			break;
		}

		if (Skip_claim && pno == 0) continue;

		for (dothis = Al_El; dothis; dothis = dothis->Nxt)
		{	if (dothis->Seqno == nst)
				break;
		}
		if (!dothis)
		{	printf("%3d: proc %d, no matching stmnt %d\n",
				depth, pno - Have_claim, nst);
			lost_trail();
		}

		i = nproc - nstop + Skip_claim;

		if (dothis->n->ntyp == '@')
		{	if (pno == i-1)
			{	run = run->nxt;
				nstop++;
				if (verbose&4)
				{	if (columns == 2)
					{	dotag(stdout, "<end>\n");
						continue;
					}
					if (Have_claim && pno == 0)
					printf("%3d: claim terminates\n",
						depth);
					else
					printf("%3d: proc %d terminates\n",
						depth, pno - Have_claim);
				}
				continue;
			}
			if (pno <= 1) continue;	/* init dies before never */
			printf("%3d: stop error, ", depth);
			printf("proc %d (i=%d) trans %d, %c\n",
				pno - Have_claim, i, nst, dothis->n->ntyp);
			lost_trail();
		}

		if (0 && !xspin && (verbose&32))
		{	printf("step %d i=%d pno %d stmnt %d\n", depth, i, pno, nst);
		}

		for (X = run; X; X = X->nxt)
		{	if (--i == pno)
				break;
		}

		if (!X)
		{	if (verbose&32)
			{	printf("%3d: no process %d (stmnt %d)\n", depth, pno - Have_claim, nst);
				printf(" max %d (%d - %d + %d) claim %d ",
					nproc - nstop + Skip_claim,
					nproc, nstop, Skip_claim, Have_claim);
				printf("active processes:\n");
				for (X = run; X; X = X->nxt)
				{	printf("\tpid %d\tproctype %s\n", X->pid, X->n->name);
				}
				printf("\n");
				continue;	
			} else
			{	printf("%3d:\tproc  %d (?) ", depth, pno);
				lost_trail();
			}
		} else
		{	int min_seq = find_min(X->ps);
			int max_seq = find_max(X->ps);

			if (nst < min_seq || nst > max_seq)
			{	printf("%3d: error: invalid statement: ", depth);
				if (verbose&32)
				{	printf("pid %d:%d (%s:%d:%d) stmnt %d (valid range %d .. %d)\n",
					pno, X->pid, X->n->name, X->tn, X->b, nst, min_seq, max_seq);
				}
				continue;
				/* lost_trail(); */
			}
			X->pc  = dothis;
		}

		lineno = dothis->n->ln;
		Fname  = dothis->n->fn;

		if (dothis->n->ntyp == D_STEP)
		{	Element *g, *og = dothis;
			do {
				g = eval_sub(og);
				if (g && depth >= jumpsteps
				&& ((verbose&32) || ((verbose&4) && not_claim())))
				{	if (columns != 2)
					{	p_talk(og, 1);
		
						if (og->n->ntyp == D_STEP)
						og = og->n->sl->this->frst;
		
						printf("\t[");
						comment(stdout, og->n, 0);
						printf("]\n");
					}
					if (verbose&1) dumpglobals();
					if (verbose&2) dumplocal(X);
					if (xspin) printf("\n");
				}
				og = g;
			} while (g && g != dothis->nxt);
			if (X != NULL)
			{	X->pc = g?huntele(g, 0, -1):g;
			}
		} else
		{
keepgoing:		if (dothis->merge_start)
				a = dothis->merge_start;
			else
				a = dothis->merge;

			if (X != NULL)
			{	X->pc = eval_sub(dothis);
				if (X->pc) X->pc = huntele(X->pc, 0, a);
			}

			if (depth >= jumpsteps
			&& ((verbose&32) || ((verbose&4) && not_claim())))	/* -v or -p */
			{	if (columns != 2)
				{	p_talk(dothis, 1);
	
					if (dothis->n->ntyp == D_STEP)
					dothis = dothis->n->sl->this->frst;
		
					printf("\t[");
					comment(stdout, dothis->n, 0);
					printf("]");
					if (a && (verbose&32))
					printf("\t<merge %d now @%d>",
						dothis->merge,
						(X && X->pc)?X->pc->seqno:-1);
					printf("\n");
				}
				if (verbose&1) dumpglobals();
				if (verbose&2) dumplocal(X);
				if (xspin) printf("\n");

				if (X && !X->pc)
				{	X->pc = dothis;
					printf("\ttransition failed\n");
					a = 0;	/* avoid inf loop */
				}
			}
			if (a && X && X->pc && X->pc->seqno != a)
			{	dothis = X->pc;
				goto keepgoing;
		}	}

		if (Have_claim && X && X->pid == 0
		&&  dothis->n
		&&  lastclaim != dothis->n->ln)
		{	lastclaim = dothis->n->ln;
			if (columns == 2)
			{	char t[128];
				sprintf(t, "#%d", lastclaim);
				pstext(0, t);
			} else
			{
				printf("Never claim moves to line %d\t[", lastclaim);
				comment(stdout, dothis->n, 0);
				printf("]\n");
	}	}	}
	printf("spin: trail ends after %d steps\n", depth);
	wrapup(0);
}

static void
lost_trail(void)
{	int d, p, n, l;

	while (fscanf(fd, "%d:%d:%d:%d\n", &d, &p, &n, &l) == 4)
	{	printf("step %d: proc  %d ", d, p); whichproc(p);
		printf("(state %d) - d %d\n", n, l);
	}
	wrapup(1);	/* no return */
}

int
pc_value(Lextok *n)
{	int i = nproc - nstop;
	int pid = eval(n);
	RunList *Y;

	for (Y = run; Y; Y = Y->nxt)
	{	if (--i == pid)
			return Y->pc->seqno;
	}
	return 0;
}