0b55f123 |
1 | /***** tl_spin: tl_buchi.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 int tl_verbose, tl_clutter, Total, Max_Red; |
18 | |
19 | FILE *tl_out; /* if standalone: = stdout; */ |
20 | |
21 | typedef struct Transition { |
22 | Symbol *name; |
23 | Node *cond; |
24 | int redundant, merged, marked; |
25 | struct Transition *nxt; |
26 | } Transition; |
27 | |
28 | typedef struct State { |
29 | Symbol *name; |
30 | Transition *trans; |
31 | Graph *colors; |
32 | unsigned char redundant; |
33 | unsigned char accepting; |
34 | unsigned char reachable; |
35 | struct State *nxt; |
36 | } State; |
37 | |
38 | static State *never = (State *) 0; |
39 | static int hitsall; |
40 | |
41 | static int |
42 | sametrans(Transition *s, Transition *t) |
43 | { |
44 | if (strcmp(s->name->name, t->name->name) != 0) |
45 | return 0; |
46 | return isequal(s->cond, t->cond); |
47 | } |
48 | |
49 | static Node * |
50 | Prune(Node *p) |
51 | { |
52 | if (p) |
53 | switch (p->ntyp) { |
54 | case PREDICATE: |
55 | case NOT: |
56 | case FALSE: |
57 | case TRUE: |
58 | #ifdef NXT |
59 | case NEXT: |
60 | #endif |
61 | return p; |
62 | case OR: |
63 | p->lft = Prune(p->lft); |
64 | if (!p->lft) |
65 | { releasenode(1, p->rgt); |
66 | return ZN; |
67 | } |
68 | p->rgt = Prune(p->rgt); |
69 | if (!p->rgt) |
70 | { releasenode(1, p->lft); |
71 | return ZN; |
72 | } |
73 | return p; |
74 | case AND: |
75 | p->lft = Prune(p->lft); |
76 | if (!p->lft) |
77 | return Prune(p->rgt); |
78 | p->rgt = Prune(p->rgt); |
79 | if (!p->rgt) |
80 | return p->lft; |
81 | return p; |
82 | } |
83 | releasenode(1, p); |
84 | return ZN; |
85 | } |
86 | |
87 | static State * |
88 | findstate(char *nm) |
89 | { State *b; |
90 | for (b = never; b; b = b->nxt) |
91 | if (!strcmp(b->name->name, nm)) |
92 | return b; |
93 | if (strcmp(nm, "accept_all")) |
94 | { if (strncmp(nm, "accept", 6)) |
95 | { int i; char altnm[64]; |
96 | for (i = 0; i < 64; i++) |
97 | if (nm[i] == '_') |
98 | break; |
99 | if (i >= 64) |
100 | Fatal("name too long %s", nm); |
101 | sprintf(altnm, "accept%s", &nm[i]); |
102 | return findstate(altnm); |
103 | } |
104 | /* Fatal("buchi: no state %s", nm); */ |
105 | } |
106 | return (State *) 0; |
107 | } |
108 | |
109 | static void |
110 | Dfs(State *b) |
111 | { Transition *t; |
112 | |
113 | if (!b || b->reachable) return; |
114 | b->reachable = 1; |
115 | |
116 | if (b->redundant) |
117 | printf("/* redundant state %s */\n", |
118 | b->name->name); |
119 | for (t = b->trans; t; t = t->nxt) |
120 | { if (!t->redundant) |
121 | { Dfs(findstate(t->name->name)); |
122 | if (!hitsall |
123 | && strcmp(t->name->name, "accept_all") == 0) |
124 | hitsall = 1; |
125 | } |
126 | } |
127 | } |
128 | |
129 | void |
130 | retarget(char *from, char *to) |
131 | { State *b; |
132 | Transition *t; |
133 | Symbol *To = tl_lookup(to); |
134 | |
135 | if (tl_verbose) printf("replace %s with %s\n", from, to); |
136 | |
137 | for (b = never; b; b = b->nxt) |
138 | { if (!strcmp(b->name->name, from)) |
139 | b->redundant = 1; |
140 | else |
141 | for (t = b->trans; t; t = t->nxt) |
142 | { if (!strcmp(t->name->name, from)) |
143 | t->name = To; |
144 | } } |
145 | } |
146 | |
147 | #ifdef NXT |
148 | static Node * |
149 | nonxt(Node *n) |
150 | { |
151 | switch (n->ntyp) { |
152 | case U_OPER: |
153 | case V_OPER: |
154 | case NEXT: |
155 | return ZN; |
156 | case OR: |
157 | n->lft = nonxt(n->lft); |
158 | n->rgt = nonxt(n->rgt); |
159 | if (!n->lft || !n->rgt) |
160 | return True; |
161 | return n; |
162 | case AND: |
163 | n->lft = nonxt(n->lft); |
164 | n->rgt = nonxt(n->rgt); |
165 | if (!n->lft) |
166 | { if (!n->rgt) |
167 | n = ZN; |
168 | else |
169 | n = n->rgt; |
170 | } else if (!n->rgt) |
171 | n = n->lft; |
172 | return n; |
173 | } |
174 | return n; |
175 | } |
176 | #endif |
177 | |
178 | static Node * |
179 | combination(Node *s, Node *t) |
180 | { Node *nc; |
181 | #ifdef NXT |
182 | Node *a = nonxt(s); |
183 | Node *b = nonxt(t); |
184 | |
185 | if (tl_verbose) |
186 | { printf("\tnonxtA: "); dump(a); |
187 | printf("\n\tnonxtB: "); dump(b); |
188 | printf("\n"); |
189 | } |
190 | /* if there's only a X(f), its equivalent to true */ |
191 | if (!a || !b) |
192 | nc = True; |
193 | else |
194 | nc = tl_nn(OR, a, b); |
195 | #else |
196 | nc = tl_nn(OR, s, t); |
197 | #endif |
198 | if (tl_verbose) |
199 | { printf("\tcombo: "); dump(nc); |
200 | printf("\n"); |
201 | } |
202 | return nc; |
203 | } |
204 | |
205 | Node * |
206 | unclutter(Node *n, char *snm) |
207 | { Node *t, *s, *v, *u; |
208 | Symbol *w; |
209 | |
210 | /* check only simple cases like !q && q */ |
211 | for (t = n; t; t = t->rgt) |
212 | { if (t->rgt) |
213 | { if (t->ntyp != AND || !t->lft) |
214 | return n; |
215 | if (t->lft->ntyp != PREDICATE |
216 | #ifdef NXT |
217 | && t->lft->ntyp != NEXT |
218 | #endif |
219 | && t->lft->ntyp != NOT) |
220 | return n; |
221 | } else |
222 | { if (t->ntyp != PREDICATE |
223 | #ifdef NXT |
224 | && t->ntyp != NEXT |
225 | #endif |
226 | && t->ntyp != NOT) |
227 | return n; |
228 | } |
229 | } |
230 | |
231 | for (t = n; t; t = t->rgt) |
232 | { if (t->rgt) |
233 | v = t->lft; |
234 | else |
235 | v = t; |
236 | if (v->ntyp == NOT |
237 | && v->lft->ntyp == PREDICATE) |
238 | { w = v->lft->sym; |
239 | for (s = n; s; s = s->rgt) |
240 | { if (s == t) continue; |
241 | if (s->rgt) |
242 | u = s->lft; |
243 | else |
244 | u = s; |
245 | if (u->ntyp == PREDICATE |
246 | && strcmp(u->sym->name, w->name) == 0) |
247 | { if (tl_verbose) |
248 | { printf("BINGO %s:\t", snm); |
249 | dump(n); |
250 | printf("\n"); |
251 | } |
252 | return False; |
253 | } |
254 | } |
255 | } } |
256 | return n; |
257 | } |
258 | |
259 | static void |
260 | clutter(void) |
261 | { State *p; |
262 | Transition *s; |
263 | |
264 | for (p = never; p; p = p->nxt) |
265 | for (s = p->trans; s; s = s->nxt) |
266 | { s->cond = unclutter(s->cond, p->name->name); |
267 | if (s->cond |
268 | && s->cond->ntyp == FALSE) |
269 | { if (s != p->trans |
270 | || s->nxt) |
271 | s->redundant = 1; |
272 | } |
273 | } |
274 | } |
275 | |
276 | static void |
277 | showtrans(State *a) |
278 | { Transition *s; |
279 | |
280 | for (s = a->trans; s; s = s->nxt) |
281 | { printf("%s ", s->name?s->name->name:"-"); |
282 | dump(s->cond); |
283 | printf(" %d %d %d\n", s->redundant, s->merged, s->marked); |
284 | } |
285 | } |
286 | |
287 | static int |
288 | mergetrans(void) |
289 | { State *b; |
290 | Transition *s, *t; |
291 | Node *nc; int cnt = 0; |
292 | |
293 | for (b = never; b; b = b->nxt) |
294 | { if (!b->reachable) continue; |
295 | |
296 | for (s = b->trans; s; s = s->nxt) |
297 | { if (s->redundant) continue; |
298 | |
299 | for (t = s->nxt; t; t = t->nxt) |
300 | if (!t->redundant |
301 | && !strcmp(s->name->name, t->name->name)) |
302 | { if (tl_verbose) |
303 | { printf("===\nstate %s, trans to %s redundant\n", |
304 | b->name->name, s->name->name); |
305 | showtrans(b); |
306 | printf(" conditions "); |
307 | dump(s->cond); printf(" <-> "); |
308 | dump(t->cond); printf("\n"); |
309 | } |
310 | |
311 | if (!s->cond) /* same as T */ |
312 | { releasenode(1, t->cond); /* T or t */ |
313 | nc = True; |
314 | } else if (!t->cond) |
315 | { releasenode(1, s->cond); |
316 | nc = True; |
317 | } else |
318 | { nc = combination(s->cond, t->cond); |
319 | } |
320 | t->cond = rewrite(nc); |
321 | t->merged = 1; |
322 | s->redundant = 1; |
323 | cnt++; |
324 | break; |
325 | } } } |
326 | return cnt; |
327 | } |
328 | |
329 | static int |
330 | all_trans_match(State *a, State *b) |
331 | { Transition *s, *t; |
332 | int found, result = 0; |
333 | |
334 | if (a->accepting != b->accepting) |
335 | goto done; |
336 | |
337 | for (s = a->trans; s; s = s->nxt) |
338 | { if (s->redundant) continue; |
339 | found = 0; |
340 | for (t = b->trans; t; t = t->nxt) |
341 | { if (t->redundant) continue; |
342 | if (sametrans(s, t)) |
343 | { found = 1; |
344 | t->marked = 1; |
345 | break; |
346 | } } |
347 | if (!found) |
348 | goto done; |
349 | } |
350 | for (s = b->trans; s; s = s->nxt) |
351 | { if (s->redundant || s->marked) continue; |
352 | found = 0; |
353 | for (t = a->trans; t; t = t->nxt) |
354 | { if (t->redundant) continue; |
355 | if (sametrans(s, t)) |
356 | { found = 1; |
357 | break; |
358 | } } |
359 | if (!found) |
360 | goto done; |
361 | } |
362 | result = 1; |
363 | done: |
364 | for (s = b->trans; s; s = s->nxt) |
365 | s->marked = 0; |
366 | return result; |
367 | } |
368 | |
369 | #ifndef NO_OPT |
370 | #define BUCKY |
371 | #endif |
372 | |
373 | #ifdef BUCKY |
374 | static int |
375 | all_bucky(State *a, State *b) |
376 | { Transition *s, *t; |
377 | int found, result = 0; |
378 | |
379 | for (s = a->trans; s; s = s->nxt) |
380 | { if (s->redundant) continue; |
381 | found = 0; |
382 | for (t = b->trans; t; t = t->nxt) |
383 | { if (t->redundant) continue; |
384 | |
385 | if (isequal(s->cond, t->cond)) |
386 | { if (strcmp(s->name->name, b->name->name) == 0 |
387 | && strcmp(t->name->name, a->name->name) == 0) |
388 | { found = 1; /* they point to each other */ |
389 | t->marked = 1; |
390 | break; |
391 | } |
392 | if (strcmp(s->name->name, t->name->name) == 0 |
393 | && strcmp(s->name->name, "accept_all") == 0) |
394 | { found = 1; |
395 | t->marked = 1; |
396 | break; |
397 | /* same exit from which there is no return */ |
398 | } |
399 | } |
400 | } |
401 | if (!found) |
402 | goto done; |
403 | } |
404 | for (s = b->trans; s; s = s->nxt) |
405 | { if (s->redundant || s->marked) continue; |
406 | found = 0; |
407 | for (t = a->trans; t; t = t->nxt) |
408 | { if (t->redundant) continue; |
409 | |
410 | if (isequal(s->cond, t->cond)) |
411 | { if (strcmp(s->name->name, a->name->name) == 0 |
412 | && strcmp(t->name->name, b->name->name) == 0) |
413 | { found = 1; |
414 | t->marked = 1; |
415 | break; |
416 | } |
417 | if (strcmp(s->name->name, t->name->name) == 0 |
418 | && strcmp(s->name->name, "accept_all") == 0) |
419 | { found = 1; |
420 | t->marked = 1; |
421 | break; |
422 | } |
423 | } |
424 | } |
425 | if (!found) |
426 | goto done; |
427 | } |
428 | result = 1; |
429 | done: |
430 | for (s = b->trans; s; s = s->nxt) |
431 | s->marked = 0; |
432 | return result; |
433 | } |
434 | |
435 | static int |
436 | buckyballs(void) |
437 | { State *a, *b, *c, *d; |
438 | int m, cnt=0; |
439 | |
440 | do { |
441 | m = 0; cnt++; |
442 | for (a = never; a; a = a->nxt) |
443 | { if (!a->reachable) continue; |
444 | |
445 | if (a->redundant) continue; |
446 | |
447 | for (b = a->nxt; b; b = b->nxt) |
448 | { if (!b->reachable) continue; |
449 | |
450 | if (b->redundant) continue; |
451 | |
452 | if (all_bucky(a, b)) |
453 | { m++; |
454 | if (tl_verbose) |
455 | { printf("%s bucky match %s\n", |
456 | a->name->name, b->name->name); |
457 | } |
458 | |
459 | if (a->accepting && !b->accepting) |
460 | { if (strcmp(b->name->name, "T0_init") == 0) |
461 | { c = a; d = b; |
462 | b->accepting = 1; |
463 | } else |
464 | { c = b; d = a; |
465 | } |
466 | } else |
467 | { c = a; d = b; |
468 | } |
469 | |
470 | retarget(c->name->name, d->name->name); |
471 | if (!strncmp(c->name->name, "accept", 6) |
472 | && Max_Red == 0) |
473 | { char buf[64]; |
474 | sprintf(buf, "T0%s", &(c->name->name[6])); |
475 | retarget(buf, d->name->name); |
476 | } |
477 | break; |
478 | } |
479 | } } |
480 | } while (m && cnt < 10); |
481 | return cnt-1; |
482 | } |
483 | #endif |
484 | |
485 | static int |
486 | mergestates(int v) |
487 | { State *a, *b; |
488 | int m, cnt=0; |
489 | |
490 | if (tl_verbose) |
491 | return 0; |
492 | |
493 | do { |
494 | m = 0; cnt++; |
495 | for (a = never; a; a = a->nxt) |
496 | { if (v && !a->reachable) continue; |
497 | |
498 | if (a->redundant) continue; /* 3.3.10 */ |
499 | |
500 | for (b = a->nxt; b; b = b->nxt) |
501 | { if (v && !b->reachable) continue; |
502 | |
503 | if (b->redundant) continue; /* 3.3.10 */ |
504 | |
505 | if (all_trans_match(a, b)) |
506 | { m++; |
507 | if (tl_verbose) |
508 | { printf("%d: state %s equals state %s\n", |
509 | cnt, a->name->name, b->name->name); |
510 | showtrans(a); |
511 | printf("==\n"); |
512 | showtrans(b); |
513 | } |
514 | retarget(a->name->name, b->name->name); |
515 | if (!strncmp(a->name->name, "accept", 6) |
516 | && Max_Red == 0) |
517 | { char buf[64]; |
518 | sprintf(buf, "T0%s", &(a->name->name[6])); |
519 | retarget(buf, b->name->name); |
520 | } |
521 | break; |
522 | } |
523 | #if 0 |
524 | else if (tl_verbose) |
525 | { printf("\n%d: state %s differs from state %s [%d,%d]\n", |
526 | cnt, a->name->name, b->name->name, |
527 | a->accepting, b->accepting); |
528 | showtrans(a); |
529 | printf("==\n"); |
530 | showtrans(b); |
531 | printf("\n"); |
532 | } |
533 | #endif |
534 | } } |
535 | } while (m && cnt < 10); |
536 | return cnt-1; |
537 | } |
538 | |
539 | static int tcnt; |
540 | |
541 | static void |
542 | rev_trans(Transition *t) /* print transitions in reverse order... */ |
543 | { |
544 | if (!t) return; |
545 | rev_trans(t->nxt); |
546 | |
547 | if (t->redundant && !tl_verbose) return; |
548 | fprintf(tl_out, "\t:: ("); |
549 | if (dump_cond(t->cond, t->cond, 1)) |
550 | fprintf(tl_out, "1"); |
551 | fprintf(tl_out, ") -> goto %s\n", t->name->name); |
552 | tcnt++; |
553 | } |
554 | |
555 | static void |
556 | printstate(State *b) |
557 | { |
558 | if (!b || (!tl_verbose && !b->reachable)) return; |
559 | |
560 | b->reachable = 0; /* print only once */ |
561 | fprintf(tl_out, "%s:\n", b->name->name); |
562 | |
563 | if (tl_verbose) |
564 | { fprintf(tl_out, " /* "); |
565 | dump(b->colors->Other); |
566 | fprintf(tl_out, " */\n"); |
567 | } |
568 | |
569 | if (strncmp(b->name->name, "accept", 6) == 0 |
570 | && Max_Red == 0) |
571 | fprintf(tl_out, "T0%s:\n", &(b->name->name[6])); |
572 | |
573 | fprintf(tl_out, "\tif\n"); |
574 | tcnt = 0; |
575 | rev_trans(b->trans); |
576 | if (!tcnt) fprintf(tl_out, "\t:: false\n"); |
577 | fprintf(tl_out, "\tfi;\n"); |
578 | Total++; |
579 | } |
580 | |
581 | void |
582 | addtrans(Graph *col, char *from, Node *op, char *to) |
583 | { State *b; |
584 | Transition *t; |
585 | |
586 | t = (Transition *) tl_emalloc(sizeof(Transition)); |
587 | t->name = tl_lookup(to); |
588 | t->cond = Prune(dupnode(op)); |
589 | |
590 | if (tl_verbose) |
591 | { printf("\n%s <<\t", from); dump(op); |
592 | printf("\n\t"); dump(t->cond); |
593 | printf(">> %s\n", t->name->name); |
594 | } |
595 | if (t->cond) t->cond = rewrite(t->cond); |
596 | |
597 | for (b = never; b; b = b->nxt) |
598 | if (!strcmp(b->name->name, from)) |
599 | { t->nxt = b->trans; |
600 | b->trans = t; |
601 | return; |
602 | } |
603 | b = (State *) tl_emalloc(sizeof(State)); |
604 | b->name = tl_lookup(from); |
605 | b->colors = col; |
606 | b->trans = t; |
607 | if (!strncmp(from, "accept", 6)) |
608 | b->accepting = 1; |
609 | b->nxt = never; |
610 | never = b; |
611 | } |
612 | |
613 | static void |
614 | clr_reach(void) |
615 | { State *p; |
616 | for (p = never; p; p = p->nxt) |
617 | p->reachable = 0; |
618 | hitsall = 0; |
619 | } |
620 | |
621 | void |
622 | fsm_print(void) |
623 | { State *b; int cnt1, cnt2=0; |
624 | extern void put_uform(void); |
625 | |
626 | if (tl_clutter) clutter(); |
627 | |
628 | b = findstate("T0_init"); |
629 | if (b && (Max_Red == 0)) |
630 | b->accepting = 1; |
631 | |
632 | mergestates(0); |
633 | b = findstate("T0_init"); |
634 | |
635 | fprintf(tl_out, "never { /* "); |
636 | put_uform(); |
637 | fprintf(tl_out, " */\n"); |
638 | |
639 | do { |
640 | clr_reach(); |
641 | Dfs(b); |
642 | cnt1 = mergetrans(); |
643 | cnt2 = mergestates(1); |
644 | if (tl_verbose) |
645 | printf("/* >>%d,%d<< */\n", cnt1, cnt2); |
646 | } while (cnt2 > 0); |
647 | |
648 | #ifdef BUCKY |
649 | buckyballs(); |
650 | clr_reach(); |
651 | Dfs(b); |
652 | #endif |
653 | if (b && b->accepting) |
654 | fprintf(tl_out, "accept_init:\n"); |
655 | |
656 | if (!b && !never) |
657 | { fprintf(tl_out, " 0 /* false */;\n"); |
658 | } else |
659 | { printstate(b); /* init state must be first */ |
660 | for (b = never; b; b = b->nxt) |
661 | printstate(b); |
662 | } |
663 | if (hitsall) |
664 | fprintf(tl_out, "accept_all:\n skip\n"); |
665 | fprintf(tl_out, "}\n"); |
666 | } |