determinize.cc 21.8 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
3
// Copyright (C) 2015, 2016 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
#include <algorithm>
21
#include <deque>
22
#include <stack>
23
24
#include <utility>
#include <unordered_map>
25
26
#include <set>
#include <map>
27

28
29
30
31
32
33
34

#include <spot/misc/bddlt.hh>
#include <spot/twaalgos/sccinfo.hh>
#include <spot/twaalgos/determinize.hh>
#include <spot/twaalgos/degen.hh>
#include <spot/twaalgos/sccfilter.hh>
#include <spot/twaalgos/simulation.hh>
35

36
37
38

namespace spot
{
39
40
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
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
  namespace node_helper
  {
    using brace_t = unsigned;
    void renumber(std::vector<brace_t>& braces,
                  const std::vector<unsigned>& decr_by);
    void truncate_braces(std::vector<brace_t>& braces,
                         const std::vector<unsigned>& rem_succ_of,
                         std::vector<size_t>& nb_braces);
  };

  class safra_state
  {
  public:
    using state_t = unsigned;
    using color_t = unsigned;
    using bdd_id_t = unsigned;
    using nodes_t = std::map<state_t, std::vector<node_helper::brace_t>>;
    using succs_t = std::vector<std::pair<safra_state, bdd_id_t>>;
    using safra_node_t = std::pair<state_t, std::vector<node_helper::brace_t>>;

    bool operator<(const safra_state& other) const;
    // Printh the number of states in each brace
    safra_state(state_t state_number, bool init_state = false,
                bool acceptance_scc = false);
    // Given a certain transition_label, compute all the successors of that
    // label, and return that new node.
    void
    compute_succs(const const_twa_graph_ptr& aut,
                  succs_t& res,
                  const scc_info& scc,
                  const std::map<int, bdd>& implications,
                  const std::vector<bool>& is_connected,
                  std::unordered_map<bdd, unsigned, bdd_hash>& bdd2num,
                  std::vector<bdd>& all_bdds,
                  bool scc_opt,
                  bool use_bisimulation,
                  bool use_stutter) const;
    // Compute successor for transition ap
    safra_state
    compute_succ(const const_twa_graph_ptr& aut,
                 const bdd& ap,
                 const scc_info& scc,
                 const std::map<int, bdd>& implications,
                 const std::vector<bool>& is_connected,
                 bool scc_opt,
                 bool use_bisimulation) const;
    // scc_id has to be an accepting SCC.  This function tries to find a node
    // who lives in that SCC and if it does, we return the brace_id of that SCC.
    unsigned find_scc_brace_id(unsigned scc_id, const scc_info& scc);
    // The outermost brace of each node cannot be green
    void ungreenify_last_brace();
    // When a nodes a implies a node b, remove the node a.
    void merge_redundant_states(const std::map<int, bdd>& implications,
                                const scc_info& scc,
                                const std::vector<bool>& is_connected);
    // Used when creating the list of successors
    // A new intermediate node is created with  src's braces and with dst as id
    // A merge is done if dst already existed in *this
    void update_succ(const std::vector<node_helper::brace_t>& braces,
                     state_t dst, const acc_cond::mark_t acc);
    // Return the emitted color, red or green
    color_t finalize_construction();
    // A list of nodes similar to the ones of a
    // safra tree.  These are constructed in the same way as the powerset
    // algorithm.
    nodes_t nodes_;
    // A counter that indicates the nomber of states within a brace.
    // This enables us to compute the red value
    std::vector<size_t> nb_braces_;
    // A bitfield to know if a brace can emit green.
    std::vector<bool> is_green_;
    color_t color_;
  };

113
114
  namespace
  {
115
116
    using power_set = std::map<safra_state, int>;
    const char* const sub[10] =
117
118
119
120
121
122
123
124
125
126
127
128
      {
	"\u2080",
	"\u2081",
	"\u2082",
	"\u2083",
	"\u2084",
	"\u2085",
	"\u2086",
	"\u2087",
	"\u2088",
	"\u2089",
      };
129
130
131
132
133
134
135
136
137
138
139
140
141

