/***** spin: run.c *****/

/* Copyright (c) 1991-2000 by Lucent Technologies - Bell Laboratories     */
/* All Rights Reserved.  This software is for educational purposes only.  */
/* Permission is given to distribute this code provided that this intro-  */
/* ductory message is not removed and no monies are exchanged.            */
/* No guarantee is expressed or implied by the distribution of this code. */
/* Software written by Gerard J. Holzmann as part of the book:            */
/* `Design and Validation of Computer Protocols,' ISBN 0-13-539925-4,     */
/* Prentice Hall, Englewood Cliffs, NJ, 07632.                            */
/* Send bug-reports and/or questions to: [email protected]    */

#include <stdlib.h>
#include "spin.h"
#ifdef PC
#include "y_tab.h"
#else
#include "y.tab.h"
#endif

extern RunList  *X, *run;
extern Symbol   *Fname;
extern Element  *LastStep;
extern int      Rvous, lineno, Tval, interactive, MadeChoice;
extern int      TstOnly, verbose, s_trail, xspin, jumpsteps, depth;
extern int      nproc, nstop, no_print, like_java;

static long     Seed = 1;
static int      E_Check = 0, Escape_Check = 0;

static int      eval_sync(Element *);
static int      pc_enabled(Lextok *n);
extern void     sr_buf(int, int);

void
Srand(unsigned int s)
{       Seed = s;
}

long
Rand(void)
{       /* CACM 31(10), Oct 1988 */
       Seed = 16807*(Seed%127773) - 2836*(Seed/127773);
       if (Seed <= 0) Seed += 2147483647;
       return Seed;
}

Element *
rev_escape(SeqList *e)
{       Element *r;

       if (!e)
               return (Element *) 0;

       if (r = rev_escape(e->nxt)) /* reversed order */
               return r;

       return eval_sub(e->this->frst);
}

