emptiness.cc 23.4 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
3
// Copyright (C) 2009, 2011-2017 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
Guillaume Sadegh's avatar
Guillaume Sadegh committed
4
// Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
5
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
6
7
8
9
10
11
// et Marie Curie.
//
// 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
12
// the Free Software Foundation; either version 3 of the License, or
13
14
15
16
17
18
19
20
// (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
21
// along with this program.  If not, see <http://www.gnu.org/licenses/>.
22

23
#include <sstream>
24
#include <memory>
25
26
#include <spot/twaalgos/emptiness.hh>
#include <spot/twaalgos/bfssteps.hh>
27
#include <spot/twaalgos/couvreurnew.hh>
28
29
30
31
32
33
34
35
#include <spot/twaalgos/gtec/gtec.hh>
#include <spot/twaalgos/gv04.hh>
#include <spot/twaalgos/magic.hh>
#include <spot/misc/hash.hh>
#include <spot/twaalgos/se05.hh>
#include <spot/twaalgos/tau03.hh>
#include <spot/twaalgos/tau03opt.hh>
#include <spot/twa/bddprint.hh>
36
#include <spot/twaalgos/product.hh>
37
38
39

namespace spot
{
40
41
42

  // emptiness_check_result
  //////////////////////////////////////////////////////////////////////
43

44
  twa_run_ptr
45
46
  emptiness_check_result::accepting_run()
  {
47
    return nullptr;
48
49
  }

50
51
52
53
54
55
  const unsigned_statistics*
  emptiness_check_result::statistics() const
  {
    return dynamic_cast<const unsigned_statistics*>(this);
  }

56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
  const char*
  emptiness_check_result::parse_options(char* options)
  {
    option_map old(o_);
    const char* s = o_.parse_options(options);
    options_updated(old);
    return s;
  }

  void
  emptiness_check_result::options_updated(const option_map&)
  {
  }


71
72
73
  // emptiness_check
  //////////////////////////////////////////////////////////////////////

74
75
76
77
  emptiness_check::~emptiness_check()
  {
  }

78
79
80
81
82
83
  const unsigned_statistics*
  emptiness_check::statistics() const
  {
    return dynamic_cast<const unsigned_statistics*>(this);
  }

84
85
86
87
88
89
  const ec_statistics*
  emptiness_check::emptiness_check_statistics() const
  {
    return dynamic_cast<const ec_statistics*>(this);
  }

90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
  const char*
  emptiness_check::parse_options(char* options)
  {
    option_map old(o_);
    const char* s = o_.parse_options(options);
    options_updated(old);
    return s;
  }

  void
  emptiness_check::options_updated(const option_map&)
  {
  }

  bool
  emptiness_check::safe() const
  {
    return true;
  }

110
111
112
113
114
  std::ostream&
  emptiness_check::print_stats(std::ostream& os) const
  {
    return os;
  }
115

116
117
118
119
120
121
122
123
  // emptiness_check_instantiator
  //////////////////////////////////////////////////////////////////////

  namespace
  {
    struct ec_algo
    {
      const char* name;
124
      emptiness_check_ptr(*construct)(const const_twa_ptr&,
125
                                      spot::option_map);
126
127
128
129
130
131
      unsigned int min_acc;
      unsigned int max_acc;
    };

    ec_algo ec_algos[] =
      {
132
        { "Cou99",     couvreur99,                    0, -1U },
133
134
        { "Cou99new",  get_couvreur99_new,            0, -1U },
        { "Cou99abs",  get_couvreur99_new_abstract,   0, -1U },
135
136
137
138
139
        { "CVWY90",    magic_search,                  0,   1 },
        { "GV04",      explicit_gv04_check,           0,   1 },
        { "SE05",      se05,                          0,   1 },
        { "Tau03",     explicit_tau03_search,         1, -1U },
        { "Tau03_opt", explicit_tau03_opt_search,     0, -1U },
140
141
142
143
      };
  }

  emptiness_check_instantiator::emptiness_check_instantiator(option_map o,
144
                                                             void* i)
145
146
147
148
149
    : o_(o), info_(i)
  {
  }

