0b55f123 |
1 | /***** tl_spin: tl_trans.c *****/ |
2 | |
3 | /* Copyright (c) 1995-2003 by Lucent Technologies, Bell Laboratories. */ |
4 | /* All Rights Reserved. This software is for educational purposes only. */ |
5 | /* No guarantee whatsoever is expressed or implied by the distribution of */ |
6 | /* this code. Permission is given to distribute this code provided that */ |
7 | /* this introductory message is not removed and no monies are exchanged. */ |
8 | /* Software written by Gerard J. Holzmann. For tool documentation see: */ |
9 | /* http://spinroot.com/ */ |
10 | /* Send all bug-reports and/or questions to: bugs@spinroot.com */ |
11 | |
12 | /* Based on the translation algorithm by Gerth, Peled, Vardi, and Wolper, */ |
13 | /* presented at the PSTV Conference, held in 1995, Warsaw, Poland 1995. */ |
14 | |
15 | #include "tl.h" |
16 | |
17 | extern FILE *tl_out; |
18 | extern int tl_errs, tl_verbose, tl_terse, newstates; |
19 | |
20 | int Stack_mx=0, Max_Red=0, Total=0; |
21 | |
22 | static Mapping *Mapped = (Mapping *) 0; |
23 | static Graph *Nodes_Set = (Graph *) 0; |
24 | static Graph *Nodes_Stack = (Graph *) 0; |
25 | |
26 | static char dumpbuf[2048]; |
27 | static int Red_cnt = 0; |
28 | static int Lab_cnt = 0; |
29 | static int Base = 0; |
30 | static int Stack_sz = 0; |
31 | |
32 | static Graph *findgraph(char *); |
33 | static Graph *pop_stack(void); |
34 | static Node *Duplicate(Node *); |
35 | static Node *flatten(Node *); |
36 | static Symbol *catSlist(Symbol *, Symbol *); |
37 | static Symbol *dupSlist(Symbol *); |
38 | static char *newname(void); |
39 | static int choueka(Graph *, int); |
40 | static int not_new(Graph *); |
41 | static int set_prefix(char *, int, Graph *); |
42 | static void Addout(char *, char *); |
43 | static void fsm_trans(Graph *, int, char *); |
44 | static void mkbuchi(void); |
45 | static void expand_g(Graph *); |
46 | static void fixinit(Node *); |
47 | static void liveness(Node *); |
48 | static void mk_grn(Node *); |
49 | static void mk_red(Node *); |
50 | static void ng(Symbol *, Symbol *, Node *, Node *, Node *); |
51 | static void push_stack(Graph *); |
52 | static void sdump(Node *); |
53 | |
54 | static void |
55 | dump_graph(Graph *g) |
56 | { Node *n1; |
57 | |
58 | printf("\n\tnew:\t"); |
59 | for (n1 = g->New; n1; n1 = n1->nxt) |
60 | { dump(n1); printf(", "); } |
61 | printf("\n\told:\t"); |
62 | for (n1 = g->Old; n1; n1 = n1->nxt) |
63 | { dump(n1); printf(", "); } |
64 | printf("\n\tnxt:\t"); |
65 | for (n1 = g->Next; n1; n1 = n1->nxt) |
66 | { dump(n1); printf(", "); } |
67 | printf("\n\tother:\t"); |
68 | for (n1 = g->Other; n1; n1 = n1->nxt) |
69 | { dump(n1); printf(", "); } |
70 | printf("\n"); |
71 | } |
72 | |
73 | static void |
74 | push_stack(Graph *g) |
75 | { |
76 | if (!g) return; |
77 | |
78 | g->nxt = Nodes_Stack; |
79 | Nodes_Stack = g; |
80 | if (tl_verbose) |
81 | { Symbol *z; |
82 | printf("\nPush %s, from ", g->name->name); |
83 | for (z = g->incoming; z; z = z->next) |
84 | printf("%s, ", z->name); |
85 | dump_graph(g); |
86 | } |
87 | Stack_sz++; |
88 | if (Stack_sz > Stack_mx) Stack_mx = Stack_sz; |
89 | } |
90 | |
91 | static Graph * |
92 | pop_stack(void) |
93 | { Graph *g = Nodes_Stack; |
94 | |
95 | if (g) Nodes_Stack = g->nxt; |
96 | |
97 | Stack_sz--; |
98 | |
99 | return g; |
100 | } |
101 | |
102 | static char * |
103 | newname(void) |
104 | { static int cnt = 0; |
105 | static char buf[32]; |
106 | sprintf(buf, "S%d", cnt++); |
107 | return buf; |
108 | } |
109 | |
110 | static int |
111 | has_clause(int tok, Graph *p, Node *n) |
112 | { Node *q, *qq; |
113 | |
114 | switch (n->ntyp) { |
115 | case AND: |
116 | return has_clause(tok, p, n->lft) && |
117 | has_clause(tok, p, n->rgt); |
118 | case OR: |
119 | return has_clause(tok, p, n->lft) || |
120 | has_clause(tok, p, n->rgt); |
121 | } |
122 | |
123 | for (q = p->Other; q; q = q->nxt) |
124 | { qq = right_linked(q); |
125 | if (anywhere(tok, n, qq)) |
126 | return 1; |
127 | } |
128 | return 0; |
129 | } |
130 | |
131 | static void |
132 | mk_grn(Node *n) |
133 | { Graph *p; |
134 | |
135 | n = right_linked(n); |
136 | more: |
137 | for (p = Nodes_Set; p; p = p->nxt) |
138 | if (p->outgoing |
139 | && has_clause(AND, p, n)) |
140 | { p->isgrn[p->grncnt++] = |
141 | (unsigned char) Red_cnt; |
142 | Lab_cnt++; |
143 | } |
144 | |
145 | if (n->ntyp == U_OPER) /* 3.4.0 */ |
146 | { n = n->rgt; |
147 | goto more; |
148 | } |
149 | } |
150 | |
151 | static void |
152 | mk_red(Node *n) |
153 | { Graph *p; |
154 | |
155 | n = right_linked(n); |
156 | for (p = Nodes_Set; p; p = p->nxt) |
157 | { if (p->outgoing |
158 | && has_clause(0, p, n)) |
159 | { if (p->redcnt >= 63) |
160 | Fatal("too many Untils", (char *)0); |
161 | p->isred[p->redcnt++] = |
162 | (unsigned char) Red_cnt; |
163 | Lab_cnt++; Max_Red = Red_cnt; |
164 | } } |
165 | } |
166 | |
167 | static void |
168 | liveness(Node *n) |
169 | { |
170 | if (n) |
171 | switch (n->ntyp) { |
172 | #ifdef NXT |
173 | case NEXT: |
174 | liveness(n->lft); |
175 | break; |
176 | #endif |
177 | case U_OPER: |
178 | Red_cnt++; |
179 | mk_red(n); |
180 | mk_grn(n->rgt); |
181 | /* fall through */ |
182 | case V_OPER: |
183 | case OR: case AND: |
184 | liveness(n->lft); |
185 | liveness(n->rgt); |
186 | break; |
187 | } |
188 | } |
189 | |
190 | static Graph * |
191 | findgraph(char *nm) |
192 | { Graph *p; |
193 | Mapping *m; |
194 | |
195 | for (p = Nodes_Set; p; p = p->nxt) |
196 | if (!strcmp(p->name->name, nm)) |
197 | return p; |
198 | for (m = Mapped; m; m = m->nxt) |
199 | if (strcmp(m->from, nm) == 0) |
200 | return m->to; |
201 | |
202 | printf("warning: node %s not found\n", nm); |
203 | return (Graph *) 0; |
204 | } |
205 | |
206 | static void |
207 | Addout(char *to, char *from) |
208 | { Graph *p = findgraph(from); |
209 | Symbol *s; |
210 | |
211 | if (!p) return; |
212 | s = getsym(tl_lookup(to)); |
213 | s->next = p->outgoing; |
214 | p->outgoing = s; |
215 | } |
216 | |
217 | #ifdef NXT |
218 | int |
219 | only_nxt(Node *n) |
220 | { |
221 | switch (n->ntyp) { |
222 | case NEXT: |
223 | return 1; |
224 | case OR: |
225 | case AND: |
226 | return only_nxt(n->rgt) && only_nxt(n->lft); |
227 | default: |
228 | return 0; |
229 | } |
230 | } |
231 | #endif |
232 | |
233 | int |
234 | dump_cond(Node *pp, Node *r, int first) |
235 | { Node *q; |
236 | int frst = first; |
237 | |
238 | if (!pp) return frst; |
239 | |
240 | q = dupnode(pp); |
241 | q = rewrite(q); |
242 | |
243 | if (q->ntyp == PREDICATE |
244 | || q->ntyp == NOT |
245 | #ifndef NXT |
246 | || q->ntyp == OR |
247 | #endif |
248 | || q->ntyp == FALSE) |
249 | { if (!frst) fprintf(tl_out, " && "); |
250 | dump(q); |
251 | frst = 0; |
252 | #ifdef NXT |
253 | } else if (q->ntyp == OR) |
254 | { if (!frst) fprintf(tl_out, " && "); |
255 | fprintf(tl_out, "(("); |
256 | frst = dump_cond(q->lft, r, 1); |
257 | |
258 | if (!frst) |
259 | fprintf(tl_out, ") || ("); |
260 | else |
261 | { if (only_nxt(q->lft)) |
262 | { fprintf(tl_out, "1))"); |
263 | return 0; |
264 | } |
265 | } |
266 | |
267 | frst = dump_cond(q->rgt, r, 1); |
268 | |
269 | if (frst) |
270 | { if (only_nxt(q->rgt)) |
271 | fprintf(tl_out, "1"); |
272 | else |
273 | fprintf(tl_out, "0"); |
274 | frst = 0; |
275 | } |
276 | |
277 | fprintf(tl_out, "))"); |
278 | #endif |
279 | } else if (q->ntyp == V_OPER |
280 | && !anywhere(AND, q->rgt, r)) |
281 | { frst = dump_cond(q->rgt, r, frst); |
282 | } else if (q->ntyp == AND) |
283 | { |
284 | frst = dump_cond(q->lft, r, frst); |
285 | frst = dump_cond(q->rgt, r, frst); |
286 | } |
287 | |
288 | return frst; |
289 | } |
290 | |
291 | static int |
292 | choueka(Graph *p, int count) |
293 | { int j, k, incr_cnt = 0; |
294 | |
295 | for (j = count; j <= Max_Red; j++) /* for each acceptance class */ |
296 | { int delta = 0; |
297 | |
298 | /* is state p labeled Grn-j OR not Red-j ? */ |
299 | |
300 | for (k = 0; k < (int) p->grncnt; k++) |
301 | if (p->isgrn[k] == j) |
302 | { delta = 1; |
303 | break; |
304 | } |
305 | if (delta) |
306 | { incr_cnt++; |
307 | continue; |
308 | } |
309 | for (k = 0; k < (int) p->redcnt; k++) |
310 | if (p->isred[k] == j) |
311 | { delta = 1; |
312 | break; |
313 | } |
314 | |
315 | if (delta) break; |
316 | |
317 | incr_cnt++; |
318 | } |
319 | return incr_cnt; |
320 | } |
321 | |
322 | static int |
323 | set_prefix(char *pref, int count, Graph *r2) |
324 | { int incr_cnt = 0; /* acceptance class 'count' */ |
325 | |
326 | if (Lab_cnt == 0 |
327 | || Max_Red == 0) |
328 | sprintf(pref, "accept"); /* new */ |
329 | else if (count >= Max_Red) |
330 | sprintf(pref, "T0"); /* cycle */ |
331 | else |
332 | { incr_cnt = choueka(r2, count+1); |
333 | if (incr_cnt + count >= Max_Red) |
334 | sprintf(pref, "accept"); /* last hop */ |
335 | else |
336 | sprintf(pref, "T%d", count+incr_cnt); |
337 | } |
338 | return incr_cnt; |
339 | } |
340 | |
341 | static void |
342 | fsm_trans(Graph *p, int count, char *curnm) |
343 | { Graph *r; |
344 | Symbol *s; |
345 | char prefix[128], nwnm[256]; |
346 | |
347 | if (!p->outgoing) |
348 | addtrans(p, curnm, False, "accept_all"); |
349 | |
350 | for (s = p->outgoing; s; s = s->next) |
351 | { r = findgraph(s->name); |
352 | if (!r) continue; |
353 | if (r->outgoing) |
354 | { (void) set_prefix(prefix, count, r); |
355 | sprintf(nwnm, "%s_%s", prefix, s->name); |
356 | } else |
357 | strcpy(nwnm, "accept_all"); |
358 | |
359 | if (tl_verbose) |
360 | { printf("maxred=%d, count=%d, curnm=%s, nwnm=%s ", |
361 | Max_Red, count, curnm, nwnm); |
362 | printf("(greencnt=%d,%d, redcnt=%d,%d)\n", |
363 | r->grncnt, r->isgrn[0], |
364 | r->redcnt, r->isred[0]); |
365 | } |
366 | addtrans(p, curnm, r->Old, nwnm); |
367 | } |
368 | } |
369 | |
370 | static void |
371 | mkbuchi(void) |
372 | { Graph *p; |
373 | int k; |
374 | char curnm[64]; |
375 | |
376 | for (k = 0; k <= Max_Red; k++) |
377 | for (p = Nodes_Set; p; p = p->nxt) |
378 | { if (!p->outgoing) |
379 | continue; |
380 | if (k != 0 |
381 | && !strcmp(p->name->name, "init") |
382 | && Max_Red != 0) |
383 | continue; |
384 | |
385 | if (k == Max_Red |
386 | && strcmp(p->name->name, "init") != 0) |
387 | strcpy(curnm, "accept_"); |
388 | else |
389 | sprintf(curnm, "T%d_", k); |
390 | |
391 | strcat(curnm, p->name->name); |
392 | |
393 | fsm_trans(p, k, curnm); |
394 | } |
395 | fsm_print(); |
396 | } |
397 | |
398 | static Symbol * |
399 | dupSlist(Symbol *s) |
400 | { Symbol *p1, *p2, *p3, *d = ZS; |
401 | |
402 | for (p1 = s; p1; p1 = p1->next) |
403 | { for (p3 = d; p3; p3 = p3->next) |
404 | { if (!strcmp(p3->name, p1->name)) |
405 | break; |
406 | } |
407 | if (p3) continue; /* a duplicate */ |
408 | |
409 | p2 = getsym(p1); |
410 | p2->next = d; |
411 | d = p2; |
412 | } |
413 | return d; |
414 | } |
415 | |
416 | static Symbol * |
417 | catSlist(Symbol *a, Symbol *b) |
418 | { Symbol *p1, *p2, *p3, *tmp; |
419 | |
420 | /* remove duplicates from b */ |
421 | for (p1 = a; p1; p1 = p1->next) |
422 | { p3 = ZS; |
423 | for (p2 = b; p2; p2 = p2->next) |
424 | { if (strcmp(p1->name, p2->name)) |
425 | { p3 = p2; |
426 | continue; |
427 | } |
428 | tmp = p2->next; |
429 | tfree((void *) p2); |
430 | if (p3) |
431 | p3->next = tmp; |
432 | else |
433 | b = tmp; |
434 | } } |
435 | if (!a) return b; |
436 | if (!b) return a; |
437 | if (!b->next) |
438 | { b->next = a; |
439 | return b; |
440 | } |
441 | /* find end of list */ |
442 | for (p1 = a; p1->next; p1 = p1->next) |
443 | ; |
444 | p1->next = b; |
445 | return a; |
446 | } |
447 | |
448 | static void |
449 | fixinit(Node *orig) |
450 | { Graph *p1, *g; |
451 | Symbol *q1, *q2 = ZS; |
452 | |
453 | ng(tl_lookup("init"), ZS, ZN, ZN, ZN); |
454 | p1 = pop_stack(); |
455 | p1->nxt = Nodes_Set; |
456 | p1->Other = p1->Old = orig; |
457 | Nodes_Set = p1; |
458 | |
459 | for (g = Nodes_Set; g; g = g->nxt) |
460 | { for (q1 = g->incoming; q1; q1 = q2) |
461 | { q2 = q1->next; |
462 | Addout(g->name->name, q1->name); |
463 | tfree((void *) q1); |
464 | } |
465 | g->incoming = ZS; |
466 | } |
467 | } |
468 | |
469 | static Node * |
470 | flatten(Node *p) |
471 | { Node *q, *r, *z = ZN; |
472 | |
473 | for (q = p; q; q = q->nxt) |
474 | { r = dupnode(q); |
475 | if (z) |
476 | z = tl_nn(AND, r, z); |
477 | else |
478 | z = r; |
479 | } |
480 | if (!z) return z; |
481 | z = rewrite(z); |
482 | return z; |
483 | } |
484 | |
485 | static Node * |
486 | Duplicate(Node *n) |
487 | { Node *n1, *n2, *lst = ZN, *d = ZN; |
488 | |
489 | for (n1 = n; n1; n1 = n1->nxt) |
490 | { n2 = dupnode(n1); |
491 | if (lst) |
492 | { lst->nxt = n2; |
493 | lst = n2; |
494 | } else |
495 | d = lst = n2; |
496 | } |
497 | return d; |
498 | } |
499 | |
500 | static void |
501 | ng(Symbol *s, Symbol *in, Node *isnew, Node *isold, Node *next) |
502 | { Graph *g = (Graph *) tl_emalloc(sizeof(Graph)); |
503 | |
504 | if (s) g->name = s; |
505 | else g->name = tl_lookup(newname()); |
506 | |
507 | if (in) g->incoming = dupSlist(in); |
508 | if (isnew) g->New = flatten(isnew); |
509 | if (isold) g->Old = Duplicate(isold); |
510 | if (next) g->Next = flatten(next); |
511 | |
512 | push_stack(g); |
513 | } |
514 | |
515 | static void |
516 | sdump(Node *n) |
517 | { |
518 | switch (n->ntyp) { |
519 | case PREDICATE: strcat(dumpbuf, n->sym->name); |
520 | break; |
521 | case U_OPER: strcat(dumpbuf, "U"); |
522 | goto common2; |
523 | case V_OPER: strcat(dumpbuf, "V"); |
524 | goto common2; |
525 | case OR: strcat(dumpbuf, "|"); |
526 | goto common2; |
527 | case AND: strcat(dumpbuf, "&"); |
528 | common2: sdump(n->rgt); |
529 | common1: sdump(n->lft); |
530 | break; |
531 | #ifdef NXT |
532 | case NEXT: strcat(dumpbuf, "X"); |
533 | goto common1; |
534 | #endif |
535 | case NOT: strcat(dumpbuf, "!"); |
536 | goto common1; |
537 | case TRUE: strcat(dumpbuf, "T"); |
538 | break; |
539 | case FALSE: strcat(dumpbuf, "F"); |
540 | break; |
541 | default: strcat(dumpbuf, "?"); |
542 | break; |
543 | } |
544 | } |
545 | |
546 | Symbol * |
547 | DoDump(Node *n) |
548 | { |
549 | if (!n) return ZS; |
550 | |
551 | if (n->ntyp == PREDICATE) |
552 | return n->sym; |
553 | |
554 | dumpbuf[0] = '\0'; |
555 | sdump(n); |
556 | return tl_lookup(dumpbuf); |
557 | } |
558 | |
559 | static int |
560 | not_new(Graph *g) |
561 | { Graph *q1; Node *tmp, *n1, *n2; |
562 | Mapping *map; |
563 | |
564 | tmp = flatten(g->Old); /* duplicate, collapse, normalize */ |
565 | g->Other = g->Old; /* non normalized full version */ |
566 | g->Old = tmp; |
567 | |
568 | g->oldstring = DoDump(g->Old); |
569 | |
570 | tmp = flatten(g->Next); |
571 | g->nxtstring = DoDump(tmp); |
572 | |
573 | if (tl_verbose) dump_graph(g); |
574 | |
575 | Debug2("\tformula-old: [%s]\n", g->oldstring?g->oldstring->name:"true"); |
576 | Debug2("\tformula-nxt: [%s]\n", g->nxtstring?g->nxtstring->name:"true"); |
577 | for (q1 = Nodes_Set; q1; q1 = q1->nxt) |
578 | { Debug2(" compare old to: %s", q1->name->name); |
579 | Debug2(" [%s]", q1->oldstring?q1->oldstring->name:"true"); |
580 | |
581 | Debug2(" compare nxt to: %s", q1->name->name); |
582 | Debug2(" [%s]", q1->nxtstring?q1->nxtstring->name:"true"); |
583 | |
584 | if (q1->oldstring != g->oldstring |
585 | || q1->nxtstring != g->nxtstring) |
586 | { Debug(" => different\n"); |
587 | continue; |
588 | } |
589 | Debug(" => match\n"); |
590 | |
591 | if (g->incoming) |
592 | q1->incoming = catSlist(g->incoming, q1->incoming); |
593 | |
594 | /* check if there's anything in g->Other that needs |
595 | adding to q1->Other |
596 | */ |
597 | for (n2 = g->Other; n2; n2 = n2->nxt) |
598 | { for (n1 = q1->Other; n1; n1 = n1->nxt) |
599 | if (isequal(n1, n2)) |
600 | break; |
601 | if (!n1) |
602 | { Node *n3 = dupnode(n2); |
603 | /* don't mess up n2->nxt */ |
604 | n3->nxt = q1->Other; |
605 | q1->Other = n3; |
606 | } } |
607 | |
608 | map = (Mapping *) tl_emalloc(sizeof(Mapping)); |
609 | map->from = g->name->name; |
610 | map->to = q1; |
611 | map->nxt = Mapped; |
612 | Mapped = map; |
613 | |
614 | for (n1 = g->Other; n1; n1 = n2) |
615 | { n2 = n1->nxt; |
616 | releasenode(1, n1); |
617 | } |
618 | for (n1 = g->Old; n1; n1 = n2) |
619 | { n2 = n1->nxt; |
620 | releasenode(1, n1); |
621 | } |
622 | for (n1 = g->Next; n1; n1 = n2) |
623 | { n2 = n1->nxt; |
624 | releasenode(1, n1); |
625 | } |
626 | return 1; |
627 | } |
628 | |
629 | if (newstates) tl_verbose=1; |
630 | Debug2(" New Node %s [", g->name->name); |
631 | for (n1 = g->Old; n1; n1 = n1->nxt) |
632 | { Dump(n1); Debug(", "); } |
633 | Debug2("] nr %d\n", Base); |
634 | if (newstates) tl_verbose=0; |
635 | |
636 | Base++; |
637 | g->nxt = Nodes_Set; |
638 | Nodes_Set = g; |
639 | |
640 | return 0; |
641 | } |
642 | |
643 | static void |
644 | expand_g(Graph *g) |
645 | { Node *now, *n1, *n2, *nx; |
646 | int can_release; |
647 | |
648 | if (!g->New) |
649 | { Debug2("\nDone with %s", g->name->name); |
650 | if (tl_verbose) dump_graph(g); |
651 | if (not_new(g)) |
652 | { if (tl_verbose) printf("\tIs Not New\n"); |
653 | return; |
654 | } |
655 | if (g->Next) |
656 | { Debug(" Has Next ["); |
657 | for (n1 = g->Next; n1; n1 = n1->nxt) |
658 | { Dump(n1); Debug(", "); } |
659 | Debug("]\n"); |
660 | |
661 | ng(ZS, getsym(g->name), g->Next, ZN, ZN); |
662 | } |
663 | return; |
664 | } |
665 | |
666 | if (tl_verbose) |
667 | { Symbol *z; |
668 | printf("\nExpand %s, from ", g->name->name); |
669 | for (z = g->incoming; z; z = z->next) |
670 | printf("%s, ", z->name); |
671 | printf("\n\thandle:\t"); Explain(g->New->ntyp); |
672 | dump_graph(g); |
673 | } |
674 | |
675 | if (g->New->ntyp == AND) |
676 | { if (g->New->nxt) |
677 | { n2 = g->New->rgt; |
678 | while (n2->nxt) |
679 | n2 = n2->nxt; |
680 | n2->nxt = g->New->nxt; |
681 | } |
682 | n1 = n2 = g->New->lft; |
683 | while (n2->nxt) |
684 | n2 = n2->nxt; |
685 | n2->nxt = g->New->rgt; |
686 | |
687 | releasenode(0, g->New); |
688 | |
689 | g->New = n1; |
690 | push_stack(g); |
691 | return; |
692 | } |
693 | |
694 | can_release = 0; /* unless it need not go into Old */ |
695 | now = g->New; |
696 | g->New = g->New->nxt; |
697 | now->nxt = ZN; |
698 | |
699 | if (now->ntyp != TRUE) |
700 | { if (g->Old) |
701 | { for (n1 = g->Old; n1->nxt; n1 = n1->nxt) |
702 | if (isequal(now, n1)) |
703 | { can_release = 1; |
704 | goto out; |
705 | } |
706 | n1->nxt = now; |
707 | } else |
708 | g->Old = now; |
709 | } |
710 | out: |
711 | switch (now->ntyp) { |
712 | case FALSE: |
713 | push_stack(g); |
714 | break; |
715 | case TRUE: |
716 | releasenode(1, now); |
717 | push_stack(g); |
718 | break; |
719 | case PREDICATE: |
720 | case NOT: |
721 | if (can_release) releasenode(1, now); |
722 | push_stack(g); |
723 | break; |
724 | case V_OPER: |
725 | Assert(now->rgt != ZN, now->ntyp); |
726 | Assert(now->lft != ZN, now->ntyp); |
727 | Assert(now->rgt->nxt == ZN, now->ntyp); |
728 | Assert(now->lft->nxt == ZN, now->ntyp); |
729 | n1 = now->rgt; |
730 | n1->nxt = g->New; |
731 | |
732 | if (can_release) |
733 | nx = now; |
734 | else |
735 | nx = getnode(now); /* now also appears in Old */ |
736 | nx->nxt = g->Next; |
737 | |
738 | n2 = now->lft; |
739 | n2->nxt = getnode(now->rgt); |
740 | n2->nxt->nxt = g->New; |
741 | g->New = flatten(n2); |
742 | push_stack(g); |
743 | ng(ZS, g->incoming, n1, g->Old, nx); |
744 | break; |
745 | |
746 | case U_OPER: |
747 | Assert(now->rgt->nxt == ZN, now->ntyp); |
748 | Assert(now->lft->nxt == ZN, now->ntyp); |
749 | n1 = now->lft; |
750 | |
751 | if (can_release) |
752 | nx = now; |
753 | else |
754 | nx = getnode(now); /* now also appears in Old */ |
755 | nx->nxt = g->Next; |
756 | |
757 | n2 = now->rgt; |
758 | n2->nxt = g->New; |
759 | |
760 | goto common; |
761 | |
762 | #ifdef NXT |
763 | case NEXT: |
764 | Assert(now->lft != ZN, now->ntyp); |
765 | nx = dupnode(now->lft); |
766 | nx->nxt = g->Next; |
767 | g->Next = nx; |
768 | if (can_release) releasenode(0, now); |
769 | push_stack(g); |
770 | break; |
771 | #endif |
772 | |
773 | case OR: |
774 | Assert(now->rgt->nxt == ZN, now->ntyp); |
775 | Assert(now->lft->nxt == ZN, now->ntyp); |
776 | n1 = now->lft; |
777 | nx = g->Next; |
778 | |
779 | n2 = now->rgt; |
780 | n2->nxt = g->New; |
781 | common: |
782 | n1->nxt = g->New; |
783 | |
784 | ng(ZS, g->incoming, n1, g->Old, nx); |
785 | g->New = flatten(n2); |
786 | |
787 | if (can_release) releasenode(1, now); |
788 | |
789 | push_stack(g); |
790 | break; |
791 | } |
792 | } |
793 | |
794 | Node * |
795 | twocases(Node *p) |
796 | { Node *q; |
797 | /* 1: ([]p1 && []p2) == [](p1 && p2) */ |
798 | /* 2: (<>p1 || <>p2) == <>(p1 || p2) */ |
799 | |
800 | if (!p) return p; |
801 | |
802 | switch(p->ntyp) { |
803 | case AND: |
804 | case OR: |
805 | case U_OPER: |
806 | case V_OPER: |
807 | p->lft = twocases(p->lft); |
808 | p->rgt = twocases(p->rgt); |
809 | break; |
810 | #ifdef NXT |
811 | case NEXT: |
812 | #endif |
813 | case NOT: |
814 | p->lft = twocases(p->lft); |
815 | break; |
816 | |
817 | default: |
818 | break; |
819 | } |
820 | if (p->ntyp == AND /* 1 */ |
821 | && p->lft->ntyp == V_OPER |
822 | && p->lft->lft->ntyp == FALSE |
823 | && p->rgt->ntyp == V_OPER |
824 | && p->rgt->lft->ntyp == FALSE) |
825 | { q = tl_nn(V_OPER, False, |
826 | tl_nn(AND, p->lft->rgt, p->rgt->rgt)); |
827 | } else |
828 | if (p->ntyp == OR /* 2 */ |
829 | && p->lft->ntyp == U_OPER |
830 | && p->lft->lft->ntyp == TRUE |
831 | && p->rgt->ntyp == U_OPER |
832 | && p->rgt->lft->ntyp == TRUE) |
833 | { q = tl_nn(U_OPER, True, |
834 | tl_nn(OR, p->lft->rgt, p->rgt->rgt)); |
835 | } else |
836 | q = p; |
837 | return q; |
838 | } |
839 | |
840 | void |
841 | trans(Node *p) |
842 | { Node *op; |
843 | Graph *g; |
844 | |
845 | if (!p || tl_errs) return; |
846 | |
847 | p = twocases(p); |
848 | |
849 | if (tl_verbose || tl_terse) |
850 | { fprintf(tl_out, "\t/* Normlzd: "); |
851 | dump(p); |
852 | fprintf(tl_out, " */\n"); |
853 | } |
854 | if (tl_terse) |
855 | return; |
856 | |
857 | op = dupnode(p); |
858 | |
859 | ng(ZS, getsym(tl_lookup("init")), p, ZN, ZN); |
860 | while ((g = Nodes_Stack) != (Graph *) 0) |
861 | { Nodes_Stack = g->nxt; |
862 | expand_g(g); |
863 | } |
864 | if (newstates) |
865 | return; |
866 | |
867 | fixinit(p); |
868 | liveness(flatten(op)); /* was: liveness(op); */ |
869 | |
870 | mkbuchi(); |
871 | if (tl_verbose) |
872 | { printf("/*\n"); |
873 | printf(" * %d states in Streett automaton\n", Base); |
874 | printf(" * %d Streett acceptance conditions\n", Max_Red); |
875 | printf(" * %d Buchi states\n", Total); |
876 | printf(" */\n"); |
877 | } |
878 | } |