simulation.cc 25.3 KB
Newer Older
Thomas Badie's avatar
Thomas Badie committed
1
// -*- coding: utf-8 -*-
2
3
// Copyright (C) 2012-2017 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
Thomas Badie's avatar
Thomas Badie committed
4
5
6
7
8
//
// 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
9
// the Free Software Foundation; either version 3 of the License, or
Thomas Badie's avatar
Thomas Badie committed
10
11
12
13
14
15
16
17
// (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
18
// along with this program.  If not, see <http://www.gnu.org/licenses/>.
Thomas Badie's avatar
Thomas Badie committed
19
20
21
22

#include <queue>
#include <map>
#include <utility>
Thomas Badie's avatar
Thomas Badie committed
23
24
#include <cmath>
#include <limits>
25
26
27
28
29
30
31
#include <spot/twaalgos/simulation.hh>
#include <spot/misc/minato.hh>
#include <spot/twa/bddprint.hh>
#include <spot/twaalgos/reachiter.hh>
#include <spot/twaalgos/sccfilter.hh>
#include <spot/twaalgos/sccinfo.hh>
#include <spot/twaalgos/sepsets.hh>
32
#include <spot/twaalgos/isdet.hh>
33
#include <spot/misc/bddlt.hh>
Thomas Badie's avatar
Thomas Badie committed
34

35
//  Simulation-based reduction, implemented using bdd-based signatures.
Thomas Badie's avatar
Thomas Badie committed
36
//
37
38
39
40
//  The signature of a state is a Boolean function (implemented as a
//  BDD) representing the set of outgoing transitions of that state.
//  Two states with the same signature are equivalent and can be
//  merged.
Thomas Badie's avatar
Thomas Badie committed
41
//
42
43
44
45
46
47
48
49
// We define signatures in a way that implications between signatures
//  entail language inclusion.  These inclusions are used to remove
//  redundant transitions, but this occurs implicitly while
//  transforming the signature into irredundant-sum-of-product before
//  building the automaton: redundant terms that are left over
//  correspond to ignored transitions.
//
//  See our Spin'13 paper for background on this procedure.
Thomas Badie's avatar
Thomas Badie committed
50

Thomas Badie's avatar
Thomas Badie committed
51
52
53
54
55
namespace spot
{
  namespace
  {
    // Used to get the signature of the state.
56
    typedef std::vector<bdd> vector_state_bdd;
Thomas Badie's avatar
Thomas Badie committed
57
58

