Return to pret2.c CVS log

Up to [Research Unix] / researchv10no / cmd / pret

Annotation of researchv10no/cmd/pret/pret2.c, revision 1.1

1.1     ! root        1: #include <stdio.h>
        !             2: #include "pret.h"
        !             3: #include "pret.d"
        !             4: 
        !             5:  struct COL column[MANY];
        !             6:  struct ROW row[MANY];
        !             7: 
        !             8:  struct ENTRY *rowtail;
        !             9:  struct ENTRY *coltail;
        !            10:  struct ENTRY *base;           /* base of transition table */
        !            11: 
        !            12:  struct ENTRY *newentry();
        !            13:  struct PILAR *newunit();
        !            14: 
        !            15:  int nrrows = 0;       /* raw nr of rows (incremented by addrow() */
        !            16:  int nrcols = 0;       /* number of columns per table             */
        !            17:  int redrows = 0;      /* reduced nr of rows (set by remap()      */
        !            18:  int extras = 0;       /* counts replicated processes             */
        !            19: 
        !            20: extern char procname[MAXNAME], refname[MAXNAME];
        !            21: extern int anyerror, pid, rid, curstate, lastloop;
        !            22: 
        !            23: struct ENTRY *
        !            24: find(R, C)
        !            25: { register int i;
        !            26:   register int r = R;
        !            27:   register int c = C;
        !            28:   register struct ENTRY *here = base;
        !            29: 
        !            30:        if (r >= nrrows || c >= nrcols || r < 0 || c < 0)
        !            31:                whoops ("bad table index");
        !            32:        for (i = 0; i < r; i++)
        !            33:                here = here->nextrow;
        !            34:        for (i = 0; i < c; i++)
        !            35:                here = here->nextcol;
        !            36:        return here;
        !            37: }
        !            38: 
        !            39: getrowname(where, which)
        !            40:        char *where;
        !            41: {      strcpy(where, row[which].name);
        !            42: }
        !            43: 
        !            44: setrowname(which)
        !            45: { char stro[256];
        !            46:   extern linenumber;
        !            47:   extern char filename[];
        !            48: 
        !            49:        sprintf(stro, "%d/%d:%s", linenumber, nrrows, filename);
        !            50:        strcpy(row[which].name, stro);
        !            51: }
        !            52: 
        !            53: deadlabels()
        !            54: { register int i;
        !            55:        for (i = 0; i < nrrows; i++)
        !            56:        switch(row[i].refcount)
        !            57:        {       case ADR: printf("%s: undeclared label\n", row[i].name);
        !            58:                          anyerror++;
        !            59:                          break;
        !            60:                case DCL: printf("%s: unused label\n", row[i].name);
        !            61:                          break;
        !            62:                case ADR+DCL:
        !            63:                          break;
        !            64:                default:  whoops("cannot happen - label");
        !            65:        }
        !            66: }
        !            67: 
        !            68: remap()
        !            69: { register int i, j;
        !            70: 
        !            71:        for (i = j = 0; i < nrrows; i++)
        !            72:                if (row[i].mapping == NOSTATE)
        !            73:                        row[i].maptwo = j++;
        !            74:        redrows = j;
        !            75: }
        !            76: 
        !            77: purgerows(how)
        !            78: { int i; extern int linecode, assertion, inertion;
        !            79: 
        !            80:        for (i = 0; i < nrrows; i++)
        !            81:        {       row[i].mapping = NOSTATE;
        !            82:                row[i].maptwo = i;
        !            83:        }
        !            84:        redrows = nrrows;
        !            85: /* -> bug if (!linecode) */
        !            86:        if (!linecode || rid==assertion || rid==inertion)
        !            87:                transitrows();  /* remove dummy transitions */
        !            88:        remap();
        !            89: 
        !            90:        if (!linecode && !how)
        !            91:        {       minimize();
        !            92:                remap();
        !            93:        }
        !            94: }
        !            95: 
        !            96: target(y)
        !            97: { int i = 0;
        !            98:   int x = y;
        !            99:        while (row[x].mapping != NOSTATE)
        !           100:        {       x = row[x].mapping;
        !           101:                if (i++ > nrrows)
        !           102:                {       printf("%s: ", (pid == NONE) ? procname : refname);
        !           103:                        whoops("contains unconditional, infinite loop");
        !           104:                }
        !           105:        }
        !           106:        return x;
        !           107: }
        !           108: 
        !           109: enterowname(how, stri, bang)
        !           110:        char *stri, bang;
        !           111: { register int i;
        !           112:   char stro[256];
        !           113:   extern int linenumber;
        !           114:   extern char filename[];
        !           115: 
        !           116:        switch(how) {
        !           117:        case LAB:       sprintf(stro, "%s: %s", stri, filename);
        !           118:                        for (i = 0; i < nrrows; i++)
        !           119:                                if (strcmp(stro, row[i].name) == 0)
        !           120:                                        break;
        !           121: 
        !           122:                        if (i < nrrows)
        !           123:                        {       if (bang == DCL && (row[i].refcount & DCL))
        !           124:                                {       fprintf(stderr, "%d/%d %s %s\n",
        !           125:                                                i, nrrows, stro, row[i].name);
        !           126:                                        yyerror("label redeclared, %s", stro);
        !           127:                                }else
        !           128:                                        row[i].refcount |= bang;
        !           129:                                break;
        !           130:                        } else
        !           131:                        {       addrow();
        !           132:                                row[i].refcount = bang;
        !           133:                                row[i].labeled = 0;
        !           134:                                strcpy(row[i].name, stro);
        !           135:                        }
        !           136:                        break;
        !           137:        case NEW:       i = nrrows;
        !           138:                        sprintf(stro, "%d/%d:%s", linenumber, i, filename);
        !           139:                        addrow();
        !           140:                        row[i].refcount = bang;
        !           141:                        row[i].labeled = 0;
        !           142:                        strcpy(row[i].name, stro);
        !           143:                        break;
        !           144:        case OLD:       for (i = 0; i < nrrows; i++)
        !           145:                                if (strcmp(stri, row[i].name) == 0)
        !           146:                                        break;
        !           147:                        if (i == nrrows)
        !           148:                                whoops("cannot happen - rows");
        !           149:                        break;
        !           150:        }
        !           151:        return i;
        !           152: }
        !           153: 
        !           154: labelrow(n)
        !           155: {
        !           156:        if (n < 0 || n >= nrrows)
        !           157:                whoops("cannot happen - labelrow");
        !           158:        row[n].labeled = 1;
        !           159: 
        !           160: }
        !           161: 
        !           162: deadrows(p, r)
        !           163: { register int i, j, k;
        !           164:   struct ENTRY *it;
        !           165:   struct PILAR  *at;
        !           166:   char fld[128];
        !           167:   extern int nrprocs;
        !           168: 
        !           169:        for (i = 0; i < nrrows; i++)
        !           170:                row[i].reached = 0;
        !           171: 
        !           172:        for (i = 0; i < nrrows; i++)
        !           173:        {       if (row[i].mapping != NOSTATE)
        !           174:                        continue;
        !           175:                it = find(i, 0);
        !           176:                for (j = 0; j < nrcols; j++, it = it->nextcol)
        !           177:                {       at = it->pilar;
        !           178:                        do
        !           179:                        {       if (at->transf != NOSTATE)
        !           180:                                {       k = target(at->transf);
        !           181:                                        if (k != i)
        !           182:                                                row[k].reached = 1;
        !           183:                                }
        !           184:                                at = at->nxtp;
        !           185:                        } while (at != NULL);
        !           186:        }       }
        !           187: 
        !           188:        fld[0] = '\0';
        !           189:        for (i = k = 0; i < nrrows; i++)
        !           190:        {       if (row[i].mapping != NOSTATE)
        !           191:                        continue;
        !           192:                if (row[i].reached == 0 && row[i].maptwo != 0)
        !           193:                {       j = strlen(fld); k++;
        !           194:                        sprintf(&fld[j], "%d, ", row[i].maptwo);
        !           195:        }       }
        !           196: 
        !           197:        if (p == NONE)
        !           198:                refsize(r, redrows, k);
        !           199:        else
        !           200:                procsize(p, redrows, k);
        !           201: }
        !           202: 
        !           203: deadends(tb)
        !           204:        FILE *tb;
        !           205: { register int i, j, x;
        !           206:   struct ENTRY *it;
        !           207:   struct PILAR  *at;
        !           208:   char field[256];
        !           209:   int nrdeads = 0;
        !           210: 
        !           211:        if (nrrows == 0)
        !           212:                return;
        !           213: 
        !           214:        field[0] = '\0';
        !           215:        for (i = 0; i < nrrows; i++)
        !           216:        {       if (row[i].mapping != NOSTATE)
        !           217:                        continue;
        !           218:                it = find(i, 0);
        !           219:                for (j = 0; j < nrcols; j++, it = it->nextcol)
        !           220:                {       for (at = it->pilar; at != NULL; at = at->nxtp)
        !           221:                                if (at->transf != NOSTATE)
        !           222:                                        break;
        !           223:                        if (at != NULL)
        !           224:                                break;
        !           225:                }
        !           226:                if (j == nrcols)
        !           227:                {       x = strlen(field);
        !           228:                        sprintf(&field[x], "%d,", row[i].maptwo);
        !           229:                        nrdeads++;
        !           230:        }       }
        !           231:        if ((i = lastloop) >= 0)
        !           232:        {       if (i >= nrrows || row[i].mapping != NOSTATE)
        !           233:                        whoops("cannot happen - deadends");
        !           234:                x = strlen(field);
        !           235:                sprintf(&field[x], "%d,", row[i].maptwo);
        !           236:                nrdeads++;
        !           237:        }
        !           238:        fprintf(tb, "ENDSTATES %d: %s\n", nrdeads, field);
        !           239: }
        !           240: 
        !           241: transitrows()
        !           242: { register int i, j;
        !           243:   struct ENTRY *here, *there;
        !           244:                                        /* maintain row 0 as initial state */
        !           245:        here = base->nextrow;
        !           246:        for (i = 1; i < nrrows; i++, here = here->nextrow)
        !           247:        {       if (here->nrpils != 1 || here->pilar->code != NONE)
        !           248:                        continue;
        !           249: 
        !           250:                there = here->nextcol;
        !           251:                for (j = 1; j < nrcols; j++, there = there->nextcol)
        !           252:                        if (there->nrpils != 0)
        !           253:                                break;
        !           254:                if (j == nrcols)
        !           255:                {       row[i].mapping = here->pilar->transf;
        !           256:                        row[here->pilar->transf].labeled |= row[i].labeled;
        !           257:        }       }
        !           258: }
        !           259: 
        !           260: entercolname(val, what)
        !           261: { register int i;
        !           262: 
        !           263:        for (i = 0; i < nrcols; i++)
        !           264:                if (column[i].ccode == val && column[i].coltype == what)
        !           265:                        break;
        !           266:        if (i == nrcols)
        !           267:        {       addcol();
        !           268:                column[i].ccode = val;
        !           269:                column[i].coltype = what;
        !           270:        }
        !           271:        return i;
        !           272: }
        !           273: 
        !           274: addrow()
        !           275: { register i = nrcols;
        !           276:   struct ENTRY *lastcol, *thiscol;
        !           277:   char uni[32];
        !           278: 
        !           279:        if (nrcols == 0)
        !           280:        {       rowtail = coltail = base = newentry();
        !           281:                sprintf(uni, "%4d", curstate);
        !           282:                column[0].ccode = -1;
        !           283:                column[0].coltype = SPN;
        !           284:                strcpy(row[0].name, uni);
        !           285:                nrrows = nrcols = 1;
        !           286:        } else
        !           287:        {       if (nrrows == MANY)
        !           288:                        whoops("too many rows");
        !           289:                lastcol = rowtail;
        !           290:                rowtail = thiscol = lastcol->nextrow = newentry();
        !           291:                for (--i; i > 0; i--)
        !           292:                {       thiscol = thiscol->nextcol = newentry();
        !           293:                        lastcol = lastcol->nextcol;
        !           294:                        lastcol->nextrow = thiscol;
        !           295:                }
        !           296:                nrrows++;
        !           297:        }
        !           298: }
        !           299: 
        !           300: addcol()
        !           301: { register int i = nrrows;
        !           302:   struct ENTRY *lstrow, *thisrow;
        !           303: 
        !           304:        if (nrcols == 0)
        !           305:                whoops("cannot happen - columns");
        !           306:        else
        !           307:        {       lstrow = coltail;
        !           308:                coltail = thisrow = lstrow->nextcol = newentry();
        !           309:                if (nrcols++ == MANY)
        !           310:                        whoops("too many columns");
        !           311:                for (--i; i > 0; i--)
        !           312:                {       thisrow = thisrow->nextrow = newentry();
        !           313:                        lstrow = lstrow->nextrow;
        !           314:                        lstrow->nextcol = thisrow;
        !           315:        }       }
        !           316: }
        !           317: 
        !           318: setrans(r, c, tr, to)
        !           319: { struct ENTRY *ft;
        !           320:   struct PILAR  *pt;
        !           321:   int i;
        !           322:        ft = find(r, c);
        !           323:        pt = ft->pilar;
        !           324:        for (i = ft->nrpils++; i > 0; i--)
        !           325:                pt = pt->nxtp;
        !           326: 
        !           327:        pt->code = to;
        !           328:        pt->transf = tr;
        !           329: 
        !           330:        pt->nxtp = newunit();
        !           331: }
        !           332: 
        !           333: badstates(tb)
        !           334:        FILE *tb;
        !           335: { struct ENTRY *this, *that;
        !           336:   struct PILAR *at;
        !           337:   int i, k, x, nrbads = 0, nrlabs = 0;
        !           338:   char field[512], labfield[512];
        !           339: 
        !           340:        if (nrrows == 0)
        !           341:                return;
        !           342: 
        !           343:        labfield[0] = field[0] = '\0';
        !           344:        for (i = 0, this = base; this != NULL; this = this->nextrow, i++)
        !           345:        {       if (row[i].mapping != NOSTATE)
        !           346:                        continue;
        !           347: 
        !           348:                if (row[i].labeled)
        !           349:                {       sprintf(&labfield[strlen(labfield)], "%d,", row[i].maptwo);
        !           350:                        nrlabs++;
        !           351:                }
        !           352:                that = find(i, 0);
        !           353:                for (k = 0; k < nrcols; k++, that = that->nextcol)
        !           354:                {       if (!SPNT(column[k].coltype))
        !           355:                                continue;
        !           356: 
        !           357:                        for (at = that->pilar, x = 0; at != NULL; at = at->nxtp)
        !           358:                        {       if (at->transf == NOSTATE)
        !           359:                                        continue;
        !           360:                                x++; break;
        !           361:                        }
        !           362:                        if (x > 0)
        !           363:                        {       sprintf(&field[strlen(field)],"%d,",row[i].maptwo);
        !           364:                                nrbads++;
        !           365:                                break;
        !           366:                }       }
        !           367:        }
        !           368:        fprintf(tb, "BADSTATES %d: %s\n", nrbads, field);
        !           369:        fprintf(tb, "LABSTATES %d: %s\n", nrlabs, labfield);
        !           370: }
        !           371: 
        !           372: dumpforw(tb)
        !           373:        FILE *tb;
        !           374: { struct ENTRY *this, *that;
        !           375:   struct PILAR *at;
        !           376:   char field[256];
        !           377:   int i, j, k, x, y; extern int linecode;
        !           378: 
        !           379:        if (pid == NONE)
        !           380:                fprintf(tb, "%s %d:", "REF", rid);
        !           381:        else
        !           382:                fprintf(tb, "%s %d:", "PROC", pid+extras);
        !           383: 
        !           384:        fprintf(tb, "%d/%d:", redrows, nrcols);
        !           385:        for (i = 0; i < nrcols; i++)
        !           386:                fprintf(tb, "%d(%d),", column[i].ccode, column[i].coltype);
        !           387:        putc('\n', tb);
        !           388: 
        !           389:        for (i = 0, this = base; this != NULL; this = this->nextrow, i++)
        !           390:        {       if (row[i].mapping != NOSTATE)
        !           391:                        continue;
        !           392: 
        !           393:                that = find(i, 0);
        !           394:                for (k = 0; k < nrcols; k++, that = that->nextcol)
        !           395:                {       y = 0; field[0] = '\0';
        !           396:                        for (at = that->pilar; at != NULL; at = at->nxtp)
        !           397:                        {       if (at->transf == NOSTATE)
        !           398:                                        continue;
        !           399: 
        !           400:                                j = row[ target(at->transf) ].maptwo;
        !           401: 
        !           402:                                if ((x = strlen(field)) > 200)
        !           403:                                        whoops("string overflow");
        !           404: 
        !           405:                                sprintf(&field[x], "[%d,%d]", j, at->code);
        !           406:                                y++;
        !           407:                        }
        !           408: 
        !           409:                        if (y > 0)
        !           410:                        {       fprintf(tb, "%d/%d ", row[i].maptwo, k);
        !           411:                                fprintf(tb, "(%d) %s\n", y, field);
        !           412:        }       }       }
        !           413:        fprintf(tb, "0/0 (0)\n");
        !           414: 
        !           415:        if (linecode)
        !           416:        {       fprintf(tb, "rownames:\n");
        !           417:                for (i = 0; i < redrows; i++)
        !           418:                        fprintf(tb, "%s\n", row[i].name);
        !           419:        }
        !           420: }
        !           421: 
        !           422: wrapup(r, p, tb, np, vb)
        !           423:        FILE *tb;
        !           424: {
        !           425:        int i;
        !           426:        extern struct PROCTABLE proctable[MAXPROC];
        !           427: 
        !           428:        purgerows(np);
        !           429:        dumpforw(tb);
        !           430:        deadends(tb);
        !           431:        badstates(tb);
        !           432:        putcalls(tb);
        !           433:        numlocvars(tb);
        !           434: 
        !           435:        if (r == NONE)
        !           436:        for (i = 1; i < proctable[p].replic; i++)
        !           437:        {       extras++;
        !           438:                twiddle("_PROCID");
        !           439:                dumpforw(tb);
        !           440:                deadends(tb);
        !           441:                badstates(tb);
        !           442:                putcalls(tb);
        !           443:                numlocvars(tb);
        !           444:        }
        !           445: 
        !           446:        if (vb)
        !           447:        {       deadrows(p, r);
        !           448:                deadlabels();
        !           449:        }
        !           450: 
        !           451:        release();
        !           452:        scrapcalltable();
        !           453: }

This archive runs on limited infrastructure. Preserving old code on modern bandwidth. Automated agents are requested to crawl responsibly.