Element *
eval_sub(Element *e)
{       Element *f, *g;
       SeqList *z;
       int i, j, k;

       if (!e->n)
               return ZE;
#ifdef DEBUG
       printf("\n\teval_sub(%d %s: line %d) ",
               e->Seqno, e->esc?"+esc":"", e->n?e->n->ln:0);
       comment(stdout, e->n, 0);
       printf("\n");
#endif
       if (e->n->ntyp == GOTO)
       {       if (Rvous) return ZE;
               LastStep = e; f = get_lab(e->n, 1);
               cross_dsteps(e->n, f->n);
               return f;
       }
       if (e->n->ntyp == UNLESS)
       {       /* escapes were distributed into sequence */
               return eval_sub(e->sub->this->frst);
       } else if (e->sub)      /* true for IF, DO, and UNLESS */
       {       Element *has_else = ZE;
               Element *bas_else = ZE;
               int nr_else, nr_choices = 0;

               if (interactive
               && !MadeChoice && !E_Check
               && !Escape_Check
               && !(e->status&(D_ATOM))
               && depth >= jumpsteps)
               {       printf("Select stmnt (");
                       whoruns(0); printf(")\n");
                       if (nproc-nstop > 1)
                       printf("\tchoice 0: other process\n");
               }
               for (z = e->sub, j=0; z; z = z->nxt)
               {       j++;
                       if (interactive
                       && !MadeChoice && !E_Check
                       && !Escape_Check
                       && !(e->status&(D_ATOM))
                       && depth >= jumpsteps
                       && z->this->frst
                       && (xspin || (verbose&32) || Enabled0(z->this->frst)))
                       {       if (z->this->frst->n->ntyp == ELSE)
                               {       has_else = (Rvous)?ZE:z->this->frst->nxt;
                                       nr_else = j;
                                       continue;
                               }
                               printf("\tchoice %d: ", j);
#if 0
                               if (z->this->frst->n)
                                       printf("line %d, ", z->this->frst->n->ln);
#endif
                               if (!Enabled0(z->this->frst))
                                       printf("unexecutable, ");
                               else
                                       nr_choices++;
                               comment(stdout, z->this->frst->n, 0);
                               printf("\n");
               }       }

               if (nr_choices == 0 && has_else)
                       printf("\tchoice %d: (else)\n", nr_else);

               if (interactive && depth >= jumpsteps
               && !Escape_Check
               && !(e->status&(D_ATOM))
               && !E_Check)
               {       if (!MadeChoice)
                       {       char buf[256];
                               if (xspin)
                                       printf("Make Selection %d\n\n", j);
                               else
                                       printf("Select [0-%d]: ", j);
                               fflush(stdout);
                               scanf("%s", buf);
                               if (isdigit(buf[0]))
                                       k = atoi(buf);
                               else
                               {       if (buf[0] == 'q')
                                               alldone(0);
                                       k = -1;
                               }
                       } else
                       {       k = MadeChoice;
                               MadeChoice = 0;
                       }
                       if (k < 1 || k > j)
                       {       if (k != 0) printf("\tchoice outside range\n");
                               return ZE;
                       }
                       k--;
               } else
               {       if (e->n && e->n->indstep >= 0)
                               k = 0;  /* select 1st executable guard */
                       else
                               k = Rand()%j;   /* nondeterminism */
               }
               has_else = ZE;
               bas_else = ZE;
               for (i = 0, z = e->sub; i < j+k; i++)
               {       if (z->this->frst
                       &&  z->this->frst->n->ntyp == ELSE)
                       {       bas_else = z->this->frst;
                               has_else = (Rvous)?ZE:bas_else->nxt;
                               if (!interactive || depth < jumpsteps
                               || Escape_Check
                               || (e->status&(D_ATOM)))
                               {       z = (z->nxt)?z->nxt:e->sub;
                                       continue;
                               }
                       }
                       if (i >= k)
                       {       if (f = eval_sub(z->this->frst))
                                       return f;
                               else if (interactive && depth >= jumpsteps
                               && !(e->status&(D_ATOM)))
                               {       if (!E_Check && !Escape_Check)
                                               printf("\tunexecutable\n");
                                       return ZE;
                       }       }
                       z = (z->nxt)?z->nxt:e->sub;
               }
               LastStep = bas_else;
               return has_else;
       } else
       {       if (e->n->ntyp == ATOMIC
               ||  e->n->ntyp == D_STEP)
               {       f = e->n->sl->this->frst;
                       g = e->n->sl->this->last;
                       g->nxt = e->nxt;
                       if (!(g = eval_sub(f))) /* atomic guard */
                               return ZE;
                       return g;
               } else if (e->n->ntyp == NON_ATOMIC)
               {       f = e->n->sl->this->frst;
                       g = e->n->sl->this->last;
                       g->nxt = e->nxt;                /* close it */
                       return eval_sub(f);
               } else if (e->n->ntyp == '.')
               {       if (!Rvous) return e->nxt;
                       return eval_sub(e->nxt);
               } else
               {       SeqList *x;
                       if (!(e->status & (D_ATOM))
                       &&  e->esc && verbose&32)
                       {       printf("Stmnt [");
                               comment(stdout, e->n, 0);
                               printf("] has escape(s): ");
                               for (x = e->esc; x; x = x->nxt)
                               {       printf("[");
                                       g = x->this->frst;
                                       if (g->n->ntyp == ATOMIC
                                       ||  g->n->ntyp == NON_ATOMIC)
                                               g = g->n->sl->this->frst;
                                       comment(stdout, g->n, 0);
                                       printf("] ");
                               }
                               printf("\n");
                       }

                       if (!(e->status & D_ATOM))      /* escapes don't reach inside d_steps */
                       {       Escape_Check++;
                               if (like_java)
                               {       if (g = rev_escape(e->esc))
                                       {       if (verbose&4)
                                                       printf("\tEscape taken\n");
                                               Escape_Check--;
                                               return g;
                                       }
                               } else
                               {       for (x = e->esc; x; x = x->nxt)
                                       {       if (g = eval_sub(x->this->frst))
                                               {       if (verbose&4)
                                                               printf("\tEscape taken\n");
                                                       Escape_Check--;
                                                       return g;
                               }       }       }
                               Escape_Check--;
                       }

                       switch (e->n->ntyp) {
                       case TIMEOUT: case RUN:
                       case PRINT:
                       case ASGN: case ASSERT:
                       case 's': case 'r': case 'c':
                               /* toplevel statements only */
                               LastStep = e;
                       default:
                               break;
                       }
                       if (Rvous)
                       {
                               return (eval_sync(e))?e->nxt:ZE;
                       }
                       return (eval(e->n))?e->nxt:ZE;
               }
       }
       return ZE; /* not reached */
}

static int
eval_sync(Element *e)
{       /* allow only synchronous receives
          and related node types    */
       Lextok *now = (e)?e->n:ZN;

       if (!now
       ||  now->ntyp != 'r'
       ||  now->val >= 2       /* no rv with a poll */
       ||  !q_is_sync(now))
       {
               return 0;
       }

       LastStep = e;
       return eval(now);
}

