remfin.cc 21.4 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
// Copyright (C) 2015, 2016 Laboratoire de Recherche et
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
// Développement de l'Epita.
//
// This file is part of Spot, a model checking library.
//
// Spot is free software; you can redistribute it and/or modify it
// under the terms of the GNU General Public License as published by
// the Free Software Foundation; either version 3 of the License, or
// (at your option) any later version.
//
// Spot is distributed in the hope that it will be useful, but WITHOUT
// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
// License for more details.
//
// You should have received a copy of the GNU General Public License
// along with this program.  If not, see <http://www.gnu.org/licenses/>.

20
21
#include <spot/twaalgos/remfin.hh>
#include <spot/twaalgos/sccinfo.hh>
22
#include <iostream>
23
24
25
26
#include <spot/twaalgos/cleanacc.hh>
#include <spot/twaalgos/totgba.hh>
#include <spot/twaalgos/isdet.hh>
#include <spot/twaalgos/mask.hh>
27
28
29
30
31
32
33
34
35
36
37
38

//#define TRACE
#ifdef TRACE
#define trace std::cerr
#else
#define trace while (0) std::cerr
#endif

namespace spot
{
  namespace
  {
39
40
41
42
43
44
45
46
47
48
49
50
    // Check whether the SCC composed of all states STATES, and
    // visiting all acceptance marks in SETS contains non-accepting
    // cycles.
    //
    // A cycle is accepting (in a Rabin automaton) if there exists an
    // acceptance pair (Fᵢ, Iᵢ) such that some states from Iᵢ are
    // visited while no states from Fᵢ are visited.
    //
    // Consequently, a cycle is non-accepting if for all acceptance
    // pairs (Fᵢ, Iᵢ), either no states from Iᵢ are visited or some
    // states from Fᵢ are visited.  (This corresponds to an accepting
    // cycle with Streett acceptance.)
51
52
53
54
    static bool
    is_scc_ba_type(const const_twa_graph_ptr& aut,
		   const std::vector<unsigned>& states,
		   std::vector<bool>& final,
55
56
		   acc_cond::mark_t inf_pairs,
		   acc_cond::mark_t inf_alone,
57
		   acc_cond::mark_t sets)
58
59
60
61
62
63
64
65
    {
      // Consider the SCC as one large cycle and check its
      // intersection with all Fᵢs and Iᵢs: This is the SETS
      // variable.
      //
      // Let f=[F₁,F₂,...] and i=[I₁,I₂,...] be bitvectors where bit
      // Fᵢ (resp. Iᵢ) indicates that Fᵢ (resp. Iᵢ) has been visited
      // in the SCC.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
66
      acc_cond::mark_t f = (sets << 1U) & inf_pairs;
67
      acc_cond::mark_t i = sets & inf_pairs;
68
69
70
71
72
73
74
      // If we have i&!f = [0,0,...] that means that the cycle formed
      // by the entire SCC is not accepting.  However that does not
      // necessarily imply that all cycles in the SCC are also
      // non-accepting.  We may have a smaller cycle that is
      // accepting, but which becomes non-accepting when extended with
      // more states.
      i -= f;
75
      i |= (inf_alone & sets);
76
77
78
79
80
81
82
83
84
85
86
87
88
89
      if (!i)
	{
	  // Check whether the SCC is accepting.  We do that by simply
	  // converting that SCC into a TGBA and running our emptiness
	  // check.  This is not a really smart implementation and
	  // could be improved.
	  std::vector<bool> keep(aut->num_states(), false);
	  for (auto s: states)
	    keep[s] = true;
	  auto sccaut = mask_keep_states(aut, keep, states.front());
	  // Force SBA to false.  It does not affect the emptiness
	  // check result, however it prevent recurring into this
	  // procedure, because empty() will call to_tgba() wich will
	  // call remove_fin()...
90
	  sccaut->prop_state_acc(false);
91
	  // If SCCAUT is empty, the SCC is BA-type (and none
92
	  // of its states are final).  If SCCAUT is nonempty, the SCC
93
	  // is not BA type.
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
	  return sccaut->is_empty();
	}
      // The bits remaining sets in i corresponds to I₁s that have
      // been seen with seeing the mathing F₁.  In this SCC any state
      // in these I₁ is therefore final.  Otherwise we do not know: it
      // is possible that there is a non-accepting cycle in the SCC
      // that do not visit Fᵢ.
      std::set<unsigned> unknown;
      for (auto s: states)
	{
	  if (aut->state_acc_sets(s) & i)
	    final[s] = true;
	  else
	    unknown.insert(s);
	}
      // Check whether it is possible to build non-accepting cycles
      // using only the "unknown" states.
      while (!unknown.empty())
	{
	  std::vector<bool> keep(aut->num_states(), false);
	  for (auto s: unknown)
	    keep[s] = true;

	  scc_info si(mask_keep_states(aut, keep, *unknown.begin()));
	  unsigned scc_max = si.scc_count();
	  for (unsigned scc = 0; scc < scc_max; ++scc)
	    {
	      for (auto s: si.states_of(scc))
		unknown.erase(s);
123
	      if (si.is_rejecting_scc(scc)) // this includes trivial SCCs
124
125
		continue;
	      if (!is_scc_ba_type(aut, si.states_of(scc),
126
				  final, inf_pairs, 0U, si.acc(scc)))
127
128
129
130
		return false;
	    }
	}
      return true;
131
132
133
134
135
    }