    std::string subscript(unsigned start)
    {
      std::string res;
      do
        {
          res = sub[start % 10] + res;
          start /= 10;
        }
      while (start);
      return res;
    }

142
143
144
145
146
147
148
149
150
    // Returns true if lhs has a smaller nesting pattern than rhs
    // If lhs and rhs are the same, return false.
    bool nesting_cmp(const std::vector<node_helper::brace_t>& lhs,
                     const std::vector<node_helper::brace_t>& rhs)
    {
      size_t m = std::min(lhs.size(), rhs.size());
      size_t i = 0;
      for (; i < m; ++i)
        {
151
152
          if (lhs[i] != rhs[i])
            return lhs[i] < rhs[i];
153
154
155
156
        }
      return lhs.size() > rhs.size();
    }

157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
    // Used to remove all acceptance whos value is above and equal max_acc
    void remove_dead_acc(twa_graph_ptr& aut, unsigned max_acc)
    {
      assert(max_acc < 32);
      unsigned mask = (1 << max_acc) - 1;
      for (auto& t: aut->edges())
	{
	  t.acc &= mask;
	}
    }

    struct compare
    {
      bool
      operator() (const safra_state::safra_node_t& lhs,
		  const safra_state::safra_node_t& rhs)
173
      {
174
	return lhs.second < rhs.second;
175
      }
176
    };
177

178
179
180
    // Return the sorteds nodes in ascending order
    std::vector<safra_state::safra_node_t>
    sorted_nodes(const safra_state::nodes_t& nodes)
181
    {
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
      std::vector<safra_state::safra_node_t> res;
      for (auto& n: nodes)
	res.emplace_back(n.first, n.second);
      std::sort(res.begin(), res.end(), compare());
      return res;
    }

    std::string
    nodes_to_string(const safra_state::nodes_t& states)
    {
      auto copy = sorted_nodes(states);
      std::ostringstream os;
      std::stack<unsigned> s;
      bool first = true;
      for (auto& n: copy)
	{
	  auto it = n.second.begin();
	  // Find brace on top of stack in vector
	  // If brace is not present, then we close it as no other ones of that
	  // type will be found since we ordered our vector
	  while (!s.empty())
	    {
	      it = std::lower_bound(n.second.begin(), n.second.end(),
				    s.top());
	      if (it == n.second.end() || *it != s.top())
		{
		  os << subscript(s.top()) << '}';
		  s.pop();
		}
	      else
		{
		  if (*it == s.top())
		    ++it;
		  break;
		}
	    }
	  // Add new braces
	  while (it != n.second.end())
	    {
	      os << '{' << subscript(*it);
	      s.push(*it);
	      ++it;
	      first = true;
	    }
	  if (!first)
	    os << ' ';
	  os << n.first;
	  first = false;
	}
      // Finish unwinding stack to print last braces
      while (!s.empty())
	{
	  os << subscript(s.top()) << '}';
	  s.pop();
	}
      return os.str();
    }

    std::vector<std::string>*
    print_debug(std::map<safra_state, int>& states)
    {
      auto res = new std::vector<std::string>(states.size());
      for (auto& p: states)
	(*res)[p.second] = nodes_to_string(p.first.nodes_);
      return res;
247
    }
248

249
250
  }

251
252
253
254
255

  std::vector<bool> find_scc_paths(const scc_info& scc);

  unsigned
  safra_state::find_scc_brace_id(unsigned scc_id, const scc_info& scc)
256
  {
257
    for (auto& n: nodes_)
258
      {
259
260
	if (scc_id == scc.scc_of(n.first))
	  return n.second.front();
261
      }
262
263
264
265
266
267
268
269
270
271
272
273
274
275
    return -1U;
  }

