1 /***** spin: guided.c *****/
2
3 /*
4 * This file is part of the public release of Spin. It is subject to the
5 * terms in the LICENSE file that is included in this source directory.
6 * Tool documentation is available at http://spinroot.com
7 */
8
9 #include "spin.h"
10 #include <sys/types.h>
11 #include <sys/stat.h>
12 #include <limits.h>
13 #include "y.tab.h"
14
15 extern RunList *run_lst, *X_lst;
16 extern Element *Al_El;
17 extern Symbol *Fname, *oFname;
18 extern int verbose, lineno, xspin, jumpsteps, depth, merger, cutoff;
19 extern int nproc, nstop, Tval, ntrail, columns;
20 extern short Have_claim, Skip_claim, has_code;
21 extern void ana_src(int, int);
22 extern char **trailfilename;
23
24 int TstOnly = 0, prno;
25
26 static int lastclaim = -1;
27 static FILE *fd;
28 static void lost_trail(void);
29
30 static void
whichproc(int p)31 whichproc(int p)
32 { RunList *oX;
33
34 for (oX = run_lst; oX; oX = oX->nxt)
35 if (oX->pid == p)
36 { printf("(%s) ", oX->n->name);
37 break;
38 }
39 }
40
41 static int
newer(char * f1,char * f2)42 newer(char *f1, char *f2)
43 {
44 #if defined(WIN32) || defined(WIN64)
45 struct _stat x, y;
46 #else
47 struct stat x, y;
48 #endif
49
50 if (stat(f1, (struct stat *)&x) < 0) return 0;
51 if (stat(f2, (struct stat *)&y) < 0) return 1;
52 if (x.st_mtime < y.st_mtime) return 0;
53
54 return 1;
55 }
56
57 void
hookup(void)58 hookup(void)
59 { Element *e;
60
61 for (e = Al_El; e; e = e->Nxt)
62 if (e->n
63 && (e->n->ntyp == ATOMIC
64 || e->n->ntyp == NON_ATOMIC
65 || e->n->ntyp == D_STEP))
66 (void) huntstart(e);
67 }
68
69 int
not_claim(void)70 not_claim(void)
71 {
72 return (!Have_claim || !X_lst || X_lst->pid != 0);
73 }
74
75 int globmin = INT_MAX;
76 int globmax = 0;
77
78 int
find_min(Sequence * s)79 find_min(Sequence *s)
80 { SeqList *l;
81 Element *e;
82
83 if (s->minel < 0)
84 { s->minel = INT_MAX;
85 for (e = s->frst; e; e = e->nxt)
86 { if (e->status & 512)
87 { continue;
88 }
89 e->status |= 512;
90
91 if (e->n->ntyp == ATOMIC
92 || e->n->ntyp == NON_ATOMIC
93 || e->n->ntyp == D_STEP)
94 { int n = find_min(e->n->sl->this);
95 if (n < s->minel)
96 { s->minel = n;
97 }
98 } else if (e->Seqno < s->minel)
99 { s->minel = e->Seqno;
100 }
101 for (l = e->sub; l; l = l->nxt)
102 { int n = find_min(l->this);
103 if (n < s->minel)
104 { s->minel = n;
105 } } }
106 }
107 if (s->minel < globmin)
108 { globmin = s->minel;
109 }
110 return s->minel;
111 }
112
113 int
find_max(Sequence * s)114 find_max(Sequence *s)
115 {
116 if (s->last->Seqno > globmax)
117 { globmax = s->last->Seqno;
118 }
119 return s->last->Seqno;
120 }
121
122 void
match_trail(void)123 match_trail(void)
124 { int i, a, nst;
125 Element *dothis;
126 char snap[512], *q;
127
128 if (has_code)
129 { printf("spin: important:\n");
130 printf(" =======================================warning====\n");
131 printf(" this model contains embedded c code statements\n");
132 printf(" these statements will not be executed when the trail\n");
133 printf(" is replayed in this way -- they are just printed,\n");
134 printf(" which will likely lead to inaccurate variable values.\n");
135 printf(" for an accurate replay use: ./pan -r\n");
136 printf(" =======================================warning====\n\n");
137 }
138
139 /*
140 * if source model name is leader.pml
141 * look for the trail file under these names:
142 * leader.pml.trail
143 * leader.pml.tra
144 * leader.trail
145 * leader.tra
146 */
147
148 if (trailfilename)
149 { if (strlen(*trailfilename) < sizeof(snap))
150 { strcpy(snap, (const char *) *trailfilename);
151 } else
152 { fatal("filename %s too long", *trailfilename);
153 }
154 } else
155 { if (ntrail)
156 sprintf(snap, "%s%d.trail", oFname->name, ntrail);
157 else
158 sprintf(snap, "%s.trail", oFname->name);
159 }
160
161 if ((fd = fopen(snap, "r")) == NULL)
162 { snap[strlen(snap)-2] = '\0'; /* .tra */
163 if ((fd = fopen(snap, "r")) == NULL)
164 { if ((q = strchr(oFname->name, '.')) != NULL)
165 { *q = '\0';
166 if (ntrail)
167 sprintf(snap, "%s%d.trail",
168 oFname->name, ntrail);
169 else
170 sprintf(snap, "%s.trail",
171 oFname->name);
172 *q = '.';
173
174 if ((fd = fopen(snap, "r")) != NULL)
175 goto okay;
176
177 snap[strlen(snap)-2] = '\0'; /* last try */
178 if ((fd = fopen(snap, "r")) != NULL)
179 goto okay;
180 }
181 printf("spin: cannot find trail file\n");
182 alldone(1);
183 } }
184 okay:
185 if (xspin == 0 && newer(oFname->name, snap))
186 { printf("spin: warning, \"%s\" is newer than %s\n",
187 oFname->name, snap);
188 }
189 Tval = 1;
190
191 /*
192 * sets Tval because timeouts may be part of trail
193 * this used to also set m_loss to 1, but that is
194 * better handled with the runtime -m flag
195 */
196
197 hookup();
198
199 while (fscanf(fd, "%d:%d:%d\n", &depth, &prno, &nst) == 3)
200 { if (depth == -2)
201 { if (verbose)
202 { printf("starting claim %d\n", prno);
203 }
204 start_claim(prno);
205 continue;
206 }
207 if (depth == -4)
208 { if (verbose&32)
209 { printf("using statement merging\n");
210 }
211 merger = 1;
212 ana_src(0, 1);
213 continue;
214 }
215 if (depth == -1)
216 { if (1 || verbose)
217 { if (columns == 2)
218 dotag(stdout, " CYCLE>\n");
219 else
220 dotag(stdout, "<<<<<START OF CYCLE>>>>>\n");
221 }
222 continue;
223 }
224 if (depth <= -5
225 && depth >= -8)
226 { printf("spin: used search permutation, replay with ./pan -r\n");
227 return; /* permuted: -5, -6, -7, -8 */
228 }
229
230 if (cutoff > 0 && depth >= cutoff)
231 { printf("-------------\n");
232 printf("depth-limit (-u%d steps) reached\n", cutoff);
233 break;
234 }
235
236 if (Skip_claim && prno == 0) continue;
237
238 for (dothis = Al_El; dothis; dothis = dothis->Nxt)
239 { if (dothis->Seqno == nst)
240 break;
241 }
242 if (!dothis)
243 { printf("%3d: proc %d, no matching stmnt %d\n",
244 depth, prno - Have_claim, nst);
245 lost_trail();
246 }
247
248 i = nproc - nstop + Skip_claim;
249
250 if (dothis->n->ntyp == '@')
251 { if (prno == i-1)
252 { run_lst = run_lst->nxt;
253 nstop++;
254 if (verbose&4)
255 { if (columns == 2)
256 { dotag(stdout, "<end>\n");
257 continue;
258 }
259 if (Have_claim && prno == 0)
260 printf("%3d: claim terminates\n",
261 depth);
262 else
263 printf("%3d: proc %d terminates\n",
264 depth, prno - Have_claim);
265 }
266 continue;
267 }
268 if (prno <= 1) continue; /* init dies before never */
269 printf("%3d: stop error, ", depth);
270 printf("proc %d (i=%d) trans %d, %c\n",
271 prno - Have_claim, i, nst, dothis->n->ntyp);
272 lost_trail();
273 }
274
275 if (0 && !xspin && (verbose&32))
276 { printf("step %d i=%d pno %d stmnt %d\n", depth, i, prno, nst);
277 }
278
279 for (X_lst = run_lst; X_lst; X_lst = X_lst->nxt)
280 { if (--i == prno)
281 break;
282 }
283
284 if (!X_lst)
285 { if (verbose&32)
286 { printf("%3d: no process %d (stmnt %d)\n", depth, prno - Have_claim, nst);
287 printf(" max %d (%d - %d + %d) claim %d ",
288 nproc - nstop + Skip_claim,
289 nproc, nstop, Skip_claim, Have_claim);
290 printf("active processes:\n");
291 for (X_lst = run_lst; X_lst; X_lst = X_lst->nxt)
292 { printf("\tpid %d\tproctype %s\n", X_lst->pid, X_lst->n->name);
293 }
294 printf("\n");
295 continue;
296 } else
297 { printf("%3d:\tproc %d (?) ", depth, prno);
298 lost_trail();
299 }
300 } else
301 { int min_seq = find_min(X_lst->ps);
302 int max_seq = find_max(X_lst->ps);
303
304 if (nst < min_seq || nst > max_seq)
305 { printf("%3d: error: invalid statement", depth);
306 if (verbose&32)
307 { printf(": pid %d:%d (%s:%d:%d) stmnt %d (valid range %d .. %d)",
308 prno, X_lst->pid, X_lst->n->name, X_lst->tn, X_lst->b,
309 nst, min_seq, max_seq);
310 }
311 printf("\n");
312 continue;
313 /* lost_trail(); */
314 }
315 X_lst->pc = dothis;
316 }
317
318 lineno = dothis->n->ln;
319 Fname = dothis->n->fn;
320
321 if (dothis->n->ntyp == D_STEP)
322 { Element *g, *og = dothis;
323 do {
324 g = eval_sub(og);
325 if (g && depth >= jumpsteps
326 && ((verbose&32) || ((verbose&4) && not_claim())))
327 { if (columns != 2)
328 { p_talk(og, 1);
329
330 if (og->n->ntyp == D_STEP)
331 og = og->n->sl->this->frst;
332
333 printf("\t[");
334 comment(stdout, og->n, 0);
335 printf("]\n");
336 }
337 if (verbose&1) dumpglobals();
338 if (verbose&2) dumplocal(X_lst, 0);
339 if (xspin) printf("\n");
340 }
341 og = g;
342 } while (g && g != dothis->nxt);
343 if (X_lst != NULL)
344 { X_lst->pc = g?huntele(g, 0, -1):g;
345 }
346 } else
347 {
348 keepgoing: if (dothis->merge_start)
349 a = dothis->merge_start;
350 else
351 a = dothis->merge;
352
353 if (X_lst != NULL)
354 { X_lst->pc = eval_sub(dothis);
355 if (X_lst->pc) X_lst->pc = huntele(X_lst->pc, 0, a);
356 }
357
358 if (depth >= jumpsteps
359 && ((verbose&32) || ((verbose&4) && not_claim()))) /* -v or -p */
360 { if (columns != 2)
361 { p_talk(dothis, 1);
362
363 if (dothis->n->ntyp == D_STEP)
364 dothis = dothis->n->sl->this->frst;
365
366 printf("\t[");
367 comment(stdout, dothis->n, 0);
368 printf("]");
369 if (a && (verbose&32))
370 printf("\t<merge %d now @%d>",
371 dothis->merge,
372 (X_lst && X_lst->pc)?X_lst->pc->seqno:-1);
373 printf("\n");
374 }
375 if (verbose&1) dumpglobals();
376 if (verbose&2) dumplocal(X_lst, 0);
377 if (xspin) printf("\n");
378
379 if (X_lst && !X_lst->pc)
380 { X_lst->pc = dothis;
381 printf("\ttransition failed\n");
382 a = 0; /* avoid inf loop */
383 }
384 }
385 if (a && X_lst && X_lst->pc && X_lst->pc->seqno != a)
386 { dothis = X_lst->pc;
387 goto keepgoing;
388 } }
389
390 if (Have_claim && X_lst && X_lst->pid == 0
391 && dothis->n
392 && lastclaim != dothis->n->ln)
393 { lastclaim = dothis->n->ln;
394 if (columns == 2)
395 { char t[128];
396 sprintf(t, "#%d", lastclaim);
397 pstext(0, t);
398 } else
399 {
400 printf("Never claim moves to line %d\t[", lastclaim);
401 comment(stdout, dothis->n, 0);
402 printf("]\n");
403 } } }
404 printf("spin: trail ends after %d steps\n", depth);
405 wrapup(0);
406 }
407
408 static void
lost_trail(void)409 lost_trail(void)
410 { int d, p, n, l;
411
412 while (fscanf(fd, "%d:%d:%d:%d\n", &d, &p, &n, &l) == 4)
413 { printf("step %d: proc %d ", d, p); whichproc(p);
414 printf("(state %d) - d %d\n", n, l);
415 }
416 wrapup(1); /* no return */
417 }
418
419 int
pc_value(Lextok * n)420 pc_value(Lextok *n)
421 { int i = nproc - nstop;
422 int pid = eval(n);
423 RunList *Y;
424
425 for (Y = run_lst; Y; Y = Y->nxt)
426 { if (--i == pid)
427 return Y->pc->seqno;
428 }
429 return 0;
430 }
431