![[BACK]](/cvsweb/icons/back.gif){kind=icon}
Return to pret2.c CVS log ![[TXT]](/cvsweb/icons/text.gif){kind=icon}
![[DIR]](/cvsweb/icons/dir.gif){kind=icon}
Up to [Research Unix] / researchv10dc / cmd / pret|
Return to pret2.c CVS log | Up to [Research Unix] / researchv10dc / cmd / pret |
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.