sys/src/cmd/spin/guided.c

   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 }