1 /***** ltl2ba : buchi.c *****/
2 
3 /* Written by Denis Oddoux, LIAFA, France                                 */
4 /* Copyright (c) 2001  Denis Oddoux                                       */
5 /* Modified by Paul Gastin, LSV, France                                   */
6 /* Copyright (c) 2007  Paul Gastin                                        */
7 /*                                                                        */
8 /* This program is free software; you can redistribute it and/or modify   */
9 /* it under the terms of the GNU General Public License as published by   */
10 /* the Free Software Foundation; either version 2 of the License, or      */
11 /* (at your option) any later version.                                    */
12 /*                                                                        */
13 /* This program is distributed in the hope that it will be useful,        */
14 /* but WITHOUT ANY WARRANTY; without even the implied warranty of         */
15 /* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the          */
16 /* GNU General Public License for more details.                           */
17 /*                                                                        */
18 /* You should have received a copy of the GNU General Public License      */
19 /* along with this program; if not, write to the Free Software            */
20 /* Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA*/
21 /*                                                                        */
22 /* Based on the translation algorithm by Gastin and Oddoux,               */
23 /* presented at the 13th International Conference on Computer Aided       */
24 /* Verification, CAV 2001, Paris, France.                                 */
25 /* Proceedings - LNCS 2102, pp. 53-65                                     */
26 /*                                                                        */
27 /* Send bug-reports and/or questions to Paul Gastin                       */
28 /* http://www.lsv.ens-cachan.fr/~gastin                                   */
29 
30 #include "ltl2ba.h"
31 
32 /********************************************************************\
33 |*              Structures and shared variables                     *|
34 \********************************************************************/
35 
36 extern GState **init, *gstates;
37 extern struct rusage tr_debut, tr_fin;
38 extern struct timeval t_diff;
39 extern int tl_verbose, tl_stats, tl_simp_diff, tl_simp_fly, tl_simp_scc,
40   init_size, *final;
41 
42 extern int gstate_id;
43 
44 extern FILE *tl_out;
45 BState *bstack, *bstates, *bremoved;
46 static BScc *scc_stack;
47 int accept, bstate_count = 0, btrans_count = 0;
48 static int rank;
49 
50 /********************************************************************\
51 |*        Simplification of the generalized Buchi automaton         *|
52 \********************************************************************/
53 
free_bstate(BState * s)54 void free_bstate(BState *s) /* frees a state and its transitions */
55 {
56   free_btrans(s->trans->nxt, s->trans, 1);
57   tfree(s);
58 }
59 
remove_bstate(BState * s,BState * s1)60 BState *remove_bstate(BState *s, BState *s1) /* removes a state */
61 {
62   BState *prv = s->prv;
63   s->prv->nxt = s->nxt;
64   s->nxt->prv = s->prv;
65   free_btrans(s->trans->nxt, s->trans, 0);
66   s->trans = (BTrans *)0;
67   s->nxt = bremoved->nxt;
68   bremoved->nxt = s;
69   s->prv = s1;
70   for(s1 = bremoved->nxt; s1 != bremoved; s1 = s1->nxt)
71     if(s1->prv == s)
72       s1->prv = s->prv;
73   return prv;
74 }
75 
copy_btrans(BTrans * from,BTrans * to)76 void copy_btrans(BTrans *from, BTrans *to) {
77   to->to    = from->to;
78   copy_set(from->pos, to->pos, 1);
79   copy_set(from->neg, to->neg, 1);
80 }
81 
simplify_btrans()82 int simplify_btrans() /* simplifies the transitions */
83 {
84   BState *s;
85   BTrans *t, *t1;
86   int changed = 0;
87 
88   if(tl_stats) getrusage(RUSAGE_SELF, &tr_debut);
89 
90   for (s = bstates->nxt; s != bstates; s = s->nxt)
91     for (t = s->trans->nxt; t != s->trans;) {
92       t1 = s->trans->nxt;
93       copy_btrans(t, s->trans);
94       while((t == t1) || (t->to != t1->to) ||
95             !included_set(t1->pos, t->pos, 1) ||
96             !included_set(t1->neg, t->neg, 1))
97         t1 = t1->nxt;
98       if(t1 != s->trans) {
99         BTrans *free = t->nxt;
100         t->to    = free->to;
101         copy_set(free->pos, t->pos, 1);
102         copy_set(free->neg, t->neg, 1);
103         t->nxt   = free->nxt;
104         if(free == s->trans) s->trans = t;
105         free_btrans(free, 0, 0);
106         changed++;
107       }
108       else
109         t = t->nxt;
110     }
111 
112   if(tl_stats) {
113     getrusage(RUSAGE_SELF, &tr_fin);
114     timeval_subtract (&t_diff, &tr_fin.ru_utime, &tr_debut.ru_utime);
115     fprintf(tl_out, "\nSimplification of the Buchi automaton - transitions: %ld.%06lis",
116 		t_diff.tv_sec, t_diff.tv_usec);
117     fprintf(tl_out, "\n%i transitions removed\n", changed);
118 
119   }
120   return changed;
121 }
122 
same_btrans(BTrans * s,BTrans * t)123 int same_btrans(BTrans *s, BTrans *t) /* returns 1 if the transitions are identical */
124 {
125   return((s->to == t->to) &&
126 	 same_sets(s->pos, t->pos, 1) &&
127 	 same_sets(s->neg, t->neg, 1));
128 }
129 
remove_btrans(BState * to)130 void remove_btrans(BState *to)
131 {             /* redirects transitions before removing a state from the automaton */
132   BState *s;
133   BTrans *t;
134   for (s = bstates->nxt; s != bstates; s = s->nxt)
135     for (t = s->trans->nxt; t != s->trans; t = t->nxt)
136       if (t->to == to) { /* transition to a state with no transitions */
137 	BTrans *free = t->nxt;
138 	t->to = free->to;
139 	copy_set(free->pos, t->pos, 1);
140 	copy_set(free->neg, t->neg, 1);
141 	t->nxt   = free->nxt;
142 	if(free == s->trans) s->trans = t;
143 	free_btrans(free, 0, 0);
144       }
145 }
146 
retarget_all_btrans()147 void retarget_all_btrans()
148 {             /* redirects transitions before removing a state from the automaton */
149   BState *s;
150   BTrans *t;
151   for (s = bstates->nxt; s != bstates; s = s->nxt)
152     for (t = s->trans->nxt; t != s->trans; t = t->nxt)
153       if (!t->to->trans) { /* t->to has been removed */
154 	t->to = t->to->prv;
155 	if(!t->to) { /* t->to has no transitions */
156 	  BTrans *free = t->nxt;
157 	  t->to = free->to;
158 	  copy_set(free->pos, t->pos, 1);
159 	  copy_set(free->neg, t->neg, 1);
160 	  t->nxt   = free->nxt;
161 	  if(free == s->trans) s->trans = t;
162 	  free_btrans(free, 0, 0);
163 	}
164       }
165   while(bremoved->nxt != bremoved) { /* clean the 'removed' list */
166     s = bremoved->nxt;
167     bremoved->nxt = bremoved->nxt->nxt;
168     tfree(s);
169   }
170 }
171 
all_btrans_match(BState * a,BState * b)172 int all_btrans_match(BState *a, BState *b) /* decides if the states are equivalent */
173 {
174   BTrans *s, *t;
175 
176   /* the states have to be both final or both non final,
177    * or at least one of them has to be in a trivial SCC
178    * (incoming == -1), as the acceptance condition of
179    * such a state can be modified without changing the
180    * language of the automaton
181    */
182   if (((a->final == accept) || (b->final == accept)) &&
183       (a->final + b->final != 2 * accept)  /* final condition of a and b differs */
184       && a->incoming >=0   /* a is not in a trivial SCC */
185       && b->incoming >=0)  /* b is not in a trivial SCC */
186     return 0;  /* states can not be matched */
187 
188   for (s = a->trans->nxt; s != a->trans; s = s->nxt) {
189                                 /* all transitions from a appear in b */
190     copy_btrans(s, b->trans);
191     t = b->trans->nxt;
192     while(!same_btrans(s, t))
193       t = t->nxt;
194     if(t == b->trans) return 0;
195   }
196   for (s = b->trans->nxt; s != b->trans; s = s->nxt) {
197                                 /* all transitions from b appear in a */
198     copy_btrans(s, a->trans);
199     t = a->trans->nxt;
200     while(!same_btrans(s, t))
201       t = t->nxt;
202     if(t == a->trans) return 0;
203   }
204   return 1;
205 }
206 
simplify_bstates()207 int simplify_bstates() /* eliminates redundant states */
208 {
209   BState *s, *s1, *s2;
210   int changed = 0;
211 
212   if(tl_stats) getrusage(RUSAGE_SELF, &tr_debut);
213 
214   for (s = bstates->nxt; s != bstates; s = s->nxt) {
215     if(s->trans == s->trans->nxt) { /* s has no transitions */
216       s = remove_bstate(s, (BState *)0);
217       changed++;
218       continue;
219     }
220     bstates->trans = s->trans;
221     bstates->final = s->final;
222     s1 = s->nxt;
223     while(!all_btrans_match(s, s1))
224       s1 = s1->nxt;
225     if(s1 != bstates) { /* s and s1 are equivalent */
226       /* we now want to remove s and replace it by s1 */
227       if(s1->incoming == -1) {  /* s1 is in a trivial SCC */
228         s1->final = s->final; /* change the final condition of s1 to that of s */
229 
230         /* We may have to update the SCC status of s1
231          * stored in s1->incoming, because we will retarget the incoming
232          * transitions of s to s1.
233          *
234          * If both s1 and s are in trivial SCC, then retargeting
235          * the incoming transitions does not change the status of s1,
236          * it remains in a trivial SCC.
237          *
238          * If s1 was in a trivial SCC, but s was not, then
239          * s1 has to have a transition to s that corresponds to a
240          * self-loop of s (as both states have the same outgoing transitions).
241          * But then, s1 will not remain a trivial SCC after retargeting.
242          * In particular, afterwards the final condition of s1 may not be
243          * changed anymore.
244          *
245          * If both s1 and s are in non-trivial SCC, merging does not
246          * change the SCC status of s1.
247          *
248          * If we are here, s1->incoming==1 and thus s1 forms a trivial SCC.
249          * We therefore can set the status of s1 to that of s,
250          * which correctly handles the first two cases above.
251          */
252         s1->incoming = s->incoming;
253       }
254       s = remove_bstate(s, s1);
255       changed++;
256     }
257   }
258   retarget_all_btrans();
259 
260   /*
261    * As merging equivalent states can change the 'final' attribute of
262    * the remaining state, it is possible that now there are two
263    * different states with the same id and final values.
264    * This would lead to multiply-defined labels in the generated neverclaim.
265    * We iterate over all states and assign new ids (previously unassigned)
266    * to these states to disambiguate.
267    * Fix from ltl3ba.
268    */
269   for (s = bstates->nxt; s != bstates; s = s->nxt) {  /* For all states s*/
270     for (s2 = s->nxt; s2 != bstates; s2 = s2->nxt) {  /*  and states s2 to the right of s */
271       if(s->final == s2->final && s->id == s2->id) {  /* if final and id match */
272         s->id = ++gstate_id;                          /* disambiguate by assigning unused id */
273       }
274     }
275   }
276 
277   if(tl_stats) {
278     getrusage(RUSAGE_SELF, &tr_fin);
279     timeval_subtract (&t_diff, &tr_fin.ru_utime, &tr_debut.ru_utime);
280     fprintf(tl_out, "\nSimplification of the Buchi automaton - states: %ld.%06lis",
281 		t_diff.tv_sec, t_diff.tv_usec);
282     fprintf(tl_out, "\n%i states removed\n", changed);
283   }
284 
285   return changed;
286 }
287 
bdfs(BState * s)288 int bdfs(BState *s) {
289   BTrans *t;
290   BScc *c;
291   BScc *scc = (BScc *)tl_emalloc(sizeof(BScc));
292   scc->bstate = s;
293   scc->rank = rank;
294   scc->theta = rank++;
295   scc->nxt = scc_stack;
296   scc_stack = scc;
297 
298   s->incoming = 1;
299 
300   for (t = s->trans->nxt; t != s->trans; t = t->nxt) {
301     if (t->to->incoming == 0) {
302       int result = bdfs(t->to);
303       scc->theta = min(scc->theta, result);
304     }
305     else {
306       for(c = scc_stack->nxt; c != 0; c = c->nxt)
307 	if(c->bstate == t->to) {
308 	  scc->theta = min(scc->theta, c->rank);
309 	  break;
310 	}
311     }
312   }
313   if(scc->rank == scc->theta) {
314     if(scc_stack == scc) { /* s is alone in a scc */
315       s->incoming = -1;
316       for (t = s->trans->nxt; t != s->trans; t = t->nxt)
317 	if (t->to == s)
318 	  s->incoming = 1;
319     }
320     scc_stack = scc->nxt;
321   }
322   return scc->theta;
323 }
324 
simplify_bscc()325 void simplify_bscc() {
326   BState *s;
327   rank = 1;
328   scc_stack = 0;
329 
330   if(bstates == bstates->nxt) return;
331 
332   for(s = bstates->nxt; s != bstates; s = s->nxt)
333     s->incoming = 0; /* state color = white */
334 
335   bdfs(bstates->prv);
336 
337   for(s = bstates->nxt; s != bstates; s = s->nxt)
338     if(s->incoming == 0)
339       remove_bstate(s, 0);
340 }
341 
342 
343 
344 
345 /********************************************************************\
346 |*              Generation of the Buchi automaton                   *|
347 \********************************************************************/
348 
find_bstate(GState ** state,int final,BState * s)349 BState *find_bstate(GState **state, int final, BState *s)
350 {                       /* finds the corresponding state, or creates it */
351   if((s->gstate == *state) && (s->final == final)) return s; /* same state */
352 
353   s = bstack->nxt; /* in the stack */
354   bstack->gstate = *state;
355   bstack->final = final;
356   while(!(s->gstate == *state) || !(s->final == final))
357     s = s->nxt;
358   if(s != bstack) return s;
359 
360   s = bstates->nxt; /* in the solved states */
361   bstates->gstate = *state;
362   bstates->final = final;
363   while(!(s->gstate == *state) || !(s->final == final))
364     s = s->nxt;
365   if(s != bstates) return s;
366 
367   s = bremoved->nxt; /* in the removed states */
368   bremoved->gstate = *state;
369   bremoved->final = final;
370   while(!(s->gstate == *state) || !(s->final == final))
371     s = s->nxt;
372   if(s != bremoved) return s;
373 
374   s = (BState *)tl_emalloc(sizeof(BState)); /* creates a new state */
375   s->gstate = *state;
376   s->id = (*state)->id;
377   s->incoming = 0;
378   s->final = final;
379   s->trans = emalloc_btrans(); /* sentinel */
380   s->trans->nxt = s->trans;
381   s->nxt = bstack->nxt;
382   bstack->nxt = s;
383   return s;
384 }
385 
next_final(int * set,int fin)386 int next_final(int *set, int fin) /* computes the 'final' value */
387 {
388   if((fin != accept) && in_set(set, final[fin + 1]))
389     return next_final(set, fin + 1);
390   return fin;
391 }
392 
make_btrans(BState * s)393 void make_btrans(BState *s) /* creates all the transitions from a state */
394 {
395   int state_trans = 0;
396   GTrans *t;
397   BTrans *t1;
398   BState *s1;
399   if(s->gstate->trans)
400     for(t = s->gstate->trans->nxt; t != s->gstate->trans; t = t->nxt) {
401       int fin = next_final(t->final, (s->final == accept) ? 0 : s->final);
402       BState *to = find_bstate(&t->to, fin, s);
403 
404       for(t1 = s->trans->nxt; t1 != s->trans;) {
405 	if(tl_simp_fly &&
406 	   (to == t1->to) &&
407 	   included_set(t->pos, t1->pos, 1) &&
408 	   included_set(t->neg, t1->neg, 1)) { /* t1 is redondant */
409 	  BTrans *free = t1->nxt;
410 	  t1->to->incoming--;
411 	  t1->to = free->to;
412 	  copy_set(free->pos, t1->pos, 1);
413 	  copy_set(free->neg, t1->neg, 1);
414 	  t1->nxt   = free->nxt;
415 	  if(free == s->trans) s->trans = t1;
416 	  free_btrans(free, 0, 0);
417 	  state_trans--;
418 	}
419 	else if(tl_simp_fly &&
420 		(t1->to == to ) &&
421 		included_set(t1->pos, t->pos, 1) &&
422 		included_set(t1->neg, t->neg, 1)) /* t is redondant */
423 	  break;
424 	else
425 	  t1 = t1->nxt;
426       }
427       if(t1 == s->trans) {
428 	BTrans *trans = emalloc_btrans();
429 	trans->to = to;
430 	trans->to->incoming++;
431 	copy_set(t->pos, trans->pos, 1);
432 	copy_set(t->neg, trans->neg, 1);
433 	trans->nxt = s->trans->nxt;
434 	s->trans->nxt = trans;
435 	state_trans++;
436       }
437     }
438 
439   if(tl_simp_fly) {
440     if(s->trans == s->trans->nxt) { /* s has no transitions */
441       free_btrans(s->trans->nxt, s->trans, 1);
442       s->trans = (BTrans *)0;
443       s->prv = (BState *)0;
444       s->nxt = bremoved->nxt;
445       bremoved->nxt = s;
446       for(s1 = bremoved->nxt; s1 != bremoved; s1 = s1->nxt)
447 	if(s1->prv == s)
448 	  s1->prv = (BState *)0;
449       return;
450     }
451     bstates->trans = s->trans;
452     bstates->final = s->final;
453     s1 = bstates->nxt;
454     while(!all_btrans_match(s, s1))
455       s1 = s1->nxt;
456     if(s1 != bstates) { /* s and s1 are equivalent */
457       free_btrans(s->trans->nxt, s->trans, 1);
458       s->trans = (BTrans *)0;
459       s->prv = s1;
460       s->nxt = bremoved->nxt;
461       bremoved->nxt = s;
462       for(s1 = bremoved->nxt; s1 != bremoved; s1 = s1->nxt)
463 	if(s1->prv == s)
464 	  s1->prv = s->prv;
465       return;
466     }
467   }
468   s->nxt = bstates->nxt; /* adds the current state to 'bstates' */
469   s->prv = bstates;
470   s->nxt->prv = s;
471   bstates->nxt = s;
472   btrans_count += state_trans;
473   bstate_count++;
474 }
475 
476 /********************************************************************\
477 |*                  Display of the Buchi automaton                  *|
478 \********************************************************************/
479 
print_buchi(BState * s)480 void print_buchi(BState *s) /* dumps the Buchi automaton */
481 {
482   BTrans *t;
483   if(s == bstates) return;
484 
485   print_buchi(s->nxt); /* begins with the last state */
486 
487   fprintf(tl_out, "state ");
488   if(s->id == -1)
489     fprintf(tl_out, "init");
490   else {
491     if(s->final == accept)
492       fprintf(tl_out, "accept");
493     else
494       fprintf(tl_out, "T%i", s->final);
495     fprintf(tl_out, "_%i", s->id);
496   }
497   fprintf(tl_out, "\n");
498   for(t = s->trans->nxt; t != s->trans; t = t->nxt) {
499     if (empty_set(t->pos, 1) && empty_set(t->neg, 1))
500       fprintf(tl_out, "1");
501     print_set(t->pos, 1);
502     if (!empty_set(t->pos, 1) && !empty_set(t->neg, 1)) fprintf(tl_out, " & ");
503     print_set(t->neg, 2);
504     fprintf(tl_out, " -> ");
505     if(t->to->id == -1)
506       fprintf(tl_out, "init\n");
507     else {
508       if(t->to->final == accept)
509 	fprintf(tl_out, "accept");
510       else
511 	fprintf(tl_out, "T%i", t->to->final);
512       fprintf(tl_out, "_%i\n", t->to->id);
513     }
514   }
515 }
516 
print_spin_buchi()517 void print_spin_buchi() {
518   BTrans *t;
519   BState *s;
520   int accept_all = 0;
521   if(bstates->nxt == bstates) { /* empty automaton */
522     fprintf(tl_out, "never {    /* ");
523     put_uform();
524     fprintf(tl_out, " */\n");
525     fprintf(tl_out, "T0_init:\n");
526     fprintf(tl_out, "\tfalse;\n");
527     fprintf(tl_out, "}\n");
528     return;
529   }
530   if(bstates->nxt->nxt == bstates && bstates->nxt->id == 0) { /* true */
531     fprintf(tl_out, "never {    /* ");
532     put_uform();
533     fprintf(tl_out, " */\n");
534     fprintf(tl_out, "accept_init:\n");
535     fprintf(tl_out, "\tif\n");
536     fprintf(tl_out, "\t:: (1) -> goto accept_init\n");
537     fprintf(tl_out, "\tfi;\n");
538     fprintf(tl_out, "}\n");
539     return;
540   }
541 
542   fprintf(tl_out, "never { /* ");
543   put_uform();
544   fprintf(tl_out, " */\n");
545   for(s = bstates->prv; s != bstates; s = s->prv) {
546     if(s->id == 0) { /* accept_all at the end */
547       accept_all = 1;
548       continue;
549     }
550     if(s->final == accept)
551       fprintf(tl_out, "accept_");
552     else fprintf(tl_out, "T%i_", s->final);
553     if(s->id == -1)
554       fprintf(tl_out, "init:\n");
555     else fprintf(tl_out, "S%i:\n", s->id);
556     if(s->trans->nxt == s->trans) {
557       fprintf(tl_out, "\tfalse;\n");
558       continue;
559     }
560     fprintf(tl_out, "\tif\n");
561     for(t = s->trans->nxt; t != s->trans; t = t->nxt) {
562       BTrans *t1;
563       fprintf(tl_out, "\t:: (");
564       spin_print_set(t->pos, t->neg);
565       for(t1 = t; t1->nxt != s->trans; )
566 	if (t1->nxt->to->id == t->to->id &&
567 	    t1->nxt->to->final == t->to->final) {
568 	  fprintf(tl_out, ") || (");
569 	  spin_print_set(t1->nxt->pos, t1->nxt->neg);
570 	  t1->nxt = t1->nxt->nxt;
571 	}
572 	else  t1 = t1->nxt;
573       fprintf(tl_out, ") -> goto ");
574       if(t->to->final == accept)
575 	fprintf(tl_out, "accept_");
576       else fprintf(tl_out, "T%i_", t->to->final);
577       if(t->to->id == 0)
578 	fprintf(tl_out, "all\n");
579       else if(t->to->id == -1)
580 	fprintf(tl_out, "init\n");
581       else fprintf(tl_out, "S%i\n", t->to->id);
582     }
583     fprintf(tl_out, "\tfi;\n");
584   }
585   if(accept_all) {
586     fprintf(tl_out, "accept_all:\n");
587     fprintf(tl_out, "\tskip\n");
588   }
589   fprintf(tl_out, "}\n");
590 }
591 
592 /********************************************************************\
593 |*                       Main method                                *|
594 \********************************************************************/
595 
mk_buchi()596 void mk_buchi()
597 {/* generates a Buchi automaton from the generalized Buchi automaton */
598   int i;
599   BState *s = (BState *)tl_emalloc(sizeof(BState));
600   GTrans *t;
601   BTrans *t1;
602   accept = final[0] - 1;
603 
604   if(tl_stats) getrusage(RUSAGE_SELF, &tr_debut);
605 
606   bstack        = (BState *)tl_emalloc(sizeof(BState)); /* sentinel */
607   bstack->nxt   = bstack;
608   bremoved      = (BState *)tl_emalloc(sizeof(BState)); /* sentinel */
609   bremoved->nxt = bremoved;
610   bstates       = (BState *)tl_emalloc(sizeof(BState)); /* sentinel */
611   bstates->nxt  = s;
612   bstates->prv  = s;
613 
614   s->nxt        = bstates; /* creates (unique) inital state */
615   s->prv        = bstates;
616   s->id = -1;
617   s->incoming = 1;
618   s->final = 0;
619   s->gstate = 0;
620   s->trans = emalloc_btrans(); /* sentinel */
621   s->trans->nxt = s->trans;
622   for(i = 0; i < init_size; i++)
623     if(init[i])
624       for(t = init[i]->trans->nxt; t != init[i]->trans; t = t->nxt) {
625 	int fin = next_final(t->final, 0);
626 	BState *to = find_bstate(&t->to, fin, s);
627 	for(t1 = s->trans->nxt; t1 != s->trans;) {
628 	  if(tl_simp_fly &&
629 	     (to == t1->to) &&
630 	     included_set(t->pos, t1->pos, 1) &&
631 	     included_set(t->neg, t1->neg, 1)) { /* t1 is redondant */
632 	    BTrans *free = t1->nxt;
633 	    t1->to->incoming--;
634 	    t1->to = free->to;
635 	    copy_set(free->pos, t1->pos, 1);
636 	    copy_set(free->neg, t1->neg, 1);
637 	    t1->nxt   = free->nxt;
638 	    if(free == s->trans) s->trans = t1;
639 	    free_btrans(free, 0, 0);
640 	  }
641 	else if(tl_simp_fly &&
642 		(t1->to == to ) &&
643 		included_set(t1->pos, t->pos, 1) &&
644 		included_set(t1->neg, t->neg, 1)) /* t is redondant */
645 	  break;
646 	  else
647 	    t1 = t1->nxt;
648 	}
649 	if(t1 == s->trans) {
650 	  BTrans *trans = emalloc_btrans();
651 	  trans->to = to;
652 	  trans->to->incoming++;
653 	  copy_set(t->pos, trans->pos, 1);
654 	  copy_set(t->neg, trans->neg, 1);
655 	  trans->nxt = s->trans->nxt;
656 	  s->trans->nxt = trans;
657 	}
658       }
659 
660   while(bstack->nxt != bstack) { /* solves all states in the stack until it is empty */
661     s = bstack->nxt;
662     bstack->nxt = bstack->nxt->nxt;
663     if(!s->incoming) {
664       free_bstate(s);
665       continue;
666     }
667     make_btrans(s);
668   }
669 
670   retarget_all_btrans();
671 
672   if(tl_stats) {
673     getrusage(RUSAGE_SELF, &tr_fin);
674     timeval_subtract (&t_diff, &tr_fin.ru_utime, &tr_debut.ru_utime);
675     fprintf(tl_out, "\nBuilding the Buchi automaton : %ld.%06lis",
676 		t_diff.tv_sec, t_diff.tv_usec);
677     fprintf(tl_out, "\n%i states, %i transitions\n", bstate_count, btrans_count);
678   }
679 
680   if(tl_verbose) {
681     fprintf(tl_out, "\nBuchi automaton before simplification\n");
682     print_buchi(bstates->nxt);
683     if(bstates == bstates->nxt)
684       fprintf(tl_out, "empty automaton, refuses all words\n");
685   }
686 
687   if(tl_simp_diff) {
688     simplify_btrans();
689     if(tl_simp_scc) simplify_bscc();
690     while(simplify_bstates()) { /* simplifies as much as possible */
691       simplify_btrans();
692       if(tl_simp_scc) simplify_bscc();
693     }
694 
695     if(tl_verbose) {
696       fprintf(tl_out, "\nBuchi automaton after simplification\n");
697       print_buchi(bstates->nxt);
698       if(bstates == bstates->nxt)
699 	fprintf(tl_out, "empty automaton, refuses all words\n");
700       fprintf(tl_out, "\n");
701     }
702   }
703 
704   print_spin_buchi();
705 }
706