/***** 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 voidwhichproc(int p){ RunList *oX; for (oX = run; oX; oX = oX->nxt) if (oX->pid == p) { printf("(%s) ", oX->n->name); break; }} static intnewer(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;} voidhookup(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);} intnot_claim(void){ return (!Have_claim || !X || X->pid != 0);} int globmin = INT_MAX;int globmax = 0; intfind_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;} intfind_max(Sequence *s){ if (s->last->Seqno > globmax) { globmax = s->last->Seqno; } return s->last->Seqno;} voidmatch_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 voidlost_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 */} intpc_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;}
/***** 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;
}