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 for (X = run; X; X = X->nxt) 192 { if (--i == pno) 193 break; 194 } 195 if (!X) 196 { printf("%3d: no process %d ", depth, pno - Have_claim); 197 printf("(state %d)\n", nst); 198 lost_trail(); 199 } 200 X->pc = dothis; 201 lineno = dothis->n->ln; 202 Fname = dothis->n->fn; 203 204 if (dothis->n->ntyp == D_STEP) 205 { Element *g, *og = dothis; 206 do { 207 g = eval_sub(og); 208 if (g && depth >= jumpsteps 209 && ((verbose&32) || ((verbose&4) && not_claim()))) 210 { if (columns != 2) 211 { p_talk(og, 1); 212 213 if (og->n->ntyp == D_STEP) 214 og = og->n->sl->this->frst; 215 216 printf("\t["); 217 comment(stdout, og->n, 0); 218 printf("]\n"); 219 } 220 if (verbose&1) dumpglobals(); 221 if (verbose&2) dumplocal(X); 222 if (xspin) printf("\n"); 223 } 224 og = g; 225 } while (g && g != dothis->nxt); 226 if (X != NULL) 227 { X->pc = g?huntele(g, 0, -1):g; 228 } 229 } else 230 { 231 keepgoing: if (dothis->merge_start) 232 a = dothis->merge_start; 233 else 234 a = dothis->merge; 235 236 if (X != NULL) 237 { X->pc = eval_sub(dothis); 238 if (X->pc) X->pc = huntele(X->pc, 0, a); 239 } 240 241 if (depth >= jumpsteps 242 && ((verbose&32) || ((verbose&4) && not_claim()))) /* -v or -p */ 243 { if (columns != 2) 244 { p_talk(dothis, 1); 245 246 if (dothis->n->ntyp == D_STEP) 247 dothis = dothis->n->sl->this->frst; 248 249 printf("\t["); 250 comment(stdout, dothis->n, 0); 251 printf("]"); 252 if (a && (verbose&32)) 253 printf("\t<merge %d now @%d>", 254 dothis->merge, 255 (X && X->pc)?X->pc->seqno:-1); 256 printf("\n"); 257 } 258 if (verbose&1) dumpglobals(); 259 if (verbose&2) dumplocal(X); 260 if (xspin) printf("\n"); 261 262 if (X && !X->pc) 263 { X->pc = dothis; 264 printf("\ttransition failed\n"); 265 a = 0; /* avoid inf loop */ 266 } 267 } 268 if (a && X && X->pc && X->pc->seqno != a) 269 { dothis = X->pc; 270 goto keepgoing; 271 } } 272 273 if (Have_claim && X && X->pid == 0 274 && dothis && dothis->n 275 && lastclaim != dothis->n->ln) 276 { lastclaim = dothis->n->ln; 277 if (columns == 2) 278 { char t[128]; 279 sprintf(t, "#%d", lastclaim); 280 pstext(0, t); 281 } else 282 { 283 printf("Never claim moves to line %d\t[", lastclaim); 284 comment(stdout, dothis->n, 0); 285 printf("]\n"); 286 } } } 287 printf("spin: trail ends after %d steps\n", depth); 288 wrapup(0); 289 } 290 291 static void 292 lost_trail(void) 293 { int d, p, n, l; 294 295 while (fscanf(fd, "%d:%d:%d:%d\n", &d, &p, &n, &l) == 4) 296 { printf("step %d: proc %d ", d, p); whichproc(p); 297 printf("(state %d) - d %d\n", n, l); 298 } 299 wrapup(1); /* no return */ 300 } 301 302 int 303 pc_value(Lextok *n) 304 { int i = nproc - nstop; 305 int pid = eval(n); 306 RunList *Y; 307 308 for (Y = run; Y; Y = Y->nxt) 309 { if (--i == pid) 310 return Y->pc->seqno; 311 } 312 return 0; 313 } 314