  unsigned int
150
  emptiness_check_instantiator::min_sets() const
151
152
153
154
155
  {
    return static_cast<ec_algo*>(info_)->min_acc;
  }

  unsigned int
156
  emptiness_check_instantiator::max_sets() const
157
158
159
160
  {
    return static_cast<ec_algo*>(info_)->max_acc;
  }

161
  emptiness_check_ptr
162
  emptiness_check_instantiator::instantiate(const const_twa_ptr& a) const
163
164
165
166
  {
    return static_cast<ec_algo*>(info_)->construct(a, o_);
  }

167
168
  emptiness_check_instantiator_ptr
  make_emptiness_check_instantiator(const char* name, const char** err)
169
170
171
172
173
174
175
176
177
  {
    // Skip spaces.
    while (*name && strchr(" \t\n", *name))
      ++name;

    const char* opt_str = strchr(name, '(');
    option_map o;
    if (opt_str)
      {
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
        const char* opt_start = opt_str + 1;
        const char* opt_end = strchr(opt_start, ')');
        if (!opt_end)
          {
            *err = opt_start;
            return nullptr;
          }
        std::string opt(opt_start, opt_end);

        const char* res = o.parse_options(opt.c_str());
        if (res)
          {
            *err  = opt.c_str() - res + opt_start;
            return nullptr;
          }
193
194
195
196
197
198
199
200
201
202
203
204
205
206
      }

    if (!opt_str)
      opt_str = name + strlen(name);

    // Ignore spaces before `(' (or trailing spaces).
    while (opt_str > name && strchr(" \t\n", *--opt_str))
      continue;
    std::string n(name, opt_str + 1);


    ec_algo* info = ec_algos;
    for (unsigned i = 0; i < sizeof(ec_algos)/sizeof(*ec_algos); ++i, ++info)
      if (n == info->name)
207
208
        {
          *err = nullptr;
209

210
          struct emptiness_check_instantiator_aux:
211
            public emptiness_check_instantiator
212
213
214
215
216
217
218
219
          {
            emptiness_check_instantiator_aux(option_map o, void* i):
              emptiness_check_instantiator(o, i)
            {
            }
          };
          return std::make_shared<emptiness_check_instantiator_aux>(o, info);
        }
220
    *err = name;
221
    return nullptr;
222
223
  }

224
  // twa_run
225
226
  //////////////////////////////////////////////////////////////////////

227
228
229
230
231
232
233
234
235
236
237
238
239
  twa_run::~twa_run()
  {
    for (auto i : prefix)
      i.s->destroy();
    for (auto i : cycle)
      i.s->destroy();
  }

  twa_run::twa_run(const twa_run& run)
  {
    aut = run.aut;
    for (step s : run.prefix)
      {
240
        s.s = s.s->clone();
241
        prefix.emplace_back(s);
242
243
244
      }
    for (step s : run.cycle)
      {
245
        s.s = s.s->clone();
246
        cycle.emplace_back(s);
247
248
249
250
251
252
253
254
      }
  }

  twa_run&
  twa_run::operator=(const twa_run& run)
  {
    if (&run != this)
      {
255
256
        this->~twa_run();
        new(this) twa_run(run);
257
258
259
260
261
      }
    return *this;
  }

