remfin.cc 27.1 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
3
// Copyright (C) 2015-2017 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
//
// 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
#include <spot/twaalgos/alternation.hh>
28
#include "spot/priv/enumflags.hh"
29
30
31
32
33
34
35
36
37
38
39
40

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

namespace spot
{
  namespace
  {
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
    enum class strategy_t : unsigned
    {
      trivial     = 1,
      weak        = 2,
      alternation = 4,
      street      = 8,
      rabin       = 16
    };

    using strategy_flags = strong_enum_flags<strategy_t>;
    using strategy =
        std::function<twa_graph_ptr(const const_twa_graph_ptr& aut)>;

    twa_graph_ptr
    remove_fin_impl(const const_twa_graph_ptr&, const strategy_flags);

    using EdgeMask = std::vector<bool>;

    template< typename Edges, typename Apply >
    void for_each_edge(const_twa_graph_ptr aut,
                       const Edges& edges,
                       const EdgeMask& mask,
                       Apply apply)
    {
      for (const auto& e: edges)
        {
          unsigned edge_id = aut->edge_number(e);
          if (mask[edge_id])
            apply(edge_id);
        }
    }

    template< typename Edges >
    acc_cond::mark_t scc_acc_marks(const_twa_graph_ptr aut,
                                   const Edges& edges,
                                   const EdgeMask& mask)
    {
      acc_cond::mark_t scc_mark = 0U;
      for_each_edge(aut, edges, mask, [&] (unsigned e)
        {
          const auto& ed = aut->edge_data(e);
          scc_mark |= ed.acc;
        });
      return scc_mark;
    }

