simulation.cc 24 KB
Newer Older
Thomas Badie's avatar
Thomas Badie committed
1
// -*- coding: utf-8 -*-
2
3
// Copyright (C) 2012, 2013, 2014, 2015, 2016 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
164
165
        if (in->is_alternating())
          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
278
        // We run through the map bdd/list<state>, and we update
        // the previous_class_ with the new data.
        for (auto& p: bdd_lstate_)
Thomas Badie's avatar
Thomas Badie committed
279
          {
280
281
282
283
284
285
286
287
288
289
290
291
292
            // 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.
            if (p.first == bddfalse)
              for (auto s: p.second)
                previous_class_[s] = bddfalse;
            else
              for (auto s: p.second)
                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
309
310
311
            nb_partition_before = bdd_lstate_.size();
            bdd_lstate_.clear();
            nb_po_before = po_size_;
            po_size_ = 0;
            update_sig();
            go_to_next_it();
          }

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
        for (unsigned s = 0; s < size_a_; ++s)
351
          bdd_lstate_[compute_sig(s)].emplace_back(s);
352
      }
Thomas Badie's avatar
Thomas Badie committed
353
354


355
      // This method renames the color set, updates the partial order.
356
357
      void go_to_next_it()
      {
358
        int nb_new_color = bdd_lstate_.size() - used_var_.size();
Thomas Badie's avatar
Thomas Badie committed
359

Thomas Badie's avatar
Thomas Badie committed
360
361
362

        // If we have created more partitions, we need to use more
        // variables.
363
        for (int i = 0; i < nb_new_color; ++i)
Thomas Badie's avatar
Thomas Badie committed
364
365
          {
            assert(!free_var_.empty());
366
            used_var_.emplace_back(bdd_ithvar(free_var_.front()));
Thomas Badie's avatar
Thomas Badie committed
367
368
369
            free_var_.pop();
          }

Thomas Badie's avatar
Thomas Badie committed
370
371
372

        // If we have reduced the number of partition, we 'free' them
        // in the free_var_ list.
373
        for (int i = 0; i > nb_new_color; --i)
374
375
376
377
378
379
380
          {
            assert(!used_var_.empty());
            free_var_.push(bdd_var(used_var_.front()));
            used_var_.pop_front();
          }


381
        assert((bdd_lstate_.size() == used_var_.size())
382
383
               || (bdd_lstate_.find(bddfalse) != bdd_lstate_.end()
                   && bdd_lstate_.size() == used_var_.size() + 1));
Thomas Badie's avatar
Thomas Badie committed
384

385
386
387
388
389
        // 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
390

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

393
        for (auto& p: bdd_lstate_)
Thomas Badie's avatar
Thomas Badie committed
394
          {
395
396
397
398
399
            // 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.
400
401
402
            bdd acc = bddfalse;
            if (p.first != bddfalse)
              acc = *it_bdd;
403
            now_to_next.emplace_back(p.first, acc);
404
            ++it_bdd;
Thomas Badie's avatar
Thomas Badie committed
405
406
          }

407
        // Update the partial order.
408

409
410
411
412
413
414
415
        // This loop follows the pattern given by the paper.
        // foreach class do
        // |  foreach class do
        // |  | update po if needed
        // |  od
        // od

416
        for (unsigned n = 0; n < sz; ++n)
Thomas Badie's avatar
Thomas Badie committed
417
          {
418
419
            bdd n_sig = now_to_next[n].first;
            bdd n_class = now_to_next[n].second;
420
421
422
423
424
425
426
427
428
429
430
            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_;
                    }
                }
431
            relation_[now_to_next[n].second] = n_class;
Thomas Badie's avatar
Thomas Badie committed
432
          }
433
434
435
      }

      // Build the minimal resulting automaton.
436
      twa_graph_ptr build_result(std::vector<bdd>* implications = nullptr)
