c3992a2fc554217b1af6f29d7004de30fe3467a3
1 /***** tl_spin: tl_trans.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. */
18 extern int tl_errs
, tl_verbose
, tl_terse
, newstates
;
20 int Stack_mx
=0, Max_Red
=0, Total
=0;
22 static Mapping
*Mapped
= (Mapping
*) 0;
23 static Graph
*Nodes_Set
= (Graph
*) 0;
24 static Graph
*Nodes_Stack
= (Graph
*) 0;
26 static char dumpbuf
[2048];
27 static int Red_cnt
= 0;
28 static int Lab_cnt
= 0;
30 static int Stack_sz
= 0;
32 static Graph
*findgraph(char *);
33 static Graph
*pop_stack(void);
34 static Node
*Duplicate(Node
*);
35 static Node
*flatten(Node
*);
36 static Symbol
*catSlist(Symbol
*, Symbol
*);
37 static Symbol
*dupSlist(Symbol
*);
38 static char *newname(void);
39 static int choueka(Graph
*, int);
40 static int not_new(Graph
*);
41 static int set_prefix(char *, int, Graph
*);
42 static void Addout(char *, char *);
43 static void fsm_trans(Graph
*, int, char *);
44 static void mkbuchi(void);
45 static void expand_g(Graph
*);
46 static void fixinit(Node
*);
47 static void liveness(Node
*);
48 static void mk_grn(Node
*);
49 static void mk_red(Node
*);
50 static void ng(Symbol
*, Symbol
*, Node
*, Node
*, Node
*);
51 static void push_stack(Graph
*);
52 static void sdump(Node
*);
59 for (n1
= g
->New
; n1
; n1
= n1
->nxt
)
60 { dump(n1
); printf(", "); }
62 for (n1
= g
->Old
; n1
; n1
= n1
->nxt
)
63 { dump(n1
); printf(", "); }
65 for (n1
= g
->Next
; n1
; n1
= n1
->nxt
)
66 { dump(n1
); printf(", "); }
67 printf("\n\tother:\t");
68 for (n1
= g
->Other
; n1
; n1
= n1
->nxt
)
69 { dump(n1
); printf(", "); }
82 printf("\nPush %s, from ", g
->name
->name
);
83 for (z
= g
->incoming
; z
; z
= z
->next
)
84 printf("%s, ", z
->name
);
88 if (Stack_sz
> Stack_mx
) Stack_mx
= Stack_sz
;
93 { Graph
*g
= Nodes_Stack
;
95 if (g
) Nodes_Stack
= g
->nxt
;
104 { static int cnt
= 0;
106 sprintf(buf
, "S%d", cnt
++);
111 has_clause(int tok
, Graph
*p
, Node
*n
)
116 return has_clause(tok
, p
, n
->lft
) &&
117 has_clause(tok
, p
, n
->rgt
);
119 return has_clause(tok
, p
, n
->lft
) ||
120 has_clause(tok
, p
, n
->rgt
);
123 for (q
= p
->Other
; q
; q
= q
->nxt
)
124 { qq
= right_linked(q
);
125 if (anywhere(tok
, n
, qq
))
137 for (p
= Nodes_Set
; p
; p
= p
->nxt
)
139 && has_clause(AND
, p
, n
))
140 { p
->isgrn
[p
->grncnt
++] =
141 (unsigned char) Red_cnt
;
145 if (n
->ntyp
== U_OPER
) /* 3.4.0 */
156 for (p
= Nodes_Set
; p
; p
= p
->nxt
)
158 && has_clause(0, p
, n
))
159 { if (p
->redcnt
>= 63)
160 Fatal("too many Untils", (char *)0);
161 p
->isred
[p
->redcnt
++] =
162 (unsigned char) Red_cnt
;
163 Lab_cnt
++; Max_Red
= Red_cnt
;
195 for (p
= Nodes_Set
; p
; p
= p
->nxt
)
196 if (!strcmp(p
->name
->name
, nm
))
198 for (m
= Mapped
; m
; m
= m
->nxt
)
199 if (strcmp(m
->from
, nm
) == 0)
202 printf("warning: node %s not found\n", nm
);
207 Addout(char *to
, char *from
)
208 { Graph
*p
= findgraph(from
);
212 s
= getsym(tl_lookup(to
));
213 s
->next
= p
->outgoing
;
226 return only_nxt(n
->rgt
) && only_nxt(n
->lft
);
234 dump_cond(Node
*pp
, Node
*r
, int first
)
238 if (!pp
) return frst
;
243 if (q
->ntyp
== PREDICATE
249 { if (!frst
) fprintf(tl_out
, " && ");
253 } else if (q
->ntyp
== OR
)
254 { if (!frst
) fprintf(tl_out
, " && ");
255 fprintf(tl_out
, "((");
256 frst
= dump_cond(q
->lft
, r
, 1);
259 fprintf(tl_out
, ") || (");
261 { if (only_nxt(q
->lft
))
262 { fprintf(tl_out
, "1))");
267 frst
= dump_cond(q
->rgt
, r
, 1);
270 { if (only_nxt(q
->rgt
))
271 fprintf(tl_out
, "1");
273 fprintf(tl_out
, "0");
277 fprintf(tl_out
, "))");
279 } else if (q
->ntyp
== V_OPER
280 && !anywhere(AND
, q
->rgt
, r
))
281 { frst
= dump_cond(q
->rgt
, r
, frst
);
282 } else if (q
->ntyp
== AND
)
284 frst
= dump_cond(q
->lft
, r
, frst
);
285 frst
= dump_cond(q
->rgt
, r
, frst
);
292 choueka(Graph
*p
, int count
)
293 { int j
, k
, incr_cnt
= 0;
295 for (j
= count
; j
<= Max_Red
; j
++) /* for each acceptance class */
298 /* is state p labeled Grn-j OR not Red-j ? */
300 for (k
= 0; k
< (int) p
->grncnt
; k
++)
301 if (p
->isgrn
[k
] == j
)
309 for (k
= 0; k
< (int) p
->redcnt
; k
++)
310 if (p
->isred
[k
] == j
)
323 set_prefix(char *pref
, int count
, Graph
*r2
)
324 { int incr_cnt
= 0; /* acceptance class 'count' */
328 sprintf(pref
, "accept"); /* new */
329 else if (count
>= Max_Red
)
330 sprintf(pref
, "T0"); /* cycle */
332 { incr_cnt
= choueka(r2
, count
+1);
333 if (incr_cnt
+ count
>= Max_Red
)
334 sprintf(pref
, "accept"); /* last hop */
336 sprintf(pref
, "T%d", count
+incr_cnt
);
342 fsm_trans(Graph
*p
, int count
, char *curnm
)
345 char prefix
[128], nwnm
[256];
348 addtrans(p
, curnm
, False
, "accept_all");
350 for (s
= p
->outgoing
; s
; s
= s
->next
)
351 { r
= findgraph(s
->name
);
354 { (void) set_prefix(prefix
, count
, r
);
355 sprintf(nwnm
, "%s_%s", prefix
, s
->name
);
357 strcpy(nwnm
, "accept_all");
360 { printf("maxred=%d, count=%d, curnm=%s, nwnm=%s ",
361 Max_Red
, count
, curnm
, nwnm
);
362 printf("(greencnt=%d,%d, redcnt=%d,%d)\n",
363 r
->grncnt
, r
->isgrn
[0],
364 r
->redcnt
, r
->isred
[0]);
366 addtrans(p
, curnm
, r
->Old
, nwnm
);
376 for (k
= 0; k
<= Max_Red
; k
++)
377 for (p
= Nodes_Set
; p
; p
= p
->nxt
)
381 && !strcmp(p
->name
->name
, "init")
386 && strcmp(p
->name
->name
, "init") != 0)
387 strcpy(curnm
, "accept_");
389 sprintf(curnm
, "T%d_", k
);
391 strcat(curnm
, p
->name
->name
);
393 fsm_trans(p
, k
, curnm
);
400 { Symbol
*p1
, *p2
, *p3
, *d
= ZS
;
402 for (p1
= s
; p1
; p1
= p1
->next
)
403 { for (p3
= d
; p3
; p3
= p3
->next
)
404 { if (!strcmp(p3
->name
, p1
->name
))
407 if (p3
) continue; /* a duplicate */
417 catSlist(Symbol
*a
, Symbol
*b
)
418 { Symbol
*p1
, *p2
, *p3
, *tmp
;
420 /* remove duplicates from b */
421 for (p1
= a
; p1
; p1
= p1
->next
)
423 for (p2
= b
; p2
; p2
= p2
->next
)
424 { if (strcmp(p1
->name
, p2
->name
))
441 /* find end of list */
442 for (p1
= a
; p1
->next
; p1
= p1
->next
)
451 Symbol
*q1
, *q2
= ZS
;
453 ng(tl_lookup("init"), ZS
, ZN
, ZN
, ZN
);
456 p1
->Other
= p1
->Old
= orig
;
459 for (g
= Nodes_Set
; g
; g
= g
->nxt
)
460 { for (q1
= g
->incoming
; q1
; q1
= q2
)
462 Addout(g
->name
->name
, q1
->name
);
471 { Node
*q
, *r
, *z
= ZN
;
473 for (q
= p
; q
; q
= q
->nxt
)
476 z
= tl_nn(AND
, r
, z
);
487 { Node
*n1
, *n2
, *lst
= ZN
, *d
= ZN
;
489 for (n1
= n
; n1
; n1
= n1
->nxt
)
501 ng(Symbol
*s
, Symbol
*in
, Node
*isnew
, Node
*isold
, Node
*next
)
502 { Graph
*g
= (Graph
*) tl_emalloc(sizeof(Graph
));
505 else g
->name
= tl_lookup(newname());
507 if (in
) g
->incoming
= dupSlist(in
);
508 if (isnew
) g
->New
= flatten(isnew
);
509 if (isold
) g
->Old
= Duplicate(isold
);
510 if (next
) g
->Next
= flatten(next
);
519 case PREDICATE
: strcat(dumpbuf
, n
->sym
->name
);
521 case U_OPER
: strcat(dumpbuf
, "U");
523 case V_OPER
: strcat(dumpbuf
, "V");
525 case OR
: strcat(dumpbuf
, "|");
527 case AND
: strcat(dumpbuf
, "&");
528 common2
: sdump(n
->rgt
);
529 common1
: sdump(n
->lft
);
532 case NEXT
: strcat(dumpbuf
, "X");
535 case NOT
: strcat(dumpbuf
, "!");
537 case TRUE
: strcat(dumpbuf
, "T");
539 case FALSE
: strcat(dumpbuf
, "F");
541 default: strcat(dumpbuf
, "?");
551 if (n
->ntyp
== PREDICATE
)
556 return tl_lookup(dumpbuf
);
561 { Graph
*q1
; Node
*tmp
, *n1
, *n2
;
564 tmp
= flatten(g
->Old
); /* duplicate, collapse, normalize */
565 g
->Other
= g
->Old
; /* non normalized full version */
568 g
->oldstring
= DoDump(g
->Old
);
570 tmp
= flatten(g
->Next
);
571 g
->nxtstring
= DoDump(tmp
);
573 if (tl_verbose
) dump_graph(g
);
575 Debug2("\tformula-old: [%s]\n", g
->oldstring
?g
->oldstring
->name
:"true");
576 Debug2("\tformula-nxt: [%s]\n", g
->nxtstring
?g
->nxtstring
->name
:"true");
577 for (q1
= Nodes_Set
; q1
; q1
= q1
->nxt
)
578 { Debug2(" compare old to: %s", q1
->name
->name
);
579 Debug2(" [%s]", q1
->oldstring
?q1
->oldstring
->name
:"true");
581 Debug2(" compare nxt to: %s", q1
->name
->name
);
582 Debug2(" [%s]", q1
->nxtstring
?q1
->nxtstring
->name
:"true");
584 if (q1
->oldstring
!= g
->oldstring
585 || q1
->nxtstring
!= g
->nxtstring
)
586 { Debug(" => different\n");
589 Debug(" => match\n");
592 q1
->incoming
= catSlist(g
->incoming
, q1
->incoming
);
594 /* check if there's anything in g->Other that needs
597 for (n2
= g
->Other
; n2
; n2
= n2
->nxt
)
598 { for (n1
= q1
->Other
; n1
; n1
= n1
->nxt
)
602 { Node
*n3
= dupnode(n2
);
603 /* don't mess up n2->nxt */
608 map
= (Mapping
*) tl_emalloc(sizeof(Mapping
));
609 map
->from
= g
->name
->name
;
614 for (n1
= g
->Other
; n1
; n1
= n2
)
618 for (n1
= g
->Old
; n1
; n1
= n2
)
622 for (n1
= g
->Next
; n1
; n1
= n2
)
629 if (newstates
) tl_verbose
=1;
630 Debug2(" New Node %s [", g
->name
->name
);
631 for (n1
= g
->Old
; n1
; n1
= n1
->nxt
)
632 { Dump(n1
); Debug(", "); }
633 Debug2("] nr %d\n", Base
);
634 if (newstates
) tl_verbose
=0;
645 { Node
*now
, *n1
, *n2
, *nx
;
649 { Debug2("\nDone with %s", g
->name
->name
);
650 if (tl_verbose
) dump_graph(g
);
652 { if (tl_verbose
) printf("\tIs Not New\n");
656 { Debug(" Has Next [");
657 for (n1
= g
->Next
; n1
; n1
= n1
->nxt
)
658 { Dump(n1
); Debug(", "); }
661 ng(ZS
, getsym(g
->name
), g
->Next
, ZN
, ZN
);
668 printf("\nExpand %s, from ", g
->name
->name
);
669 for (z
= g
->incoming
; z
; z
= z
->next
)
670 printf("%s, ", z
->name
);
671 printf("\n\thandle:\t"); Explain(g
->New
->ntyp
);
675 if (g
->New
->ntyp
== AND
)
680 n2
->nxt
= g
->New
->nxt
;
682 n1
= n2
= g
->New
->lft
;
685 n2
->nxt
= g
->New
->rgt
;
687 releasenode(0, g
->New
);
694 can_release
= 0; /* unless it need not go into Old */
696 g
->New
= g
->New
->nxt
;
699 if (now
->ntyp
!= TRUE
)
701 { for (n1
= g
->Old
; n1
->nxt
; n1
= n1
->nxt
)
702 if (isequal(now
, n1
))
721 if (can_release
) releasenode(1, now
);
725 Assert(now
->rgt
!= ZN
, now
->ntyp
);
726 Assert(now
->lft
!= ZN
, now
->ntyp
);
727 Assert(now
->rgt
->nxt
== ZN
, now
->ntyp
);
728 Assert(now
->lft
->nxt
== ZN
, now
->ntyp
);
735 nx
= getnode(now
); /* now also appears in Old */
739 n2
->nxt
= getnode(now
->rgt
);
740 n2
->nxt
->nxt
= g
->New
;
741 g
->New
= flatten(n2
);
743 ng(ZS
, g
->incoming
, n1
, g
->Old
, nx
);
747 Assert(now
->rgt
->nxt
== ZN
, now
->ntyp
);
748 Assert(now
->lft
->nxt
== ZN
, now
->ntyp
);
754 nx
= getnode(now
); /* now also appears in Old */
764 Assert(now
->lft
!= ZN
, now
->ntyp
);
765 nx
= dupnode(now
->lft
);
768 if (can_release
) releasenode(0, now
);
774 Assert(now
->rgt
->nxt
== ZN
, now
->ntyp
);
775 Assert(now
->lft
->nxt
== ZN
, now
->ntyp
);
784 ng(ZS
, g
->incoming
, n1
, g
->Old
, nx
);
785 g
->New
= flatten(n2
);
787 if (can_release
) releasenode(1, now
);
797 /* 1: ([]p1 && []p2) == [](p1 && p2) */
798 /* 2: (<>p1 || <>p2) == <>(p1 || p2) */
807 p
->lft
= twocases(p
->lft
);
808 p
->rgt
= twocases(p
->rgt
);
814 p
->lft
= twocases(p
->lft
);
820 if (p
->ntyp
== AND
/* 1 */
821 && p
->lft
->ntyp
== V_OPER
822 && p
->lft
->lft
->ntyp
== FALSE
823 && p
->rgt
->ntyp
== V_OPER
824 && p
->rgt
->lft
->ntyp
== FALSE
)
825 { q
= tl_nn(V_OPER
, False
,
826 tl_nn(AND
, p
->lft
->rgt
, p
->rgt
->rgt
));
828 if (p
->ntyp
== OR
/* 2 */
829 && p
->lft
->ntyp
== U_OPER
830 && p
->lft
->lft
->ntyp
== TRUE
831 && p
->rgt
->ntyp
== U_OPER
832 && p
->rgt
->lft
->ntyp
== TRUE
)
833 { q
= tl_nn(U_OPER
, True
,
834 tl_nn(OR
, p
->lft
->rgt
, p
->rgt
->rgt
));
845 if (!p
|| tl_errs
) return;
849 if (tl_verbose
|| tl_terse
)
850 { fprintf(tl_out
, "\t/* Normlzd: ");
852 fprintf(tl_out
, " */\n");
859 ng(ZS
, getsym(tl_lookup("init")), p
, ZN
, ZN
);
860 while ((g
= Nodes_Stack
) != (Graph
*) 0)
861 { Nodes_Stack
= g
->nxt
;
868 liveness(flatten(op
)); /* was: liveness(op); */
873 printf(" * %d states in Streett automaton\n", Base
);
874 printf(" * %d Streett acceptance conditions\n", Max_Red
);
875 printf(" * %d Buchi states\n", Total
);
This page took 0.046359 seconds and 3 git commands to generate.