  safra_state
  safra_state::compute_succ(const const_twa_graph_ptr& aut,
			    const bdd& ap,
			    const scc_info& scc,
			    const std::map<int, bdd>& implications,
			    const std::vector<bool>& is_connected,
			    bool scc_opt,
			    bool use_bisimulation) const
  {
    safra_state ss = safra_state(nb_braces_.size());
    for (auto& node: nodes_)
276
      {
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
	for (auto& t: aut->out(node.first))
	  {
	    if (!bdd_implies(ap, t.cond))
	      continue;
	    // Check if we are leaving the SCC, if so we delete all the
	    // braces as no cycles can be found with that node
	    if (scc_opt && scc.scc_of(node.first) != scc.scc_of(t.dst))
	      if (scc.is_accepting_scc(scc.scc_of(t.dst)))
		{
		  // Find scc_id in the safra state currently being
		  // constructed
		  unsigned scc_id = ss.find_scc_brace_id(scc.scc_of(t.dst),
							 scc);
		  // If SCC is present in node use the same id
		  if (scc_id != -1U)
		    ss.update_succ({ scc_id }, t.dst,
				   { /* empty */ });
		  // Create a new SCC
		  else
		    ss.update_succ({ /* no braces */ }, t.dst,
				   { 0 });
		}
	      else
		// When entering non accepting SCC don't create any braces
		ss.update_succ({ /* no braces */ }, t.dst, { /* empty */ });
	    else
	      ss.update_succ(node.second, t.dst, t.acc);
	    assert(ss.nb_braces_.size() == ss.is_green_.size());
	  }
306
      }
307
308
309
310
311
    if (use_bisimulation)
      ss.merge_redundant_states(implications, scc, is_connected);
    ss.ungreenify_last_brace();
    ss.color_ = ss.finalize_construction();
    return ss;
312
  }
313

314
315
316
317
318
319
320
321
322
323
324
325
  void
  safra_state::compute_succs(const const_twa_graph_ptr& aut,
			     succs_t& res,
			     const scc_info& scc,
			     const std::map<int, bdd>& implications,
			     const std::vector<bool>& is_connected,
			     std::unordered_map<bdd, unsigned, bdd_hash>&
			     bdd2num,
			     std::vector<bdd>& all_bdds,
			     bool scc_opt,
			     bool use_bisimulation,
			     bool use_stutter) const
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
351
352
353
354
355
356
357
358
359
360
361
362
    for (auto& ap: all_bdds)
      {
	safra_state ss = *this;

	if (use_stutter && aut->prop_stutter_invariant())
	  {
	    std::vector<color_t> colors;
	    unsigned int counter = 0;
	    std::map<safra_state, unsigned int> safra2id;
	    bool stop = false;
	    while (!stop)
	      {
		auto pair = safra2id.insert({ss, counter++});
		// insert should never fail
		assert(pair.second);
		ss = ss.compute_succ(aut, ap, scc, implications, is_connected,
				     scc_opt, use_bisimulation);
		colors.push_back(ss.color_);
		stop = safra2id.find(ss) != safra2id.end();
	      }
	    // Add color of final transition that loops back
	    colors.push_back(ss.color_);
	    unsigned int loop_start = safra2id[ss];
	    for (auto& min: safra2id)
	      {
		if (min.second >= loop_start && ss < min.first)
		  ss = min.first;
	      }
	    ss.color_ = *std::min_element(colors.begin(), colors.end());
	  }
	else
	  ss = compute_succ(aut, ap, scc, implications, is_connected,
			    scc_opt, use_bisimulation);
	unsigned bdd_idx = bdd2num[ap];
	res.emplace_back(ss, bdd_idx);
      }
363
364
  }

365
366
367
368
369
370
371
372
373
374
375
376
377
378
  void
  safra_state::merge_redundant_states(const std::map<int, bdd>& implications,
                                      const scc_info& scc,
                                      const std::vector<bool>& is_connected)
  {
    std::vector<int> to_remove;
    for (auto& n1: nodes_)
      {
        for (auto& n2: nodes_)
          {
            if (n1 == n2)
              continue;
            // index to see if there is a path from scc2 -> scc1
            unsigned idx = scc.scc_count() * scc.scc_of(n2.first) +
379
	      scc.scc_of(n1.first);
380
381
            if (bdd_implies(implications.at(n1.first),
                            implications.at(n2.first)) && !is_connected[idx])
382
383
384
	      {
		to_remove.push_back(n1.first);
	      }
385
386
387
388
389
390
391
392
393
394
395
396
          }
      }
    for (auto& n: to_remove)
      {
        for (auto& brace: nodes_[n])
          {
            --nb_braces_[brace];
          }
        nodes_.erase(n);
      }
  }

