/***** spin: sched.c *****/
-/* Copyright (c) 1989-2003 by Lucent Technologies, Bell Laboratories. */
-/* All Rights Reserved. This software is for educational purposes only. */
-/* No guarantee whatsoever is expressed or implied by the distribution of */
-/* this code. Permission is given to distribute this code provided that */
-/* this introductory message is not removed and no monies are exchanged. */
-/* Software written by Gerard J. Holzmann. For tool documentation see: */
-/* http://spinroot.com/ */
-/* Send all bug-reports and/or questions to: bugs@spinroot.com */
+/*
+ * 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 <stdlib.h>
#include "spin.h"
extern Symbol *Fname, *context;
extern int lineno, nr_errs, dumptab, xspin, jumpsteps, columns;
extern int u_sync, Elcnt, interactive, TstOnly, cutoff;
-extern short has_enabled;
-extern int limited_vis;
+extern short has_enabled, has_priority, has_code, replay;
+extern int limited_vis, product, nclaims, old_priority_rules;
+extern int old_scope_rules, scope_seq[128], scope_level, has_stdin;
+
+extern int pc_highest(Lextok *n);
RunList *X = (RunList *) 0;
RunList *run = (RunList *) 0;
RunList *LastX = (RunList *) 0; /* previous executing proc */
ProcList *rdy = (ProcList *) 0;
Element *LastStep = ZE;
-int nproc=0, nstop=0, Tval=0;
+int nproc=0, nstop=0, Tval=0, Priority_Sum = 0;
int Rvous=0, depth=0, nrRdy=0, MadeChoice;
short Have_claim=0, Skip_claim=0;
-static int Priority_Sum = 0;
static void setlocals(RunList *);
static void setparams(RunList *, ProcList *, Lextok *);
static void talk(RunList *);
r->n = p->n;
r->tn = p->tn;
+ r->b = p->b;
r->pid = nproc++ - nstop + Skip_claim;
+ r->priority = weight;
+ p->priority = (unsigned char) weight; /* not quite the best place of course */
- if ((verbose&4) || (verbose&32))
- printf("Starting %s with pid %d\n", p->n->name, r->pid);
-
+ if (!noparams && ((verbose&4) || (verbose&32)))
+ { printf("Starting %s with pid %d",
+ p->n?p->n->name:"--", r->pid);
+ if (has_priority) printf(" priority %d", r->priority);
+ printf("\n");
+ }
if (!p->s)
- fatal("parsing error, no sequence %s", p->n?p->n->name:"--");
+ fatal("parsing error, no sequence %s",
+ p->n?p->n->name:"--");
r->pc = huntele(p->s->frst, p->s->frst->status, -1);
r->ps = p->s;
r->nxt = run;
r->prov = p->prov;
- r->priority = weight;
+ if (weight < 1 || weight > 255)
+ { fatal("bad process priority, valid range: 1..255", (char *) 0);
+ }
+
if (noparams) setlocals(r);
Priority_Sum += weight;
+
run = r;
}
ProcList *
-ready(Symbol *n, Lextok *p, Sequence *s, int det, Lextok *prov)
+ready(Symbol *n, Lextok *p, Sequence *s, int det, Lextok *prov, enum btypes b)
/* n=name, p=formals, s=body det=deterministic prov=provided */
{ ProcList *r = (ProcList *) emalloc(sizeof(ProcList));
Lextok *fp, *fpt; int j; extern int Npars;
r->n = n;
r->p = p;
r->s = s;
+ r->b = b;
r->prov = prov;
- r->tn = nrRdy++;
- r->det = (short) det;
+ r->tn = (short) nrRdy++;
+ n->sc = scope_seq[scope_level]; /* scope_level should be 0 */
+
+ if (det != 0 && det != 1)
+ { fprintf(stderr, "spin: bad value for det (cannot happen)\n");
+ }
+ r->det = (unsigned char) det;
r->nxt = rdy;
rdy = r;
run->pid - Have_claim, run->n->name);
pstext(run->pid - Have_claim, Buf);
} else
- printf("proc %d = %s\n",
- run->pid - Have_claim, run->n->name);
+ { printf("proc %d = %s\n",
+ run->pid - Have_claim, run->n->name);
+ }
return;
}
if (dumptab
|| analyze
+ || product
|| s_trail
|| !(verbose&4))
return;
Symbol *s = m->sym; /* proctype name */
Lextok *n = m->lft; /* actual parameters */
- if (m->val < 1) m->val = 1; /* minimum priority */
+ if (m->val < 1)
+ { m->val = 1; /* minimum priority */
+ }
for (p = rdy; p; p = p->nxt)
- if (strcmp(s->name, p->n->name) == 0)
+ { if (strcmp(s->name, p->n->name) == 0)
{ if (nproc-nstop >= MAXP)
{ printf("spin: too many processes (%d max)\n", MAXP);
break;
setparams(run, p, n);
setlocals(run); /* after setparams */
return run->pid - Have_claim + Skip_claim; /* effective simu pid */
- }
+ } }
return 0; /* process not found */
}
RunList *r, *q = (RunList *) 0;
for (p = rdy; p; p = p->nxt)
- if (p->tn == n
- && strcmp(p->n->name, ":never:") == 0)
+ if (p->tn == n && p->b == N_CLAIM)
{ runnable(p, 1, 1);
goto found;
}
- printf("spin: couldn't find claim (ignored)\n");
+ printf("spin: couldn't find claim %d (ignored)\n", n);
+ if (verbose&32)
+ for (p = rdy; p; p = p->nxt)
+ printf("\t%d = %s\n", p->tn, p->n->name);
+
Skip_claim = 1;
goto done;
found:
/* move claim to far end of runlist, and reassign it pid 0 */
if (columns == 2)
- { depth = 0;
- pstext(0, "0::never:");
+ { extern char Buf[];
+ depth = 0;
+ sprintf(Buf, "%d:%s", 0, p->n->name);
+ pstext(0, Buf);
for (r = run; r; r = r->nxt)
- { if (!strcmp(r->n->name, ":never:"))
- continue;
- sprintf(Buf, "%d:%s",
- r->pid+1, r->n->name);
- pstext(r->pid+1, Buf);
- } }
+ { if (r->b != N_CLAIM)
+ { sprintf(Buf, "%d:%s", r->pid+1, r->n->name);
+ pstext(r->pid+1, Buf);
+ } } }
if (run->pid == 0) return; /* it is the first process started */
nproc - Have_claim + Skip_claim,
(xspin || nproc!=1)?"es":"");
short_cut:
- if (xspin) alldone(0); /* avoid an abort from xspin */
+ if (s_trail || xspin) alldone(0); /* avoid an abort from xspin */
if (fini) alldone(1);
}
return e;
}
+static int
+x_can_run(void) /* the currently selected process in X can run */
+{
+ if (X->prov && !eval(X->prov))
+ {
+if (0) printf("pid %d cannot run: not provided\n", X->pid);
+ return 0;
+ }
+ if (has_priority && !old_priority_rules)
+ { Lextok *n = nn(ZN, CONST, ZN, ZN);
+ n->val = X->pid;
+if (0) printf("pid %d %s run (priority)\n", X->pid, pc_highest(n)?"can":"cannot");
+ return pc_highest(n);
+ }
+if (0) printf("pid %d can run\n", X->pid);
+ return 1;
+}
+
static RunList *
pickproc(RunList *Y)
{ SeqList *z; Element *has_else;
return NULL;
}
if (!interactive || depth < jumpsteps)
- { /* was: j = (int) Rand()%(nproc-nstop); */
+ { if (has_priority && !old_priority_rules) /* new 6.3.2 */
+ { j = Rand()%(nproc-nstop);
+ for (X = run; X; X = X->nxt)
+ { if (j-- <= 0)
+ break;
+ }
+ if (X == NULL)
+ { fatal("unexpected, pickproc", (char *)0);
+ }
+ j = nproc - nstop;
+ while (j-- > 0)
+ { if (x_can_run())
+ { Y = X;
+ break;
+ }
+ X = (X->nxt)?X->nxt:run;
+ }
+ return Y;
+ }
if (Priority_Sum < nproc-nstop)
fatal("cannot happen - weights", (char *)0);
j = (int) Rand()%Priority_Sum;
X = X->nxt;
if (!X) { Y = NULL; X = run; }
}
+
} else
{ int only_choice = -1;
int no_choice = 0, proc_no_ch, proc_k;
Choices[X->pid] = (short) k;
- if (!X->pc
- || (X->prov && !eval(X->prov)))
+ if (!X->pc || !x_can_run())
{ if (X == run)
Choices[X->pid] = 0;
continue;
} else
{ char buf[256];
fflush(stdout);
- scanf("%s", buf);
+ if (scanf("%64s", buf) == 0)
+ { printf("\tno input\n");
+ goto try_again;
+ }
j = -1;
- if (isdigit(buf[0]))
+ if (isdigit((int) buf[0]))
j = atoi(buf);
else
{ if (buf[0] == 'q')
return Y;
}
+void
+multi_claims(void)
+{ ProcList *p, *q = NULL;
+
+ if (nclaims > 1)
+ { printf(" the model contains %d never claims:", nclaims);
+ for (p = rdy; p; p = p->nxt)
+ { if (p->b == N_CLAIM)
+ { printf("%s%s", q?", ":" ", p->n->name);
+ q = p;
+ } }
+ printf("\n");
+ printf(" only one claim is used in a verification run\n");
+ printf(" choose which one with ./pan -a -N name (defaults to -N %s)\n",
+ q?q->n->name:"--");
+ printf(" or use e.g.: spin -search -ltl %s %s\n",
+ q?q->n->name:"--", Fname?Fname->name:"filename");
+ }
+}
+
void
sched(void)
{ Element *e;
dumplabels();
return;
}
+ if (has_code && !analyze)
+ { printf("spin: warning: c_code fragments remain uninterpreted\n");
+ printf(" in random simulations with spin; use ./pan -r instead\n");
+ }
if (has_enabled && u_sync > 0)
{ printf("spin: error, cannot use 'enabled()' in ");
printf("models with synchronous channels.\n");
nr_errs++;
}
- if (analyze)
+ if (product)
+ { sync_product();
+ alldone(0);
+ }
+ if (analyze && (!replay || has_code))
{ gensrc();
+ multi_claims();
return;
- } else if (s_trail)
+ }
+ if (replay && !has_code)
+ { return;
+ }
+ if (s_trail)
{ match_trail();
return;
}
+
if (claimproc)
printf("warning: never claim not used in random simulation\n");
if (eventmap)
depth++; LastStep = ZE;
oX = X; /* a rendezvous could change it */
go = 1;
- if (X && X->prov && X->pc
+ if (X->pc
&& !(X->pc->status & D_ATOM)
- && !eval(X->prov))
+ && !x_can_run())
{ if (!xspin && ((verbose&32) || (verbose&4)))
{ p_talk(X->pc, 1);
printf("\t<<Not Enabled>>\n");
&& ((verbose&32) || (verbose&4)))
{ if (X == oX)
if (!(e->status & D_ATOM) || (verbose&32)) /* no talking in d_steps */
- { p_talk(X->pc, 1);
+ { if (!LastStep) LastStep = X->pc;
+ /* A. Tanaka, changed order */
+ p_talk(LastStep, 1);
printf(" [");
- if (!LastStep) LastStep = X->pc;
comment(stdout, LastStep->n, 0);
printf("]\n");
}
if (xspin)
printf("\n");
}
- if (oX != X)
+ if (oX != X
+ || (X->pc->status & (ATOM|D_ATOM))) /* new 5.0 */
{ e = silent_moves(e);
notbeyond = 0;
}
}
} else
{ depth--;
- if (oX->pc->status & D_ATOM)
- non_fatal("stmnt in d_step blocks", (char *)0);
-
- if (X->pc->n->ntyp == '@'
+ if (oX->pc && (oX->pc->status & D_ATOM))
+ { non_fatal("stmnt in d_step blocks", (char *)0);
+ }
+ if (X->pc
+ && X->pc->n
+ && X->pc->n->ntyp == '@'
&& X->pid == (nproc-nstop-1))
{ if (X != run && Y != NULL)
Y->nxt = X->nxt;
X = (X->nxt) ? X->nxt : run;
} else
{ if (p_blocked(X->pid))
- { if (Tval) break;
- Tval = 1;
- if (depth >= jumpsteps)
+ { if (Tval && !has_stdin)
+ { break;
+ }
+ if (!Tval && depth >= jumpsteps)
{ oX = X;
X = (RunList *) 0; /* to suppress indent */
dotag(stdout, "timeout\n");
X = oX;
+ Tval = 1;
} } } }
+
+ if (!run || !X) break; /* new 5.0 */
+
Y = pickproc(X);
notbeyond = 0;
}
printf(" [");
comment(stdout, s_was->n, 0);
printf("]\n");
- tmp = orun; orun = X; X = tmp;
+ tmp = orun; /* orun = X; */ X = tmp;
if (!LastStep) LastStep = X->pc;
p_talk(LastStep, 1);
printf(" [");
int i;
for (t = r->symtab; t; t = t->next)
- if (strcmp(t->name, s->name) == 0)
+ if (strcmp(t->name, s->name) == 0
+ && (old_scope_rules
+ || strcmp((const char *)t->bscp, (const char *)s->bscp) == 0))
return; /* it's already there */
t = (Symbol *) emalloc(sizeof(Symbol));
t->name = s->name;
t->type = s->type;
t->hidden = s->hidden;
+ t->isarray = s->isarray;
t->nbits = s->nbits;
t->nel = s->nel;
t->ini = s->ini;
t->setat = depth;
t->context = r->n;
+
+ t->bscp = (unsigned char *) emalloc(strlen((const char *)s->bscp)+1);
+ strcpy((char *)t->bscp, (const char *)s->bscp);
+
if (s->type != STRUCT)
{ if (s->val) /* if already initialized, copy info */
{ t->val = (int *) emalloc(s->nel*sizeof(int));
for (i = 0; i < s->nel; i++)
t->val[i] = s->val[i];
} else
- (void) checkvar(t, 0); /* initialize it */
+ { (void) checkvar(t, 0); /* initialize it */
+ }
} else
{ if (s->Sval)
fatal("saw preinitialized struct %s", s->name);
if (!a)
fatal("missing actual parameters: '%s'", p->n->name);
- if (t->sym->nel != 1)
+ if (t->sym->nel > 1 || t->sym->isarray)
fatal("array in parameter list, %s", t->sym->name);
k = eval(a->lft);
ft = Sym_typ(t);
if (at != ft && (at == CHAN || ft == CHAN))
- { char buf[128], tag1[64], tag2[64];
+ { char buf[256], tag1[64], tag2[64];
(void) sputtype(tag1, ft);
(void) sputtype(tag2, at);
sprintf(buf, "type-clash in params of %s(..), (%s<-> %s)",
return ZS;
}
for (r = X->symtab; r; r = r->next)
- if (strcmp(r->name, s->name) == 0)
- break;
+ { if (strcmp(r->name, s->name) == 0
+ && (old_scope_rules
+ || strcmp((const char *)r->bscp, (const char *)s->bscp) == 0))
+ { break;
+ } }
if (!r)
{ addsymbol(X, s);
r = X->symtab;
printf(" -");
else
printf("%2d", X->pid - Have_claim);
- printf(" (%s) ", X->n->name);
+ if (old_priority_rules)
+ { printf(" (%s) ", X->n->name);
+ } else
+ { printf(" (%s:%d) ", X->n->name, X->priority);
+ }
}
static void
void
p_talk(Element *e, int lnr)
{ static int lastnever = -1;
+ static char nbuf[128];
int newnever = -1;
if (e && e->n)
whoruns(lnr);
if (e)
- { printf("line %3d %s (state %d)",
+ { if (e->n)
+ { char *ptr = e->n->fn->name;
+ char *qtr = nbuf;
+ while (*ptr != '\0')
+ { if (*ptr != '"')
+ { *qtr++ = *ptr;
+ }
+ ptr++;
+ }
+ *qtr = '\0';
+ } else
+ { strcpy(nbuf, "-");
+ }
+ printf("%s:%d (state %d)",
+ nbuf,
e->n?e->n->ln:-1,
- e->n?e->n->fn->name:"-",
e->seqno);
if (!xspin
&& ((e->status&ENDSTATE) || has_lab(e, 2))) /* 2=end */
{ fatal("remote ref to label '%s' inside d_step",
n->sym->name);
}
- if ((i = find_lab(n->sym, n->lft->sym, 1)) == 0)
- fatal("unknown labelname: %s", n->sym->name);
+ if ((i = find_lab(n->sym, n->lft->sym, 1)) == 0) /* remotelab */
+ { fatal("unknown labelname: %s", n->sym->name);
+ }
return i;
}
} }
if (prno < 0)
- return 0; /* non-existing process */
+ { return 0; /* non-existing process */
+ }
#if 0
i = nproc - nstop;
for (Y = run; Y; Y = Y->nxt)
printf(" %s: i=%d, prno=%d, ->pid=%d\n", Y->n->name, i, prno, Y->pid);
}
#endif
- i = nproc - nstop;
+ i = nproc - nstop + Skip_claim; /* 6.0: added Skip_claim */
for (Y = run; Y; Y = Y->nxt)
if (--i == prno)
{ if (strcmp(Y->n->name, n->lft->sym->name) != 0)
}
if (strcmp(n->sym->name, "_p") == 0)
{ if (Y->pc)
- return Y->pc->seqno;
+ { return Y->pc->seqno;
+ }
/* harmless, can only happen with -t */
return 0;
}
-#if 1
- /* new 4.0 allow remote variables */
+
+ /* check remote variables */
oX = X;
X = Y;
n->lft = n->rgt;
os = n->sym;
- n->sym = findloc(n->sym);
-
+ if (!n->sym->context)
+ { n->sym->context = Y->n;
+ }
+ { int rs = old_scope_rules;
+ old_scope_rules = 1; /* 6.4.0 */
+ n->sym = findloc(n->sym);
+ old_scope_rules = rs;
+ }
i = getval(n);
n->sym = os;
n->lft = onl;
X = oX;
return i;
-#else
- break;
-#endif
}
printf("remote ref: %s[%d] ", n->lft->sym->name, prno-added);
non_fatal("%s not found", n->sym->name);
projects / plan9front.git / blobdiff