simulation.cc 24 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
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
444
445
        auto state_mapping = new std::vector<unsigned>();
        state_mapping->resize(a_->num_states());
        res->set_named_prop("simulated-states", state_mapping);

446
447
        // Non atomic propositions variables (= acc and class)
        bdd nonapvars = all_proms_ & bdd_support(all_class_var_);
448

449
        auto* gb = res->create_namer<int>();
450

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

468
469
470
471
        // Acceptance of states.  Only used if Sba && Cosimulation.
        std::vector<acc_cond::mark_t> accst;
        if (Sba && Cosimulation)
          accst.resize(res->num_states(), 0U);
472

473
        stat.states = bdd_lstate_.size();
474
        stat.edges = 0;
475

Thomas Badie's avatar
Thomas Badie committed
476
477
478
        unsigned nb_satoneset = 0;
        unsigned nb_minato = 0;

479
480
481
482
        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
483
          {
484
485
486
            // 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()];
487
488

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

Thomas Badie's avatar
Thomas Badie committed
491
492
493
            if (Cosimulation)
              sig = bdd_compose(sig, bddfalse, bdd_var(bdd_initial));

Thomas Badie's avatar
Thomas Badie committed
494
495
496
497
498
499
500
501
502
503
504
            // 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);

505
            // First loop over all possible valuations atomic properties.
Thomas Badie's avatar
Thomas Badie committed
506
            while (all_atomic_prop != bddfalse)
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
              {
                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);
522

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

525
526
527
                bdd cond_acc_dest;
                while ((cond_acc_dest = isop.next()) != bddfalse)
                  {
528
                    ++stat.edges;
529

Thomas Badie's avatar
Thomas Badie committed
530
531
                    ++nb_minato;

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
563
564
565
566
567
568
569
                    // 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
570
571
          }

572
573
        res->set_init_state(gb->get_state(previous_class_
                                          [a_->get_init_state_number()].id()));
Thomas Badie's avatar
Thomas Badie committed
574

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

577
578
579
580
581
582
583
584
585
586
587
588
589
590
        // 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;
              }
          }
591

592
593
594
595
596
597
598
        // 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();
599

600
        delete gb;
601
602
603
        res->prop_copy(original_,
                       { false, // state-based acc forced below
                         true,  // weakness preserved,
604
                         false, true, // determinism improved
605
                         true, // completeness preserved
606
607
                         true, // stutter inv.
                       });
608
        // !unambiguous and !semi-deterministic are not preserved
609
        if (!Cosimulation)
610
          res->prop_universal(nb_minato == nb_satoneset);
611
612
613
        if (Sba)
          res->prop_state_acc(true);
        return res;
614
615
616
617
618
619
620
621
622
623
      }


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

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

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

Thomas Badie's avatar
Thomas Badie committed
647
    protected:
648
      // The automaton which is simulated.
649
      twa_graph_ptr a_;
Thomas Badie's avatar
Thomas Badie committed
650

651
      // Implications between classes.
652
      map_bdd_bdd relation_;
Thomas Badie's avatar
Thomas Badie committed
653

654
      // Represent the class of each state at the previous iteration.
655
      vector_state_bdd previous_class_;
Thomas Badie's avatar
Thomas Badie committed
656

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

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

665
666
      // 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
667

668
669
      // Size of the automaton.
      unsigned int size_a_;
Thomas Badie's avatar
Thomas Badie committed
670

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

674
675
676
677
      // Whether to compute implications between classes.  This is costly
      // and useless for deterministic automata.
      bool want_implications_;

678
679
      // All the class variable:
      bdd all_class_var_;
Thomas Badie's avatar
Thomas Badie committed
680
681
682
683

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

Thomas Badie's avatar
Thomas Badie committed
684
685
      bdd all_proms_;

686
      automaton_size stat;
687

688
      std::unique_ptr<scc_info> scc_info_;
Thomas Badie's avatar
Thomas Badie committed
689

690
      const const_twa_graph_ptr original_;
Thomas Badie's avatar
Thomas Badie committed
691
692
    };

Thomas Badie's avatar
Thomas Badie committed
693
694
  } // End namespace anonymous.

Thomas Badie's avatar
Thomas Badie committed
695

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

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

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

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

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

732
733

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

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

749
        direct_simulation<true, Sba> cosimul(res);
750
        res = cosimul.run();
751

752
753
754
755
        if (Sba)
          res = scc_filter_states(res, false);
        else
          res = scc_filter(res, false);
756
757

        next.set_size(res);
758
759
760
761
762
      }
    while (prev != next);
    return res;
  }

763
764
  twa_graph_ptr
  iterated_simulations(const const_twa_graph_ptr& t)
765
766
767
768
  {
    return iterated_simulations_<false>(t);
  }

769
770
  twa_graph_ptr
  iterated_simulations_sba(const const_twa_graph_ptr& t)
771
772
773
774
  {
    return iterated_simulations_<true>(t);
  }

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