1 /***** tl_spin: tl_buchi.c *****/
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 */
12 /* Based on the translation algorithm by Gerth, Peled, Vardi, and Wolper, */
13 /* presented at the PSTV Conference, held in 1995, Warsaw, Poland 1995. */
17 extern int tl_verbose
, tl_clutter
, Total
, Max_Red
;
19 FILE *tl_out
; /* if standalone: = stdout; */
21 typedef struct Transition
{
24 int redundant
, merged
, marked
;
25 struct Transition
*nxt
;
28 typedef struct State
{
32 unsigned char redundant
;
33 unsigned char accepting
;
34 unsigned char reachable
;
38 static State
*never
= (State
*) 0;
42 sametrans(Transition
*s
, Transition
*t
)
44 if (strcmp(s
->name
->name
, t
->name
->name
) != 0)
46 return isequal(s
->cond
, t
->cond
);
63 p
->lft
= Prune(p
->lft
);
65 { releasenode(1, p
->rgt
);
68 p
->rgt
= Prune(p
->rgt
);
70 { releasenode(1, p
->lft
);
75 p
->lft
= Prune(p
->lft
);
78 p
->rgt
= Prune(p
->rgt
);
90 for (b
= never
; b
; b
= b
->nxt
)
91 if (!strcmp(b
->name
->name
, nm
))
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
++)
100 Fatal("name too long %s", nm
);
101 sprintf(altnm
, "accept%s", &nm
[i
]);
102 return findstate(altnm
);
104 /* Fatal("buchi: no state %s", nm); */
113 if (!b
|| b
->reachable
) return;
117 printf("/* redundant state %s */\n",
119 for (t
= b
->trans
; t
; t
= t
->nxt
)
121 { Dfs(findstate(t
->name
->name
));
123 && strcmp(t
->name
->name
, "accept_all") == 0)
130 retarget(char *from
, char *to
)
133 Symbol
*To
= tl_lookup(to
);
135 if (tl_verbose
) printf("replace %s with %s\n", from
, to
);
137 for (b
= never
; b
; b
= b
->nxt
)
138 { if (!strcmp(b
->name
->name
, from
))
141 for (t
= b
->trans
; t
; t
= t
->nxt
)
142 { if (!strcmp(t
->name
->name
, from
))
157 n
->lft
= nonxt(n
->lft
);
158 n
->rgt
= nonxt(n
->rgt
);
159 if (!n
->lft
|| !n
->rgt
)
163 n
->lft
= nonxt(n
->lft
);
164 n
->rgt
= nonxt(n
->rgt
);
179 combination(Node
*s
, Node
*t
)
186 { printf("\tnonxtA: "); dump(a
);
187 printf("\n\tnonxtB: "); dump(b
);
190 /* if there's only a X(f), its equivalent to true */
194 nc
= tl_nn(OR
, a
, b
);
196 nc
= tl_nn(OR
, s
, t
);
199 { printf("\tcombo: "); dump(nc
);
206 unclutter(Node
*n
, char *snm
)
207 { Node
*t
, *s
, *v
, *u
;
210 /* check only simple cases like !q && q */
211 for (t
= n
; t
; t
= t
->rgt
)
213 { if (t
->ntyp
!= AND
|| !t
->lft
)
215 if (t
->lft
->ntyp
!= PREDICATE
217 && t
->lft
->ntyp
!= NEXT
219 && t
->lft
->ntyp
!= NOT
)
222 { if (t
->ntyp
!= PREDICATE
231 for (t
= n
; t
; t
= t
->rgt
)
237 && v
->lft
->ntyp
== PREDICATE
)
239 for (s
= n
; s
; s
= s
->rgt
)
240 { if (s
== t
) continue;
245 if (u
->ntyp
== PREDICATE
246 && strcmp(u
->sym
->name
, w
->name
) == 0)
248 { printf("BINGO %s:\t", snm
);
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
);
268 && s
->cond
->ntyp
== FALSE
)
280 for (s
= a
->trans
; s
; s
= s
->nxt
)
281 { printf("%s ", s
->name
?s
->name
->name
:"-");
283 printf(" %d %d %d\n", s
->redundant
, s
->merged
, s
->marked
);
291 Node
*nc
; int cnt
= 0;
293 for (b
= never
; b
; b
= b
->nxt
)
294 { if (!b
->reachable
) continue;
296 for (s
= b
->trans
; s
; s
= s
->nxt
)
297 { if (s
->redundant
) continue;
299 for (t
= s
->nxt
; t
; t
= t
->nxt
)
301 && !strcmp(s
->name
->name
, t
->name
->name
))
303 { printf("===\nstate %s, trans to %s redundant\n",
304 b
->name
->name
, s
->name
->name
);
306 printf(" conditions ");
307 dump(s
->cond
); printf(" <-> ");
308 dump(t
->cond
); printf("\n");
311 if (!s
->cond
) /* same as T */
312 { releasenode(1, t
->cond
); /* T or t */
315 { releasenode(1, s
->cond
);
318 { nc
= combination(s
->cond
, t
->cond
);
320 t
->cond
= rewrite(nc
);
330 all_trans_match(State
*a
, State
*b
)
332 int found
, result
= 0;
334 if (a
->accepting
!= b
->accepting
)
337 for (s
= a
->trans
; s
; s
= s
->nxt
)
338 { if (s
->redundant
) continue;
340 for (t
= b
->trans
; t
; t
= t
->nxt
)
341 { if (t
->redundant
) continue;
350 for (s
= b
->trans
; s
; s
= s
->nxt
)
351 { if (s
->redundant
|| s
->marked
) continue;
353 for (t
= a
->trans
; t
; t
= t
->nxt
)
354 { if (t
->redundant
) continue;
364 for (s
= b
->trans
; s
; s
= s
->nxt
)
375 all_bucky(State
*a
, State
*b
)
377 int found
, result
= 0;
379 for (s
= a
->trans
; s
; s
= s
->nxt
)
380 { if (s
->redundant
) continue;
382 for (t
= b
->trans
; t
; t
= t
->nxt
)
383 { if (t
->redundant
) continue;
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 */
392 if (strcmp(s
->name
->name
, t
->name
->name
) == 0
393 && strcmp(s
->name
->name
, "accept_all") == 0)
397 /* same exit from which there is no return */
404 for (s
= b
->trans
; s
; s
= s
->nxt
)
405 { if (s
->redundant
|| s
->marked
) continue;
407 for (t
= a
->trans
; t
; t
= t
->nxt
)
408 { if (t
->redundant
) continue;
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)
417 if (strcmp(s
->name
->name
, t
->name
->name
) == 0
418 && strcmp(s
->name
->name
, "accept_all") == 0)
430 for (s
= b
->trans
; s
; s
= s
->nxt
)
437 { State
*a
, *b
, *c
, *d
;
442 for (a
= never
; a
; a
= a
->nxt
)
443 { if (!a
->reachable
) continue;
445 if (a
->redundant
) continue;
447 for (b
= a
->nxt
; b
; b
= b
->nxt
)
448 { if (!b
->reachable
) continue;
450 if (b
->redundant
) continue;
455 { printf("%s bucky match %s\n",
456 a
->name
->name
, b
->name
->name
);
459 if (a
->accepting
&& !b
->accepting
)
460 { if (strcmp(b
->name
->name
, "T0_init") == 0)
470 retarget(c
->name
->name
, d
->name
->name
);
471 if (!strncmp(c
->name
->name
, "accept", 6)
474 sprintf(buf
, "T0%s", &(c
->name
->name
[6]));
475 retarget(buf
, d
->name
->name
);
480 } while (m
&& cnt
< 10);
495 for (a
= never
; a
; a
= a
->nxt
)
496 { if (v
&& !a
->reachable
) continue;
498 if (a
->redundant
) continue; /* 3.3.10 */
500 for (b
= a
->nxt
; b
; b
= b
->nxt
)
501 { if (v
&& !b
->reachable
) continue;
503 if (b
->redundant
) continue; /* 3.3.10 */
505 if (all_trans_match(a
, b
))
508 { printf("%d: state %s equals state %s\n",
509 cnt
, a
->name
->name
, b
->name
->name
);
514 retarget(a
->name
->name
, b
->name
->name
);
515 if (!strncmp(a
->name
->name
, "accept", 6)
518 sprintf(buf
, "T0%s", &(a
->name
->name
[6]));
519 retarget(buf
, b
->name
->name
);
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
);
535 } while (m
&& cnt
< 10);
542 rev_trans(Transition
*t
) /* print transitions in reverse order... */
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
);
558 if (!b
|| (!tl_verbose
&& !b
->reachable
)) return;
560 b
->reachable
= 0; /* print only once */
561 fprintf(tl_out
, "%s:\n", b
->name
->name
);
564 { fprintf(tl_out
, " /* ");
565 dump(b
->colors
->Other
);
566 fprintf(tl_out
, " */\n");
569 if (strncmp(b
->name
->name
, "accept", 6) == 0
571 fprintf(tl_out
, "T0%s:\n", &(b
->name
->name
[6]));
573 fprintf(tl_out
, "\tif\n");
576 if (!tcnt
) fprintf(tl_out
, "\t:: false\n");
577 fprintf(tl_out
, "\tfi;\n");
582 addtrans(Graph
*col
, char *from
, Node
*op
, char *to
)
586 t
= (Transition
*) tl_emalloc(sizeof(Transition
));
587 t
->name
= tl_lookup(to
);
588 t
->cond
= Prune(dupnode(op
));
591 { printf("\n%s <<\t", from
); dump(op
);
592 printf("\n\t"); dump(t
->cond
);
593 printf(">> %s\n", t
->name
->name
);
595 if (t
->cond
) t
->cond
= rewrite(t
->cond
);
597 for (b
= never
; b
; b
= b
->nxt
)
598 if (!strcmp(b
->name
->name
, from
))
603 b
= (State
*) tl_emalloc(sizeof(State
));
604 b
->name
= tl_lookup(from
);
607 if (!strncmp(from
, "accept", 6))
616 for (p
= never
; p
; p
= p
->nxt
)
623 { State
*b
; int cnt1
, cnt2
=0;
624 extern void put_uform(void);
626 if (tl_clutter
) clutter();
628 b
= findstate("T0_init");
629 if (b
&& (Max_Red
== 0))
633 b
= findstate("T0_init");
635 fprintf(tl_out
, "never { /* ");
637 fprintf(tl_out
, " */\n");
643 cnt2
= mergestates(1);
645 printf("/* >>%d,%d<< */\n", cnt1
, cnt2
);
653 if (b
&& b
->accepting
)
654 fprintf(tl_out
, "accept_init:\n");
657 { fprintf(tl_out
, " 0 /* false */;\n");
659 { printstate(b
); /* init state must be first */
660 for (b
= never
; b
; b
= b
->nxt
)
664 fprintf(tl_out
, "accept_all:\n skip\n");
665 fprintf(tl_out
, "}\n");
This page took 0.069367 seconds and 4 git commands to generate.