/***** spin: guided.c *****/

/*
* This file is part of the public release of Spin. It is subject to the
* terms in the LICENSE file that is included in this source directory.
* Tool documentation is available at http://spinroot.com
*/

#include "spin.h"
#include <sys/types.h>
#include <sys/stat.h>
#include <limits.h>
#include "y.tab.h"

extern RunList  *run, *X;
extern Element  *Al_El;
extern Symbol   *Fname, *oFname;
extern int      verbose, lineno, xspin, jumpsteps, depth, merger, cutoff;
extern int      nproc, nstop, Tval, ntrail, columns;
extern short    Have_claim, Skip_claim, has_code;
extern void ana_src(int, int);
extern char     **trailfilename;

int     TstOnly = 0, pno;

static int      lastclaim = -1;
static FILE     *fd;
static void     lost_trail(void);

static void
whichproc(int p)
{       RunList *oX;

       for (oX = run; oX; oX = oX->nxt)
               if (oX->pid == p)
               {       printf("(%s) ", oX->n->name);
                       break;
               }
}

static int
newer(char *f1, char *f2)
{
#if defined(WIN32) || defined(WIN64)
       struct _stat x, y;
#else
       struct stat x, y;
#endif

       if (stat(f1, (struct stat *)&x) < 0) return 0;
       if (stat(f2, (struct stat *)&y) < 0) return 1;
       if (x.st_mtime < y.st_mtime) return 0;

       return 1;
}

void
hookup(void)
{       Element *e;

       for (e = Al_El; e; e = e->Nxt)
               if (e->n
               && (e->n->ntyp == ATOMIC
               ||  e->n->ntyp == NON_ATOMIC
               ||  e->n->ntyp == D_STEP))
                       (void) huntstart(e);
}

int
not_claim(void)
{
       return (!Have_claim || !X || X->pid != 0);
}

int globmin = INT_MAX;
int globmax = 0;

int
find_min(Sequence *s)
{       SeqList *l;
       Element *e;

       if (s->minel < 0)
       {       s->minel = INT_MAX;
               for (e = s->frst; e; e = e->nxt)
               {       if (e->status & 512)
                       {       continue;
                       }
                       e->status |= 512;

                       if (e->n->ntyp == ATOMIC
                       ||  e->n->ntyp == NON_ATOMIC
                       ||  e->n->ntyp == D_STEP)
                       {       int n = find_min(e->n->sl->this);
                               if (n < s->minel)
                               {       s->minel = n;
                               }
                       } else if (e->Seqno < s->minel)
                       {       s->minel = e->Seqno;
                       }
                       for (l = e->sub; l; l = l->nxt)
                       {       int n = find_min(l->this);
                               if (n < s->minel)
                               {       s->minel = n;
               }       }       }
       }
       if (s->minel < globmin)
       {       globmin = s->minel;
       }
       return s->minel;
}

int
find_max(Sequence *s)
{
       if (s->last->Seqno > globmax)
       {       globmax = s->last->Seqno;
       }
       return s->last->Seqno;
}

