simulation.cc 24.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
            nb_partition_before = bdd_lstate_.size();
            nb_po_before = po_size_;
            po_size_ = 0;
            update_sig();
308
            // print_partition();
Thomas Badie's avatar
Thomas Badie committed
309
310
311
            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
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
        // Non atomic propositions variables (= acc and class)
        bdd nonapvars = all_proms_ & bdd_support(all_class_var_);
454

455
        auto* gb = res->create_namer<int>();
456

457
458
        if (implications)
          implications->resize(bdd_lstate_.size());
459
460
        // Create one state per class.
        for (auto& p: sorted_classes_)
Thomas Badie's avatar
Thomas Badie committed
461
          {
462
            bdd cl = previous_class_[p->second.front()];
463
464
465
466
            // 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());
467
468
            if (implications)
              (*implications)[s] = relation_[cl];
Thomas Badie's avatar
Thomas Badie committed
469
470
          }

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

476
        stat.states = bdd_lstate_.size();
477
        stat.edges = 0;
478

Thomas Badie's avatar
Thomas Badie committed
479
480
481
        unsigned nb_satoneset = 0;
        unsigned nb_minato = 0;

482
483
484
        auto all_inf = all_inf_;
        // For each class, we will create
        // all the edges between the states.
485
        for (auto& p: sorted_classes_)
Thomas Badie's avatar
Thomas Badie committed
486
          {
487
488
            // All states in p.second have the same class, so just
            // pick the class of the first one first one.
489
            bdd src = previous_class_[p->second.front()];
490
491

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

Thomas Badie's avatar
Thomas Badie committed
494
495
496
            if (Cosimulation)
              sig = bdd_compose(sig, bddfalse, bdd_var(bdd_initial));

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

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

Thomas Badie's avatar
Thomas Badie committed
526
527
                ++nb_satoneset;

528
529
530
                bdd cond_acc_dest;
                while ((cond_acc_dest = isop.next()) != bddfalse)
                  {
531
                    ++stat.edges;
532

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

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
570
571
572
                    // 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
573
574
          }

575
576
        res->set_init_state(gb->get_state(previous_class_
                                          [a_->get_init_state_number()].id()));
Thomas Badie's avatar
Thomas Badie committed
577

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

580
581
582
583
584
585
586
587
588
589
590
591
592
593
        // 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;
              }
          }
594

595
596
597
598
599
600
601
        // 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();
602

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


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

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

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

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

653
      // Implications between classes.
654
      map_bdd_bdd relation_;
Thomas Badie's avatar
Thomas Badie committed
655

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

659
      // The list of states for each class at the current_iteration.
660
661
      // Computed in `update_sig'.
      map_bdd_lstate bdd_lstate_;
662
663
664
665
      // 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
666

667
668
669
      // 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
670

671
672
      // 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
673

674
675
      // Size of the automaton.
      unsigned int size_a_;
Thomas Badie's avatar
Thomas Badie committed
676

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

680
681
682
683
      // Whether to compute implications between classes.  This is costly
      // and useless for deterministic automata.
      bool want_implications_;

684
685
      // All the class variable:
      bdd all_class_var_;
Thomas Badie's avatar
Thomas Badie committed
686
687
688
689

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

Thomas Badie's avatar
Thomas Badie committed
690
691
      bdd all_proms_;

692
      automaton_size stat;
693

694
      std::unique_ptr<scc_info> scc_info_;
Thomas Badie's avatar
Thomas Badie committed
695

696
      const const_twa_graph_ptr original_;
Thomas Badie's avatar
Thomas Badie committed
697
698
    };

Thomas Badie's avatar
Thomas Badie committed
699
700
  } // End namespace anonymous.

Thomas Badie's avatar
Thomas Badie committed
701

702
703
  twa_graph_ptr
  simulation(const const_twa_graph_ptr& t)
Thomas Badie's avatar
Thomas Badie committed
704
  {
705
706
707
    direct_simulation<false, false> simul(t);
    return simul.run();
  }
Thomas Badie's avatar
Thomas Badie committed
708

709
710
  twa_graph_ptr
  simulation(const const_twa_graph_ptr& t,
711
             std::vector<bdd>* implications)
712
713
714
715
716
  {
    direct_simulation<false, false> simul(t);
    return simul.run(implications);
  }

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

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

731
732
  twa_graph_ptr
  cosimulation_sba(const const_twa_graph_ptr& t)
733
734
  {
    direct_simulation<true, true> simul(t);
Thomas Badie's avatar
Thomas Badie committed
735
736
737
    return simul.run();
  }

738
739

  template<bool Sba>
740
741
  twa_graph_ptr
  iterated_simulations_(const const_twa_graph_ptr& t)
742
  {
743
    twa_graph_ptr res = nullptr;
744
745
746
747
748
749
    automaton_size prev;
    automaton_size next;

    do
      {
        prev = next;
750
        direct_simulation<false, Sba> simul(res ? res : t);
751
        res = simul.run();
752
        if (res->prop_deterministic())
753
          break;
Thomas Badie's avatar
Thomas Badie committed
754

755
        direct_simulation<true, Sba> cosimul(res);
756
        res = cosimul.run();
757

758
759
760
761
        if (Sba)
          res = scc_filter_states(res, false);
        else
          res = scc_filter(res, false);
762
763

        next.set_size(res);
764
765
766
767
768
      }
    while (prev != next);
    return res;
  }

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

775
776
  twa_graph_ptr
  iterated_simulations_sba(const const_twa_graph_ptr& t)
777
778
779
780
  {
    return iterated_simulations_<true>(t);
  }

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