/***** spin: pangen2.h *****/
/* 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: gerard@research.bell-labs.com */
static char *Nvr1[] = { /* allow separate compilation */
"#ifdef VERI",
"void",
"check_claim(int st)",
"{",
" if (st == endclaim)",
" uerror(\"claim violated!\");",
" if (stopstate[VERI][st])",
" uerror(\"endstate in claim reached\");",
"}",
"#endif",
0,
};
static char *Pre0[] = {
"#include <stdio.h>",
"#include <signal.h>",
"#include <stdlib.h>",
"#include <string.h>", /* was strings.h -- string.h is ANSI */
/* new */
"#include <errno.h>",
/* end */
"#define Offsetof(X, Y) ((unsigned long)(&(((X *)0)->Y)))",
"#ifndef max",
"#define max(a,b) (((a)<(b)) ? (b) : (a))",
"#endif",
0,
};
static char *Preamble[] = {
"#ifdef CNTRSTACK",
"#define onstack_now() (LL[trpt->j6] && LL[trpt->j7])",
"#define onstack_put() LL[trpt->j6]++; LL[trpt->j7]++",
"#define onstack_zap() LL[trpt->j6]--; LL[trpt->j7]--",
"#endif",
"#if !defined(SAFETY) && !defined(NOCOMP)",
/*
* V_A identifies states in the current statespace
* A_V identifies states in the 'other' statespace
* S_A remembers how many leading bytes in the sv
* are used for these markers + fairness bits
*/
"#define V_A (((now._a_t&1)?2:1) << (now._a_t&2))",
"#define A_V (((now._a_t&1)?1:2) << (now._a_t&2))",
"int S_A = 0;",
"#else",
"#define V_A 0",
"#define A_V 0",
"#define S_A 0",
"#endif",
"#ifdef MA",
"#define onstack_put() ;",
"#define onstack_zap() gstore((char *) &now, vsize, 4)",
"#else",
"#if defined(FULLSTACK) && !defined(BITSTATE)",
"#define onstack_put() trpt->ostate = Lstate",
"#define onstack_zap() { \\",
" if (trpt->ostate) \\",
" trpt->ostate->tagged = \\",
" (S_A)? (trpt->ostate->tagged&~V_A) : 0; \\",
" }",
"#endif",
"#endif",
"struct H_el {",
" struct H_el *nxt;",
"#ifdef FULLSTACK",
" unsigned tagged;",
"#if defined(BITSTATE) && !defined(NOREDUCE) && !defined(SAFETY)",
" unsigned proviso;", /* uses just 1 bit 0/1 */
"#endif",
"#endif",
"#if defined(CHECK) || (defined(COLLAPSE) && !defined(FULLSTACK))",
" unsigned long st_id;",
"#endif",
"#ifdef COLLAPSE",
"#if VECTORSZ<65536",
" unsigned short ln;", /* length of vector */
"#else",
" unsigned long ln;", /* length of vector */
"#endif",
"#endif",
"#ifdef REACH",
" unsigned D;",
"#endif",
" unsigned state;",
"} **H_tab, **S_Tab;\n",
"typedef struct Trail {",
" short st; /* current state */",
" uchar pr; /* process id */",
" uchar tau; /* 8 bit-flags */",
" uchar o_pm; /* 8 more bit-flags */",
"#if 0",
" Meaning of bit-flags:",
" tau&1 -> timeout enabled",
" tau&2 -> request to enable timeout 1 level up (in claim)",
" tau&4 -> current transition is a claim move",
" tau&8 -> current transition is an atomic move",
" tau&16 -> last move was truncated on stack",
" tau&32 -> current transition is a preselected move",
" tau&64 -> at least one next state is not on the stack",
" tau&128 -> current transition is a stutter move",
" o_pm&1 -> the current pid moved -- implements else",
" o_pm&2 -> this is an acceptance state",
" o_pm&4 -> this is a progress state",
" o_pm&8 -> fairness alg rule 1 undo mark",
" o_pm&16 -> fairness alg rule 3 undo mark",
" o_pm&32 -> fairness alg rule 2 undo mark",
" o_pm&64 -> the current proc applied rule2",
" o_pm&128 -> a fairness, dummy move - all procs blocked",
"#endif",
"#if defined(FULLSTACK) && defined(MA)",
" uchar proviso;",
"#endif",
" char o_n, o_ot, o_m; /* to save locals */",
"#ifdef EVENT_TRACE",
"#if nstates_event<256",
" uchar o_event;",
"#else",
" unsigned short o_event;",
"#endif",
"#endif",
" short o_tt, o_To;", /* used in new_state() */
"#ifdef HAS_UNLESS",
" short e_state; /* if escape trans - state of origin */",
"#endif",
"#if defined(FULLSTACK) && !defined(MA)",
" struct H_el *ostate; /* pointer to stored state */",
"#endif",
"#ifdef CNTRSTACK",
" long j6, j7;",
"#endif",
" Trans *o_t;", /* transition fct, next state */
" union {",
" int oval;", /* single backup value of variable */
" int *ovals;", /* ptr to multiple values */
" } bup;",
"} Trail;",
"Trail *trail, *trpt;",
"FILE *efd;",
"uchar *this;",
"long maxdepth=10000;",
"#ifdef SC", /* stack cycling */
"long omaxdepth;",
"char *stackfile;",
"#endif",
"uchar *SS, *LL;",
"uchar HASH_NR = 0;",
"",
"#ifdef MEMCNT",
"double memcnt = (double) 0;",
"double overhead = (double) 0;",
"double memlim = (double) (1<<30);",
"#endif",
"/* for emalloc: */",
"static char *have;",
"static long left = 0L;",
"static double fragment = (double) 0;",
"static unsigned long grow;",
"",
"unsigned int HASH_CONST[] = {",
" /* asuming 4 bytes per int */",
" 0x88888EEF, 0x00400007,",
" 0x04c11db7, 0x100d4e63,",
" 0x0fc22f87, 0x3ff0c3ff,",
" 0x38e84cd7, 0x02b148e9,",
" 0x98b2e49d, 0xb616d379,",
" 0xa5247fd9, 0xbae92a15,",
" 0xb91c8bc5, 0x8e5880f3,",
" 0xacd7c069, 0xb4c44bb3,",
" 0x2ead1fb7, 0x8e428171,",
" 0xdbebd459, 0x828ae611,",
" 0x6cb25933, 0x86cdd651,",
" 0x9e8f5f21, 0xd5f8d8e7,",
" 0x9c4e956f, 0xb5cf2c71,",
" 0x2e805a6d, 0x33fc3a55,",
" 0xaf203ed1, 0xe31f5909,",
" 0x5276db35, 0x0c565ef7,",
" 0x273d1aa5, 0x8923b1dd,",
" 0",
"};",
"int mreached=0, done=0, errors=0, Nrun=1, single=0;",
"double nstates=0, nlinks=0, truncs=0, truncs2=0;",
"double nlost=0, nShadow=0, hcmp=0, ngrabs=0;",
"unsigned long nr_states=0; /* nodes in DFA */",
"long Fa=0, Fh=0, Zh=0, Zn=0;",
"long PUT=0, PROBE=0, ZAPS=0;",
"long Ccheck=0, Cholds=0;",
"unsigned long mask;",
"int a_cycles=0, upto=1, strict=0, verbose = 0;",
"int state_tables=0, fairness=0, no_rck=0, Nr_Trails=0;",
"#ifndef INLINE",
"int TstOnly=0;",
"#endif",
"#ifdef BITSTATE",
"int ssize=22;",
"#else",
"int ssize=18;",
"#endif",
"int hmax=0, svmax=0, smax=0;",
"int Maxbody=0, XX;",
"uchar *noptr; /* used by macro Pptr(x) */",
"State A_Root; /* root of acceptance cycles */",
"State now; /* the full state vector */",
"#ifdef VAR_RANGES",
"void logval(char *, int);",
"void dumpranges(void);",
"#endif",
"#ifdef MA",
"#define INLINE_REV",
"extern void dfa_init(unsigned short);",
"extern int dfa_member(unsigned short);",
"extern int dfa_store(unsigned char *);",
"unsigned int maxgs = 0;",
"#endif",
"#if !defined(NOCOMP) || defined(BITSTATE)",
"State comp_now; /* compressed state vector */",
"State comp_msk;",
"uchar *Mask = (uchar *) &comp_msk;",
"#endif",
"#ifdef COLLAPSE",
"State comp_tmp;",
"char *scratch = (char *) &comp_tmp;",
"#endif",
"Stack *stack; /* for queues, processes */",
"Svtack *svtack; /* for old state vectors */",
"long J1, J2, J3, J4, j1, j2, j3, j4;",
"long A_depth = 0, depth = 0;",
"uchar warned = 0, iterative = 0, like_java = 0, every_error = 0;",
"uchar noasserts = 0, noends = 0;",
"#if SYNC>0 && ASYNC==0",
"void set_recvs(void);",
"int no_recvs(int);",
"#endif",
"#if SYNC",
"#define IfNotBlocked if (boq != -1) continue;",
"#define UnBlock boq = -1",
"#else",
"#define IfNotBlocked /* cannot block */",
"#define UnBlock /* don't bother */",
"#endif\n",
"void active_procs(void);",
"void cleanup(void);",
"void do_the_search(void);",
"void find_shorter(int);",
"void iniglobals(void);",
"void stopped(int);",
"void wrapup(void);",
#if 0
"void bup_q(int, int);",
"void unbup_q(int, int);",
#endif
"int *grab_ints(int);",
"void ungrab_ints(int *, int);",
0,
};
static char *Tail[] = {
"Trans *",
"settr( int t_id, int a, int b, int c, int d,",
" char *t, int g, int tpe0, int tpe1)",
"{ Trans *tmp = (Trans *) emalloc(sizeof(Trans));\n",
" tmp->atom = a&(6|32); /* only (2|8|32) have meaning */",
" if (!g) tmp->atom |= 8; /* no global references */",
" tmp->st = b;",
" tmp->tpe[0] = tpe0;",
" tmp->tpe[1] = tpe1;",
" tmp->tp = t;",
" tmp->t_id = t_id;",
" tmp->forw = c;",
" tmp->back = d;",
" return tmp;",
"}\n",
"Trans *",
"cpytr(Trans *a)",
"{ Trans *tmp = (Trans *) emalloc(sizeof(Trans));\n",
" int i;",
" tmp->atom = a->atom;",
" tmp->st = a->st;",
"#ifdef HAS_UNLESS",
" tmp->e_trans = a->e_trans;",
" for (i = 0; i < HAS_UNLESS; i++)",
" tmp->escp[i] = a->escp[i];",
"#endif",
" tmp->tpe[0] = a->tpe[0];",
" tmp->tpe[1] = a->tpe[1];",
" for (i = 0; i < 6; i++)",
" { tmp->qu[i] = a->qu[i];",
" tmp->ty[i] = a->ty[i];",
" }",
" tmp->tp = (char *) emalloc(strlen(a->tp)+1);",
" strcpy(tmp->tp, a->tp);",
" tmp->t_id = a->t_id;",
" tmp->forw = a->forw;",
" tmp->back = a->back;",
" return tmp;",
"}\n",
"#ifndef NOREDUCE",
"int",
"srinc_set(int n)",
"{ if (n <= 2) return LOCAL;",
" if (n <= 2+ DELTA) return Q_FULL_F; /* 's' or nfull */",
" if (n <= 2+2*DELTA) return Q_EMPT_F; /* 'r' or nempty */",
" if (n <= 2+3*DELTA) return Q_EMPT_T; /* empty */",
" if (n <= 2+4*DELTA) return Q_FULL_T; /* full */",
" if (n == 5*DELTA) return GLOBAL;",
" if (n == 6*DELTA) return TIMEOUT_F;",
" if (n == 7*DELTA) return ALPHA_F;",
" Uerror(\"cannot happen srinc_class\");",
" return BAD;",
"}",
"int",
"srunc(int n, int m)",
"{ switch(m) {",
" case Q_FULL_F: return n-2;",
" case Q_EMPT_F: return n-2-DELTA;",
" case Q_EMPT_T: return n-2-2*DELTA;",
" case Q_FULL_T: return n-2-3*DELTA;",
" case ALPHA_F:",
" case TIMEOUT_F: return 257; /* non-zero, and > MAXQ */",
" }",
" Uerror(\"cannot happen srunc\");",
" return 0;",
"}",
"#endif",
/* new */
"uchar *visited;",
"void",
"dovisit(int n, int m, int is, uchar reach[])",
"{ Trans *z;",
" if (is >= m || !trans[n][is]",
" || is <= 0 || visited[is])",
" return;",
" visited[is] = 1;",
" for (z = trans[n][is]; z; z = z->nxt)",
" { int i, j;",
" dovisit(n, m, z->st, reach);",
"#ifdef HAS_UNLESS",
" for (i = 0; i < HAS_UNLESS; i++)",
" { j = trans[n][is]->escp[i];",
" if (!j) break;",
" dovisit(n, m, j, reach);",
" }",
"#endif",
" }",
"}",
"void",
"check_unreachable(int n, int m, int is, short srcln[], uchar reach[])",
"{ int i; static int oldm=0;",
" if (m > oldm) /* not much memory */",
" { visited = (uchar *) emalloc(m * sizeof(uchar));",
" oldm = m;",
" } else",
" memset(visited, 0, m);",
" dovisit(n, m, is, reach);",
" for (i = 1; i < m; i++)",
" if (!visited[i] && reach[i] == 0)",
" { if (0) printf(\"%%s: merged state %%d, line %%d\\n\",",
" procname[n], i, srcln[i]);",
" reach[i] = 1;",
" }",
"}",
"int cnt;",
"int",
"isthere(Trans *a, int b)", /* is b already in a's list? */
"{ Trans *t;",
" for (t = a; t; t = t->nxt)",
" if (t->t_id == b)",
" return 1;",
" return 0;",
"}",
"#ifndef NOREDUCE",
"int",
"mark_safety(Trans *t) /* for conditional safety */",
"{ int g = 0, h, i, j, k;",
"",
" if (!t) return 0;",
" if (t->qu[0])",
" return (t->qu[1])?2:1; /* marked */",
"",
" for (i = 0; i < 2; i++)",
" { j = srinc_set(t->tpe[i]);",
" if (j >= GLOBAL)",
" return -1;",
" if (j != LOCAL)",
" { k = srunc(t->tpe[i], j);",
" if (g == 0",
" || t->qu[0] != k",
" || t->ty[0] != j)",
" { t->qu[g] = k;",
" t->ty[g] = j;",
" g++;",
" } } }",
" return g;",
"}",
"#endif",
"void",
"retrans(int n, int m, int is, short srcln[], uchar reach[])",
" /* process n, with m states, is=initial state */",
"{ Trans *T0, *T1, *T2, *T3;",
" int i, j, k, p, h, g, aa;",
" if (state_tables >= 4)",
" { printf(\"STEP 1 proctype %%s\\n\", ",
" procname[n]);",
" for (i = 1; i < m; i++)",
" for (T0 = trans[n][i]; T0; T0 = T0->nxt)",
" crack(n, i, T0, srcln);",
" return;",
" }",
" do {",
" for (i = 1, cnt = 0; i < m; i++)",
" { T2 = trans[n][i];",
" T1 = T2?T2->nxt:(Trans *)0;",
"/* prescan: */ for (T0 = T1; T0; T0 = T0->nxt)",
"/* choice in choice */ { if (T0->st && trans[n][T0->st]",
" && trans[n][T0->st]->nxt)",
" break;",
" }",
"#if 0",
" if (T0)",
" printf(\"\\tstate %%d / %%d: choice in choice\\n\",",
" i, T0->st);",
"#endif",
" if (T0)",
" for (T0 = T1; T0; T0 = T0->nxt)",
" { T3 = trans[n][T0->st];",
" if (!T3->nxt)",
" { T2->nxt = cpytr(T0);",
" T2 = T2->nxt;",
" imed(T2, T0->st, n);",
" continue;",
" }",
" do { T3 = T3->nxt;",
" T2->nxt = cpytr(T3);",
" T2 = T2->nxt;",
" imed(T2, T0->st, n);",
" } while (T3->nxt);",
" cnt++;",
" }",
" }",
" } while (cnt);",
" if (state_tables >= 3)",
" { printf(\"STEP 2 proctype %%s\\n\", ",
" procname[n]);",
" for (i = 1; i < m; i++)",
" for (T0 = trans[n][i]; T0; T0 = T0->nxt)",
" crack(n, i, T0, srcln);",
" return;",
" }",
" for (i = 1; i < m; i++)",
" { if (trans[n][i] && trans[n][i]->nxt) /* optimize */",
" { T1 = trans[n][i]->nxt;",
"#if 0",
" printf(\"\\t\\tpull %%d (%%d) to %%d\\n\",",
" T1->st, T1->forw, i);",
"#endif",
" if (!trans[n][T1->st]) continue;",
" T0 = cpytr(trans[n][T1->st]);",
" trans[n][i] = T0;",
" reach[T1->st] = 1;",
" imed(T0, T1->st, n);",
" for (T1 = T1->nxt; T1; T1 = T1->nxt)",
" {",
"#if 0",
" printf(\"\\t\\tpull %%d (%%d) to %%d\\n\",",
" T1->st, T1->forw, i);",
"#endif",
" if (!trans[n][T1->st]) continue;",
" T0->nxt = cpytr(trans[n][T1->st]);",
" T0 = T0->nxt;",
" reach[T1->st] = 1;",
" imed(T0, T1->st, n);",
" } } }",
" if (state_tables >= 2)",
" { printf(\"STEP 3 proctype %%s\\n\", ",
" procname[n]);",
" for (i = 1; i < m; i++)",
" for (T0 = trans[n][i]; T0; T0 = T0->nxt)",
" crack(n, i, T0, srcln);",
" return;",
" }",
"#ifdef HAS_UNLESS",
" for (i = 1; i < m; i++)",
" { if (!trans[n][i]) continue;",
" /* check for each state i if an",
" * escape to some state p is defined",
" * if so, copy and mark p's transitions",
" * and prepend them to the transition-",
" * list of state i",
" */",
" if (!like_java) /* the default */",
" { for (T0 = trans[n][i]; T0; T0 = T0->nxt)",
" for (k = HAS_UNLESS-1; k >= 0; k--)",
" { if (p = T0->escp[k])",
" for (T1 = trans[n][p]; T1; T1 = T1->nxt)",
" { if (isthere(trans[n][i], T1->t_id))",
" continue;",
" T2 = cpytr(T1);",
" T2->e_trans = p;",
" T2->nxt = trans[n][i];",
" trans[n][i] = T2;",
" } }",
" } else /* outermost unless checked first */",
" { Trans *T4;",
" T4 = T3 = (Trans *) 0;",
" for (T0 = trans[n][i]; T0; T0 = T0->nxt)",
" for (k = HAS_UNLESS-1; k >= 0; k--)",
" { if (p = T0->escp[k])",
" for (T1 = trans[n][p]; T1; T1 = T1->nxt)",
" { if (isthere(trans[n][i], T1->t_id))",
" continue;",
" T2 = cpytr(T1);",
" T2->nxt = (Trans *) 0;",
" T2->e_trans = p;",
" if (T3) T3->nxt = T2;",
" else T4 = T2;",
" T3 = T2;",
" } }",
" if (T4)",
" { T3->nxt = trans[n][i];",
" trans[n][i] = T4;",
" }",
" }",
" }",
"#endif",
"#ifndef NOREDUCE",
" for (i = 1; i < m; i++)",
" {",
" if (a_cycles)",
" { /* moves through these states are visible */",
"#if PROG_LAB>0 && defined(HAS_NP)",
" if (progstate[n][i])",
" goto degrade;",
" for (T1 = trans[n][i]; T1; T1 = T1->nxt)",
" if (progstate[n][T1->st])",
" goto degrade;",
"#endif",
" if (accpstate[n][i] || visstate[n][i])",
" goto degrade;",
" for (T1 = trans[n][i]; T1; T1 = T1->nxt)",
" if (accpstate[n][T1->st])",
" goto degrade;",
" }",
" T1 = trans[n][i];",
" if (!T1) continue;",
" g = mark_safety(T1); /* V3.3.1 */",
" if (g < 0) goto degrade; /* global */",
" /* check if mixing of guards preserves reduction */",
" if (T1->nxt)",
" { k = 0;",
" for (T0 = T1; T0; T0 = T0->nxt)",
" { if (!(T0->atom&8))",
" goto degrade;",
" for (aa = 0; aa < 2; aa++)",
" { if (srinc_set(T0->tpe[aa])",
" >= GLOBAL)",
" goto degrade;",
" if (T0->tpe[aa]",
" && T0->tpe[aa]",
" != T1->tpe[0])",
" k = 1;",
" } }",
" /* g = 0; V3.3.1 */",
" if (k) /* non-uniform selection */",
" for (T0 = T1; T0; T0 = T0->nxt)",
" for (aa = 0; aa < 2; aa++)",
" { j = srinc_set(T0->tpe[aa]);",
" if (j != LOCAL)",
" { k = srunc(T0->tpe[aa], j);",
" for (h = 0; h < 6; h++)",
" if (T1->qu[h] == k",
" && T1->ty[h] == j)",
" break;",
" if (h >= 6)",
" { T1->qu[g%%6] = k;",
" T1->ty[g%%6] = j;",
" g++;",
" } } }",
" if (g > 6)",
" { T1->qu[0] = 0; /* turn it off */",
"#if 1",
" printf(\"pan: warning, line %%d, \",",
" srcln[i]);",
" printf(\"too many stmnt types (%%d)\",",
" g);",
" printf(\" in selection\\n\");",
"#endif",
" goto degrade;",
" }",
" }",
" /* mark all options global if >=1 is global */",
" for (T1 = trans[n][i]; T1; T1 = T1->nxt)",
" if (!(T1->atom&8)) break;",
" if (T1)",
"degrade: for (T1 = trans[n][i]; T1; T1 = T1->nxt)",
" T1->atom &= ~8; /* mark as unsafe */",
" /* can only mix 'r's or 's's if on same chan */",
" /* and not mixed with other local operations */",
" T1 = trans[n][i];",
" if (!T1 || T1->qu[0]) continue;",
" j = T1->tpe[0];",
" if (T1->nxt && T1->atom&8)",
" { if (j == 5*DELTA)",
" {",
"#if 1",
" printf(\"warning: line %%d \", srcln[i]);",
" printf(\"mixed condition \");",
" printf(\"(defeats reduction)\\n\");",
"#endif",
" goto degrade;",
" }",
" for (T0 = T1; T0; T0 = T0->nxt)",
" for (aa = 0; aa < 2; aa++)",
" if (T0->tpe[aa] && T0->tpe[aa] != j)",
" {",
"#if 1",
" printf(\"warning: line %%d \", srcln[i]);",
" printf(\"[%%d-%%d] mixed %%stion \",",
" T0->tpe[aa], j, ",
" (j==5*DELTA)?\"condi\":\"selec\");",
" printf(\"(defeats reduction)\\n\");",
" printf(\" '%%s' <-> '%%s'\\n\",",
" T1->tp, T0->tp);",
"#endif",
" goto degrade;",
" } }",
" }",
"#endif",
" for (i = 1; i < m; i++)", /* R */
" { T2 = trans[n][i];",
" if (!T2",
" || T2->nxt",
" || strncmp(T2->tp, \".(goto)\", 7)",
" || !stopstate[n][i])",
" continue;",
" stopstate[n][T2->st] = 1;",
" }",
" if (state_tables)",
" { printf(\"proctype \");",
" if (!strcmp(procname[n], \":init:\"))",
" printf(\"init\\n\");",
" else",
" printf(\"%%s\\n\", procname[n]);",
" for (i = 1; i < m; i++)",
" reach[i] = 1;",
" tagtable(n, m, is, srcln, reach);",
" } else",
" for (i = 1; i < m; i++)",
" { int nrelse;",
" if (strcmp(procname[n], \":never:\") != 0)",
" for (T0 = trans[n][i]; T0; T0 = T0->nxt)",
" { if (T0->st == i",
" && strcmp(T0->tp, \"(1)\") == 0)",
" { printf(\"error: proctype '%%s' \",",
" procname[n]);",
" printf(\"line %%d, state %%d: has un\",",
" srcln[i], i);",
" printf(\"conditional self-loop\\n\");",
" exit(1);",
" } }",
" nrelse = 0;",
" for (T0 = trans[n][i]; T0; T0 = T0->nxt)",
" { if (strcmp(T0->tp, \"else\") == 0)",
" nrelse++;",
" }",
" if (nrelse > 1)",
" { printf(\"error: proctype '%%s' state\",",
" procname[n]);",
" printf(\" %%d, inherits %%d\", i, nrelse);",
" printf(\" 'else' stmnts\\n\");",
" exit(1);",
" } }",
" check_unreachable(n, m, is, srcln, reach);",
"}\n",
"void",
"imed(Trans *T, int v, int n) /* set intermediate state */",
"{ progstate[n][T->st] |= progstate[n][v];",
" accpstate[n][T->st] |= accpstate[n][v];",
" stopstate[n][T->st] |= stopstate[n][v];",
"}\n",
"void",
"tagtable(int n, int m, int is, short srcln[], uchar reach[])",
"{ Trans *z;\n",
" if (is >= m || !trans[n][is]",
" || is <= 0 || reach[is] == 0)",
" return;",
" reach[is] = 0;",
" if (state_tables)",
" for (z = trans[n][is]; z; z = z->nxt)",
" crack(n, is, z, srcln);",
" for (z = trans[n][is]; z; z = z->nxt)",
" { int i, j;",
" tagtable(n, m, z->st, srcln, reach);",
"#ifdef HAS_UNLESS",
" for (i = 0; i < HAS_UNLESS; i++)",
" { j = trans[n][is]->escp[i];",
" if (!j) break;",
" tagtable(n, m, j, srcln, reach);",
" }",
"#endif",
" }",
"}\n",
"void",
"crack(int n, int j, Trans *z, short srcln[])",
"{ int i;\n",
" if (!z) return;",
" printf(\"\tstate %%3d -(tr %%3d)-> state %%3d \",",
" j, z->forw, z->st);",
" printf(\"[id %%3d tp %%3d\", z->t_id, z->tpe[0]);",
" if (z->tpe[1]) printf(\",%%d\", z->tpe[1]);",
"#ifdef HAS_UNLESS",
" if (z->e_trans)",
" printf(\" org %%3d\", z->e_trans);",
" else if (state_tables >= 2)",
" for (i = 0; i < HAS_UNLESS; i++)",
" { if (!z->escp[i]) break;",
" printf(\" esc %%d\", z->escp[i]);",
" }",
"#endif",
" printf(\"]\");",
" printf(\" [%%s%%s%%s%%s%%s] line %%d => \",",
" z->atom&6?\"A\":z->atom&32?\"D\":\"-\",",
" accpstate[n][j]?\"a\" :\"-\",",
" stopstate[n][j]?\"e\" : \"-\",",
" progstate[n][j]?\"p\" : \"-\",",
" z->atom & 8 ?\"L\":\"G\",",
" srcln[j]);",
" for (i = 0; z->tp[i]; i++)",
" if (z->tp[i] == \'\\n\')",
" printf(\"\\\\n\");",
" else",
" putchar(z->tp[i]);",
"#if 0",
" printf(\"\\n\");",
"#else",
" if (z->qu[0])",
" { printf(\"\\t[\");",
" for (i = 0; i < 6; i++)",
" if (z->qu[i])",
" printf(\"(%%d,%%d)\",",
" z->qu[i], z->ty[i]);",
" printf(\"]\");",
" }",
" printf(\"\\n\");",
"#endif",
" fflush(stdout);",
"}",
"",
"#ifdef VAR_RANGES",
"#define BYTESIZE 32 /* 2^8 : 2^3 = 256:8 = 32 */",
"",
"typedef struct Vr_Ptr {",
" char *nm;",
" unsigned char vals[BYTESIZE];",
" struct Vr_Ptr *nxt;",
"} Vr_Ptr;",
"Vr_Ptr *ranges = (Vr_Ptr *) 0;",
"",
"void",
"logval(char *s, int v)",
"{ Vr_Ptr *tmp;",
"",
" if (v<0 || v > 255) return;",
" for (tmp = ranges; tmp; tmp = tmp->nxt)",
" if (!strcmp(tmp->nm, s))",
" goto found;",
" tmp = (Vr_Ptr *) emalloc(sizeof(Vr_Ptr));",
" tmp->nxt = ranges;",
" ranges = tmp;",
" tmp->nm = s;",
"found:",
" tmp->vals[(v)/8] |= 1<<((v)%%8);",
"}",
"",
"void",
"dumpval(unsigned char X[], int range)",
"{ int w, x, i, j = -1;",
"",
" for (w = i = 0; w < range; w++)",
" for (x = 0; x < 8; x++, i++)",
" {",
"from: if ((X[w] & (1<<x)))",
" { printf(\"%%d\", i);",
" j = i;",
" goto upto;",
" } }",
" return;",
" for (w = 0; w < range; w++)",
" for (x = 0; x < 8; x++, i++)",
" {",
"upto: if (!(X[w] & (1<<x)))",
" { if (i-1 == j)",
" printf(\", \");",
" else",
" printf(\"-%%d, \", i-1);",
" goto from;",
" } }",
" if (j >= 0 && j != 255)",
" printf(\"-255\");",
"}",
"",
"void",
"dumpranges(void)",
"{ Vr_Ptr *tmp;",
" printf(\"\\nValues assigned within \");",
" printf(\"interval [0..255]:\\n\");",
" for (tmp = ranges; tmp; tmp = tmp->nxt)",
" { printf(\"\\t%%s\\t: \", tmp->nm);",
" dumpval(tmp->vals, BYTESIZE);",
" printf(\"\\n\");",
" }",
"}",
"#endif",
0,
};
|