    // Check whether the SCC contains non-accepting cycles.
88
89
90
91
92
93
94
95
96
    //
    // 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.)
97
98
99
100
101
102
103
104
105
    //
    // final are those edges which are used in the resulting tba
    // acceptance condition.
    bool is_scc_tba_type(const_twa_graph_ptr aut,
                         const scc_info& si,
                         const unsigned scc,
                         std::vector<bool> keep,
                         const rs_pairs_view& aut_pairs,
                         std::vector<bool>& final)
106
    {
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
      if (si.is_rejecting_scc(scc))
        return true;

      auto scc_acc = scc_acc_marks(aut, si.inner_edges_of(scc), keep);
      auto scc_pairs = rs_pairs_view(aut_pairs.pairs(), scc_acc);
      // If there is one aut_fin_alone that is not in the SCC,
      // any cycle in the SCC is accepting.
      if (scc_pairs.fins_alone().proper_subset(aut_pairs.fins_alone()))
        {
          for_each_edge(aut, si.edges_of(scc), keep, [&](unsigned e)
            {
              final[e] = true;
            });
          return true;
        }

      auto scc_infs_alone = scc_pairs.infs_alone();
      // Firstly consider whole SCC as one large cycle.
      // If there is no inf without matching fin then the cycle formed
126
127
128
129
130
      // 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.
131
      if (!scc_infs_alone)
132
133
134
135
136
        {
          // 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.
137
138
          auto& states = si.states_of(scc);
          std::vector<bool> keep_states(aut->num_states(), false);
139
          for (auto s: states)
140
141
142
143
144
145
146
            keep_states[s] = true;
          auto sccaut = mask_keep_accessible_states(aut,
                                                    keep_states,
                                                    states.front());

          // Prevent recurring into this function, by skipping the rabin straegy
          auto skip = strategy_t::rabin;
147
148
          // If SCCAUT is empty, the SCC is BA-type (and none
          // of its states are final).  If SCCAUT is nonempty, the SCC
149
150
          // is not BA type
          return remove_fin_impl(sccaut, skip)->is_empty();
151
        }
152
153
154
155
156

      // Remaining infs corresponds to I₁s that have been seen with seeing
      // the mathing F₁.cIn this SCC any edge 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ᵢ.
157
      std::set<unsigned> unknown;
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
      for_each_edge(aut, si.inner_edges_of(scc), keep, [&](unsigned e)
        {
          const auto& ed = aut->edge_data(e);
          if (ed.acc & scc_infs_alone)
              final[e] = true;
          else
              unknown.insert(e);
        });
      // Check whether it is possible to build non-accepting cycles
      // using only the "unknown" edges.
      keep.assign(aut->edge_vector().size(), false);

      // Erase edges that cannot form cycle, ie. that edge whose 'dst'
      // is not 'src' of any unknown edges.
      std::vector<unsigned> remove;
      do
        {
          remove.clear();
          std::set<unsigned> srcs;
          for (auto e: unknown)
            srcs.insert(aut->edge_storage(e).src);
          for (auto e: unknown)
            if (!srcs.count(aut->edge_storage(e).dst))
              remove.push_back(e);
          for (auto r: remove)
            unknown.erase(r);
        }
      while (!remove.empty());

187
      // Check whether it is possible to build non-accepting cycles
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
      // using only the "unknown" edges.
      using filter_data_t = std::pair< const_twa_graph_ptr, std::vector<bool> >;

      scc_info::edge_filter filter =
        [](const twa_graph::edge_storage_t& t, unsigned, void* data)
          -> scc_info::edge_filter_choice
        {
          const_twa_graph_ptr aut;
          std::vector<bool> keep;
          std::tie(aut, keep) = *static_cast<filter_data_t*>(data);

          if (keep[aut->edge_number(t)])
            return scc_info::edge_filter_choice::keep;
          else
            return scc_info::edge_filter_choice::ignore;
        };

205
      while (!unknown.empty())
206
        {
207
208
209
          std::vector<bool> keep(aut->edge_vector().size(), false);
          for (auto e: unknown)
            keep[e] = true;
210

211
212
213
214
215
          auto filter_data = filter_data_t{aut, keep};
          auto init = aut->edge_storage(*unknown.begin()).src;
          scc_info si(aut, init, filter, &filter_data);

          for (unsigned uscc = 0; uscc < si.scc_count(); ++uscc)
216
            {
217
218
219
220
221
              for_each_edge(aut, si.edges_of(uscc), keep, [&](unsigned e)
                {
                  unknown.erase(e);
                });
              if (si.is_rejecting_scc(uscc))
222
                continue;
223
              if (!is_scc_tba_type(aut, si, uscc, keep, aut_pairs, final))
224
225
226
                return false;
            }
        }
227
      return true;
228
229
    }

230
231
232
    // Specialized conversion from transition based Rabin acceptance to
    // transition based Büchi acceptance.
    // Is able to detect SCCs that are TBA-type (i.e., they can be
233
234
235
236
237
238
    // converted to Büchi acceptance without chaning their structure).
    //
    // 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.
    //
239
    // We essentially apply this method SCC-wise. The paper is
240
241
    // concerned about *deterministic* automata, but we apply the
    // algorithm on non-deterministic automata as well: in the worst
242
243
    // case it is possible that a TBA-type SCC with some
    // non-deterministic has one accepting and one rejecting run for
244
    // the same word.  In this case we may fail to detect the
245
    // TBA-typeness of the SCC, but the resulting automaton should
246
    // be correct nonetheless.
247
248
    twa_graph_ptr
    tra_to_tba(const const_twa_graph_ptr& inaut)
249
    {
250
251
      // cleanup acceptance for easy detection of alone fins and infs
      auto aut = cleanup_acceptance(inaut);
252

253
254
255
      std::vector<acc_cond::rs_pair> pairs;
      if (!aut->acc().is_rabin_like(pairs))
        return nullptr;
256

257
258
259
260
261
262
263
264
265
266
267
268
269
270
      auto aut_pairs = rs_pairs_view(pairs);
      auto code = aut->get_acceptance();
      if (code.is_t())
        return nullptr;

      // if is TBA type
      scc_info si{aut};
      std::vector<bool> scc_is_tba_type(si.scc_count(), false);
      std::vector<bool> final(aut->edge_vector().size(), false);
      std::vector<bool> keep(aut->edge_vector().size(), true);

      for (unsigned scc = 0; scc < si.scc_count(); ++scc)
        scc_is_tba_type[scc] = is_scc_tba_type(aut, si, scc, keep,
                                               aut_pairs, final);
271

272
273
      auto res = make_twa_graph(aut->get_dict());
      res->copy_ap_of(aut);
274
275
      res->prop_copy(aut, { false, false, false, false, false, true });
      res->new_states(aut->num_states());
276
      res->set_buchi();
277
      res->set_init_state(aut->get_init_state_number());
278
      trival deterministic = aut->prop_universal();
279
      trival complete = aut->prop_complete();
280
281

      std::vector<unsigned> state_map(aut->num_states());
282
      for (unsigned scc = 0; scc < si.scc_count(); ++scc)
283
        {
284
          auto states = si.states_of(scc);
285

286
          if (scc_is_tba_type[scc])
287
            {
288
              for (const auto& e: si.edges_of(scc))
289
                {
290
291
                  bool acc = final[aut->edge_number(e)];
                  res->new_acc_edge(e.src, e.dst, e.cond, acc);
292
293
294
295
                }
            }
          else
            {
296
              complete = trival::maybe();
297
298
299
300

              // The main copy is only accepting for inf_alone
              // and for all Inf sets that have no matching Fin
              // sets in this SCC.
301
302
303
304
              auto scc_pairs = rs_pairs_view(pairs, si.acc(scc));
              auto scc_infs_alone = scc_pairs.infs_alone();

              for (const auto& e: si.edges_of(scc))
305
                {
306
307
                  bool acc{e.acc & scc_infs_alone};
                  res->new_acc_edge(e.src, e.dst, e.cond, acc);
308
309
                }

310
              auto fins_alone = aut_pairs.fins_alone();
311

312
              for (auto r: scc_pairs.fins().sets())
313
                {
314
                  unsigned base = res->new_states(states.size());
315
                  for (auto s: states)
316
317
                      state_map[s] = base++;
                  for (const auto& e: si.inner_edges_of(scc))
318
                    {
319
                      if (e.acc.has(r))
320
                        continue;
321
322
323
324
325
326
327
328
329
330
                      auto src = state_map[e.src];
                      auto dst = state_map[e.dst];
                      bool cacc = fins_alone.has(r)
                                ? true
                                : ((scc_pairs.paired_with(r) & e.acc) != 0);
                      res->new_acc_edge(src, dst, e.cond, cacc);
                      // We need only one non-deterministic jump per
                      // cycle.  As an approximation, we only do
                      // them on back-links.
                      if (e.dst <= e.src)
331
                        {
332
333
334
                          deterministic = false;
                          bool jacc = ((e.acc & scc_infs_alone) != 0);
                          res->new_acc_edge(e.src, dst, e.cond, jacc);
335
336
337
338
339
                        }
                    }
                }
            }
        }
340
      res->prop_complete(complete);
341
      res->prop_universal(deterministic);
342
      res->purge_dead_states();
343
344
      res->merge_edges();

345
346
      return res;
    }
347

348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
    // Transforms automaton from transition based acceptance to state based
    // acceptance.
    void make_state_acc(twa_graph_ptr & aut)
    {
      unsigned nst = aut->num_states();
      for (unsigned s = 0; s < nst; ++s)
        {
          acc_cond::mark_t acc = 0U;
          for (auto& t: aut->out(s))
            acc |= t.acc;
          for (auto& t: aut->out(s))
            t.acc = acc;
        }
      aut->prop_state_acc(true);
    }

364
365
366
367
368
369
    // 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)
370
    //  {}    => Inf(1)&Inf(3) | Inf(1)&Inf(2)
371
372
373
374
375
376
    //  {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();
377
      if (pos->sub.op == acc_cond::acc_op::Or)
378
        --pos;
379
380
      auto start = &acc.front();
      while (pos > start)
381
        {
382
          if (pos->sub.op == acc_cond::acc_op::Fin)
383
384
385
386
387
388
389
390
391
            {
              // 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{};
                }
392
              pos -= pos->sub.size + 1;
393
394
395
396
            }
          else
            {
              // We have a conjunction of Fin and Inf sets.
397
              auto end = pos - pos->sub.size - 1;
398
399
400
401
              acc_cond::mark_t fin = 0U;
              acc_cond::mark_t inf = 0U;
              while (pos > end)
                {
402
                  switch (pos->sub.op)
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
                    {
                    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;
426
427
              w[1].sub.op = acc_cond::acc_op::Inf;
              w[1].sub.size = 1;
428
429
430
431
432
433
434
              acc_cond::acc_code c;
              c.insert(c.end(), w, w + 2);
              auto p = res.emplace(fin, c);
              if (!p.second)
                p.first->second |= std::move(c);
            }
        }
435
436
      return res;
    }
437

438
    static twa_graph_ptr
439
    remove_fin_weak(const const_twa_graph_ptr& aut)
440
441
442
    {
      // Clone the original automaton.
      auto res = make_twa_graph(aut,
443
444
                                {
                                  true, // state based
445
446
447
448
449
                                  true, // inherently weak
                                  true, true, // determinisitic
                                  true,       // complete
                                  true,  // stutter inv.
                                });
450
451
452
453
454
      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();
455
      res->prop_state_acc(true);
456
      unsigned n = res->num_states();
457

458
      for (unsigned src = 0; src < n; ++src)
459
        {
460
461
          if (!si.reachable_state(src))
            continue;
462
463
464
465
466
          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;
          for (auto& t: res->out(src))
467
            t.acc = acc;
468
        }
469
470
      return res;
    }
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495

