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