2011-03-30 12:46:40 +00:00
|
|
|
/***** spin: guided.c *****/
|
|
|
|
|
2017-11-22 20:09:31 +00:00
|
|
|
/*
|
|
|
|
* 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
|
|
|
|
*/
|
2011-03-30 12:46:40 +00:00
|
|
|
|
|
|
|
#include "spin.h"
|
|
|
|
#include <sys/types.h>
|
|
|
|
#include <sys/stat.h>
|
2017-11-22 20:09:31 +00:00
|
|
|
#include <limits.h>
|
2011-03-30 12:46:40 +00:00
|
|
|
#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;
|
2017-11-22 20:09:31 +00:00
|
|
|
extern short Have_claim, Skip_claim, has_code;
|
2011-03-30 12:46:40 +00:00
|
|
|
extern void ana_src(int, int);
|
2017-11-22 20:09:31 +00:00
|
|
|
extern char **trailfilename;
|
2011-03-30 12:46:40 +00:00
|
|
|
|
|
|
|
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);
|
|
|
|
}
|
|
|
|
|
2017-11-22 20:09:31 +00:00
|
|
|
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;
|
|
|
|
}
|
|
|
|
|
2011-03-30 12:46:40 +00:00
|
|
|
void
|
|
|
|
match_trail(void)
|
|
|
|
{ int i, a, nst;
|
|
|
|
Element *dothis;
|
|
|
|
char snap[512], *q;
|
|
|
|
|
2017-11-22 20:09:31 +00:00
|
|
|
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");
|
|
|
|
}
|
|
|
|
|
2011-03-30 12:46:40 +00:00
|
|
|
/*
|
|
|
|
* 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
|
|
|
|
*/
|
|
|
|
|
2017-11-22 20:09:31 +00:00
|
|
|
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);
|
|
|
|
}
|
2011-03-30 12:46:40 +00:00
|
|
|
|
|
|
|
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))
|
2017-11-22 20:09:31 +00:00
|
|
|
{ printf("spin: warning, \"%s\" is newer than %s\n",
|
|
|
|
oFname->name, snap);
|
|
|
|
}
|
2011-03-30 12:46:40 +00:00
|
|
|
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)
|
2017-11-22 20:09:31 +00:00
|
|
|
{ if (depth == -2)
|
2011-03-30 12:46:40 +00:00
|
|
|
{ if (verbose)
|
2017-11-22 20:09:31 +00:00
|
|
|
{ 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)
|
2011-03-30 12:46:40 +00:00
|
|
|
{ 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();
|
|
|
|
}
|
2017-11-22 20:09:31 +00:00
|
|
|
|
|
|
|
if (0 && !xspin && (verbose&32))
|
|
|
|
{ printf("step %d i=%d pno %d stmnt %d\n", depth, i, pno, nst);
|
|
|
|
}
|
|
|
|
|
2011-03-30 12:46:40 +00:00
|
|
|
for (X = run; X; X = X->nxt)
|
|
|
|
{ if (--i == pno)
|
|
|
|
break;
|
|
|
|
}
|
2017-11-22 20:09:31 +00:00
|
|
|
|
2011-03-30 12:46:40 +00:00
|
|
|
if (!X)
|
2017-11-22 20:09:31 +00:00
|
|
|
{ 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;
|
2011-03-30 12:46:40 +00:00
|
|
|
}
|
2017-11-22 20:09:31 +00:00
|
|
|
|
2011-03-30 12:46:40 +00:00
|
|
|
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
|
2017-11-22 20:09:31 +00:00
|
|
|
&& dothis->n
|
2011-03-30 12:46:40 +00:00
|
|
|
&& 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;
|
|
|
|
}
|