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