    twa_graph_ptr trivial_strategy(const const_twa_graph_ptr& aut)
    {
      return (!aut->acc().uses_fin_acceptance())
             ? std::const_pointer_cast<twa_graph>(aut)
             : nullptr;
    }

    twa_graph_ptr weak_strategy(const const_twa_graph_ptr& aut)
    {
      // FIXME: we should check whether the automaton is inherently weak.
      return (aut->prop_weak().is_true())
             ? remove_fin_weak(aut)
             : nullptr;
    }

    twa_graph_ptr alternation_strategy(const const_twa_graph_ptr& aut)
    {
      return (!aut->is_existential())
             ? remove_fin(remove_alternation(aut))
             : nullptr;
    }

    twa_graph_ptr street_strategy(const const_twa_graph_ptr& aut)
    {
496
497
498
      return (aut->get_acceptance().used_inf_fin_sets().first)
             ? streett_to_generalized_buchi_maybe(aut)
             : nullptr;
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
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
572
573
574
575
576
577
578
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
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
    }

    twa_graph_ptr rabin_strategy(const const_twa_graph_ptr& aut)
    {
      return rabin_to_buchi_maybe(aut);
    }

    twa_graph_ptr default_strategy(const const_twa_graph_ptr& aut)
    {
      {
        // We want a clean acceptance condition, i.e., one where all
        // sets are useful.  If that is not the case, clean it first.
        acc_cond::mark_t unused = aut->acc().all_sets();
        for (auto& t: aut->edges())
          {
            unused -= t.acc;
            if (!unused)
              break;
          }
        if (unused)
          return remove_fin(cleanup_acceptance(aut));
      }

      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;
      acc_cond::mark_t allinf = 0U;
      acc_cond::mark_t allfin = 0U;
      {
        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.emplace_back(p.first);
            allfin |= p.first;
            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->sub.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;
                      }
                  }
              }
            if (inf == 0U)
              {
                has_true_term = true;
              }
            code.emplace_back(std::move(p.second));
            keep.emplace_back(inf);
            allinf |= inf;
            add.emplace_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";
            // 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;
                  }
              }
            for (unsigned i = 0; i < sz; ++i)
              {
                acc_cond::mark_t m = 0U;
                for (auto f: rem[i].sets())
                  m.set(exs[f]);
                trace << "rem[" << i << "] = " << rem[i]
                      << "  m = " << m << '\n';
                add[i] = m;
                code[i] &= acc.inf(m);
                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;
            acc_cond::mark_t m({one});
            auto c = acc.inf(m);
            for (unsigned i = 0; i < sz; ++i)
              {
                if (!code[i].is_t())
                  continue;
                add[i] = m;
                code[i] &= std::move(c);
                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)
        new_code |= std::move(c);

      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();
      auto res = make_twa_graph(aut->get_dict());
      res->copy_ap_of(aut);
      res->prop_copy(aut, { true, false, false, false, false, true });
      res->new_states(nst);
      res->set_acceptance(aut->num_sets() + extra_sets, new_code);
      res->set_init_state(aut->get_init_state_number());

      bool sbacc = aut->prop_state_acc().is_true();
      scc_info si(aut);
      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';

          // What to keep and add into the main copy
          acc_cond::mark_t main_sets = 0U;
          acc_cond::mark_t main_add = 0U;
          bool intersects_fin = false;
          for (unsigned i = 0; i < cs; ++i)
            if (!(m & rem[i]))
              {
                main_sets |= keep[i];
                main_add |= add[i];
              }
            else
              {
                intersects_fin = true;
              }
          trace << "main_sets " << main_sets << "\nmain_add "
                << main_add << '\n';

          // Create the main copy
          for (auto s: states)
            for (auto& t: aut->out(s))
              {
                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);
              }

          // 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))
            continue;

          // 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];
                        res->new_edge(ns, nd, t.cond, (t.acc & k) | a);
                        // We need only one non-deterministic jump per
                        // cycle.  As an approximation, we only do
                        // them on back-links.
                        if (t.dst <= s)
                          {
                            acc_cond::mark_t a = 0U;
                            if (sbacc)
                              a = (t.acc & main_sets) | main_add;
                            res->new_edge(s, nd, t.cond, a);
                          }
                      }
                  }
              }
        }

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

      res->purge_dead_states();
      trace << "before cleanup: " << res->get_acceptance() << '\n';
      cleanup_acceptance_here(res);
      trace << "after cleanup: " << res->get_acceptance() << '\n';
      res->merge_edges();
      return res;
    }

    twa_graph_ptr remove_fin_impl(const const_twa_graph_ptr& aut,
                                  const strategy_flags skip = {})
    {
      auto handle = [&](strategy stra, strategy_t type)
      {
        return (type & ~skip) ? stra(aut) : nullptr;
      };

      if (auto maybe = handle(trivial_strategy, strategy_t::trivial))
        return maybe;
      if (auto maybe = handle(weak_strategy, strategy_t::weak))
        return maybe;
      if (auto maybe = handle(alternation_strategy, strategy_t::alternation))
        return maybe;
      if (auto maybe = handle(street_strategy, strategy_t::street))
        return maybe;
      if (auto maybe = handle(rabin_strategy, strategy_t::rabin))
        return maybe;
      return default_strategy(aut);
    }
782
783
  }

784
785
786
  twa_graph_ptr
  rabin_to_buchi_maybe(const const_twa_graph_ptr& aut)
  {
787
788
789
790
791
    bool is_state_acc = aut->prop_state_acc().is_true();
    auto res = tra_to_tba(aut);
    if (res && is_state_acc)
      make_state_acc(res);
    return res;
792
793
  }

794
  twa_graph_ptr remove_fin(const const_twa_graph_ptr& aut)
795
  {
796
    return remove_fin_impl(aut);
797
798
  }
}