397
398
399
400
401
  void safra_state::ungreenify_last_brace()
  {
    // Step A4: For a brace to emit green it must surround other braces.
    // Hence, the last brace cannot emit green as it is the most inside brace.
    for (auto& n: nodes_)
402
403
404
405
      {
        if (!n.second.empty())
          is_green_[n.second.back()] = false;
      }
406
407
  }

408
  safra_state::color_t safra_state::finalize_construction()
409
  {
410
411
    unsigned red = -1U;
    unsigned green = -1U;
412
413
414
    std::vector<unsigned> rem_succ_of;
    assert(is_green_.size() == nb_braces_.size());
    for (unsigned i = 0; i < is_green_.size(); ++i)
415
416
417
      {
        if (nb_braces_[i] == 0)
          {
418
            // Step A3: Brackets that do not contain any nodes emit red
419
            is_green_[i] = false;
420
421
422
423

            // First brace can now be zero with new optim making it possible to
            // emit red 0
            red = std::min(red, 2 * i);
424
          }
425
426
        else if (is_green_[i])
          {
427
            green = std::min(green, 2 * i + 1);
428
429
430
            // Step A4 Emit green
            rem_succ_of.emplace_back(i);
          }
431
432
433
      }
    for (auto& n: nodes_)
      {
434
        // Step A4 Remove all brackets inside each green pair
435
        node_helper::truncate_braces(n.second, rem_succ_of, nb_braces_);
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
      }

    // Step A5 define the rem variable
    std::vector<unsigned> decr_by(nb_braces_.size());
    unsigned decr = 0;
    for (unsigned i = 0; i < nb_braces_.size(); ++i)
      {
        // Step A5 renumber braces
        nb_braces_[i - decr] = nb_braces_[i];
        if (nb_braces_[i] == 0)
          {
            ++decr;
          }
        // Step A5, renumber braces
        decr_by[i] = decr;
      }
    nb_braces_.resize(nb_braces_.size() - decr);
    for (auto& n: nodes_)
      {
455
        node_helper::renumber(n.second, decr_by);
456
      }
457
    return std::min(red, green);
458
459
  }

460
461
  void node_helper::renumber(std::vector<brace_t>& braces,
                             const std::vector<unsigned>& decr_by)
462
  {
463
    for (unsigned idx = 0; idx < braces.size(); ++idx)
464
      {
465
        braces[idx] -= decr_by[braces[idx]];
466
467
468
469
      }
  }

  void
470
  node_helper::truncate_braces(std::vector<brace_t>& braces,
471
472
			       const std::vector<unsigned>& rem_succ_of,
			       std::vector<size_t>& nb_braces)
473
  {
474
    for (unsigned idx = 0; idx < braces.size(); ++idx)
475
476
477
478
479
      {
        bool found = false;
        // find first brace that matches rem_succ_of
        for (auto s: rem_succ_of)
          {
480
            found |= braces[idx] == s;
481
482
483
          }
        if (found)
          {
484
            assert(idx < braces.size() - 1);
485
486
            // For each deleted brace, decrement elements of nb_braces
            // This corresponds to A4 step
487
            for (unsigned i = idx + 1; i < braces.size(); ++i)
488
              {
489
                --nb_braces[braces[i]];
490
              }
491
            braces.resize(idx + 1);
492
493
494
495
496
            break;
          }
      }
  }

497
  void safra_state::update_succ(const std::vector<node_helper::brace_t>& braces,
498
                                state_t dst, const acc_cond::mark_t acc)
