projects / lttv.git / blob
? search:
summary | shortlog | log | commit | commitdiff | tree
blame | history | raw | HEAD
convert from svn repository: remove tags directory
[lttv.git] / trunk / verif / Spin / Src5.1.6 / tl_buchi.c
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 }
LTTng 2.x Viewer (LTTV)
This page took 0.04504 seconds and 4 git commands to generate.