[lttv.git] / trunk / verif / Spin / Src5.1.6 / guided.c

/***** 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 "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;
extern void ana_src(int, int);

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);
}

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

	/*
	 * 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 (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) { start_claim(pno); continue; }
		if (depth == -4) { merger = 1; ana_src(0, 1); continue; }
		if (depth == -1)
		{	if (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 (!xspin && (verbose&32))
		{	printf("i=%d pno %d\n", i, pno);
		}

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

		if (!X)
		{	if (verbose&32)
			{	printf("%3d: no process %d (step %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
		{	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;
}
Commit	Line	Data
0b55f123	1	/*** spin: guided.c ***/
	2
	3	/* Copyright (c) 1989-2003 by Lucent Technologies, Bell Laboratories. */
	4	/* All Rights Reserved. This software is for educational purposes only. */
	5	/* No guarantee whatsoever is expressed or implied by the distribution of */
	6	/* this code. Permission is given to distribute this code provided that */
	7	/* this introductory message is not removed and no monies are exchanged. */
	8	/* Software written by Gerard J. Holzmann. For tool documentation see: */
	9	/* http://spinroot.com/ */
	10	/* Send all bug-reports and/or questions to: bugs@spinroot.com */
	11
	12	#include "spin.h"
	13	#include <sys/types.h>
	14	#include <sys/stat.h>
	15	#include "y.tab.h"
	16
	17	extern RunList run, X;
	18	extern Element *Al_El;
	19	extern Symbol Fname, oFname;
	20	extern int verbose, lineno, xspin, jumpsteps, depth, merger, cutoff;
	21	extern int nproc, nstop, Tval, ntrail, columns;
	22	extern short Have_claim, Skip_claim;
	23	extern void ana_src(int, int);
	24
	25	int TstOnly = 0, pno;
	26
	27	static int lastclaim = -1;
	28	static FILE *fd;
	29	static void lost_trail(void);
	30
	31	static void
	32	whichproc(int p)
	33	{ RunList *oX;
	34
	35	for (oX = run; oX; oX = oX->nxt)
	36	if (oX->pid == p)
	37	{ printf("(%s) ", oX->n->name);
	38	break;
	39	}
	40	}
	41
	42	static int
	43	newer(char f1, char f2)
	44	{
	45	#if defined(WIN32) \|\| defined(WIN64)
	46	struct _stat x, y;
	47	#else
	48	struct stat x, y;
	49	#endif
	50
	51	if (stat(f1, (struct stat *)&x) < 0) return 0;
	52	if (stat(f2, (struct stat *)&y) < 0) return 1;
	53	if (x.st_mtime < y.st_mtime) return 0;
	54
	55	return 1;
	56	}
	57
	58	void
	59	hookup(void)
	60	{ Element *e;
	61
	62	for (e = Al_El; e; e = e->Nxt)
	63	if (e->n
	64	&& (e->n->ntyp == ATOMIC
65	\|\| e->n->ntyp == NON_ATOMIC
66	\|\| e->n->ntyp == D_STEP))
67	(void) huntstart(e);
68	}
69
70	int
71	not_claim(void)
72	{
73	return (!Have_claim \|\| !X \|\| X->pid != 0);
74	}
75
76	void
77	match_trail(void)
78	{ int i, a, nst;
79	Element *dothis;
80	char snap[512], *q;
81
82	/*
83	* if source model name is leader.pml
84	* look for the trail file under these names:
85	* leader.pml.trail
86	* leader.pml.tra
87	* leader.trail
88	* leader.tra
89	*/
90
91	if (ntrail)
92	sprintf(snap, "%s%d.trail", oFname->name, ntrail);
93	else
94	sprintf(snap, "%s.trail", oFname->name);
95
96	if ((fd = fopen(snap, "r")) == NULL)
97	{ snap[strlen(snap)-2] = '\0'; /* .tra */
98	if ((fd = fopen(snap, "r")) == NULL)
99	{ if ((q = strchr(oFname->name, '.')) != NULL)
100	{ *q = '\0';
101	if (ntrail)
102	sprintf(snap, "%s%d.trail",
103	oFname->name, ntrail);
104	else
105	sprintf(snap, "%s.trail",
106	oFname->name);
107	*q = '.';
108
109	if ((fd = fopen(snap, "r")) != NULL)
110	goto okay;
111
112	snap[strlen(snap)-2] = '\0'; /* last try */
113	if ((fd = fopen(snap, "r")) != NULL)
114	goto okay;
115	}
116	printf("spin: cannot find trail file\n");
117	alldone(1);
118	} }
119	okay:
120	if (xspin == 0 && newer(oFname->name, snap))
121	printf("spin: warning, \"%s\" is newer than %s\n",
122	oFname->name, snap);
123
124	Tval = 1;
125
126	/*
127	* sets Tval because timeouts may be part of trail
128	* this used to also set m_loss to 1, but that is
129	* better handled with the runtime -m flag
130	*/
131
132	hookup();
133
134	while (fscanf(fd, "%d:%d:%d\n", &depth, &pno, &nst) == 3)
135	{ if (depth == -2) { start_claim(pno); continue; }
136	if (depth == -4) { merger = 1; ana_src(0, 1); continue; }
137	if (depth == -1)
138	{ if (verbose)
139	{ if (columns == 2)
140	dotag(stdout, " CYCLE>\n");
141	else
142	dotag(stdout, "<<<<<START OF CYCLE>>>>>\n");
143	}
144	continue;
145	}
146
147	if (cutoff > 0 && depth >= cutoff)
148	{ printf("-------------\n");
149	printf("depth-limit (-u%d steps) reached\n", cutoff);
150	break;
151	}
152
153	if (Skip_claim && pno == 0) continue;
154
155	for (dothis = Al_El; dothis; dothis = dothis->Nxt)
156	{ if (dothis->Seqno == nst)
157	break;
158	}
159	if (!dothis)
160	{ printf("%3d: proc %d, no matching stmnt %d\n",
161	depth, pno - Have_claim, nst);
162	lost_trail();
163	}
164
165	i = nproc - nstop + Skip_claim;
166
167	if (dothis->n->ntyp == '@')
168	{ if (pno == i-1)
169	{ run = run->nxt;
170	nstop++;
171	if (verbose&4)
172	{ if (columns == 2)
173	{ dotag(stdout, "<end>\n");
174	continue;
175	}
176	if (Have_claim && pno == 0)
177	printf("%3d: claim terminates\n",
178	depth);
179	else
180	printf("%3d: proc %d terminates\n",
181	depth, pno - Have_claim);
182	}
183	continue;
184	}
185	if (pno <= 1) continue; /* init dies before never */
186	printf("%3d: stop error, ", depth);
187	printf("proc %d (i=%d) trans %d, %c\n",
188	pno - Have_claim, i, nst, dothis->n->ntyp);
189	lost_trail();
190	}
191
192	if (!xspin && (verbose&32))
193	{ printf("i=%d pno %d\n", i, pno);
194	}
195
196	for (X = run; X; X = X->nxt)
197	{ if (--i == pno)
198	break;
199	}
200
201	if (!X)
202	{ if (verbose&32)
203	{ printf("%3d: no process %d (step %d)\n", depth, pno - Have_claim, nst);
204	printf(" max %d (%d - %d + %d) claim %d",
205	nproc - nstop + Skip_claim,
206	nproc, nstop, Skip_claim, Have_claim);
207	printf("active processes:\n");
208	for (X = run; X; X = X->nxt)
209	{ printf("\tpid %d\tproctype %s\n", X->pid, X->n->name);
210	}
211	printf("\n");
212	continue;
213	} else
214	{ printf("%3d:\tproc %d (?) ", depth, pno);
215	lost_trail();
216	}
217	} else
218	{ X->pc = dothis;
219	}
220
221	lineno = dothis->n->ln;
222	Fname = dothis->n->fn;
223
224	if (dothis->n->ntyp == D_STEP)
225	{ Element g, og = dothis;
226	do {
227	g = eval_sub(og);
228	if (g && depth >= jumpsteps
229	&& ((verbose&32) \|\| ((verbose&4) && not_claim())))
230	{ if (columns != 2)
231	{ p_talk(og, 1);
232
233	if (og->n->ntyp == D_STEP)
234	og = og->n->sl->this->frst;
235
236	printf("\t[");
237	comment(stdout, og->n, 0);
238	printf("]\n");
239	}
240	if (verbose&1) dumpglobals();
241	if (verbose&2) dumplocal(X);
242	if (xspin) printf("\n");
243	}
244	og = g;
245	} while (g && g != dothis->nxt);
246	if (X != NULL)
247	{ X->pc = g?huntele(g, 0, -1):g;
248	}
249	} else
250	{
251	keepgoing: if (dothis->merge_start)
252	a = dothis->merge_start;
253	else
254	a = dothis->merge;
255
256	if (X != NULL)
257	{ X->pc = eval_sub(dothis);
258	if (X->pc) X->pc = huntele(X->pc, 0, a);
259	}
260
261	if (depth >= jumpsteps
262	&& ((verbose&32) \|\| ((verbose&4) && not_claim()))) /* -v or -p */
263	{ if (columns != 2)
264	{ p_talk(dothis, 1);
265
266	if (dothis->n->ntyp == D_STEP)
267	dothis = dothis->n->sl->this->frst;
268
269	printf("\t[");
270	comment(stdout, dothis->n, 0);
271	printf("]");
272	if (a && (verbose&32))
273	printf("\t<merge %d now @%d>",
274	dothis->merge,
275	(X && X->pc)?X->pc->seqno:-1);
276	printf("\n");
277	}
278	if (verbose&1) dumpglobals();
279	if (verbose&2) dumplocal(X);
280	if (xspin) printf("\n");
281
282	if (X && !X->pc)
283	{ X->pc = dothis;
284	printf("\ttransition failed\n");
285	a = 0; /* avoid inf loop */
286	}
287	}
288	if (a && X && X->pc && X->pc->seqno != a)
289	{ dothis = X->pc;
290	goto keepgoing;
291	} }
292
293	if (Have_claim && X && X->pid == 0
294	&& dothis->n
295	&& lastclaim != dothis->n->ln)
296	{ lastclaim = dothis->n->ln;
297	if (columns == 2)
298	{ char t[128];
299	sprintf(t, "#%d", lastclaim);
300	pstext(0, t);
301	} else
302	{
303	printf("Never claim moves to line %d\t[", lastclaim);
304	comment(stdout, dothis->n, 0);
305	printf("]\n");
306	} } }
307	printf("spin: trail ends after %d steps\n", depth);
308	wrapup(0);
309	}
310
311	static void
312	lost_trail(void)
313	{ int d, p, n, l;
314
315	while (fscanf(fd, "%d:%d:%d:%d\n", &d, &p, &n, &l) == 4)
316	{ printf("step %d: proc %d ", d, p); whichproc(p);
317	printf("(state %d) - d %d\n", n, l);
318	}
319	wrapup(1); /* no return */
320	}
321
322	int
323	pc_value(Lextok *n)
324	{ int i = nproc - nstop;
325	int pid = eval(n);
326	RunList *Y;
327
328	for (Y = run; Y; Y = Y->nxt)
329	{ if (--i == pid)
330	return Y->pc->seqno;
331	}
332	return 0;
333	}