499
  {
500
501
502
    std::vector<node_helper::brace_t> copy = braces;
    if (acc.count())
      {
503
        assert(acc.has(0) && acc.count() == 1 && "Only TBA are accepted");
504
        // Accepting edge generate new braces: step A1
505
506
507
508
509
510
511
512
513
        copy.emplace_back(nb_braces_.size());
        // nb_braces_ gets updated later so put 0 for now
        nb_braces_.emplace_back(0);
        // Newly created braces cannot emit green as they won't have
        // any braces inside them (by construction)
        is_green_.push_back(false);
      }
    auto i = nodes_.emplace(dst, copy);
    if (!i.second)
514
      {
515
516
517
        // Step A2: Only keep the smallest nesting pattern (i-e  braces_) for
        // identical nodes.  Nesting_cmp returnes true if copy is smaller
        if (nesting_cmp(copy, i.first->second))
518
          {
519
520
521
522
            // Remove brace count of replaced node
            for (auto b: i.first->second)
              --nb_braces_[b];
            i.first->second = std::move(copy);
523
524
          }
        else
525
          // Node already exists and has bigger nesting pattern value
526
527
          return;
      }
528
529
530
    // After inserting new node, update the brace count per node
    for (auto b: i.first->second)
      ++nb_braces_[b];
531
532
533
  }

  // Called only to initialize first state
534
  safra_state::safra_state(state_t val, bool init_state, bool accepting_scc)
535
536
537
538
  {
    if (init_state)
      {
        unsigned state_num = val;
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
        if (!accepting_scc)
          {
            std::vector<node_helper::brace_t> braces = { /* no braces */ };
            nodes_.emplace(state_num, std::move(braces));
          }
        else
          {
            std::vector<node_helper::brace_t> braces = { 0 };
            nodes_.emplace(state_num, std::move(braces));
            // First brace has init_state hence one state inside the first
            // braces.
            nb_braces_.push_back(1);
            // One brace set
            is_green_.push_back(true);
          }
554
555
556
557
558
      }
    else
      {
        unsigned nb_braces = val;
        // One brace set
559
        is_green_.assign(nb_braces, true);
560
        // Newly created states are the empty mocrstate
561
562
563
564
565
        nb_braces_.assign(nb_braces, 0);
      }
  }

  bool
566
  safra_state::operator<(const safra_state& other) const
