twagraph.cc 27.3 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
3
// Copyright (C) 2014, 2015, 2016, 2017 Laboratoire de Recherche et
// Développement de l'Epita.
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/twa/twagraph.hh>
#include <spot/tl/print.hh>
22
#include <spot/misc/bddlt.hh>
23
#include <vector>
24
#include <deque>
25
26
27

namespace spot
{
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61

  std::string twa_graph::format_state(unsigned n) const
  {
    if (is_univ_dest(n))
      {
        std::stringstream ss;
        bool notfirst = false;
        for (unsigned d: univ_dests(n))
          {
            if (notfirst)
              ss << '&';
            notfirst = true;
            ss << format_state(d);
          }
        return ss.str();
      }

    auto named = get_named_prop<std::vector<std::string>>("state-names");
    if (named && n < named->size())
      return (*named)[n];

    auto prod = get_named_prop
      <std::vector<std::pair<unsigned, unsigned>>>("product-states");
    if (prod && n < prod->size())
      {
        auto& p = (*prod)[n];
        std::stringstream ss;
        ss << p.first << ',' << p.second;
        return ss.str();
      }

    return std::to_string(n);
  }

62
  void
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
63
  twa_graph::release_formula_namer(namer<formula>* namer,
64
                                   bool keep_names)
65
66
67
  {
    if (keep_names)
      {
68
69
70
71
72
73
74
75
76
77
78
        auto v = new std::vector<std::string>(num_states());
        auto& n = namer->names();
        unsigned ns = n.size();
        assert(n.size() <= v->size());
        for (unsigned i = 0; i < ns; ++i)
          {
            auto f = n[i];
            if (f)
              (*v)[i] = str_psl(f);
          }
        set_named_prop("state-names", v);
79
80
81
      }
    delete namer;
  }
82

83
84
85
86
87
  /// \brief Merge universal destinations
  ///
  /// If several states have the same universal destination, merge
  /// them all.  Also remove unused destination, and any redundant
  /// state in each destination.
88
89
90
91
92
93
94
95
96
  void twa_graph::merge_univ_dests()
  {
    auto& g = get_graph();
    auto& dests = g.dests_vector();
    auto& edges = g.edge_vector();

    std::vector<unsigned> old_dests;
    std::swap(dests, old_dests);
    std::vector<unsigned> seen(old_dests.size(), -1U);
97
    internal::univ_dest_mapper<twa_graph::graph_t> uniq(g);
98
99
100
101
102
103
104
105
106

    auto fixup = [&](unsigned& in_dst)
      {
        unsigned dst = in_dst;
        if ((int) dst >= 0)       // not a universal edge
          return;
        dst = ~dst;
        unsigned& nd = seen[dst];
        if (nd == -1U)
107
108
          nd = uniq.new_univ_dests(old_dests.data() + dst + 1,
                                   old_dests.data() + dst + 1 + old_dests[dst]);
109
110
111
112
113
114
115
116
117
118
119
120
121
        in_dst = nd;
      };

    unsigned tend = edges.size();
    for (unsigned t = 1; t < tend; t++)
      {
        if (g.is_dead_edge(t))
          continue;
        fixup(edges[t].dst);
      }
    fixup(init_number_);
  }

122
  void twa_graph::merge_edges()
123
  {
124
    set_named_prop("highlight-edges", nullptr);
125
    g_.remove_dead_edges_();
126
    if (!is_existential())
127
      merge_univ_dests();
128

129
130
    typedef graph_t::edge_storage_t tr_t;
    g_.sort_edges_([](const tr_t& lhs, const tr_t& rhs)
131
132
133
134
135
136
137
138
139
140
141
142
143
                   {
                     if (lhs.src < rhs.src)
                       return true;
                     if (lhs.src > rhs.src)
                       return false;
                     if (lhs.dst < rhs.dst)
                       return true;
                     if (lhs.dst > rhs.dst)
                       return false;
                     return lhs.acc < rhs.acc;
                     // Do not sort on conditions, we'll merge
                     // them.
                   });
144

145
    auto& trans = this->edge_vector();
146
147
148
    unsigned tend = trans.size();
    unsigned out = 0;
    unsigned in = 1;
149
    // Skip any leading false edge.
150
151
152
153
    while (in < tend && trans[in].cond == bddfalse)
      ++in;
    if (in < tend)
      {
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
        ++out;
        if (out != in)
          trans[out] = trans[in];
        for (++in; in < tend; ++in)
          {
            if (trans[in].cond == bddfalse) // Unusable edge
              continue;
            // Merge edges with the same source, destination, and
            // acceptance.  (We test the source last, because this is the
            // most likely test to be true as edges are ordered by
            // sources and then destinations.)
            if (trans[out].dst == trans[in].dst
                && trans[out].acc == trans[in].acc
                && trans[out].src == trans[in].src)
              {
                trans[out].cond |= trans[in].cond;
              }
            else
              {
                ++out;
                if (in != out)
                  trans[out] = trans[in];
              }
          }
178
      }
179
180
181
    if (++out != tend)
      trans.resize(out);

182
183
184
    tend = out;
    out = in = 2;

185
    // FIXME: We could should also merge edges when using
186
187
188
189
    // fin_acceptance, but the rule for Fin sets are different than
    // those for Inf sets, (and we need to be careful if a set is used
    // both as Inf and Fin)
    if ((in < tend) && !acc().uses_fin_acceptance())
190
      {
191
192
193
194
195
196
197
198
199
200
201
        typedef graph_t::edge_storage_t tr_t;
        g_.sort_edges_([](const tr_t& lhs, const tr_t& rhs)
                       {
                         if (lhs.src < rhs.src)
                           return true;
                         if (lhs.src > rhs.src)
                           return false;
                         if (lhs.dst < rhs.dst)
                           return true;
                         if (lhs.dst > rhs.dst)
                           return false;
202
203
                         bdd_less_than_stable lt;
                         return lt(lhs.cond, rhs.cond);
204
205
206
                         // Do not sort on acceptance, we'll merge
                         // them.
                       });
207

208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
        for (; in < tend; ++in)
          {
            // Merge edges with the same source, destination,
            // and conditions.  (We test the source last, for the
            // same reason as above.)
            if (trans[out].dst == trans[in].dst
                && trans[out].cond.id() == trans[in].cond.id()
                && trans[out].src == trans[in].src)
              {
                trans[out].acc |= trans[in].acc;
              }
            else
              {
                ++out;
                if (in != out)
                  trans[out] = trans[in];
              }
          }
        if (++out != tend)
          trans.resize(out);
228
229
      }

230
    g_.chain_edges_();
231
232
  }

233
  void twa_graph::purge_unreachable_states()
234
235
  {
    unsigned num_states = g_.num_states();
236
237
238
239
240
241
242
243
244
245
    // The TODO vector serves two purposes:
    // - it is a stack of state to process,
    // - it is a set of processed states.
    // The lower 31 bits of each entry is a state on the stack. (The
    // next usable entry on the stack is indicated by todo_pos.)  The
    // 32th bit (i.e., the sign bit) of todo[x] indicates whether
    // states number x has been seen.
    std::vector<unsigned> todo(num_states, 0);
    const unsigned seen = 1 << (sizeof(unsigned)*8-1);
    const unsigned mask = seen - 1;
246
247
248
249
250
251
    unsigned todo_pos = 0;
    for (unsigned i: univ_dests(get_init_state_number()))
      {
        todo[i] |= seen;
        todo[todo_pos++] |= i;
      }
252
    do
253
      {
254
255
256
        unsigned cur = todo[--todo_pos] & mask;
        todo[todo_pos] ^= cur;        // Zero the state
        for (auto& t: g_.out(cur))
257
258
259
260
261
262
          for (unsigned dst: univ_dests(t.dst))
            if (!(todo[dst] & seen))
              {
                todo[dst] |= seen;
                todo[todo_pos++] |= dst;
              }
263
      }
264
    while (todo_pos > 0);
265
266
    // Now renumber each used state.
    unsigned current = 0;
267
268
    for (auto& v: todo)
      if (!(v & seen))
269
        v = -1U;
270
      else
271
        v = current++;
272
    if (current == todo.size())
273
      return;                        // No unreachable state.
274
275

    // Removing some non-deterministic dead state could make the
276
277
278
    // automaton universal.
    if (prop_universal().is_false())
      prop_universal(trival::maybe());
279
280
281
    if (prop_complete().is_false())
      prop_complete(trival::maybe());

282
    defrag_states(std::move(todo), current);
283
284
  }

285
  void twa_graph::purge_dead_states()
286
287
  {
    unsigned num_states = g_.num_states();
288
289
290
291
292
    std::vector<unsigned> useful(num_states, 0);

    // Make a DFS to compute a topological order.
    std::vector<unsigned> order;
    order.reserve(num_states);
293

294
295
    bool purge_unreachable_needed = false;

296
    if (is_existential())
297
      {
298
299
300
301
        std::vector<std::pair<unsigned, unsigned>> todo; // state, edge
        useful[get_init_state_number()] = 1;
        todo.emplace_back(init_number_, g_.state_storage(init_number_).succ);
        do
302
          {
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
            unsigned src;
            unsigned tid;
            std::tie(src, tid) = todo.back();
            if (tid == 0U)
              {
                todo.pop_back();
                order.emplace_back(src);
                continue;
              }
            auto& t = g_.edge_storage(tid);
            todo.back().second = t.next_succ;
            unsigned dst = t.dst;
            if (useful[dst] != 1)
              {
                todo.emplace_back(dst, g_.state_storage(dst).succ);
                useful[dst] = 1;
              }
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
350
        while (!todo.empty());
      }
    else
      {
        // state, edge, begin, end
        std::vector<std::tuple<unsigned, unsigned,
                               const unsigned*, const unsigned*>> todo;
        auto& dests = g_.dests_vector();

        auto beginend = [&](const unsigned& dst,
                            const unsigned*& begin, const unsigned*& end)
          {
            if ((int)dst < 0)
              {
                begin = dests.data() + ~dst + 1;
                end = begin + dests[~dst];
              }
            else
              {
                begin = &dst;
                end = begin + 1;
              }
          };
        {
          const unsigned* begin;
          const unsigned* end;
          beginend(init_number_, begin, end);
          todo.emplace_back(init_number_, 0U, begin, end);
        }

351
        for (;;)
352
          {
353
354
355
356
357
            unsigned& tid = std::get<1>(todo.back());
            const unsigned*& begin = std::get<2>(todo.back());
            const unsigned*& end = std::get<3>(todo.back());
            if (tid == 0U && begin == end)
              {
358
                unsigned src = std::get<0>(todo.back());
359
                todo.pop_back();
360
361
362
363
                // Last transition from a state?
                if ((int)src >= 0 && (todo.empty()
                                      || src != std::get<0>(todo.back())))
                  order.emplace_back(src);
364
365
                if (todo.empty())
                  break;
366
367
                else
                  continue;
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
              }
            unsigned dst = *begin++;
            if (begin == end)
              {
                if (tid != 0)
                  tid = g_.edge_storage(tid).next_succ;
                if (tid != 0)
                  beginend(g_.edge_storage(tid).dst, begin, end);
              }
            if (useful[dst] != 1)
              {
                auto& ss = g_.state_storage(dst);
                unsigned succ = ss.succ;
                if (succ == 0U)
                  continue;
                useful[dst] = 1;
                const unsigned* begin;
                const unsigned* end;
                beginend(g_.edge_storage(succ).dst, begin, end);
                todo.emplace_back(dst, succ, begin, end);
              }
389
          }
390
391
      }

392
393
394
    // At this point, all reachable states with successors are marked
    // as useful.
    for (;;)
395
      {
396
397
398
399
        bool univ_edge_erased = false;
        // Process states in topological order to mark those without
        // successors as useless.
        for (auto s: order)
400
          {
401
402
403
            auto t = g_.out_iteraser(s);
            bool useless = true;
            while (t)
404
              {
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
                // An edge is useful if all its
                // destinations are useful.
                bool usefuledge = true;
                for (unsigned d: univ_dests(t->dst))
                  if (!useful[d])
                    {
                      usefuledge = false;
                      break;
                    }
                // Erase any useless edge
                if (!usefuledge)
                  {
                    if (is_univ_dest(t->dst))
                      univ_edge_erased = true;
                    t.erase();
                    continue;
                  }
                // if we have a edge to a useful state, then the
                // state is useful.
                useless = false;
                ++t;
426
              }
427
428
            if (useless)
              useful[s] = 0;
429
          }
430
431
432
433
434
435
436
437
438
439
        // If we have erased any universal destination, it is possible
        // that we have have created some new dead states, so we
        // actually need to redo the whole thing again until there is
        // no more universal edge to remove.  Also we might have
        // created some unreachable states, so we will simply call
        // purge_unreachable_states() later to clean this.
        if (!univ_edge_erased)
          break;
        else
          purge_unreachable_needed = true;
440
441
      }

442
443
444
    // Is the initial state actually useful?  If not, make this an
    // empty automaton by resetting the graph.
    bool usefulinit = true;
445
    for (unsigned d: univ_dests(init_number_))
446
      if (!useful[d])
447
        {
448
          usefulinit = false;
449
450
451
          break;
        }
    if (!usefulinit)
452
453
454
455
456
457
458
459
460
      {
        g_ = graph_t();
        init_number_ = new_state();
        prop_universal(true);
        prop_complete(false);
        prop_stutter_invariant(true);
        prop_weak(true);
        return;
      }
461

462
    // Renumber each used state.
463
    unsigned current = 0;
464
465
    for (unsigned s = 0; s < num_states; ++s)
      if (useful[s])
466
        useful[s] = current++;
467
      else
468
        useful[s] = -1U;
469
    if (current == num_states)
470
      return;                        // No useless state.
471
472

    // Removing some non-deterministic dead state could make the
473
474
475
    // automaton universal.  Likewise for non-complete.
    if (prop_universal().is_false())
      prop_universal(trival::maybe());
476
477
478
    if (prop_complete().is_false())
      prop_complete(trival::maybe());

479
    defrag_states(std::move(useful), current);
480
481
482

    if (purge_unreachable_needed)
      purge_unreachable_states();
483
484
485
  }

  void twa_graph::defrag_states(std::vector<unsigned>&& newst,
486
                                unsigned used_states)
487
  {
488
    if (!is_existential())
489
      {
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
        // Running defrag_states() on alternating automata is tricky,
        // because we want to
        // #1 rename the regular states
        // #2 rename the states in universal destinations
        // #3 get rid of the unused universal destinations
        // #4 merge identical universal destinations
        //
        // graph::degrag_states() actually does only #1. It it could
        // do #2, but that would prevent use from doing #3 and #4.  It
        // cannot do #3 and #4 because the graph object does not know
        // what an initial state is, and our initial state might be
        // universal.
        //
        // As a consequence this code preforms #2, #3, and #4 before
        // calling graph::degrag_states() to finish with #1.  We clear
        // the "dests vector" of the current automaton, recreate all
        // the new destination groups using a univ_dest_mapper to
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
507
        // simplify and unify them, and extend newst with some new
508
509
510
        // entries that will point the those new universal destination
        // so that graph::defrag_states() does not have to deal with
        // universal destination in any way.
511
512
513
        auto& g = get_graph();
        auto& dests = g.dests_vector();

514
        // Clear the destination vector, saving the old one.
515
516
        std::vector<unsigned> old_dests;
        std::swap(dests, old_dests);
517
518
        // dests will be updated as a side effect of declaring new
        // destination groups to uniq.
519
520
        internal::univ_dest_mapper<twa_graph::graph_t> uniq(g);

521
522
523
524
525
526
527
528
529
        // The newst entry associated to each of the old destination
        // group.
        std::vector<unsigned> seen(old_dests.size(), -1U);

        // Rename a state if it denotes a universal destination.  This
        // function has to be applied to the destination of each edge,
        // as well as to the initial state.  The need to work on the
        // initial state is the reason it cannot be implemented in
        // graph::defrag_states().
530
531
532
533
534
535
536
        auto fixup = [&](unsigned& in_dst)
          {
            unsigned dst = in_dst;
            if ((int) dst >= 0)       // not a universal edge
              return;
            dst = ~dst;
            unsigned& nd = seen[dst];
537
            if (nd == -1U)      // An unprocessed destination group
538
              {
539
                // store all renamed destination states in tmp
540
541
542
543
544
545
546
547
548
549
550
551
                std::vector<unsigned> tmp;
                auto begin = old_dests.data() + dst + 1;
                auto end = begin + old_dests[dst];
                while (begin != end)
                  {
                    unsigned n = newst[*begin++];
                    if (n == -1U)
                      continue;
                    tmp.emplace_back(n);
                  }
                if (tmp.empty())
                  {
552
553
554
                    // All destinations of this group were marked for
                    // removal.  Mark this universal transition for
                    // removal as well.  Is this really what we expect?
555
556
557
558
                    nd = -1U;
                  }
                else
                  {
559
560
561
562
                    // register this new destination group, add et two
                    // newst, and use the index in newst to relabel
                    // the state so that graph::degrag_states() will
                    // eventually update it to the correct value.
563
564
565
566
567
568
569
570
571
572
573
574
                    nd = newst.size();
                    newst.emplace_back(uniq.new_univ_dests(tmp.begin(),
                                                           tmp.end()));
                  }
              }
            in_dst = nd;
          };
        fixup(init_number_);
        for (auto& e: edges())
          fixup(e.dst);
      }

575
    if (auto* names = get_named_prop<std::vector<std::string>>("state-names"))
576
      {
577
578
579
580
581
582
        unsigned size = names->size();
        for (unsigned s = 0; s < size; ++s)
          {
            unsigned dst = newst[s];
            if (dst == s || dst == -1U)
              continue;
583
            assert(dst < s);
584
585
586
            (*names)[dst] = std::move((*names)[s]);
          }
        names->resize(used_states);
587
      }
588
589
590
591
592
593
594
595
596
597
598
599
    if (auto hs = get_named_prop<std::map<unsigned, unsigned>>
        ("highlight-states"))
      {
        std::map<unsigned, unsigned> hs2;
        for (auto p: *hs)
          {
            unsigned dst = newst[p.first];
            if (dst != -1U)
              hs2[dst] = p.second;
          }
        std::swap(*hs, hs2);
      }
600
601
602
603
604
605
606
607
608
609
610
611
612
    if (auto os = get_named_prop<std::vector<unsigned>>("original-states"))
      {
        unsigned size = os->size();
        for (unsigned s = 0; s < size; ++s)
          {
            unsigned dst = newst[s];
            if (dst == s || dst == -1U)
              continue;
            assert(dst < s);
            (*os)[dst] = (*os)[s];
          }
        os->resize(used_states);
      }
613
614
615
616
617
618
619
620
621
622
623
624
625
    if (auto dl = get_named_prop<std::vector<unsigned>>("degen-levels"))
      {
        unsigned size = dl->size();
        for (unsigned s = 0; s < size; ++s)
          {
            unsigned dst = newst[s];
            if (dst == s || dst == -1U)
              continue;
            assert(dst < s);
            (*dl)[dst] = (*dl)[s];
          }
        dl->resize(used_states);
      }
626
627
628
629
630
631
632
633
634
635
    if (auto ss = get_named_prop<std::vector<unsigned>>("simulated-states"))
      {
        for (auto& s : *ss)
          {
            if (s >= newst.size())
              s = -1U;
            else
              s = newst[s];
          }
      }
636
    init_number_ = newst[init_number_];
637
    g_.defrag_states(std::move(newst), used_states);
638
  }
639
640
641
642
643
644
645
646
647
648

  void twa_graph::remove_unused_ap()
  {
    if (ap().empty())
      return;
    std::set<bdd> conds;
    bdd all = ap_vars();
    for (auto& e: g_.edges())
      {
        all = bdd_exist(all, bdd_support(e.cond));
649
        if (all == bddtrue)    // All APs are used.
650
651
652
653
654
655
656
657
658
659
          return;
      }
    auto d = get_dict();
    while (all != bddtrue)
      {
        unregister_ap(bdd_var(all));
        all = bdd_high(all);
      }
  }

660
661
662
663
  void twa_graph::copy_state_names_from(const const_twa_graph_ptr& other)
  {
    if (other == shared_from_this())
      return;
664

665
    auto orig = get_named_prop<std::vector<unsigned>>("original-states");
666
    auto lvl = get_named_prop<std::vector<unsigned>>("degen-levels");
667
668
    auto sims = get_named_prop<std::vector<unsigned>>("simulated-states");

669
670
    assert(!lvl || orig);

671
672
673
674
    if (orig && sims)
      throw std::runtime_error("copy_state_names_from(): original-states and "
                               "simulated-states are both set");

675
676
677
    if (orig && orig->size() != num_states())
      throw std::runtime_error("copy_state_names_from(): unexpected size "
                               "for original-states");
678
679
680
    if (lvl && lvl->size() != num_states())
      throw std::runtime_error("copy_state_names_from(): unexpected size "
                               "for degen-levels");
681

682
683
684
685
    if (sims && sims->size() != other->num_states())
      throw std::runtime_error("copy_state_names_from(): unexpected size "
                               "for simulated-states");

686
687
688
689
690
691
692
    auto names = std::unique_ptr<std::vector<std::string>>
      (new std::vector<std::string>);
    unsigned ns = num_states();
    unsigned ons = other->num_states();

    for (unsigned s = 0; s < ns; ++s)
      {
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
        std::string newname = "";
        if (sims)
          {
            for (unsigned t = 0; t < ons; ++t)
              {
                if (s == (*sims)[t])
                  newname += other->format_state(t) + ',';
              }
            assert(!newname.empty());
            newname.pop_back(); // remove trailing comma
            newname = '[' + newname + ']';
          }
        else
          {
            unsigned other_s = orig ? (*orig)[s] : s;
            if (other_s >= ons)
              throw std::runtime_error("copy_state_names_from(): state does not"
                                       " exist in source automaton");
            newname = other->format_state(other_s);
712
713
            if (lvl)
              newname += '#' + std::to_string((*lvl)[s]);
714
715
          }
        names->emplace_back(newname);
716
717
718
719
      }

    set_named_prop("state-names", names.release());
  }
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
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
  namespace
  {
    twa_graph_ptr
    copy(const const_twa_ptr& aut, twa::prop_set p,
         bool preserve_names, unsigned max_states)
    {
      twa_graph_ptr out = make_twa_graph(aut->get_dict());
      out->copy_acceptance_of(aut);
      out->copy_ap_of(aut);
      out->prop_copy(aut, p);

      std::vector<std::string>* names = nullptr;
      std::set<unsigned>* incomplete = nullptr;

      // Old highlighting maps
      typedef std::map<unsigned, unsigned> hmap;
      hmap* ohstates = nullptr;
      hmap* ohedges = nullptr;
      const_twa_graph_ptr aut_g = nullptr;
      // New highlighting maps
      hmap* nhstates = nullptr;
      hmap* nhedges = nullptr;

      if (preserve_names)
        {
          names = new std::vector<std::string>;
          out->set_named_prop("state-names", names);

          // If the input is a twa_graph and we were asked to preserve
          // names, also preserve highlights.
          aut_g = std::dynamic_pointer_cast<const twa_graph>(aut);
          if (aut_g)
            {
              ohstates = aut->get_named_prop<hmap>("highlight-states");
              if (ohstates)
                nhstates = out->get_or_set_named_prop<hmap>("highlight-states");
              ohedges = aut->get_named_prop<hmap>("highlight-edges");
              if (ohedges)
                nhedges = out->get_or_set_named_prop<hmap>("highlight-edges");
            }
        }

      // States already seen.
      state_map<unsigned> seen;
      // States to process
      std::deque<state_map<unsigned>::const_iterator> todo;

      auto new_state = [&](const state* s) -> unsigned
        {
          auto p = seen.emplace(s, 0);
          if (p.second)
            {
              p.first->second = out->new_state();
              todo.emplace_back(p.first);
              if (names)
                names->emplace_back(aut->format_state(s));
              if (ohstates)
                {
                  auto q = ohstates->find(aut_g->state_number(s));
                  if (q != ohstates->end())
                    nhstates->emplace(p.first->second, q->second);
                }
            }
          else
            {
              s->destroy();
            }
          return p.first->second;
        };

      out->set_init_state(new_state(aut->get_init_state()));
      while (!todo.empty())
        {
          const state* src1;
          unsigned src2;
          std::tie(src1, src2) = *todo.front();
          todo.pop_front();
          for (auto* t: aut->succ(src1))
            {
              unsigned edgenum = 0;
              if (SPOT_UNLIKELY(max_states < out->num_states()))
                {
                  // If we have reached the max number of state, never try
                  // to create a new one.
                  auto i = seen.find(t->dst());
                  if (i == seen.end())
                    {
                      if (!incomplete)
                        incomplete = new std::set<unsigned>;
                      incomplete->insert(src2);
                      continue;
                    }
                  edgenum = out->new_edge(src2, i->second, t->cond(), t->acc());
                }
              else
                {
                  edgenum = out->new_edge(src2, new_state(t->dst()),
                                          t->cond(), t->acc());
                }
              if (ohedges)
                {
                  auto q = ohedges->find(aut_g->edge_number(t));
                  if (q != ohedges->end())
                    nhedges->emplace(edgenum, q->second);
                }
            }
        }


      auto s = seen.begin();
      while (s != seen.end())
        {
          // Advance the iterator before deleting the "key" pointer.
          const state* ptr = s->first;
          ++s;
          ptr->destroy();
        }

      if (incomplete)
        out->set_named_prop("incomplete-states", incomplete);
      return out;
    }
  }

  twa_graph_ptr make_twa_graph(const const_twa_ptr& aut, twa::prop_set p,
                               bool preserve_names, unsigned max_states)
  {
    if (max_states == -1U && !preserve_names)
      if (auto a = std::dynamic_pointer_cast<const twa_graph>(aut))
        return std::make_shared<twa_graph>(a, p);
    return copy(aut, p, preserve_names, max_states);
  }
853
}