    // Get the list of state for each class.
59
    typedef std::map<bdd, std::list<unsigned>,
Thomas Badie's avatar
Thomas Badie committed
60
61
                     bdd_less_than> map_bdd_lstate;

Thomas Badie's avatar
Thomas Badie committed
62
63
    // This class helps to compare two automata in term of
    // size.
64
    struct automaton_size final
65
66
    {
      automaton_size()
67
        : edges(0),
68
69
70
71
          states(0)
      {
      }

72
      automaton_size(const twa_graph_ptr& a)
73
        : edges(a->num_edges()),
74
75
76
77
          states(a->num_states())
      {
      }

78
      void set_size(const twa_graph_ptr& a)
79
      {
80
81
        states = a->num_states();
        edges = a->num_edges();
82
83
      }

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
84
      inline bool operator!=(const automaton_size& r)
85
      {
86
        return edges != r.edges || states != r.states;
87
88
      }

Thomas Badie's avatar
Thomas Badie committed
89
90
91
92
93
94
95
      inline bool operator<(const automaton_size& r)
      {
        if (states < r.states)
          return true;
        if (states > r.states)
          return false;

96
        if (edges < r.edges)
Thomas Badie's avatar
Thomas Badie committed
97
          return true;
98
        if (edges > r.edges)
Thomas Badie's avatar
Thomas Badie committed
99
100
101
102
103
104
105
106
107
108
109
110
          return false;

        return false;
      }

      inline bool operator>(const automaton_size& r)
      {
        if (states < r.states)
          return false;
        if (states > r.states)
          return true;

111
        if (edges < r.edges)
Thomas Badie's avatar
Thomas Badie committed
112
          return false;
113
        if (edges > r.edges)
Thomas Badie's avatar
Thomas Badie committed
114
115
116
117
118
          return true;

        return false;
      }

119
      int edges;
120
121
      int states;
    };
Thomas Badie's avatar
Thomas Badie committed
122

Thomas Badie's avatar
Thomas Badie committed
123
    // The direct_simulation. If Cosimulation is true, we are doing a
124
125
    // cosimulation.
    template <bool Cosimulation, bool Sba>
126
    class direct_simulation final
Thomas Badie's avatar
Thomas Badie committed
127
    {
Thomas Badie's avatar
Thomas Badie committed
128
    protected:
129
      typedef std::map<bdd, bdd, bdd_less_than> map_bdd_bdd;
130
      int acc_vars;
131
      acc_cond::mark_t all_inf_;
132
    public:
133
134
135

      bdd mark_to_bdd(acc_cond::mark_t m)
      {
136
137
138
139
140
        // FIXME: Use a cache.
        bdd res = bddtrue;
        for (auto n: m.sets())
          res &= bdd_ithvar(acc_vars + n);
        return res;
141
142
      }

143
      acc_cond::mark_t bdd_to_mark(bdd b)
144
      {
145
146
147
148
        // FIXME: Use a cache.
        std::vector<unsigned> res;
        while (b != bddtrue)
          {
149
            res.emplace_back(bdd_var(b) - acc_vars);
150
151
152
            b = bdd_high(b);
          }
        return acc_cond::mark_t(res.begin(), res.end());
153
154
      }

155
      direct_simulation(const const_twa_graph_ptr& in)
156
        : po_size_(0),
Thomas Badie's avatar
Thomas Badie committed
157
          all_class_var_(bddtrue),
158
          original_(in)
159
      {
160
161
162
        if (!has_separate_sets(in))
          throw std::runtime_error
            ("direct_simulation() requires separate Inf and Fin sets");
163
        if (!in->is_existential())
164
165
          throw std::runtime_error
            ("direct_simulation() does not yet support alternation");
166

167
168
        scc_info_.reset(new scc_info(in));

169
170
        unsigned ns = in->num_states();
        size_a_ = ns;
171
        unsigned init_state_number = in->get_init_state_number();
172
173
174
175
176
177
178
179
180
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

        auto all_inf = in->get_acceptance().used_inf_fin_sets().first;
        all_inf_ = all_inf;

        // Replace all the acceptance conditions by their complements.
        // (In the case of Cosimulation, we also flip the edges.)
        if (Cosimulation)
          {
            a_ = make_twa_graph(in->get_dict());
            a_->copy_ap_of(in);
            a_->copy_acceptance_of(in);
            a_->new_states(ns);

            for (unsigned s = 0; s < ns; ++s)
              {
                for (auto& t: in->out(s))
                  {
                    acc_cond::mark_t acc;
                    if (Sba)
                      {
                        // If the acceptance is interpreted as
                        // state-based, to apply the reverse simulation
                        // on a SBA, we should pull the acceptance of
                        // the destination state on its incoming arcs
                        // (which now become outgoing arcs after
                        // transposition).
                        acc = 0U;
                        for (auto& td: in->out(t.dst))
                          {
                            acc = td.acc ^ all_inf;
                            break;
                          }
                      }
                    else
                      {
                        acc = t.acc ^ all_inf;
                      }
                    a_->new_edge(t.dst, s, t.cond, acc);
                  }
                a_->set_init_state(init_state_number);
              }
          }
        else
          {
            a_ = make_twa_graph(in, twa::prop_set::all());
            for (auto& t: a_->edges())
              t.acc ^= all_inf;
          }
        assert(a_->num_states() == size_a_);

222
223
        want_implications_ = !is_deterministic(a_);

224
225
226
227
228
229
230
231
232
233
234
235
236
        // Now, we have to get the bdd which will represent the
        // class. We register one bdd by state, because in the worst
        // case, |Class| == |State|.
        unsigned set_num = a_->get_dict()
          ->register_anonymous_variables(size_a_ + 1, this);

        unsigned n_acc = a_->num_sets();
        acc_vars = a_->get_dict()
          ->register_anonymous_variables(n_acc, this);

        all_proms_ = bddtrue;
        for (unsigned v = acc_vars; v < acc_vars + n_acc; ++v)
          all_proms_ &= bdd_ithvar(v);
Thomas Badie's avatar
Thomas Badie committed
237

Thomas Badie's avatar
Thomas Badie committed
238
        bdd_initial = bdd_ithvar(set_num++);
239
        bdd init = bdd_ithvar(set_num++);
240

241
        used_var_.emplace_back(init);
242

243
244
245
246
        // Initialize all classes to init.
        previous_class_.resize(size_a_);
        for (unsigned s = 0; s < size_a_; ++s)
          previous_class_[s] = init;
Thomas Badie's avatar
Thomas Badie committed
247

248
249
250
251
252
253
        // Put all the anonymous variable in a queue, and record all
        // of these in a variable all_class_var_ which will be used
        // to understand the destination part in the signature when
        // building the resulting automaton.
        all_class_var_ = init;
        for (unsigned i = set_num; i < set_num + size_a_ - 1; ++i)
Thomas Badie's avatar
Thomas Badie committed
254
255
256
257
258
          {
            free_var_.push(i);
            all_class_var_ &= bdd_ithvar(i);
          }

259
        relation_[init] = init;
260
      }
Thomas Badie's avatar
Thomas Badie committed
261
262


263
264
265
      // Reverse all the acceptance condition at the destruction of
      // this object, because it occurs after the return of the
      // function simulation.
Thomas Badie's avatar
Thomas Badie committed
266
      virtual ~direct_simulation()
267
      {
268
        a_->get_dict()->unregister_all_my_variables(this);
269
      }
Thomas Badie's avatar
Thomas Badie committed
270

271
      // Update the name of the classes.
272
273
      void update_previous_class()
      {
274
        std::list<bdd>::iterator it_bdd = used_var_.begin();
275

276
277
        // We run through the map bdd/list<state>, and we update
        // the previous_class_ with the new data.
278
        for (auto& p: sorted_classes_)
Thomas Badie's avatar
Thomas Badie committed
279
          {
280
281
282
283
284
285
            // If the signature of a state is bddfalse (no
            // edges) the class of this state is bddfalse
            // instead of an anonymous variable. It allows
            // simplifications in the signature by removing a
            // edge which has as a destination a state with
            // no outgoing edge.
286
287
            if (p->first == bddfalse)
              for (unsigned s: p->second)
288
289
                previous_class_[s] = bddfalse;
            else
290
              for (unsigned s: p->second)
291
292
                previous_class_[s] = *it_bdd;
            ++it_bdd;
Thomas Badie's avatar
Thomas Badie committed
293
          }
294
295
      }

Thomas Badie's avatar
Thomas Badie committed
296
      void main_loop()
297
      {
298
299
300
301
        unsigned int nb_partition_before = 0;
        unsigned int nb_po_before = po_size_ - 1;
        while (nb_partition_before != bdd_lstate_.size()
               || nb_po_before != po_size_)
Thomas Badie's avatar
Thomas Badie committed
302
          {
303
            update_previous_class();
Thomas Badie's avatar
Thomas Badie committed
304
305
306
307
308
            nb_partition_before = bdd_lstate_.size();
            nb_po_before = po_size_;
            po_size_ = 0;
            update_sig();
            go_to_next_it();
309
            // print_partition();
Thomas Badie's avatar
Thomas Badie committed
310
311
          }

312
        update_previous_class();
Thomas Badie's avatar
Thomas Badie committed
313
314
315
      }

      // The core loop of the algorithm.
316
      twa_graph_ptr run(std::vector<bdd>* implications = nullptr)
Thomas Badie's avatar
Thomas Badie committed
317
318
      {
        main_loop();
319
        return build_result(implications);
320
      }
Thomas Badie's avatar
Thomas Badie committed
321

322
      // Take a state and compute its signature.
323
      bdd compute_sig(unsigned src)
324
      {
Thomas Badie's avatar
Thomas Badie committed
325
        bdd res = bddfalse;
Thomas Badie's avatar
Thomas Badie committed
326

327
        for (auto& t: a_->out(src))
Thomas Badie's avatar
Thomas Badie committed
328
          {
329
            bdd acc = mark_to_bdd(t.acc);
330

331
332
333
334
            // to_add is a conjunction of the acceptance condition,
            // the label of the edge and the class of the
            // destination and all the class it implies.
            bdd to_add = acc & t.cond & relation_[previous_class_[t.dst]];
Thomas Badie's avatar
Thomas Badie committed
335

336
337
            res |= to_add;
          }
Thomas Badie's avatar
Thomas Badie committed
338

Thomas Badie's avatar
Thomas Badie committed
339
        // When we Cosimulate, we add a special flag to differentiate
340
        // the initial state from the other.
341
        if (Cosimulation && src == a_->get_init_state_number())
Thomas Badie's avatar
Thomas Badie committed
342
343
344
          res |= bdd_initial;

        return res;
345
346
      }

Thomas Badie's avatar
Thomas Badie committed
347

348
349
      void update_sig()
      {
350
351
        bdd_lstate_.clear();
        sorted_classes_.clear();
352
        for (unsigned s = 0; s < size_a_; ++s)
353
354
355
356
357
358
359
360
361
          {
            bdd sig = compute_sig(s);
            auto p = bdd_lstate_.emplace(std::piecewise_construct,
                                         std::make_tuple(sig),
                                         std::make_tuple());
            p.first->second.emplace_back(s);
            if (p.second)
              sorted_classes_.emplace_back(p.first);
          }
362
      }
Thomas Badie's avatar
Thomas Badie committed
363
364


365
      // This method renames the color set, updates the partial order.
366
367
      void go_to_next_it()
      {
368
        int nb_new_color = bdd_lstate_.size() - used_var_.size();
Thomas Badie's avatar
Thomas Badie committed
369

Thomas Badie's avatar
Thomas Badie committed
370
371
372

        // If we have created more partitions, we need to use more
        // variables.
373
        for (int i = 0; i < nb_new_color; ++i)
Thomas Badie's avatar
Thomas Badie committed
374
375
          {
            assert(!free_var_.empty());
376
            used_var_.emplace_back(bdd_ithvar(free_var_.front()));
Thomas Badie's avatar
Thomas Badie committed
377
378
379
            free_var_.pop();
          }

Thomas Badie's avatar
Thomas Badie committed
380
381
382

        // If we have reduced the number of partition, we 'free' them
        // in the free_var_ list.
383
        for (int i = 0; i > nb_new_color; --i)
384
385
386
387
388
389
390
          {
            assert(!used_var_.empty());
            free_var_.push(bdd_var(used_var_.front()));
            used_var_.pop_front();
          }


391
        assert((bdd_lstate_.size() == used_var_.size())
392
393
               || (bdd_lstate_.find(bddfalse) != bdd_lstate_.end()
                   && bdd_lstate_.size() == used_var_.size() + 1));
Thomas Badie's avatar
Thomas Badie committed
394

395
396
397
398
399
        // This vector links the tuple "C^(i-1), N^(i-1)" to the
        // new class coloring for the next iteration.
        std::vector<std::pair<bdd, bdd>> now_to_next;
        unsigned sz = bdd_lstate_.size();
        now_to_next.reserve(sz);
Thomas Badie's avatar
Thomas Badie committed
400

401
        std::list<bdd>::iterator it_bdd = used_var_.begin();
Thomas Badie's avatar
Thomas Badie committed
402

403
        for (auto& p: sorted_classes_)
Thomas Badie's avatar
Thomas Badie committed
404
          {
405
406
407
408
409
            // If the signature of a state is bddfalse (no edges) the
            // class of this state is bddfalse instead of an anonymous
            // variable. It allows simplifications in the signature by
            // removing an edge which has as a destination a state
            // with no outgoing edge.
410
            bdd acc = bddfalse;
411
            if (p->first != bddfalse)
412
              acc = *it_bdd;
413
            now_to_next.emplace_back(p->first, acc);
414
            ++it_bdd;
Thomas Badie's avatar
Thomas Badie committed
415
416
          }

417
        // Update the partial order.
418

419
420
421
422
423
424
425
        // This loop follows the pattern given by the paper.
        // foreach class do
        // |  foreach class do
        // |  | update po if needed
        // |  od
        // od

426
        for (unsigned n = 0; n < sz; ++n)
Thomas Badie's avatar
Thomas Badie committed
427
          {
428
429
            bdd n_sig = now_to_next[n].first;
            bdd n_class = now_to_next[n].second;
430
431
432
433
434
435
436
437
438
439
440
            if (want_implications_)
              for (unsigned m = 0; m < sz; ++m)
                {
                  if (n == m)
                    continue;
                  if (bdd_implies(n_sig, now_to_next[m].first))
                    {
                      n_class &= now_to_next[m].second;
                      ++po_size_;
                    }
                }
441
            relation_[now_to_next[n].second] = n_class;
Thomas Badie's avatar
Thomas Badie committed
442
          }
443
444
445
      }

      // Build the minimal resulting automaton.
446
      twa_graph_ptr build_result(std::vector<bdd>* implications = nullptr)
447
      {
448
449
450
        twa_graph_ptr res = make_twa_graph(a_->get_dict());
        res->copy_ap_of(a_);
        res->copy_acceptance_of(a_);
451

452
453
454
455
        auto state_mapping = new std::vector<unsigned>();
        state_mapping->resize(a_->num_states());
        res->set_named_prop("simulated-states", state_mapping);

456
457
        // Non atomic propositions variables (= acc and class)
        bdd nonapvars = all_proms_ & bdd_support(all_class_var_);
458

459
        auto* gb = res->create_namer<int>();
460

461
462
        if (implications)
          implications->resize(bdd_lstate_.size());
463
464
        // Create one state per class.
        for (auto& p: sorted_classes_)
Thomas Badie's avatar
Thomas Badie committed
465
          {
466
            bdd cl = previous_class_[p->second.front()];
467
468
469
470
            // A state may be referred to either by
            // its class, or by all the implied classes.
            auto s = gb->new_state(cl.id());
            gb->alias_state(s, relation_[cl].id());
471
            // update state_mapping
472
            for (auto& st : p->second)
473
              (*state_mapping)[st] = s;
474
475
            if (implications)
              (*implications)[s] = relation_[cl];
Thomas Badie's avatar
Thomas Badie committed
476
477
          }

478
479
480
481
        // Acceptance of states.  Only used if Sba && Cosimulation.
        std::vector<acc_cond::mark_t> accst;
        if (Sba && Cosimulation)
          accst.resize(res->num_states(), 0U);
482

483
        stat.states = bdd_lstate_.size();
484
        stat.edges = 0;
485

Thomas Badie's avatar
Thomas Badie committed
486
487
488
        unsigned nb_satoneset = 0;
        unsigned nb_minato = 0;

489
490
491
        auto all_inf = all_inf_;
        // For each class, we will create
        // all the edges between the states.
492
        for (auto& p: sorted_classes_)
Thomas Badie's avatar
Thomas Badie committed
493
          {
494
495
            // All states in p.second have the same class, so just
            // pick the class of the first one first one.
496
            bdd src = previous_class_[p->second.front()];
497
498

            // Get the signature to derive successors.
499
            bdd sig = compute_sig(p->second.front());
Thomas Badie's avatar
Thomas Badie committed
500

Thomas Badie's avatar
Thomas Badie committed
501
502
503
            if (Cosimulation)
              sig = bdd_compose(sig, bddfalse, bdd_var(bdd_initial));

Thomas Badie's avatar
Thomas Badie committed
504
505
506
507
508
509
510
511
512
513
514
            // Get all the variable in the signature.
            bdd sup_sig = bdd_support(sig);

            // Get the variable in the signature which represents the
            // conditions.
            bdd sup_all_atomic_prop = bdd_exist(sup_sig, nonapvars);

            // Get the part of the signature composed only with the atomic
            // proposition.
            bdd all_atomic_prop = bdd_exist(sig, nonapvars);

515
            // First loop over all possible valuations atomic properties.
Thomas Badie's avatar
Thomas Badie committed
516
            while (all_atomic_prop != bddfalse)
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
              {
                bdd one = bdd_satoneset(all_atomic_prop,
                                        sup_all_atomic_prop,
                                        bddtrue);
                all_atomic_prop -= one;

                // For each possible valuation, iterate over all possible
                // destination classes.   We use minato_isop here, because
                // if the same valuation of atomic properties can go
                // to two different classes C1 and C2, iterating on
                // C1 + C2 with the above bdd_satoneset loop will see
                // C1 then (!C1)C2, instead of C1 then C2.
                // With minatop_isop, we ensure that the no negative
                // class variable will be seen (likewise for promises).
                minato_isop isop(sig & one);
532

Thomas Badie's avatar
Thomas Badie committed
533
534
                ++nb_satoneset;

535
536
537
                bdd cond_acc_dest;
                while ((cond_acc_dest = isop.next()) != bddfalse)
                  {
538
                    ++stat.edges;
539

Thomas Badie's avatar
Thomas Badie committed
540
541
                    ++nb_minato;

542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
                    // Take the edge, and keep only the variable which
                    // are used to represent the class.
                    bdd dst = bdd_existcomp(cond_acc_dest,
                                             all_class_var_);

                    // Keep only ones who are acceptance condition.
                    auto acc = bdd_to_mark(bdd_existcomp(cond_acc_dest,
                                                         all_proms_));

                    // Keep the other!
                    bdd cond = bdd_existcomp(cond_acc_dest,
                                             sup_all_atomic_prop);

                    // Because we have complemented all the Inf
                    // acceptance conditions on the input automaton,
                    // we must revert them to create a new edge.
                    acc ^= all_inf;

                    if (Cosimulation)
                      {
                        if (Sba)
                          {
                            // acc should be attached to src, or rather,
                            // in our edge-based representation)
                            // to all edges leaving src.  As we
                            // can't do this here, store this in a table
                            // so we can fix it later.
                            accst[gb->get_state(src.id())] = acc;
                            acc = 0U;
                          }
                        gb->new_edge(dst.id(), src.id(), cond, acc);
                      }
                    else
                      {
                        gb->new_edge(src.id(), dst.id(), cond, acc);
                      }
                  }
              }
Thomas Badie's avatar
Thomas Badie committed
580
581
          }

582
583
        res->set_init_state(gb->get_state(previous_class_
                                          [a_->get_init_state_number()].id()));
Thomas Badie's avatar
Thomas Badie committed
584

585
586
587
        res->merge_edges(); // This helps merging some edges with
                            // identical conditions, but different
                            // mark sets.
Thomas Badie's avatar
Thomas Badie committed
588

589
590
591
592
593
594
595
596
597
598
599
600
601
602
        // Mark all accepting state in a second pass, when
        // dealing with SBA in cosimulation.
        if (Sba && Cosimulation)
          {
            unsigned ns = res->num_states();
            for (unsigned s = 0; s < ns; ++s)
              {
                acc_cond::mark_t acc = accst[s];
                if (acc == 0U)
                  continue;
                for (auto& t: res->out(s))
                  t.acc = acc;
              }
          }
603

604
605
606
607
608
609
610
        // If we recorded implications for the determinization
        // procedure, we should not remove unreachable states, as that
        // will invalidate the contents of the IMPLICATIONS vector.
        // It's OK not to purge the result, as the determinization
        // will only explore the reachable part anyway.
        if (!implications)
          res->purge_unreachable_states();
611

612
        delete gb;
613
614
615
        res->prop_copy(original_,
                       { false, // state-based acc forced below
                         true,  // weakness preserved,
616
                         false, true, // determinism improved
617
                         true, // completeness preserved
618
619
                         true, // stutter inv.
                       });
620
        // !unambiguous and !semi-deterministic are not preserved
621
622
623
624
        if (!Cosimulation && nb_minato == nb_satoneset)
          // Note that nb_minato != nb_satoneset does not imply
          // non-deterministic, because of the merge_edges() above.
          res->prop_universal(true);
625
626
627
        if (Sba)
          res->prop_state_acc(true);
        return res;
628
629
630
631
632
633
634
635
636
637
      }


      // Debug:
      // In a first time, print the signature, and the print a list
      // of each state in this partition.
      // In a second time, print foreach state, who is where,
      // where is the new class name.
      void print_partition()
      {
638
639
640
641
642
643
644
645
646
647
648
        std::cerr << "\n-----\n\nClasses from previous iteration:\n";
        unsigned ps = previous_class_.size();
        for (unsigned p = 0; p < ps; ++p)
          {
            std::cerr << "- " << a_->format_state(a_->state_from_number(p))
                      << " was in class "
                      << bdd_format_set(a_->get_dict(), previous_class_[p])
                      << '\n';
          }
        std::cerr << "\nPartition:\n";
        std::list<bdd>::iterator it_bdd = used_var_.begin();
649
        for (auto& p: sorted_classes_)
Thomas Badie's avatar
Thomas Badie committed
650
          {
651
652
653
654
655
656
            std::cerr << "- ";
            if (p->first != bddfalse)
              std::cerr << "new class " << *it_bdd++ << " from ";
            std::cerr << "sig "
                      << bdd_format_isop(a_->get_dict(), p->first);
            std::cerr << '\n';
657
            for (auto s: p->second)
658
              std::cerr << "    - "
659
660
                        << a_->format_state(a_->state_from_number(s))
                        << '\n';
Thomas Badie's avatar
Thomas Badie committed
661
          }
662
663
664
        std::cerr << "\nClass implications:\n";
        for (auto& p: relation_)
          std::cerr << "  - " << p.first << "  =>  " << p.second << '\n';
Thomas Badie's avatar
Thomas Badie committed
665

666
      }
Thomas Badie's avatar
Thomas Badie committed
667

Thomas Badie's avatar
Thomas Badie committed
668
    protected:
669
      // The automaton which is simulated.
670
      twa_graph_ptr a_;
Thomas Badie's avatar
Thomas Badie committed
671

672
      // Implications between classes.
673
      map_bdd_bdd relation_;
Thomas Badie's avatar
Thomas Badie committed
674

675
      // Represent the class of each state at the previous iteration.
676
      vector_state_bdd previous_class_;
Thomas Badie's avatar
Thomas Badie committed
677

678
      // The list of states for each class at the current_iteration.
679
680
      // Computed in `update_sig'.
      map_bdd_lstate bdd_lstate_;
681
682
683
684
      // The above map, sorted by states number instead of BDD
      // identifier to avoid non-determinism while iterating over all
      // states.
      std::vector<map_bdd_lstate::const_iterator> sorted_classes_;
Thomas Badie's avatar
Thomas Badie committed
685

686
687
688
      // The queue of free bdd. They will be used as the identifier
      // for the class.
      std::queue<int> free_var_;
Thomas Badie's avatar
Thomas Badie committed
689

690
691
      // The list of used bdd. They are in used as identifier for class.
      std::list<bdd> used_var_;
Thomas Badie's avatar
Thomas Badie committed
692

693
694
      // Size of the automaton.
      unsigned int size_a_;
Thomas Badie's avatar
Thomas Badie committed
695

696
      // Used to know when there is no evolution in the partial order.
697
      unsigned int po_size_;
Thomas Badie's avatar
Thomas Badie committed
698

699
700
701
702
      // Whether to compute implications between classes.  This is costly
      // and useless for deterministic automata.
      bool want_implications_;

703
704
      // All the class variable:
      bdd all_class_var_;
Thomas Badie's avatar
Thomas Badie committed
705
706
707
708

      // The flag to say if the outgoing state is initial or not
      bdd bdd_initial;

Thomas Badie's avatar
Thomas Badie committed
709
710
      bdd all_proms_;

711
      automaton_size stat;
712

713
      std::unique_ptr<scc_info> scc_info_;
Thomas Badie's avatar
Thomas Badie committed
714

715
      const const_twa_graph_ptr original_;
Thomas Badie's avatar
Thomas Badie committed
716
717
    };

Thomas Badie's avatar
Thomas Badie committed
718
719
  } // End namespace anonymous.

Thomas Badie's avatar
Thomas Badie committed
720

721
722
  twa_graph_ptr
  simulation(const const_twa_graph_ptr& t)
Thomas Badie's avatar
Thomas Badie committed
723
  {
724
725
726
    direct_simulation<false, false> simul(t);
    return simul.run();
  }
Thomas Badie's avatar
Thomas Badie committed
727

728
729
  twa_graph_ptr
  simulation(const const_twa_graph_ptr& t,
730
             std::vector<bdd>* implications)
731
732
733
734
735
  {
    direct_simulation<false, false> simul(t);
    return simul.run(implications);
  }

736
737
  twa_graph_ptr
  simulation_sba(const const_twa_graph_ptr& t)
738
739
  {
    direct_simulation<false, true> simul(t);
Thomas Badie's avatar
Thomas Badie committed
740
741
742
    return simul.run();
  }

743
744
  twa_graph_ptr
  cosimulation(const const_twa_graph_ptr& t)
Thomas Badie's avatar
Thomas Badie committed
745
  {
746
747
748
    direct_simulation<true, false> simul(t);
    return simul.run();
  }
Thomas Badie's avatar
Thomas Badie committed
749

750
751
  twa_graph_ptr
  cosimulation_sba(const const_twa_graph_ptr& t)
752
753
  {
    direct_simulation<true, true> simul(t);
Thomas Badie's avatar
Thomas Badie committed
754
755
756
    return simul.run();
  }

757
758

