emptiness.cc 23.4 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
// Copyright (C) 2009, 2011-2018 Laboratoire de Recherche et
3
// 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 "config.h"
24
#include <sstream>
25
#include <memory>
26
27
#include <spot/twaalgos/emptiness.hh>
#include <spot/twaalgos/bfssteps.hh>
28
#include <spot/twaalgos/couvreurnew.hh>
29
30
31
32
33
34
35
36
#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>
37
#include <spot/twaalgos/product.hh>
38
39
40

namespace spot
{
41
42
43

  // emptiness_check_result
  //////////////////////////////////////////////////////////////////////
44

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

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

57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
  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&)
  {
  }


72
73
74
  // emptiness_check
  //////////////////////////////////////////////////////////////////////

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

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

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

91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
  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;
  }

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

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

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

    ec_algo ec_algos[] =
      {
133
        { "Cou99",     couvreur99,                    0, -1U },
134
135
        { "Cou99new",  get_couvreur99_new,            0, -1U },
        { "Cou99abs",  get_couvreur99_new_abstract,   0, -1U },
136
137
138
139
140
        { "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 },
141
142
143
144
      };
  }

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

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

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

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

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

    const char* opt_str = strchr(name, '(');
    option_map o;
    if (opt_str)
      {
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
        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;
          }
194
195
196
197
198
199
200
201
202
203
204
205
206
207
      }

    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)
208
209
        {
          *err = nullptr;
210

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

225
  // twa_run
226
227
  //////////////////////////////////////////////////////////////////////

228
229
230
231
232
233
234
235
236
237
238
239
240
  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)
      {
241
        s.s = s.s->clone();
242
        prefix.emplace_back(s);
243
244
245
      }
    for (step s : run.cycle)
      {
246
        s.s = s.s->clone();
247
        cycle.emplace_back(s);
248
249
250
251
252
253
254
255
      }
  }

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

  std::ostream&
263
  operator<<(std::ostream& os, const twa_run& run)
264
  {
265
    auto& a = run.aut;
266
267
268
269
270
271
272
    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)
273
        os << '\t' << st.acc;
274
275
276
      os << '\n';
    };

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

286
287
288
289
290
291
292
  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");
  }

293
294
  namespace
  {
295
    class shortest_path final: public bfs_steps
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
322
    {
    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)
      {
323
        return this->bfs_steps::search(filter(start), l);
324
325
326
      }

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

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

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

  twa_run_ptr twa_run::reduce() const
  {
354
    ensure_non_empty_cycle("twa_run::reduce()");
355
356
357
358
359
360
361
362
363
364
365
366
367
368
    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.
369
    acc_cond::mark_t seen_acc = {};
370
371
372
373
    twa_run::steps::const_iterator seg = cycle.end();
    do
      {
        assert(seg != cycle.begin());
374
        --seg;
375
376
377
378
379
380
381
        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.
382
    seen_acc = {};
383
384
385
386
387
    do
      {
        assert(seg != cycle.end());
        seen_acc |= seg->acc;

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

391
        ++seg;
392
393
394
395
396
397
398
399
400
401
402
403
      }
    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);
404
        (void)s;
405
406
407
408
409
410
411
      }

    // 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();
412
         i != res->cycle.end(); ++i)
413
414
415
416
417
418
419
420
421
422
423
424
      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())
      {
425
426
427
        // The initial state is on the cycle.
        prefix_start->destroy();
        cycle_entry_point = *ps;
428
429
430
      }
    else
      {
431
        // This initial state is outside the cycle.  Compute the prefix.
432
433
434
435
436
437
        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();
438
439
         cycle_ep_it != res->cycle.end()
           && cycle_entry_point->compare(cycle_ep_it->s); ++cycle_ep_it)
440
441
442
443
444
      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,
445
                      res->cycle.begin(), cycle_ep_it);
446
447
448
449

    return res;
  }

450
451
452
453
454
455
456
457
  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"))
      {
458
        auto a = down_cast<const_twa_graph_ptr>(aut);
459
460
461
        if (!a)
          throw std::runtime_error("twa_run::project() confused: "
                                   "product-states found in a non-twa_graph");
462
        auto oth = down_cast<const_twa_graph_ptr>(other);
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
511
        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;
  }


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

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

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

    if (s->compare(i->s))
      {
542
543
544
545
546
547
548
        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;
549
550
551
552
      }

    for (; i != l->end(); ++serial)
      {
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
        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";
              }
          }
694
695
696
697
      }
    s->destroy();
    if (!aut->acc().accepting(all_acc))
      {
698
699
700
701
702
703
704
        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;
705
706
      }

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

    return true;
  }

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

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

    unsigned src = a->get_init_state_number();
    auto l = prefix.empty() ? &cycle : &prefix;
    auto e = l->end();
    for (auto i = l->begin(); i != e;)
      {
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
        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))
755
          if (t.dst == dst && bdd_implies(label, t.cond) && t.acc == acc)
756
757
758
759
760
            {
              (*h)[a->get_graph().index_of_edge(t)] = color;
              break;
            }
        src = dst;
761
762
763
      }
  }

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

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

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

786
    state_map<unsigned> seen;
787

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

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

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

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

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

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

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


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

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

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

868
    s->destroy();
869

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

874
}