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