1 /***** spin: guided.c *****/ 2 3 /* Copyright (c) 1991,1995 by AT&T Corporation. All Rights Reserved. */ 4 /* This software is for educational purposes only. */ 5 /* Permission is given to distribute this code provided that this intro- */ 6 /* ductory message is not removed and no monies are exchanged. */ 7 /* No guarantee is expressed or implied by the distribution of this code. */ 8 /* Software written by Gerard J. Holzmann as part of the book: */ 9 /* `Design and Validation of Computer Protocols,' ISBN 0-13-539925-4, */ 10 /* Prentice Hall, Englewood Cliffs, NJ, 07632. */ 11 /* Send bug-reports and/or questions to: gerard@research.att.com */ 12 13 #include "spin.h" 14 #include <sys/types.h> 15 #include <sys/stat.h> 16 #include "y.tab.h" 17 18 extern int nproc, nstop, Tval, Rvous, Have_claim, m_loss; 19 extern RunList *run, *X; 20 extern Element *Al_El; 21 extern Symbol *Fname, *oFname; 22 extern int verbose, lineno, xspin; 23 extern int depth; 24 25 int TstOnly = 0; 26 27 FILE *fd; 28 29 void 30 whichproc(int p) 31 { RunList *oX; 32 33 for (oX = run; oX; oX = oX->nxt) 34 if (oX->pid == p) 35 { printf("(%s) ", oX->n->name); 36 break; 37 } 38 } 39 40 int 41 newer(char *f1, char *f2) 42 { struct stat x, y; 43 44 if (stat(f1, (struct stat *)&x) < 0) return 0; 45 if (stat(f2, (struct stat *)&y) < 0) return 1; 46 if (x.st_mtime < y.st_mtime) return 0; 47 48 return 1; 49 } 50 51 void 52 match_trail(void) 53 { int i, pno, nst; 54 Element *dothis; 55 char snap[256]; 56 57 sprintf(snap, "%s.trail", oFname->name); 58 if (!(fd = fopen(snap, "r"))) 59 { printf("spin -t: cannot find %s\n", snap); 60 exit(1); 61 } 62 63 if (xspin == 0 && newer(oFname->name, snap)) 64 printf("Warning, \"%s\" newer than %s\n", oFname->name, snap); 65 66 Tval = m_loss = 1; /* timeouts and losses may be part of trail */ 67 68 while (fscanf(fd, "%d:%d:%d\n", &depth, &pno, &nst) == 3) 69 { if (depth == -2) 70 { start_claim(pno); 71 continue; 72 } 73 if (depth == -1) 74 { if (verbose) 75 printf("<<<<<START OF CYCLE>>>>>\n"); 76 continue; 77 } 78 if (Have_claim) 79 { if (pno == 0) /* verifier has claim at 0 */ 80 pno = Have_claim; 81 else 82 { if (pno <= Have_claim) 83 pno -= 1; 84 } } 85 86 for (dothis = Al_El; dothis; dothis = dothis->Nxt) 87 { if (dothis->Seqno == nst) 88 break; 89 } 90 if (!dothis) 91 { printf("%3d: proc %d, no matching transition %d\n", 92 depth, pno, nst); 93 lost_trail(); 94 } 95 i = nproc - nstop; 96 if (dothis->n->ntyp == '@') 97 { if (pno == i-1) 98 { run = run->nxt; 99 nstop++; 100 if (verbose&32 || verbose&4) 101 printf("%3d: proc %d dies\n", depth, pno); 102 continue; 103 } 104 if (pno <= 1) continue; /* init dies before never */ 105 printf("%3d: stop error, proc %d (i=%d) trans %d, %c\n", 106 depth, pno, i, nst, dothis->n->ntyp); 107 lost_trail(); 108 } 109 for (X = run; X; X = X->nxt) 110 { if (--i == pno) 111 break; 112 } 113 if (!X) 114 { printf("%3d: no process %d ", depth, pno); 115 if (Have_claim && pno == Have_claim) 116 printf("(state %d)\n", nst); 117 else 118 printf("(proc .%d state %d)\n", pno, nst); 119 lost_trail(); 120 } 121 X->pc = dothis; 122 lineno = dothis->n->ln; 123 Fname = dothis->n->fn; 124 if (verbose&32 || verbose&4) 125 { p_talk(X->pc, 1); 126 printf(" ["); 127 comment(stdout, X->pc->n, 0); 128 printf("]\n"); 129 } 130 if (dothis->n->ntyp == GOTO) 131 X->pc = get_lab(dothis->n,1); 132 else 133 { if (dothis->n->ntyp == D_STEP) 134 { Element *g = dothis; 135 do { 136 g = eval_sub(g); 137 } while (g && g != dothis->nxt); 138 if (!g) 139 { printf("%3d: d_step failed %d->%d\n", 140 depth, dothis->Seqno, dothis->nxt->Seqno); 141 wrapup(1); 142 } 143 X->pc = g; 144 } else 145 { (void) eval(dothis->n); 146 X->pc = dothis->nxt; 147 } 148 } 149 if (X->pc) X->pc = huntele(X->pc, 0); 150 if (verbose&32 || verbose&4) 151 { if (verbose&1) dumpglobals(); 152 if (verbose&2) dumplocal(X); 153 if (xspin) printf("\n"); /* xspin looks for these */ 154 } 155 } 156 printf("spin: trail ends after %d steps\n", depth); 157 wrapup(0); 158 } 159 160 void 161 lost_trail(void) 162 { int d, p, n, l; 163 164 while (fscanf(fd, "%d:%d:%d:%d\n", &d, &p, &n, &l) == 4) 165 { printf("step %d: proc %d ", d, p); whichproc(p); 166 printf("(state %d) - d %d\n", n, l); 167 } 168 wrapup(1); /* no return */ 169 } 170 171 int 172 pc_value(Lextok *n) 173 { int i = nproc - nstop; 174 int pid = eval(n); 175 RunList *Y; 176 177 for (Y = run; Y; Y = Y->nxt) 178 { if (--i == pid) 179 return Y->pc->seqno; 180 } 181 return 0; 182 } 183