567
  {
568
569
570
571
572
573
574
575
576
577
578
579
    if (nodes_ == other.nodes_)
      {
        for (auto& n: nodes_)
          {
            auto it = other.nodes_.find(n.first);
            assert(it != other.nodes_.end());
            if (nesting_cmp(n.second, it->second))
              return true;
          }
        return false;
      }

580
    return nodes_ < other.nodes_;
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
  std::vector<bool>
  find_scc_paths(const scc_info& scc)
  {
    unsigned scccount = scc.scc_count();
    std::vector<bool> res(scccount * scccount, 0);
    for (unsigned i = 0; i < scccount; ++i)
      res[i + scccount * i] = 1;
    for (unsigned i = 0; i < scccount; ++i)
      {
        std::stack<unsigned> s;
        s.push(i);
        while (!s.empty())
          {
            unsigned src = s.top();
            s.pop();
            for (auto& d: scc.succ(src))
              {
                s.push(d);
                unsigned idx = scccount * i + d;
                res[idx] = 1;
              }
          }
      }
    return res;
  }

609
  twa_graph_ptr
610
611
612
  tgba_determinisation(const const_twa_graph_ptr& a,
                       bool pretty_print, bool scc_opt,
		       bool use_bisimulation, bool use_stutter)
613
  {
614
    // Degeneralize
615
    twa_graph_ptr aut = spot::degeneralize_tba(a);
616
    std::map<int, bdd> implications;
617
618
619
620
621
    if (use_bisimulation)
      {
        aut = spot::scc_filter(aut);
        aut = simulation(aut, &implications);
      }
622
    scc_info scc = scc_info(aut);
623
    std::vector<bool> is_connected = find_scc_paths(scc);
624
625
626
627
628
629

    bdd allap = bddtrue;
    {
      typedef std::set<bdd, bdd_less_than> sup_map;
      sup_map sup;
      // Record occurrences of all guards
630
      for (auto& t: aut->edges())
631
632
633
634
635
636
637
638
639
640
641
642
        sup.emplace(t.cond);
      for (auto& i: sup)
        allap &= bdd_support(i);
    }

    // Preprocessing
    // Used to convert atomic bdd to id
    std::unordered_map<bdd, unsigned, bdd_hash> bdd2num;
    std::vector<bdd> num2bdd;
    // Nedded for compute succs
    // Used to convert large bdd to indexes
    std::unordered_map<bdd, std::pair<unsigned, unsigned>, bdd_hash> deltas;
643
    std::vector<safra_state::bdd_id_t> bddnums;
644
    for (auto& t: aut->edges())
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
      {
        auto it = deltas.find(t.cond);
        if (it == deltas.end())
          {
            bdd all = t.cond;
            unsigned prev = bddnums.size();
            while (all != bddfalse)
              {
                bdd one = bdd_satoneset(all, allap, bddfalse);
                all -= one;
                auto p = bdd2num.emplace(one, num2bdd.size());
                if (p.second)
                  num2bdd.push_back(one);
                bddnums.emplace_back(p.first->second);
              }
            deltas[t.cond] = std::make_pair(prev, bddnums.size());
          }
      }

664
665
666
    auto res = make_twa_graph(aut->get_dict());
    res->copy_ap_of(aut);
    res->prop_copy(aut,
667
                   { false, // state based
668
669
670
671
		       false, // inherently_weak
		       false, // deterministic
		       true // stutter inv
		       });
672
673

    // Given a safra_state get its associated state in output automata.
674
    // Required to create new edges from 2 safra-state
675
    power_set seen;
676
677
    auto init_state = aut->get_init_state_number();
    bool start_accepting = scc.is_accepting_scc(scc.scc_of(init_state)) ||
678
      !scc_opt;
679
    safra_state init(init_state, true, start_accepting);
680
681
682
683
684
    unsigned num = res->new_state();
    res->set_init_state(num);
    seen.insert(std::make_pair(init, num));
    std::deque<safra_state> todo;
    todo.push_back(init);
685
    unsigned sets = 0;
686
687
    using succs_t = safra_state::succs_t;
    succs_t succs;
688
689
690
691
692
    while (!todo.empty())
      {
        safra_state curr = todo.front();
        unsigned src_num = seen.find(curr)->second;
        todo.pop_front();
693
        curr.compute_succs(aut, succs, scc, implications, is_connected,
694
695
                           bdd2num, num2bdd, scc_opt, use_bisimulation,
                           use_stutter);
696
697
        for (auto s: succs)
          {
698
            // Don't construct sink state as complete does a better job at this
699
            if (s.first.nodes_.empty())
700
              continue;
701
702
703
704
705
706
707
708
709
710
711
712
            auto i = seen.find(s.first);
	    unsigned dst_num;
	    if (i != seen.end())
	      {
		dst_num = i->second;
	      }
	    else
	      {
                dst_num = res->new_state();
                todo.push_back(s.first);
                seen.insert(std::make_pair(s.first, dst_num));
              }
713
            if (s.first.color_ != -1U)
714
              {
715
                res->new_edge(src_num, dst_num, num2bdd[s.second],
716
			      {s.first.color_});
717
718
                // We only care about green acc which are odd
                if (s.first.color_ % 2 == 1)
719
720
                  sets = std::max(s.first.color_ + 1, sets);
              }
721
            else
722
              res->new_edge(src_num, dst_num, num2bdd[s.second]);
723
          }
724
        succs.clear();
725
      }
726
    remove_dead_acc(res, sets);
727
728
    // Acceptance is now min(odd) since we con emit Red on paths 0 with new opti
    res->set_acceptance(sets, acc_cond::acc_code::parity(false, true, sets));
729
    res->prop_deterministic(true);
730
    res->prop_state_acc(false);
731

732
733
    if (pretty_print)
      res->set_named_prop("state-names", print_debug(seen));
734
735
736
    return res;
  }
}