void
match_trail(void)
{       int i, a, nst;
       Element *dothis;
       char snap[512], *q;

       if (has_code)
       {       printf("spin: important:\n");
               printf("  =======================================warning====\n");
               printf("  this model contains embedded c code statements\n");
               printf("  these statements will not be executed when the trail\n");
               printf("  is replayed in this way -- they are just printed,\n");
               printf("  which will likely lead to inaccurate variable values.\n");
               printf("  for an accurate replay use: ./pan -r\n");
               printf("  =======================================warning====\n\n");
       }

       /*
        * if source model name is leader.pml
        * look for the trail file under these names:
        *      leader.pml.trail
        *      leader.pml.tra
        *      leader.trail
        *      leader.tra
        */

       if (trailfilename)
       {       if (strlen(*trailfilename) < sizeof(snap))
               {       strcpy(snap, (const char *) *trailfilename);
               } else
               {       fatal("filename %s too long", *trailfilename);
               }
       } else
       {       if (ntrail)
                       sprintf(snap, "%s%d.trail", oFname->name, ntrail);
               else
                       sprintf(snap, "%s.trail", oFname->name);
       }

       if ((fd = fopen(snap, "r")) == NULL)
       {       snap[strlen(snap)-2] = '\0';    /* .tra */
               if ((fd = fopen(snap, "r")) == NULL)
               {       if ((q = strchr(oFname->name, '.')) != NULL)
                       {       *q = '\0';
                               if (ntrail)
                                       sprintf(snap, "%s%d.trail",
                                               oFname->name, ntrail);
                               else
                                       sprintf(snap, "%s.trail",
                                               oFname->name);
                               *q = '.';

                               if ((fd = fopen(snap, "r")) != NULL)
                                       goto okay;

                               snap[strlen(snap)-2] = '\0';    /* last try */
                               if ((fd = fopen(snap, "r")) != NULL)
                                       goto okay;
                       }
                       printf("spin: cannot find trail file\n");
                       alldone(1);
       }       }
okay:
       if (xspin == 0 && newer(oFname->name, snap))
       {       printf("spin: warning, \"%s\" is newer than %s\n",
                       oFname->name, snap);
       }
       Tval = 1;

       /*
        * sets Tval because timeouts may be part of trail
        * this used to also set m_loss to 1, but that is
        * better handled with the runtime -m flag
        */

       hookup();

       while (fscanf(fd, "%d:%d:%d\n", &depth, &pno, &nst) == 3)
       {       if (depth == -2)
               {       if (verbose)
                       {       printf("starting claim %d\n", pno);
                       }
                       start_claim(pno);
                       continue;
               }
               if (depth == -4)
               {       if (verbose)
                       {       printf("using statement merging\n");
                       }
                       merger = 1;
                       ana_src(0, 1);
                       continue;
               }
               if (depth == -1)
               {       if (1 || verbose)
                       {       if (columns == 2)
                               dotag(stdout, " CYCLE>\n");
                               else
                               dotag(stdout, "<<<<<START OF CYCLE>>>>>\n");
                       }
                       continue;
               }

               if (cutoff > 0 && depth >= cutoff)
               {       printf("-------------\n");
                       printf("depth-limit (-u%d steps) reached\n", cutoff);
                       break;
               }

               if (Skip_claim && pno == 0) continue;

               for (dothis = Al_El; dothis; dothis = dothis->Nxt)
               {       if (dothis->Seqno == nst)
                               break;
               }
               if (!dothis)
               {       printf("%3d: proc %d, no matching stmnt %d\n",
                               depth, pno - Have_claim, nst);
                       lost_trail();
               }

               i = nproc - nstop + Skip_claim;

               if (dothis->n->ntyp == '@')
               {       if (pno == i-1)
                       {       run = run->nxt;
                               nstop++;
                               if (verbose&4)
                               {       if (columns == 2)
                                       {       dotag(stdout, "<end>\n");
                                               continue;
                                       }
                                       if (Have_claim && pno == 0)
                                       printf("%3d: claim terminates\n",
                                               depth);
                                       else
                                       printf("%3d: proc %d terminates\n",
                                               depth, pno - Have_claim);
                               }
                               continue;
                       }
                       if (pno <= 1) continue; /* init dies before never */
                       printf("%3d: stop error, ", depth);
                       printf("proc %d (i=%d) trans %d, %c\n",
                               pno - Have_claim, i, nst, dothis->n->ntyp);
                       lost_trail();
               }

               if (0 && !xspin && (verbose&32))
               {       printf("step %d i=%d pno %d stmnt %d\n", depth, i, pno, nst);
               }

               for (X = run; X; X = X->nxt)
               {       if (--i == pno)
                               break;
               }

               if (!X)
               {       if (verbose&32)
                       {       printf("%3d: no process %d (stmnt %d)\n", depth, pno - Have_claim, nst);
                               printf(" max %d (%d - %d + %d) claim %d ",
                                       nproc - nstop + Skip_claim,
                                       nproc, nstop, Skip_claim, Have_claim);
                               printf("active processes:\n");
                               for (X = run; X; X = X->nxt)
                               {       printf("\tpid %d\tproctype %s\n", X->pid, X->n->name);
                               }
                               printf("\n");
                               continue;
                       } else
                       {       printf("%3d:\tproc  %d (?) ", depth, pno);
                               lost_trail();
                       }
               } else
               {       int min_seq = find_min(X->ps);
                       int max_seq = find_max(X->ps);


                       if (nst < min_seq || nst > max_seq)
                       {       printf("%3d: error: invalid statement", depth);
                               if (verbose&32)
                               {       printf(": pid %d:%d (%s:%d:%d) stmnt %d (valid range %d .. %d)",
                                       pno, X->pid, X->n->name, X->tn, X->b, nst, min_seq, max_seq);
                               }
                               printf("\n");
                               continue;
                               /* lost_trail(); */
                       }
                       X->pc  = dothis;
               }

               lineno = dothis->n->ln;
               Fname  = dothis->n->fn;

               if (dothis->n->ntyp == D_STEP)
               {       Element *g, *og = dothis;
                       do {
                               g = eval_sub(og);
                               if (g && depth >= jumpsteps
                               && ((verbose&32) || ((verbose&4) && not_claim())))
                               {       if (columns != 2)
                                       {       p_talk(og, 1);

                                               if (og->n->ntyp == D_STEP)
                                               og = og->n->sl->this->frst;

                                               printf("\t[");
                                               comment(stdout, og->n, 0);
                                               printf("]\n");
                                       }
                                       if (verbose&1) dumpglobals();
                                       if (verbose&2) dumplocal(X);
                                       if (xspin) printf("\n");
                               }
                               og = g;
                       } while (g && g != dothis->nxt);
                       if (X != NULL)
                       {       X->pc = g?huntele(g, 0, -1):g;
                       }
               } else
               {
keepgoing:              if (dothis->merge_start)
                               a = dothis->merge_start;
                       else
                               a = dothis->merge;

                       if (X != NULL)
                       {       X->pc = eval_sub(dothis);
                               if (X->pc) X->pc = huntele(X->pc, 0, a);
                       }

                       if (depth >= jumpsteps
                       && ((verbose&32) || ((verbose&4) && not_claim())))      /* -v or -p */
                       {       if (columns != 2)
                               {       p_talk(dothis, 1);

                                       if (dothis->n->ntyp == D_STEP)
                                       dothis = dothis->n->sl->this->frst;

                                       printf("\t[");
                                       comment(stdout, dothis->n, 0);
                                       printf("]");
                                       if (a && (verbose&32))
                                       printf("\t<merge %d now @%d>",
                                               dothis->merge,
                                               (X && X->pc)?X->pc->seqno:-1);
                                       printf("\n");
                               }
                               if (verbose&1) dumpglobals();
                               if (verbose&2) dumplocal(X);
                               if (xspin) printf("\n");

                               if (X && !X->pc)
                               {       X->pc = dothis;
                                       printf("\ttransition failed\n");
                                       a = 0;  /* avoid inf loop */
                               }
                       }
                       if (a && X && X->pc && X->pc->seqno != a)
                       {       dothis = X->pc;
                               goto keepgoing;
               }       }

               if (Have_claim && X && X->pid == 0
               &&  dothis->n
               &&  lastclaim != dothis->n->ln)
               {       lastclaim = dothis->n->ln;
                       if (columns == 2)
                       {       char t[128];
                               sprintf(t, "#%d", lastclaim);
                               pstext(0, t);
                       } else
                       {
                               printf("Never claim moves to line %d\t[", lastclaim);
                               comment(stdout, dothis->n, 0);
                               printf("]\n");
       }       }       }
       printf("spin: trail ends after %d steps\n", depth);
       wrapup(0);
}

static void
lost_trail(void)
{       int d, p, n, l;

       while (fscanf(fd, "%d:%d:%d:%d\n", &d, &p, &n, &l) == 4)
       {       printf("step %d: proc  %d ", d, p); whichproc(p);
               printf("(state %d) - d %d\n", n, l);
       }
       wrapup(1);      /* no return */
}

int
pc_value(Lextok *n)
{       int i = nproc - nstop;
       int pid = eval(n);
       RunList *Y;

       for (Y = run; Y; Y = Y->nxt)
       {       if (--i == pid)
                       return Y->pc->seqno;
       }
       return 0;
}

You are viewing proxied material from sdf.org. The copyright of proxied material belongs to its original authors. Any comments or complaints in relation to proxied material should be directed to the original authors of the content concerned. Please see the disclaimer for more details.