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
whichproc(int p)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
newer(char * f1,char * f2)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
hookup(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
not_claim(void)72 not_claim(void)
73 {
74 return (!Have_claim || !X || X->pid != 0);
75 }
76
77 void
match_trail(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
lost_trail(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
pc_value(Lextok * n)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 }
343