static int
assign(Lextok *now)
{       int t;

       if (TstOnly) return 1;

       switch (now->rgt->ntyp) {
       case FULL:      case NFULL:
       case EMPTY:     case NEMPTY:
       case RUN:       case LEN:
               t = BYTE;
               break;
       default:
               t = Sym_typ(now->rgt);
               break;
       }
       typ_ck(Sym_typ(now->lft), t, "assignment");
       return setval(now->lft, eval(now->rgt));
}

static int
nonprogress(void)       /* np_ */
{       RunList *r;

       for (r = run; r; r = r->nxt)
       {       if (has_lab(r->pc, 4))  /* 4=progress */
                       return 0;
       }
       return 1;
}

int
eval(Lextok *now)
{
       if (now) {
       lineno = now->ln;
       Fname  = now->fn;
#ifdef DEBUG
       printf("eval ");
       comment(stdout, now, 0);
       printf("\n");
#endif
       switch (now->ntyp) {
       case CONST: return now->val;
       case   '!': return !eval(now->lft);
       case  UMIN: return -eval(now->lft);
       case   '~': return ~eval(now->lft);

       case   '/': return (eval(now->lft) / eval(now->rgt));
       case   '*': return (eval(now->lft) * eval(now->rgt));
       case   '-': return (eval(now->lft) - eval(now->rgt));
       case   '+': return (eval(now->lft) + eval(now->rgt));
       case   '%': return (eval(now->lft) % eval(now->rgt));
       case    LT: return (eval(now->lft) <  eval(now->rgt));
       case    GT: return (eval(now->lft) >  eval(now->rgt));
       case   '&': return (eval(now->lft) &  eval(now->rgt));
       case   '^': return (eval(now->lft) ^  eval(now->rgt));
       case   '|': return (eval(now->lft) |  eval(now->rgt));
       case    LE: return (eval(now->lft) <= eval(now->rgt));
       case    GE: return (eval(now->lft) >= eval(now->rgt));
       case    NE: return (eval(now->lft) != eval(now->rgt));
       case    EQ: return (eval(now->lft) == eval(now->rgt));
       case    OR: return (eval(now->lft) || eval(now->rgt));
       case   AND: return (eval(now->lft) && eval(now->rgt));
       case LSHIFT: return (eval(now->lft) << eval(now->rgt));
       case RSHIFT: return (eval(now->lft) >> eval(now->rgt));
       case   '?': return (eval(now->lft) ? eval(now->rgt->lft)
                                          : eval(now->rgt->rgt));

       case     'p': return remotevar(now);    /* only _p allowed */
       case     'q': return remotelab(now);
       case     'R': return qrecv(now, 0);     /* test only    */
       case     LEN: return qlen(now);
       case    FULL: return (qfull(now));
       case   EMPTY: return (qlen(now)==0);
       case   NFULL: return (!qfull(now));
       case  NEMPTY: return (qlen(now)>0);
       case ENABLED: if (s_trail) return 1;
                     return pc_enabled(now->lft);
       case    EVAL: return eval(now->lft);
       case  PC_VAL: return pc_value(now->lft);
       case NONPROGRESS: return nonprogress();
       case    NAME: return getval(now);

       case TIMEOUT: return Tval;
       case     RUN: return TstOnly?1:enable(now);

       case   's': return qsend(now);          /* send         */
       case   'r': return qrecv(now, 1);       /* receive or poll */
       case   'c': return eval(now->lft);      /* condition    */
       case PRINT: return TstOnly?1:interprint(stdout, now);
       case  ASGN: return assign(now);
       case ASSERT: if (TstOnly || eval(now->lft)) return 1;
                    non_fatal("assertion violated", (char *) 0);
                       printf("spin: text of failed assertion: assert(");
                       comment(stdout, now->lft, 0);
                       printf(")\n");
                    if (s_trail && !xspin) return 1;
                    wrapup(1); /* doesn't return */

       case  IF: case DO: case BREAK: case UNLESS:     /* compound */
       case   '.': return 1;   /* return label for compound */
       case   '@': return 0;   /* stop state */
       case  ELSE: return 1;   /* only hit here in guided trails */
       default   : printf("spin: bad node type %d (run)\n", now->ntyp);
                   if (s_trail) printf("spin: trail file doesn't match spec?\n");
                   fatal("aborting", 0);
       }}
       return 0;
}

