convert from svn repository: remove tags directory
[lttv.git] / trunk / verif / Spin / Src5.1.6 / tl_buchi.c
CommitLineData
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
17extern int tl_verbose, tl_clutter, Total, Max_Red;
18
19FILE *tl_out; /* if standalone: = stdout; */
20
21typedef struct Transition {
22 Symbol *name;
23 Node *cond;
24 int redundant, merged, marked;
25 struct Transition *nxt;
26} Transition;
27
28typedef 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
38static State *never = (State *) 0;
39static int hitsall;
40
41static int
42sametrans(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
49static Node *
50Prune(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
87static State *
88findstate(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
109static void
110Dfs(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
129void
130retarget(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
148static Node *
149nonxt(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
178static Node *
179combination(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
205Node *
206unclutter(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
259static void
260clutter(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
276static void
277showtrans(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
287static int
288mergetrans(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
329static int
330all_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;
363done:
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
374static int
375all_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;
429done:
430 for (s = b->trans; s; s = s->nxt)
431 s->marked = 0;
432 return result;
433}
434
435static int
436buckyballs(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
485static int
486mergestates(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
539static int tcnt;
540
541static void
542rev_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
555static void
556printstate(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
581void
582addtrans(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
613static void
614clr_reach(void)
615{ State *p;
616 for (p = never; p; p = p->nxt)
617 p->reachable = 0;
618 hitsall = 0;
619}
620
621void
622fsm_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}
This page took 0.045914 seconds and 4 git commands to generate.