Subversion Repositories planix.SVN

Rev

Rev 2 | Details | Compare with Previous | Last modification | View Log | RSS feed

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