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