    // Specialized conversion from Rabin acceptance to Büchi acceptance.
    // Is able to detect SCCs that are Büchi-type (i.e., they can be
    // converted to Büchi acceptance without chaning their structure).
Alexandre Duret-Lutz's avatar
typos    
Alexandre Duret-Lutz committed
136
    // Currently only works with state-based acceptance.
137
138
139
140
141
142
143
144
145
146
147
148
149
150
    //
    // See "Deterministic ω-automata vis-a-vis Deterministic Büchi
    // Automata", S. Krishnan, A. Puri, and R. Brayton (ISAAC'94) for
    // some details about detecting Büchi-typeness.
    //
    // We essentially apply this method SCC-wise.  The paper is
    // concerned about *deterministic* automata, but we apply the
    // algorithm on non-deterministic automata as well: in the worst
    // case it is possible that a Büchi-type SCC with some
    // non-deterministic has one accepting and one rejecting run for
    // the same word.  In this case we may fail to detect the
    // Büchi-typeness of the SCC, but the resulting automaton should
    // be correct nonetheless.
    static twa_graph_ptr
151
152
153
154
    ra_to_ba(const const_twa_graph_ptr& aut,
	     acc_cond::mark_t inf_pairs,
	     acc_cond::mark_t inf_alone,
	     acc_cond::mark_t fin_alone)
155
    {
156
      assert(aut->prop_state_acc());
157
158
159
160
161
162
163
164
165

      scc_info si(aut);
      // For state-based Rabin automata, we check each SCC for
      // BA-typeness.  If an SCC is BA-type, its final states are stored
      // in BA_FINAL_STATES.
      std::vector<bool> scc_is_ba_type(si.scc_count(), false);
      bool ba_type = false;
      std::vector<bool> ba_final_states;

166
#ifdef DEBUG
167
168
169
      acc_cond::mark_t fin;
      acc_cond::mark_t inf;
      std::tie(inf, fin) = aut->get_acceptance().used_inf_fin_sets();
170
      assert(inf == (inf_pairs | inf_alone));
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
171
      assert(fin == ((inf_pairs >> 1U) | fin_alone));
172
#endif
173
174
175
176
177
178
179
180
181
182
      ba_final_states.resize(aut->num_states(), false);
      ba_type = true;		// until proven otherwise
      unsigned scc_max = si.scc_count();
      for (unsigned scc = 0; scc < scc_max; ++scc)
	{
	  if (si.is_rejecting_scc(scc)) // this includes trivial SCCs
	    {
	      scc_is_ba_type[scc] = true;
	      continue;
	    }
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
	  bool scc_ba_type = false;
	  auto sets = si.acc(scc);
	  // If there is one fin_alone that is not in the SCC,
	  // any cycle in the SCC is accepting.  Mark all states
	  // as final.
	  if ((sets & fin_alone) != fin_alone)
	    {
	      for (auto s: si.states_of(scc))
		ba_final_states[s] = true;
	      scc_ba_type = true;
	    }
	  // Conversely, if all fin_alone appear in the SCC, then it
	  // cannot be accepting.
	  else if (sets & fin_alone)
	    {
	      scc_ba_type = false;
	    }
	  // In the generale case (no fin_alone involved), we need
	  // a dedicated check.
	  else
	    {
	      scc_ba_type = is_scc_ba_type(aut, si.states_of(scc),
					   ba_final_states,
					   inf_pairs, inf_alone, si.acc(scc));
	    }
208
209
210
211
	  ba_type &= scc_ba_type;
	  scc_is_ba_type[scc] = scc_ba_type;
	}

212
#ifdef TRACE
213
214
215
216
217
218
219
220
221
      trace << "SCC DBA-realizibility\n";
      for (unsigned scc = 0; scc < scc_max; ++scc)
	{
	    trace << scc << ": " << scc_is_ba_type[scc] << " {";
	    for (auto s: si.states_of(scc))
	      trace << ' ' << s;
	    trace << " }\n";
	}
#endif
222

223
224
225
226
227
      unsigned nst = aut->num_states();
      auto res = make_twa_graph(aut->get_dict());
      res->copy_ap_of(aut);
      res->prop_copy(aut, { true, false, false, true });
      res->new_states(nst);
228
      res->set_buchi();
229
      res->set_init_state(aut->get_init_state_number());
230
      trival deterministic = aut->prop_deterministic();
231
232
233
234
235
236
237
238
239
240
241
242

      std::vector<unsigned> state_map(aut->num_states());
      for (unsigned n = 0; n < scc_max; ++n)
	{
	  auto states = si.states_of(n);

	  if (scc_is_ba_type[n])
	    {
	      // If the SCC is BA-type, we know exactly what state need to
	      // be marked as accepting.
	      for (auto s: states)
		{
243
		  bool acc = ba_final_states[s];
244
		  for (auto& t: aut->out(s))
245
		    res->new_acc_edge(s, t.dst, t.cond, acc);
246
247
248
249
250
		}
	      continue;
	    }
	  else
	    {
251
252
253
254
255
256
	      deterministic = false;

	      // The main copy is only accepting for inf_alone
	      // and for all Inf sets that have no matching Fin
	      // sets in this SCC.
	      acc_cond::mark_t sccsets = si.acc(n);
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
257
	      acc_cond::mark_t f = (sccsets << 1U) & inf_pairs;
258
259
	      acc_cond::mark_t i = sccsets & (inf_pairs | inf_alone);
	      i -= f;
260
	      for (auto s: states)
261
262
263
264
265
		{
		  bool acc = aut->state_acc_sets(s) & i;
		  for (auto& t: aut->out(s))
		    res->new_acc_edge(s, t.dst, t.cond, acc);
		}
266

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
267
	      auto rem = sccsets & ((inf_pairs >> 1U) | fin_alone);
268
	      assert(rem != 0U);
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
	      auto sets = rem.sets();

	      unsigned ss = states.size();

	      for (auto r: sets)
		{
		  unsigned base = res->new_states(ss);
		  for (auto s: states)
		    state_map[s] = base++;
		  for (auto s: states)
		    {
		      auto ns = state_map[s];
		      acc_cond::mark_t acc = aut->state_acc_sets(s);
		      if (acc.has(r))
			continue;
284
285
		      bool jacc = acc & inf_alone;
		      bool cacc = fin_alone.has(r) || acc.has(r + 1);
286
287
288
289
290
		      for (auto& t: aut->out(s))
			{
			  if (si.scc_of(t.dst) != n)
			    continue;
			  auto nd = state_map[t.dst];
291
			  res->new_acc_edge(ns, nd, t.cond, cacc);
292
293
294
295
			  // We need only one non-deterministic jump per
			  // cycle.  As an approximation, we only do
			  // them on back-links.
			  if (t.dst <= s)
296
			    res->new_acc_edge(s, nd, t.cond, jacc);
297
298
299
300
301
302
			}
		    }
		}
	    }
	}
      res->purge_dead_states();
303
      res->prop_deterministic(deterministic);
304
305
      return res;
    }
306

307
308
309
    static twa_graph_ptr
    rabin_to_buchi_maybe(const const_twa_graph_ptr& aut)
    {
310
      if (!aut->prop_state_acc().is_true())
311
312
313
314
	return nullptr;

      auto code = aut->get_acceptance();

315
      if (code.is_t())
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
	return nullptr;

      acc_cond::mark_t inf_pairs = 0U;
      acc_cond::mark_t inf_alone = 0U;
      acc_cond::mark_t fin_alone = 0U;

      auto s = code.back().size;

      // Rabin 1
      if (code.back().op == acc_cond::acc_op::And && s == 4)
	goto start_and;
      // Co-Büchi
      else if (code.back().op == acc_cond::acc_op::Fin && s == 1)
	goto start_fin;
      // Rabin >1
      else if (code.back().op != acc_cond::acc_op::Or)
	return nullptr;

      while (s)
	{
	  --s;
	  if (code[s].op == acc_cond::acc_op::And)
	    {
	    start_and:
	      auto o1 = code[--s].op;
	      auto m1 = code[--s].mark;
	      auto o2 = code[--s].op;
	      auto m2 = code[--s].mark;
	      // We expect
	      //   Fin({n}) & Inf({n+1})
	      if (o1 != acc_cond::acc_op::Fin ||
		  o2 != acc_cond::acc_op::Inf ||
		  m1.count() != 1 ||
		  m2.count() != 1 ||
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
350
		  m2 != (m1 << 1U))
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
		return nullptr;
	      inf_pairs |= m2;
	    }
	  else if (code[s].op == acc_cond::acc_op::Fin)
	    {
	    start_fin:
	      fin_alone |= code[--s].mark;
	    }
	  else if (code[s].op == acc_cond::acc_op::Inf)
	    {
	      auto m1 = code[--s].mark;
	      if (m1.count() != 1)
		return nullptr;
	      inf_alone |= m1;
	    }
	  else
	    {
	      return nullptr;
	    }
	}

      trace << "inf_pairs: " << inf_pairs << '\n';
      trace << "inf_alone: " << inf_alone << '\n';
      trace << "fin_alone: " << fin_alone << '\n';
      return ra_to_ba(aut, inf_pairs, inf_alone, fin_alone);
    }



380
381
382
383
384
385
    // If the DNF is
    //  Fin(1)&Inf(2)&Inf(4) | Fin(2)&Fin(3)&Inf(1) |
    //  Inf(1)&Inf(3) | Inf(1)&Inf(2) | Fin(4)
    // this returns the following map:
    //  {1}   => Inf(2)&Inf(4)
    //  {2,3} => Inf(1)
386
    //  {}    => Inf(1)&Inf(3) | Inf(1)&Inf(2)
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
    //  {4}   => t
    static std::map<acc_cond::mark_t, acc_cond::acc_code>
    split_dnf_acc_by_fin(const acc_cond::acc_code& acc)
    {
      std::map<acc_cond::mark_t, acc_cond::acc_code> res;
      auto pos = &acc.back();
      if (pos->op == acc_cond::acc_op::Or)
	--pos;
      auto start = &acc.front();
      while (pos > start)
	{
	  if (pos->op == acc_cond::acc_op::Fin)
	    {
	      // We have only a Fin term, without Inf.  In this case
	      // only, the Fin() may encode a disjunction of sets.
	      for (auto s: pos[-1].mark.sets())
		{
		  acc_cond::mark_t fin = 0U;
		  fin.set(s);
		  res[fin] = acc_cond::acc_code{};
		}
	      pos -= pos->size + 1;
	    }
	  else
	    {
	      // We have a conjunction of Fin and Inf sets.
	      auto end = pos - pos->size - 1;
	      acc_cond::mark_t fin = 0U;
	      acc_cond::mark_t inf = 0U;
	      while (pos > end)
		{
		  switch (pos->op)
		    {
		    case acc_cond::acc_op::And:
		      --pos;
		      break;
		    case acc_cond::acc_op::Fin:
		      fin |= pos[-1].mark;
		      assert(pos[-1].mark.count() == 1);
		      pos -= 2;
		      break;
		    case acc_cond::acc_op::Inf:
		      inf |= pos[-1].mark;
		      pos -= 2;
		      break;
		    case acc_cond::acc_op::FinNeg:
		    case acc_cond::acc_op::InfNeg:
		    case acc_cond::acc_op::Or:
		      SPOT_UNREACHABLE();
		      break;
		    }
		}
	      assert(pos == end);
	      acc_cond::acc_word w[2];
	      w[0].mark = inf;
	      w[1].op = acc_cond::acc_op::Inf;
	      w[1].size = 1;
	      acc_cond::acc_code c;
	      c.insert(c.end(), w, w + 2);
	      auto p = res.emplace(fin, c);
	      if (!p.second)
448
		p.first->second |= std::move(c);
449
450
451
452
	    }
	}
      return res;
    }
453

454
455
456
457
458
459
460
461
462
463
464
    static twa_graph_ptr
    remove_fin_det_weak(const const_twa_graph_ptr& aut)
    {
      // Clone the original automaton.
      auto res = make_twa_graph(aut,
				{
				  true, // state based
				    true, // inherently weak
				    true, // determinisitic
				    true,  // stutter inv.
				    });
465
      res->purge_dead_states();
466
467
468
469
470
      scc_info si(res);

      // We will modify res in place, and the resulting
      // automaton will only have one acceptance set.
      acc_cond::mark_t all_acc = res->set_buchi();
471
      res->prop_state_acc(true);
472
      res->prop_deterministic(true);
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502

      unsigned sink = res->num_states();
      for (unsigned src = 0; src < sink; ++src)
	{
	  acc_cond::mark_t acc = 0U;
	  unsigned scc = si.scc_of(src);
	  if (si.is_accepting_scc(scc) && !si.is_trivial(scc))
	    acc = all_acc;
	  // Keep track of all conditions on edge leaving state
	  // SRC, so we can complete it.
	  bdd missingcond = bddtrue;
	  for (auto& t: res->out(src))
	    {
	      missingcond -= t.cond;
	      t.acc = acc;
	    }
	  // Complete the original automaton.
	  if (missingcond != bddfalse)
	    {
	      if (res->num_states() == sink)
		{
		  res->new_state();
		  res->new_acc_edge(sink, sink, bddtrue);
		}
	      res->new_edge(src, sink, missingcond);
	    }
	}
      //res->merge_edges();
      return res;
    }
503
504
  }

505
  twa_graph_ptr remove_fin(const const_twa_graph_ptr& aut)
506
507
  {
    if (!aut->acc().uses_fin_acceptance())
508
      return std::const_pointer_cast<twa_graph>(aut);
509

510
    // FIXME: we should check whether the automaton is weak.
511
    if (aut->prop_inherently_weak().is_true() && is_deterministic(aut))
512
513
      return remove_fin_det_weak(aut);

514
515
516
517
518
    if (auto maybe = streett_to_generalized_buchi_maybe(aut))
      return maybe;

    if (auto maybe = rabin_to_buchi_maybe(aut))
      return maybe;
519

520
521
522
523
524
    std::vector<acc_cond::acc_code> code;
    std::vector<acc_cond::mark_t> rem;
    std::vector<acc_cond::mark_t> keep;
    std::vector<acc_cond::mark_t> add;
    bool has_true_term = false;
525
526
    acc_cond::mark_t allinf = 0U;
    acc_cond::mark_t allfin = 0U;
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
    {
      auto acccode = aut->get_acceptance();
      if (!acccode.is_dnf())
	acccode = acccode.to_dnf();

      auto split = split_dnf_acc_by_fin(acccode);

      auto sz = split.size();
      assert(sz > 0);

      rem.reserve(sz);
      code.reserve(sz);
      keep.reserve(sz);
      add.reserve(sz);
      for (auto p: split)
	{
	  // The empty Fin should always come first
	  assert(p.first != 0U || rem.empty());
	  rem.push_back(p.first);
546
	  allfin |= p.first;
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
	  acc_cond::mark_t inf = 0U;
	  if (!p.second.empty())
	    {
	      auto pos = &p.second.back();
	      auto end = &p.second.front();
	      while (pos > end)
		{
		  switch (pos->op)
		    {
		    case acc_cond::acc_op::And:
		    case acc_cond::acc_op::Or:
		      --pos;
		      break;
		    case acc_cond::acc_op::Inf:
		      inf |= pos[-1].mark;
		      pos -= 2;
		      break;
		    case acc_cond::acc_op::Fin:
		    case acc_cond::acc_op::FinNeg:
		    case acc_cond::acc_op::InfNeg:
		      SPOT_UNREACHABLE();
		      break;
		    }
		}
	    }
572
	  if (inf == 0U)
573
574
575
576
577
	    {
	      has_true_term = true;
	    }
	  code.push_back(std::move(p.second));
	  keep.push_back(inf);
578
	  allinf |= inf;
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
	  add.push_back(0U);
	}
    }
    assert(add.size() > 0);

    acc_cond acc = aut->acc();
    unsigned extra_sets = 0;

    // Do we have common sets between the acceptance terms?
    // If so, we need extra sets to distinguish the terms.
    bool interference = false;
    {
      auto sz = keep.size();
      acc_cond::mark_t sofar = 0U;
      for (unsigned i = 0; i < sz; ++i)
	{
	  auto k = keep[i];
	  if (k & sofar)
	    {
	      interference = true;
	      break;
	    }
	  sofar |= k;
	}
      if (interference)
	{
	  trace << "We have interferences\n";
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
	  // We need extra set, but we will try
	  // to reuse the Fin number if they are
	  // not used as Inf as well.
	  std::vector<int> exs(acc.num_sets());
	  for (auto f: allfin.sets())
	    {
	      if (allinf.has(f)) // Already used as Inf
		{
		  exs[f] = acc.add_set();
		  ++extra_sets;
		}
	      else
		{
		  exs[f] = f;
		}
	    }
622
623
	  for (unsigned i = 0; i < sz; ++i)
	    {
624
625
626
627
628
	      acc_cond::mark_t m = 0U;
	      for (auto f: rem[i].sets())
		m.set(exs[f]);
	      trace << "rem[" << i << "] = " << rem[i]
		    << "  m = " << m << '\n';
629
	      add[i] = m;
630
	      code[i] &= acc.inf(m);
631
632
633
634
635
636
637
638
	      trace << "code[" << i << "] = " << code[i] << '\n';
	    }
	}
      else if (has_true_term)
	{
	  trace << "We have a true term\n";
	  unsigned one = acc.add_sets(1);
	  extra_sets += 1;
639
	  acc_cond::mark_t m({one});
640
641
642
	  auto c = acc.inf(m);
	  for (unsigned i = 0; i < sz; ++i)
	    {
643
	      if (!code[i].is_t())
644
645
		continue;
	      add[i] = m;
646
	      code[i] &= std::move(c);
647
648
649
650
651
652
653
654
655
	      c = acc.fin(0U);	// Use false for the other terms.
	      trace << "code[" << i << "] = " << code[i] << '\n';
	    }

	}
    }

    acc_cond::acc_code new_code = aut->acc().fin(0U);
    for (auto c: code)
656
      new_code |= std::move(c);
657
658
659
660
661
662
663

    unsigned cs = code.size();
    for (unsigned i = 0; i < cs; ++i)
      trace << i << " Rem " << rem[i] << "  Code " << code[i]
	    << " Keep " << keep[i] << '\n';

    unsigned nst = aut->num_states();
664
    auto res = make_twa_graph(aut->get_dict());
665
    res->copy_ap_of(aut);
666
    res->prop_copy(aut, { true, false, false, true });
667
    res->new_states(nst);
668
    res->set_acceptance(aut->num_sets() + extra_sets, new_code);
669
670
    res->set_init_state(aut->get_init_state_number());

671
    bool sbacc = aut->prop_state_acc().is_true();
672
    scc_info si(aut);
673
674
675
676
677
678
679
680
    unsigned nscc = si.scc_count();
    std::vector<unsigned> state_map(nst);
    for (unsigned n = 0; n < nscc; ++n)
      {
	auto m = si.acc(n);
	auto states = si.states_of(n);
	trace << "SCC #" << n << " uses " << m << '\n';

681
682
683
	// What to keep and add into the main copy
	acc_cond::mark_t main_sets = 0U;
	acc_cond::mark_t main_add = 0U;
684
	bool intersects_fin = false;
685
686
687
688
689
690
	for (unsigned i = 0; i < cs; ++i)
	  if (!(m & rem[i]))
	    {
	      main_sets |= keep[i];
	      main_add |= add[i];
	    }
691
692
693
694
	  else
	    {
	      intersects_fin = true;
	    }
695
696
	trace << "main_sets " << main_sets << "\nmain_add " << main_add << '\n';

697
698
699
	// Create the main copy
	for (auto s: states)
	  for (auto& t: aut->out(s))
700
701
702
703
704
705
	    {
	      acc_cond::mark_t a = 0U;
	      if (sbacc || SPOT_LIKELY(si.scc_of(t.dst) == n))
		a = (t.acc & main_sets) | main_add;
	      res->new_edge(s, t.dst, t.cond, a);
	    }
706

707
708
709
	// We do not need any other copy if the SCC is non-accepting,
	// of if it does not intersect any Fin.
	if (!intersects_fin || si.is_rejecting_scc(n))
710
711
	  continue;

712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
	// Create clones
	for (unsigned i = 0; i < cs; ++i)
	  if (m & rem[i])
	    {
	      auto r = rem[i];
	      trace << "rem[" << i << "] = " << r << " requires a copy\n";
	      unsigned base = res->new_states(states.size());
	      for (auto s: states)
		state_map[s] = base++;
	      auto k = keep[i];
	      auto a = add[i];
	      for (auto s: states)
		{
		  auto ns = state_map[s];
		  for (auto& t: aut->out(s))
		    {
		      if ((t.acc & r) || si.scc_of(t.dst) != n)
			continue;
		      auto nd = state_map[t.dst];
731
		      res->new_edge(ns, nd, t.cond, (t.acc & k) | a);
732
733
734
735
		      // We need only one non-deterministic jump per
		      // cycle.  As an approximation, we only do
		      // them on back-links.
		      if (t.dst <= s)
736
737
738
739
740
741
			{
			  acc_cond::mark_t a = 0U;
			  if (sbacc)
			    a = (t.acc & main_sets) | main_add;
			  res->new_edge(s, nd, t.cond, a);
			}
742
743
744
		    }
		}
	    }
745
      }
746

747
748
    // If the input had no Inf, the output is a state-based automaton.
    if (allinf == 0U)
749
      res->prop_state_acc(true);
750

751
    res->purge_dead_states();
752
    trace << "before cleanup: " << res->get_acceptance() << '\n';
753
    cleanup_acceptance_here(res);
754
    trace << "after cleanup: " << res->get_acceptance() << '\n';
755
    res->merge_edges();
756
757
758
    return res;
  }
}