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 } 343