437
      {
438
439
440
        twa_graph_ptr res = make_twa_graph(a_->get_dict());
        res->copy_ap_of(a_);
        res->copy_acceptance_of(a_);
441

442
443
        // Non atomic propositions variables (= acc and class)
        bdd nonapvars = all_proms_ & bdd_support(all_class_var_);
444

445
        auto* gb = res->create_namer<int>();
446

447
448
        if (implications)
          implications->resize(bdd_lstate_.size());
449
450
        // Create one state per partition.
        for (auto& p: bdd_lstate_)
Thomas Badie's avatar
Thomas Badie committed
451
          {
452
            bdd cl = previous_class_[p.second.front()];
453
454
455
456
            // 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());
457
458
            if (implications)
              (*implications)[s] = relation_[cl];
Thomas Badie's avatar
Thomas Badie committed
459
460
          }

461
462
463
464
        // Acceptance of states.  Only used if Sba && Cosimulation.
        std::vector<acc_cond::mark_t> accst;
        if (Sba && Cosimulation)
          accst.resize(res->num_states(), 0U);
465

466
        stat.states = bdd_lstate_.size();
467
        stat.edges = 0;
468

Thomas Badie's avatar
Thomas Badie committed
469
470
471
        unsigned nb_satoneset = 0;
        unsigned nb_minato = 0;

472
473
474
475
        auto all_inf = all_inf_;
        // For each class, we will create
        // all the edges between the states.
        for (auto& p: bdd_lstate_)
Thomas Badie's avatar
Thomas Badie committed
476
          {
477
478
479
            // All states in p.second have the same class, so just
            // pick the class of the first one first one.
            bdd src = previous_class_[p.second.front()];
480
481

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

Thomas Badie's avatar
Thomas Badie committed
484
485
486
            if (Cosimulation)
              sig = bdd_compose(sig, bddfalse, bdd_var(bdd_initial));

Thomas Badie's avatar
Thomas Badie committed
487
488
489
490
491
492
493
494
495
496
497
            // 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);

498
            // First loop over all possible valuations atomic properties.
Thomas Badie's avatar
Thomas Badie committed
499
            while (all_atomic_prop != bddfalse)
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
              {
                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);
515

Thomas Badie's avatar
Thomas Badie committed
516
517
                ++nb_satoneset;

518
519
520
                bdd cond_acc_dest;
                while ((cond_acc_dest = isop.next()) != bddfalse)
                  {
521
                    ++stat.edges;
522

Thomas Badie's avatar
Thomas Badie committed
523
524
                    ++nb_minato;

525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
                    // 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
563
564
          }

565
566
        res->set_init_state(gb->get_state(previous_class_
                                          [a_->get_init_state_number()].id()));
Thomas Badie's avatar
Thomas Badie committed
567

568
        res->merge_edges(); // FIXME: is this really needed?
Thomas Badie's avatar
Thomas Badie committed
569

570
571
572
573
574
575
576
577
578
579
580
581
582
583
        // 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;
              }
          }
584

585
586
587
588
589
590
591
        // 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();
592

593
        delete gb;
594
595
596
597
598
599
600
        res->prop_copy(original_,
                       { false, // state-based acc forced below
                         true,  // weakness preserved,
                         true, // determinism checked and overridden below
                               // and "unambiguous" property preserved
                         true, // stutter inv.
                       });
601
602
603
604
605
        // !unambiguous and !semi-deterministic are not preserved
        if (original_->prop_semi_deterministic().is_false())
          res->prop_semi_deterministic(trival::maybe());
        if (original_->prop_unambiguous().is_false())
          res->prop_unambiguous(trival::maybe());
606
607
        if (!Cosimulation)
          res->prop_deterministic(nb_minato == nb_satoneset);
608
609
610
        if (Sba)
          res->prop_state_acc(true);
        return res;
611
612
613
614
615
616
617
618
619
620
      }


      // 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()
      {
621
        for (auto& p: bdd_lstate_)
Thomas Badie's avatar
Thomas Badie committed
622
623
          {
            std::cerr << "partition: "
624
                      << bdd_format_isop(a_->get_dict(), p.first)
Thomas Badie's avatar
Thomas Badie committed
625
                      << std::endl;
626
            for (auto s: p.second)
627
628
629
              std::cerr << "  - "
                        << a_->format_state(a_->state_from_number(s))
                        << '\n';
Thomas Badie's avatar
Thomas Badie committed
630
631
          }

632
        std::cerr << "\nPrevious iteration\n" << std::endl;
Thomas Badie's avatar
Thomas Badie committed
633

634
635
        unsigned ps = previous_class_.size();
        for (unsigned p = 0; p < ps; ++p)
Thomas Badie's avatar
Thomas Badie committed
636
          {
637
            std::cerr << a_->format_state(a_->state_from_number(p))
Thomas Badie's avatar
Thomas Badie committed
638
                      << " was in "
639
                      << bdd_format_set(a_->get_dict(), previous_class_[p])
640
                      << '\n';
Thomas Badie's avatar
Thomas Badie committed
641
          }
642
      }