int
interprint(FILE *fd, Lextok *n)
{       Lextok *tmp = n->lft;
       char c, *s = n->sym->name;
       int i, j; char lbuf[16];
       extern char Buf[];
       char tBuf[1024];

       Buf[0] = '\0';
       if (!no_print)
       if (!s_trail || depth >= jumpsteps) {
       for (i = 0; i < (int) strlen(s); i++)
               switch (s[i]) {
               case '\"': break; /* ignore */
               case '\\':
                        switch(s[++i]) {
                        case 't': strcat(Buf, "\t"); break;
                        case 'n': strcat(Buf, "\n"); break;
                        default:  goto onechar;
                        }
                        break;
               case  '%':
                        if ((c = s[++i]) == '%')
                        {      strcat(Buf, "%"); /* literal */
                               break;
                        }
                        if (!tmp)
                        {      non_fatal("too few print args %s", s);
                               break;
                        }
                        j = eval(tmp->lft);
                        tmp = tmp->rgt;
                        switch(c) {
                        case 'c': sprintf(lbuf, "%c", j); break;
                        case 'd': sprintf(lbuf, "%d", j); break;

                        case 'e': strcpy(tBuf, Buf);   /* event name */
                                  Buf[0] = '\0';
                                  sr_buf(j, 1);
                                  strcpy(lbuf, Buf);
                                  strcpy(Buf, tBuf);
                                  break;

                        case 'o': sprintf(lbuf, "%o", j); break;
                        case 'u': sprintf(lbuf, "%u", (unsigned) j); break;
                        case 'x': sprintf(lbuf, "%x", j); break;
                        default:  non_fatal("bad print cmd: '%s'", &s[i-1]);
                                  lbuf[0] = '\0'; break;
                        }
                        goto append;
               default:
onechar:                 lbuf[0] = s[i]; lbuf[1] = '\0';
append:                  strcat(Buf, lbuf);
                        break;
               }
               dotag(fd, Buf);
       }
       if (strlen(Buf) > 1024) fatal("printf string too long", 0);
       return 1;
}

static int
Enabled1(Lextok *n)
{       int i; int v = verbose;

       if (n)
       switch (n->ntyp) {
       case 'c':
               if (has_typ(n->lft, RUN))
                       return 1;       /* conservative */
               /* else fall through */
       default:        /* side-effect free */
               verbose = 0;
E_Check++;
               i = eval(n);
E_Check--;
               verbose = v;
               return i;

       case PRINT: case  ASGN: case ASSERT:
               return 1;

       case 's':
               if (q_is_sync(n))
               {       if (Rvous) return 0;
                       TstOnly = 1; verbose = 0;
E_Check++;
                       i = eval(n);
E_Check--;
                       TstOnly = 0; verbose = v;
                       return i;
               }
               return (!qfull(n));
       case 'r':
               if (q_is_sync(n))
                       return 0;       /* it's never a user-choice */
               n->ntyp = 'R'; verbose = 0;
E_Check++;
               i = eval(n);
E_Check--;
               n->ntyp = 'r'; verbose = v;
               return i;
       }
       return 0;
}

int
Enabled0(Element *e)
{       SeqList *z;

       if (!e || !e->n)
               return 0;

       switch (e->n->ntyp) {
       case '@':
               return X->pid == (nproc-nstop-1);
       case '.':
               return 1;
       case GOTO:
               if (Rvous) return 0;
               return 1;
       case UNLESS:
               return Enabled0(e->sub->this->frst);
       case ATOMIC:
       case D_STEP:
       case NON_ATOMIC:
               return Enabled0(e->n->sl->this->frst);
       }
       if (e->sub)     /* true for IF, DO, and UNLESS */
       {       for (z = e->sub; z; z = z->nxt)
                       if (Enabled0(z->this->frst))
                               return 1;
               return 0;
       }
       for (z = e->esc; z; z = z->nxt)
       {       if (Enabled0(z->this->frst))
                       return 1;
       }
#if 0
       printf("enabled1 ");
       comment(stdout, e->n, 0);
       printf(" ==> %s\n", Enabled1(e->n)?"yes":"nope");
#endif
       return Enabled1(e->n);
}

int
pc_enabled(Lextok *n)
{       int i = nproc - nstop;
       int pid = eval(n);
       int result = 0;
       RunList *Y, *oX;

       for (Y = run; Y; Y = Y->nxt)
               if (--i == pid)
               {       oX = X; X = Y;
                       result = Enabled0(Y->pc);
                       X = oX;
                       break;
               }
       return result;
}

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.