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