Thomas Badie's avatar
Thomas Badie committed
643

Thomas Badie's avatar
Thomas Badie committed
644
    protected:
645
      // The automaton which is simulated.
646
      twa_graph_ptr a_;
Thomas Badie's avatar
Thomas Badie committed
647

648
      // Implications between classes.
649
      map_bdd_bdd relation_;
Thomas Badie's avatar
Thomas Badie committed
650

651
      // Represent the class of each state at the previous iteration.
652
      vector_state_bdd previous_class_;
Thomas Badie's avatar
Thomas Badie committed
653

654
655
656
      // The list of state for each class at the current_iteration.
      // Computed in `update_sig'.
      map_bdd_lstate bdd_lstate_;
Thomas Badie's avatar
Thomas Badie committed
657

658
659
660
      // 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
661

662
663
      // 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
664

665
666
      // Size of the automaton.
      unsigned int size_a_;
Thomas Badie's avatar
Thomas Badie committed
667

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

671
672
673
674
      // Whether to compute implications between classes.  This is costly
      // and useless for deterministic automata.
      bool want_implications_;

675
676
      // All the class variable:
      bdd all_class_var_;
Thomas Badie's avatar
Thomas Badie committed
677
678
679
680

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

Thomas Badie's avatar
Thomas Badie committed
681
682
      bdd all_proms_;

683
      automaton_size stat;
684

685
      std::unique_ptr<scc_info> scc_info_;
Thomas Badie's avatar
Thomas Badie committed
686

687
      const const_twa_graph_ptr original_;
Thomas Badie's avatar
Thomas Badie committed
688
689
    };

Thomas Badie's avatar
Thomas Badie committed
690
691
  } // End namespace anonymous.

Thomas Badie's avatar
Thomas Badie committed
692

693
694
  twa_graph_ptr
  simulation(const const_twa_graph_ptr& t)
Thomas Badie's avatar
Thomas Badie committed
695
  {
696
697
698
    direct_simulation<false, false> simul(t);
    return simul.run();
  }
Thomas Badie's avatar
Thomas Badie committed
699

700
701
  twa_graph_ptr
  simulation(const const_twa_graph_ptr& t,
702
             std::vector<bdd>* implications)
703
704
705
706
707
  {
    direct_simulation<false, false> simul(t);
    return simul.run(implications);
  }

708
709
  twa_graph_ptr
  simulation_sba(const const_twa_graph_ptr& t)
710
711
  {
    direct_simulation<false, true> simul(t);
Thomas Badie's avatar
Thomas Badie committed
712
713
714
    return simul.run();
  }

715
716
  twa_graph_ptr
  cosimulation(const const_twa_graph_ptr& t)
Thomas Badie's avatar
Thomas Badie committed
717
  {
718
719
720
    direct_simulation<true, false> simul(t);
    return simul.run();
  }
Thomas Badie's avatar
Thomas Badie committed
721

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

729
730

  template<bool Sba>
731
732
  twa_graph_ptr
  iterated_simulations_(const const_twa_graph_ptr& t)
733
  {
734
    twa_graph_ptr res = nullptr;
735
736
737
738
739
740
    automaton_size prev;
    automaton_size next;

    do
      {
        prev = next;
741
        direct_simulation<false, Sba> simul(res ? res : t);
742
        res = simul.run();
743
        if (res->prop_deterministic())
744
          break;
Thomas Badie's avatar
Thomas Badie committed
745

746
        direct_simulation<true, Sba> cosimul(res);
747
        res = cosimul.run();
748

749
750
751
752
        if (Sba)
          res = scc_filter_states(res, false);
        else
          res = scc_filter(res, false);
753
754

        next.set_size(res);
755
756
757
758
759
      }
    while (prev != next);
    return res;
  }

760
761
  twa_graph_ptr
  iterated_simulations(const const_twa_graph_ptr& t)
762
763
764
765
  {
    return iterated_simulations_<false>(t);
  }

766
767
  twa_graph_ptr
  iterated_simulations_sba(const const_twa_graph_ptr& t)
768
769
770
771
  {
    return iterated_simulations_<true>(t);
  }

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