  template<bool Sba>
759
760
  twa_graph_ptr
  iterated_simulations_(const const_twa_graph_ptr& t)
761
  {
762
    twa_graph_ptr res = nullptr;
763
764
765
766
767
768
    automaton_size prev;
    automaton_size next;

    do
      {
        prev = next;
769
        direct_simulation<false, Sba> simul(res ? res : t);
770
        res = simul.run();
771
        if (res->prop_universal())
772
          break;
Thomas Badie's avatar
Thomas Badie committed
773

774
        direct_simulation<true, Sba> cosimul(res);
775
        res = cosimul.run();
776

777
778
779
780
        if (Sba)
          res = scc_filter_states(res, false);
        else
          res = scc_filter(res, false);
781
782

        next.set_size(res);
783
784
785
786
787
      }
    while (prev != next);
    return res;
  }

788
789
  twa_graph_ptr
  iterated_simulations(const const_twa_graph_ptr& t)
790
791
792
793
  {
    return iterated_simulations_<false>(t);
  }

794
795
  twa_graph_ptr
  iterated_simulations_sba(const const_twa_graph_ptr& t)
796
797
798
799
  {
    return iterated_simulations_<true>(t);
  }

Thomas Badie's avatar
Thomas Badie committed
800
} // End namespace spot.