  std::ostream&
262
  operator<<(std::ostream& os, const twa_run& run)
263
  {
264
    auto& a = run.aut;
265
266
267
268
269
270
271
    bdd_dict_ptr d = a->get_dict();

    auto pstep = [&](const twa_run::step& st)
    {
      os << "  " << a->format_state(st.s) << "\n  |  ";
      bdd_print_formula(os, d, st.label);
      if (st.acc)
272
        os << '\t' << st.acc;
273
274
275
      os << '\n';
    };

276
277
    os << "Prefix:\n";
    for (auto& s: run.prefix)
278
      pstep(s);
279
280
    os << "Cycle:\n";
    for (auto& s: run.cycle)
281
282
283
284
      pstep(s);
    return os;
  }

285
286
287
288
289
290
291
  void twa_run::ensure_non_empty_cycle(const char* where) const
  {
    if (cycle.empty())
      throw std::runtime_error(std::string(where)
                               + " expects a non-empty cycle");
  }

292
293
  namespace
  {
294
    class shortest_path final: public bfs_steps
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
    {
    public:
      shortest_path(const const_twa_ptr& a)
        : bfs_steps(a), target(nullptr)
      {
      }

      ~shortest_path()
      {
        state_set::const_iterator i = seen.begin();
        while (i != seen.end())
          {
            const state* ptr = *i;
            ++i;
            ptr->destroy();
          }
      }

      void
      set_target(const state_set* t)
      {
        target = t;
      }

      const state*
      search(const state* start, twa_run::steps& l)
      {
322
        return this->bfs_steps::search(filter(start), l);
323
324
325
      }

      const state*
326
      filter(const state* s) override
327
328
329
330
331
332
333
334
335
336
337
338
339
      {
        state_set::const_iterator i = seen.find(s);
        if (i == seen.end())
          seen.insert(s);
        else
          {
            s->destroy();
            s = *i;
          }
        return s;
      }

      bool
340
      match(twa_run::step&, const state* dest) override
341
342
343
344
345
346
347
348
349
350
351
352
      {
        return target->find(dest) != target->end();
      }

    private:
      state_set seen;
      const state_set* target;
    };
  }

  twa_run_ptr twa_run::reduce() const
  {
353
    ensure_non_empty_cycle("twa_run::reduce()");
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
    auto& a = aut;
    auto res = std::make_shared<twa_run>(a);
    state_set ss;
    shortest_path shpath(a);
    shpath.set_target(&ss);

    // We want to find a short segment of the original cycle that
    // contains all acceptance conditions.

    const state* segment_start; // The initial state of the segment.
    const state* segment_next; // The state immediately after the segment.

    // Start from the end of the original cycle, and rewind until all
    // acceptance sets have been seen.
    acc_cond::mark_t seen_acc = 0U;
    twa_run::steps::const_iterator seg = cycle.end();
    do
      {
        assert(seg != cycle.begin());
373
        --seg;
374
375
376
377
378
379
380
381
382
383
384
385
386
        seen_acc |= seg->acc;
      }
    while (!a->acc().accepting(seen_acc));
    segment_start = seg->s;

    // Now go forward and ends the segment as soon as we have seen all
    // acceptance sets, cloning it in our result along the way.
    seen_acc = 0U;
    do
      {
        assert(seg != cycle.end());
        seen_acc |= seg->acc;

387
        twa_run::step st = { seg->s->clone(), seg->label, seg->acc };
388
        res->cycle.emplace_back(st);
389

390
        ++seg;
391
392
393
394
395
396
397
398
399
400
401
402
      }
    while (!a->acc().accepting(seen_acc));
    segment_next = seg == cycle.end() ? cycle.front().s : seg->s;

    // Close this cycle if needed, that is, compute a cycle going
    // from the state following the segment to its starting state.
    if (segment_start != segment_next)
      {
        ss.insert(segment_start);
        const state* s = shpath.search(segment_next->clone(), res->cycle);
        ss.clear();
        assert(s->compare(segment_start) == 0);
403
        (void)s;
404
405
406
407
408
409
410
      }

    // Compute the prefix: it's the shortest path from the initial
    // state of the automata to any state of the cycle.

    // Register all states from the cycle as target of the BFS.
    for (twa_run::steps::const_iterator i = res->cycle.begin();
411
         i != res->cycle.end(); ++i)
412
413
414
415
416
417
418
419
420
421
422
423
      ss.insert(i->s);

    const state* prefix_start = a->get_init_state();
    // There are two cases: either the initial state is already on
    // the cycle, or it is not.  If it is, we will have to rotate
    // the cycle so it begins on this position.  Otherwise we will shift
    // the cycle so it begins on the state that follows the prefix.
    // cycle_entry_point is that state.
    const state* cycle_entry_point;
    state_set::const_iterator ps = ss.find(prefix_start);
    if (ps != ss.end())
      {
424
425
426
        // The initial state is on the cycle.
        prefix_start->destroy();
        cycle_entry_point = *ps;
427
428
429
      }
    else
      {
430
        // This initial state is outside the cycle.  Compute the prefix.
431
432
433
434
435
436
        cycle_entry_point = shpath.search(prefix_start, res->prefix);
      }

    // Locate cycle_entry_point on the cycle.
    twa_run::steps::iterator cycle_ep_it;
    for (cycle_ep_it = res->cycle.begin();
437
438
         cycle_ep_it != res->cycle.end()
           && cycle_entry_point->compare(cycle_ep_it->s); ++cycle_ep_it)
439
440
441
442
443
      continue;
    assert(cycle_ep_it != res->cycle.end());

    // Now shift the cycle so it starts on cycle_entry_point.
    res->cycle.splice(res->cycle.end(), res->cycle,
444
                      res->cycle.begin(), cycle_ep_it);
445
446
447
448

    return res;
  }

449
450
451
452
453
454
455
456
  twa_run_ptr twa_run::project(const const_twa_ptr& other, bool right)
  {
    unsigned shift = 0;
    if (right)
      shift = aut->num_sets() - other->num_sets();
    auto res = std::make_shared<twa_run>(other);
    if (auto ps = aut->get_named_prop<const product_states>("product-states"))
      {
457
        auto a = down_cast<const_twa_graph_ptr>(aut);
458
459
460
        if (!a)
          throw std::runtime_error("twa_run::project() confused: "
                                   "product-states found in a non-twa_graph");
461
        auto oth = down_cast<const_twa_graph_ptr>(other);
462
463
464
465
466
467
468
469
470
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
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
        if (!oth)
          throw std::runtime_error("twa_run::project() confused: "
                                   "other ought to be a twa_graph");
        if (right)
          {
            for (auto& i: prefix)
              {
                unsigned s = (*ps)[a->state_number(i.s)].second;
                res->prefix.emplace_back(oth->state_from_number(s),
                                         i.label, i.acc >> shift);
              }
            for (auto& i: cycle)
              {
                unsigned s = (*ps)[a->state_number(i.s)].second;
                res->cycle.emplace_back(oth->state_from_number(s),
                                        i.label, i.acc >> shift);
              }
          }
        else
          {
            auto all = oth->acc().all_sets();
            for (auto& i: prefix)
              {
                unsigned s = (*ps)[a->state_number(i.s)].first;
                res->prefix.emplace_back(oth->state_from_number(s),
                                         i.label, i.acc & all);
              }
            for (auto& i: cycle)
              {
                unsigned s = (*ps)[a->state_number(i.s)].first;
                res->cycle.emplace_back(oth->state_from_number(s),
                                        i.label, i.acc & all);
              }
          }
      }
    else
      {
        auto all = other->acc().all_sets();
        for (auto& i: prefix)
          res->prefix.emplace_back(aut->project_state(i.s, other),
                                   i.label, (i.acc >> shift) & all);
        for (auto& i: cycle)
          res->cycle.emplace_back(aut->project_state(i.s, other),
                                  i.label, (i.acc >> shift) & all);
      }
    return res;
  }


511
512
  bool twa_run::replay(std::ostream& os, bool debug) const
  {
513
    ensure_non_empty_cycle("twa_run::replay()");
514
515
516
517
518
519
    const state* s = aut->get_init_state();
    int serial = 1;
    const twa_run::steps* l;
    std::string in;
    acc_cond::mark_t all_acc = 0U;
    bool all_acc_seen = false;
520
    state_map<std::set<int>> seen;
521
522
523

    if (prefix.empty())
      {
524
525
526
527
        l = &cycle;
        in = "cycle";
        if (!debug)
          os << "No prefix.\nCycle:\n";
528
529
530
      }
    else
      {
531
532
533
534
        l = &prefix;
        in = "prefix";
        if (!debug)
          os << "Prefix:\n";
535
536
537
538
539
540
      }

    twa_run::steps::const_iterator i = l->begin();

    if (s->compare(i->s))
      {
541
542
543
544
545
546
547
        if (debug)
          os << "ERROR: First state of run (in " << in << "): "
             << aut->format_state(i->s)
             << "\ndoes not match initial state of automata: "
             << aut->format_state(s) << '\n';
        s->destroy();
        return false;
548
549
550
551
      }

    for (; i != l->end(); ++serial)
      {
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
        if (debug)
          {
            // Keep track of the serial associated to each state so we
            // can note duplicate states and make the replay easier to read.
            auto o = seen.find(s);
            std::ostringstream msg;
            if (o != seen.end())
              {
                for (auto d: o->second)
                  msg << " == " << d;
                o->second.insert(serial);
                s->destroy();
                s = o->first;
              }
            else
              {
                seen[s].insert(serial);
              }
            os << "state " << serial << " in " << in << msg.str() << ": ";
          }
        else
          {
            os << "  ";
          }
        os << aut->format_state(s) << '\n';

        // expected outgoing transition
        bdd label = i->label;
        acc_cond::mark_t acc = i->acc;

        // compute the next expected state
        const state* next;
        ++i;
        if (i != l->end())
          {
            next = i->s;
          }
        else
          {
            if (l == &prefix)
              {
                l = &cycle;
                in = "cycle";
                i = l->begin();
                if (!debug)
                  os << "Cycle:\n";
              }
            next = l->begin()->s;
          }

        // browse the actual outgoing transitions
        twa_succ_iterator* j = aut->succ_iter(s);
        // When not debugging, S is not used as key in SEEN, so we can
        // destroy it right now.
        if (!debug)
          s->destroy();
        if (j->first())
          do
            {
              if (j->cond() != label
                  || j->acc() != acc)
                continue;

              const state* s2 = j->dst();
              if (s2->compare(next))
                {
                  s2->destroy();
                  continue;
                }
              else
                {
                  s = s2;
                  break;
                }
            }
          while (j->next());
        if (j->done())
          {
            if (debug)
              {
                os << "ERROR: no transition with label="
                   << bdd_format_formula(aut->get_dict(), label)
                   << " and acc=" << aut->acc().format(acc)
                   << " leaving state " << serial
                   << " for state " << aut->format_state(next) << '\n'
                   << "The following transitions leave state " << serial
                   << ":\n";
                if (j->first())
                  do
                    {
                      const state* s2 = j->dst();
                      os << "  * label="
                         << bdd_format_formula(aut->get_dict(),
                                               j->cond())
                         << " and acc="
                         << (aut->acc().format
                             (j->acc()))
                         << " going to " << aut->format_state(s2) << '\n';
                      s2->destroy();
                    }
                  while (j->next());
              }
            aut->release_iter(j);
            s->destroy();
            return false;
          }
        if (debug)
          {
            os << "transition with label="
               << bdd_format_formula(aut->get_dict(), label)
               << " and acc=" << aut->acc().format(acc)
               << std::endl;
          }
        else
          {
            os << "  |  ";
            bdd_print_formula(os, aut->get_dict(), label);
            os << '\t';
            aut->acc().format(acc);
            os << std::endl;
          }
        aut->release_iter(j);

        // Sum acceptance conditions.
        //
        // (Beware l and i designate the next step to consider.
        // Therefore if i is at the beginning of the cycle, `acc'
        // contains the acceptance conditions of the last transition
        // in the prefix; we should not account it.)
        if (l == &cycle && i != l->begin())
          {
            all_acc |= acc;
            if (!all_acc_seen && aut->acc().accepting(all_acc))
              {
                all_acc_seen = true;
                if (debug)
                  os << "all acceptance conditions ("
                     << aut->acc().format(all_acc)
                     << ") have been seen\n";
              }
          }
693
694
695
696
      }
    s->destroy();
    if (!aut->acc().accepting(all_acc))
      {
697
698
699
700
701
702
703
        if (debug)
          os << "ERROR: The cycle's acceptance conditions ("
             << aut->acc().format(all_acc)
             << ") do not\nmatch those of the automaton ("
             << aut->acc().format(aut->acc().all_sets())
             << ")\n";
        return false;
704
705
      }

706
    auto o = seen.begin();
707
708
    while (o != seen.end())
      {
709
710
711
712
        // Advance the iterator before deleting the "key" pointer.
        const state* ptr = o->first;
        ++o;
        ptr->destroy();
713
714
715
716
717
      }

    return true;
  }

718
719
720
  /// Note that this works only if the automaton is a twa_graph_ptr.
  void twa_run::highlight(unsigned color)
  {
721
    auto a = down_cast<twa_graph_ptr>(std::const_pointer_cast<twa>(aut));
722
723
724
    if (!a)
      throw std::runtime_error("highlight() only work for twa_graph");

725
726
    auto h = a->get_or_set_named_prop<std::map<unsigned, unsigned>>
      ("highlight-edges");
727
728
729
730
731
732

    unsigned src = a->get_init_state_number();
    auto l = prefix.empty() ? &cycle : &prefix;
    auto e = l->end();
    for (auto i = l->begin(); i != e;)
      {
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
        bdd label = i->label;
        acc_cond::mark_t acc = i->acc;
        unsigned dst;
        ++i;
        if (i != e)
          {
            dst = a->state_number(i->s);
          }
        else if (l == &prefix)
          {
            l = &cycle;
            i = l->begin();
            e = l->end();
            dst = a->state_number(i->s);
          }
        else
          {
            dst = a->state_number(l->begin()->s);
          }

        for (auto& t: a->out(src))
754
          if (t.dst == dst && bdd_implies(label, t.cond) && t.acc == acc)
755
756
757
758
759
            {
              (*h)[a->get_graph().index_of_edge(t)] = color;
              break;
            }
        src = dst;
760
761
762
      }
  }

763
  twa_graph_ptr
764
  twa_run::as_twa(bool preserve_names) const
765
  {
766
    ensure_non_empty_cycle("twa_run::as_twa()");
767
    auto d = aut->get_dict();
768
    auto res = make_twa_graph(d);
769
770
    res->copy_ap_of(aut);
    res->copy_acceptance_of(aut);
771

772
773
774
775
776
777
778
    std::vector<std::string>* names= nullptr;
    if (preserve_names)
      {
        names = new std::vector<std::string>;
        res->set_named_prop("state-names", names);
      }

779
    const state* s = aut->get_init_state();
780
781
    unsigned src;
    unsigned dst;
782
    const twa_run::steps* l;
783
    acc_cond::mark_t seen_acc = 0U;
784

785
    state_map<unsigned> seen;
786

787
788
    if (prefix.empty())
        l = &cycle;
789
    else
790
        l = &prefix;
791

792
    twa_run::steps::const_iterator i = l->begin();
793
794

    assert(s->compare(i->s) == 0);
795
    src = res->new_state();
796
    seen.emplace(i->s, src);
797
798
    if (names)
      names->push_back(aut->format_state(s));
799

800
    for (; i != l->end();)
801
802
803
      {
        // expected outgoing transition
        bdd label = i->label;
804
        acc_cond::mark_t acc = i->acc;
805
806
807
808
809
810
811
812
813
814

        // compute the next expected state
        const state* next;
        ++i;
        if (i != l->end())
          {
            next = i->s;
          }
        else
          {
815
            if (l == &prefix)
816
              {
817
                l = &cycle;
818
819
820
821
822
                i = l->begin();
              }
            next = l->begin()->s;
          }

823
        // browse the actual outgoing transitions and
824
825
826
        // look for next;
        const state* the_next = nullptr;
        for (auto j: aut->succ(s))
827
          {
828
829
            if (j->cond() != label
                || j->acc() != acc)
830
831
              continue;

832
            const state* s2 = j->dst();
833
            if (s2->compare(next) == 0)
834
              {
835
836
837
838
                the_next = s2;
                break;
              }
            s2->destroy();
839
          }
840
        s->destroy();
841
842
        if (!the_next)
          throw std::runtime_error("twa_run::as_twa() unable to replay run");
843
        s = the_next;
844
845


846
847
        auto p = seen.emplace(next, 0);
        if (p.second)
848
849
850
851
852
853
854
855
856
          {
            unsigned ns = res->new_state();
            p.first->second = ns;
            if (names)
              {
                assert(ns = names->size());
                names->push_back(aut->format_state(next));
              }
          }
857
        dst = p.first->second;
858

859
860
        res->new_edge(src, dst, label, acc);
        src = dst;
861
862

        // Sum acceptance conditions.
863
        if (l == &cycle && i != l->begin())
864
          seen_acc |= acc;
865
      }
866

867
    s->destroy();
868

869
    assert(aut->acc().accepting(seen_acc));
870
871
872
    return res;
  }

873
}