simulation.cc 24.7 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
32
#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>
#include <spot/misc/bddlt.hh>
Thomas Badie's avatar
Thomas Badie committed
33
34
35
36
37
38
39
40

// The way we developed this algorithm is the following: We take an
// automaton, and reverse all these acceptance conditions.  We reverse
// them to go make the meaning of the signature easier. We are using
// bdd, and we want to let it make all the simplification. Because of
// the format of the acceptance condition, it doesn't allow easy
// simplification. Instead of encoding them as: "a!b!c + !ab!c", we
// use them as: "ab". We complement them because we want a
41
42
// simplification if the condition of the edge A implies the
// edge of B, and if the acceptance condition of A is included
Thomas Badie's avatar
Thomas Badie committed
43
44
45
// in the acceptance condition of B. To let the bdd makes the job, we
// revert them.

46
// Then, to check if a edge i-dominates another, we'll use the bdd:
Thomas Badie's avatar
Thomas Badie committed
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
// "sig(transA) = cond(trans) & acc(trans) & implied(class(trans->state))"
// Idem for sig(transB). The 'implied'
// (represented by a hash table 'relation_' in the implementation) is
// a conjunction of all the class dominated by the class of the
// destination. This is how the relation is included in the
// signature. It makes the simplifications alone, and the work is
// done.  The algorithm is cut into several step:
//
// 1. Run through the tgba and switch the acceptance condition to their
//    negation, and initializing relation_ by the 'init_ -> init_' where
//    init_ is the bdd which represents the class. This function is the
//    constructor of Simulation.
// 2. Enter in the loop (run).
//    - Rename the class.
//    - run through the automaton and computing the signature of each
//      state. This function is `update_sig'.
//    - Enter in a double loop to adapt the partial order, and set
64
//      'relation_' accordingly.
65
// 3. Rename the class (to actualize the name in the previous_class and
Thomas Badie's avatar
Thomas Badie committed
66
67
//    in relation_).
// 4. Building an automaton with the result, with the condition:
68
69
// "a edge in the original automaton appears in the simulated one
// iff this edge is included in the set of i-maximal neighbour."
Thomas Badie's avatar
Thomas Badie committed
70
71
72
73
// This function is `build_output'.
// The automaton simulated is recomplemented to come back to its initial
// state when the object Simulation is destroyed.
//
74
// Obviously these functions are possibly cut into several little ones.
Thomas Badie's avatar
Thomas Badie committed
75
76
// This is just the general development idea.

Thomas Badie's avatar
Thomas Badie committed
77

Thomas Badie's avatar
Thomas Badie committed
78
79
80
81
82
83
84
namespace spot
{
  namespace
  {
    // Some useful typedef:

    // Used to get the signature of the state.
85
    typedef std::vector<bdd> vector_state_bdd;
Thomas Badie's avatar
Thomas Badie committed
86
87

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

91
    typedef std::map<bdd, unsigned, bdd_less_than> map_bdd_state;
Thomas Badie's avatar
Thomas Badie committed
92
93
94
95


    // This class helps to compare two automata in term of
    // size.
96
97
98
    struct automaton_size
    {
      automaton_size()
99
        : edges(0),
100
101
102
103
          states(0)
      {
      }

104
      automaton_size(const twa_graph_ptr& a)
105
        : edges(a->num_edges()),
106
107
108
109
          states(a->num_states())
      {
      }

110
      void set_size(const twa_graph_ptr& a)
111
      {
112
113
        states = a->num_states();
        edges = a->num_edges();
114
115
      }

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
116
      inline bool operator!=(const automaton_size& r)
117
      {
118
        return edges != r.edges || states != r.states;
119
120
      }

Thomas Badie's avatar
Thomas Badie committed
121
122
123
124
125
126
127
      inline bool operator<(const automaton_size& r)
      {
        if (states < r.states)
          return true;
        if (states > r.states)
          return false;

128
        if (edges < r.edges)
Thomas Badie's avatar
Thomas Badie committed
129
          return true;
130
        if (edges > r.edges)
Thomas Badie's avatar
Thomas Badie committed
131
132
133
134
135
136
137
138
139
140
141
142
          return false;

        return false;
      }

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

143
        if (edges < r.edges)
Thomas Badie's avatar
Thomas Badie committed
144
          return false;
145
        if (edges > r.edges)
Thomas Badie's avatar
Thomas Badie committed
146
147
148
149
150
          return true;

        return false;
      }

151
      int edges;
152
153
      int states;
    };
Thomas Badie's avatar
Thomas Badie committed
154

Thomas Badie's avatar
Thomas Badie committed
155
    // The direct_simulation. If Cosimulation is true, we are doing a
156
157
    // cosimulation.
    template <bool Cosimulation, bool Sba>
158
    class direct_simulation final
Thomas Badie's avatar
Thomas Badie committed
159
    {
Thomas Badie's avatar
Thomas Badie committed
160
    protected:
161
      typedef std::map<bdd, bdd, bdd_less_than> map_bdd_bdd;
162
      int acc_vars;
163
      acc_cond::mark_t all_inf_;
164
    public:
165
166
167

      bdd mark_to_bdd(acc_cond::mark_t m)
      {
168
169
170
171
172
        // FIXME: Use a cache.
        bdd res = bddtrue;
        for (auto n: m.sets())
          res &= bdd_ithvar(acc_vars + n);
        return res;
173
174
      }

175
      acc_cond::mark_t bdd_to_mark(bdd b)
176
      {
177
178
179
180
181
182
183
184
        // FIXME: Use a cache.
        std::vector<unsigned> res;
        while (b != bddtrue)
          {
            res.push_back(bdd_var(b) - acc_vars);
            b = bdd_high(b);
          }
        return acc_cond::mark_t(res.begin(), res.end());
185
186
      }

187
      direct_simulation(const const_twa_graph_ptr& in)
188
        : po_size_(0),
Thomas Badie's avatar
Thomas Badie committed
189
          all_class_var_(bddtrue),
190
          original_(in)
191
      {
192
193
194
        if (!has_separate_sets(in))
          throw std::runtime_error
            ("direct_simulation() requires separate Inf and Fin sets");
195

196
197
198
        // Call get_init_state_number() before anything else as it
        // might add a state.
        unsigned init_state_number = in->get_init_state_number();
199
200
        scc_info_.reset(new scc_info(in));

201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
        unsigned ns = in->num_states();
        assert(ns > 0);
        size_a_ = ns;

        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_);

        // 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
267

Thomas Badie's avatar
Thomas Badie committed
268
        bdd_initial = bdd_ithvar(set_num++);
269
        bdd init = bdd_ithvar(set_num++);
270

271
        used_var_.push_back(init);
272

273
274
275
276
        // 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
277

278
279
280
281
282
283
        // 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
284
285
286
287
288
          {
            free_var_.push(i);
            all_class_var_ &= bdd_ithvar(i);
          }

289
        relation_[init] = init;
290
      }
Thomas Badie's avatar
Thomas Badie committed
291
292


293
294
295
      // 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
296
      virtual ~direct_simulation()
297
      {
298
        a_->get_dict()->unregister_all_my_variables(this);
299
      }
Thomas Badie's avatar
Thomas Badie committed
300

301
      // Update the name of the classes.
302
303
      void update_previous_class()
      {
304
        std::list<bdd>::iterator it_bdd = used_var_.begin();
305

306
307
308
        // 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
309
          {
310
311
312
313
314
315
316
317
318
319
320
321
322
            // 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
323
          }
324
325
      }

Thomas Badie's avatar
Thomas Badie committed
326
      void main_loop()
327
      {
328
329
330
331
        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
332
          {
333
            update_previous_class();
Thomas Badie's avatar
Thomas Badie committed
334
335
336
337
338
339
340
341
            nb_partition_before = bdd_lstate_.size();
            bdd_lstate_.clear();
            nb_po_before = po_size_;
            po_size_ = 0;
            update_sig();
            go_to_next_it();
          }

342
        update_previous_class();
Thomas Badie's avatar
Thomas Badie committed
343
344
345
      }

      // The core loop of the algorithm.
346
      twa_graph_ptr run(std::vector<bdd>* implications = nullptr)
Thomas Badie's avatar
Thomas Badie committed
347
348
      {
        main_loop();
349
        return build_result(implications);
350
      }
Thomas Badie's avatar
Thomas Badie committed
351

352
      // Take a state and compute its signature.
353
      bdd compute_sig(unsigned src)
354
      {
Thomas Badie's avatar
Thomas Badie committed
355
        bdd res = bddfalse;
Thomas Badie's avatar
Thomas Badie committed
356

357
        for (auto& t: a_->out(src))
Thomas Badie's avatar
Thomas Badie committed
358
          {
359
            bdd acc = mark_to_bdd(t.acc);
360

361
362
363
364
            // 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
365

366
367
            res |= to_add;
          }
Thomas Badie's avatar
Thomas Badie committed
368

Thomas Badie's avatar
Thomas Badie committed
369
        // When we Cosimulate, we add a special flag to differentiate
370
        // the initial state from the other.
371
        if (Cosimulation && src == a_->get_init_state_number())
Thomas Badie's avatar
Thomas Badie committed
372
373
374
          res |= bdd_initial;

        return res;
375
376
      }

Thomas Badie's avatar
Thomas Badie committed
377

378
379
      void update_sig()
      {
380
381
        for (unsigned s = 0; s < size_a_; ++s)
          bdd_lstate_[compute_sig(s)].push_back(s);
382
      }
Thomas Badie's avatar
Thomas Badie committed
383
384


385
      // This method renames the color set, updates the partial order.
386
387
      void go_to_next_it()
      {
388
        int nb_new_color = bdd_lstate_.size() - used_var_.size();
Thomas Badie's avatar
Thomas Badie committed
389

Thomas Badie's avatar
Thomas Badie committed
390
391
392

        // If we have created more partitions, we need to use more
        // variables.
393
        for (int i = 0; i < nb_new_color; ++i)
Thomas Badie's avatar
Thomas Badie committed
394
395
396
397
398
399
          {
            assert(!free_var_.empty());
            used_var_.push_back(bdd_ithvar(free_var_.front()));
            free_var_.pop();
          }

Thomas Badie's avatar
Thomas Badie committed
400
401
402

        // If we have reduced the number of partition, we 'free' them
        // in the free_var_ list.
403
        for (int i = 0; i > nb_new_color; --i)
404
405
406
407
408
409
410
          {
            assert(!used_var_.empty());
            free_var_.push(bdd_var(used_var_.front()));
            used_var_.pop_front();
          }


411
        assert((bdd_lstate_.size() == used_var_.size())
412
413
               || (bdd_lstate_.find(bddfalse) != bdd_lstate_.end()
                   && bdd_lstate_.size() == used_var_.size() + 1));
Thomas Badie's avatar
Thomas Badie committed
414

415
416
417
418
419
        // 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
420

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

423
        for (auto& p: bdd_lstate_)
Thomas Badie's avatar
Thomas Badie committed
424
          {
425
426
427
428
429
            // 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.
430
431
432
            bdd acc = bddfalse;
            if (p.first != bddfalse)
              acc = *it_bdd;
433
            now_to_next.emplace_back(p.first, acc);
434
            ++it_bdd;
Thomas Badie's avatar
Thomas Badie committed
435
436
          }

437
        // Update the partial order.
438

439
440
441
442
443
444
445
        // This loop follows the pattern given by the paper.
        // foreach class do
        // |  foreach class do
        // |  | update po if needed
        // |  od
        // od

446
        for (unsigned n = 0; n < sz; ++n)
Thomas Badie's avatar
Thomas Badie committed
447
          {
448
449
450
            bdd n_sig = now_to_next[n].first;
            bdd n_class = now_to_next[n].second;
            for (unsigned m = 0; m < sz; ++m)
Thomas Badie's avatar
Thomas Badie committed
451
              {
452
                if (n == m)
Thomas Badie's avatar
Thomas Badie committed
453
                  continue;
454
                if (bdd_implies(n_sig, now_to_next[m].first))
Thomas Badie's avatar
Thomas Badie committed
455
                  {
456
                    n_class &= now_to_next[m].second;
Thomas Badie's avatar
Thomas Badie committed
457
458
459
                    ++po_size_;
                  }
              }
460
            relation_[now_to_next[n].second] = n_class;
Thomas Badie's avatar
Thomas Badie committed
461
          }
462
463
464
      }

      // Build the minimal resulting automaton.
465
      twa_graph_ptr build_result(std::vector<bdd>* implications = nullptr)
466
      {
467
468
469
        twa_graph_ptr res = make_twa_graph(a_->get_dict());
        res->copy_ap_of(a_);
        res->copy_acceptance_of(a_);
470

471
472
        // Non atomic propositions variables (= acc and class)
        bdd nonapvars = all_proms_ & bdd_support(all_class_var_);
473

474
        auto* gb = res->create_namer<int>();
475

476
477
        if (implications)
          implications->resize(bdd_lstate_.size());
478
479
        // Create one state per partition.
        for (auto& p: bdd_lstate_)
Thomas Badie's avatar
Thomas Badie committed
480
          {
481
            bdd cl = previous_class_[p.second.front()];
482
483
484
485
            // 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());
486
487
            if (implications)
              (*implications)[s] = relation_[cl];
Thomas Badie's avatar
Thomas Badie committed
488
489
          }

490
491
492
493
        // Acceptance of states.  Only used if Sba && Cosimulation.
        std::vector<acc_cond::mark_t> accst;
        if (Sba && Cosimulation)
          accst.resize(res->num_states(), 0U);
494

495
        stat.states = bdd_lstate_.size();
496
        stat.edges = 0;
497

Thomas Badie's avatar
Thomas Badie committed
498
499
500
        unsigned nb_satoneset = 0;
        unsigned nb_minato = 0;

501
502
503
504
        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
505
          {
506
507
508
            // 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()];
509
510

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

Thomas Badie's avatar
Thomas Badie committed
513
514
515
            if (Cosimulation)
              sig = bdd_compose(sig, bddfalse, bdd_var(bdd_initial));

Thomas Badie's avatar
Thomas Badie committed
516
517
518
519
520
521
522
523
524
525
526
            // 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);

527
            // First loop over all possible valuations atomic properties.
Thomas Badie's avatar
Thomas Badie committed
528
            while (all_atomic_prop != bddfalse)
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
              {
                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);
544

Thomas Badie's avatar
Thomas Badie committed
545
546
                ++nb_satoneset;

547
548
549
                bdd cond_acc_dest;
                while ((cond_acc_dest = isop.next()) != bddfalse)
                  {
550
                    ++stat.edges;
551

Thomas Badie's avatar
Thomas Badie committed
552
553
                    ++nb_minato;

554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
                    // 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
592
593
          }

594
595
        res->set_init_state(gb->get_state(previous_class_
                                          [a_->get_init_state_number()].id()));
Thomas Badie's avatar
Thomas Badie committed
596

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

599
600
601
602
603
604
605
606
607
608
609
610
611
612
        // 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;
              }
          }
613

614
        res->purge_unreachable_states();
615

616
        delete gb;
617
618
619
620
621
622
623
        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.
                       });
624
        if (nb_minato == nb_satoneset && !Cosimulation)
625
626
627
628
          res->prop_deterministic(true);
        if (Sba)
          res->prop_state_acc(true);
        return res;
629
630
631
632
633
634
635
636
637
638
      }


      // 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()
      {
639
        for (auto& p: bdd_lstate_)
Thomas Badie's avatar
Thomas Badie committed
640
641
          {
            std::cerr << "partition: "
642
                      << bdd_format_isop(a_->get_dict(), p.first)
Thomas Badie's avatar
Thomas Badie committed
643
                      << std::endl;
644
            for (auto s: p.second)
645
646
647
              std::cerr << "  - "
                        << a_->format_state(a_->state_from_number(s))
                        << '\n';
Thomas Badie's avatar
Thomas Badie committed
648
649
          }

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

652
653
        unsigned ps = previous_class_.size();
        for (unsigned p = 0; p < ps; ++p)
Thomas Badie's avatar
Thomas Badie committed
654
          {
655
            std::cerr << a_->format_state(a_->state_from_number(p))
Thomas Badie's avatar
Thomas Badie committed
656
                      << " was in "
657
                      << bdd_format_set(a_->get_dict(), previous_class_[p])
658
                      << '\n';
Thomas Badie's avatar
Thomas Badie committed
659
          }
660
      }
Thomas Badie's avatar
Thomas Badie committed
661

Thomas Badie's avatar
Thomas Badie committed
662
    protected:
663
      // The automaton which is simulated.
664
      twa_graph_ptr a_;
Thomas Badie's avatar
Thomas Badie committed
665

666
      // Implications between classes.
667
      map_bdd_bdd relation_;
Thomas Badie's avatar
Thomas Badie committed
668

669
      // Represent the class of each state at the previous iteration.
670
      vector_state_bdd previous_class_;
Thomas Badie's avatar
Thomas Badie committed
671

672
673
674
      // 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
675

676
677
678
      // 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
679

680
681
      // 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
682

683
684
      // Size of the automaton.
      unsigned int size_a_;
Thomas Badie's avatar
Thomas Badie committed
685

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

689
690
      // All the class variable:
      bdd all_class_var_;
Thomas Badie's avatar
Thomas Badie committed
691
692
693
694

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

Thomas Badie's avatar
Thomas Badie committed
695
696
      bdd all_proms_;

697
      automaton_size stat;
698

699
      std::unique_ptr<scc_info> scc_info_;
Thomas Badie's avatar
Thomas Badie committed
700

701
      const const_twa_graph_ptr original_;
Thomas Badie's avatar
Thomas Badie committed
702
703
    };

Thomas Badie's avatar
Thomas Badie committed
704
705
  } // End namespace anonymous.

Thomas Badie's avatar
Thomas Badie committed
706

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

714
715
  twa_graph_ptr
  simulation(const const_twa_graph_ptr& t,
716
             std::vector<bdd>* implications)
717
718
719
720
721
  {
    direct_simulation<false, false> simul(t);
    return simul.run(implications);
  }

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

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

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

743
744

  template<bool Sba>
745
746
  twa_graph_ptr
  iterated_simulations_(const const_twa_graph_ptr& t)
747
  {
748
    twa_graph_ptr res = nullptr;
749
750
751
752
753
754
    automaton_size prev;
    automaton_size next;

    do
      {
        prev = next;
755
        direct_simulation<false, Sba> simul(res ? res : t);
756
        res = simul.run();
757
        if (res->prop_deterministic())
758
          break;
Thomas Badie's avatar
Thomas Badie committed
759

760
        direct_simulation<true, Sba> cosimul(res);
761
        res = cosimul.run();
762

763
764
765
766
        if (Sba)
          res = scc_filter_states(res, false);
        else
          res = scc_filter(res, false);
767
768

        next.set_size(res);
769
770
771
772
773
      }
    while (prev != next);
    return res;
  }

774
775
  twa_graph_ptr
  iterated_simulations(const const_twa_graph_ptr& t)
776
777
778
779
  {
    return iterated_simulations_<false>(t);
  }

780
781
  twa_graph_ptr
  iterated_simulations_sba(const const_twa_graph_ptr& t)
782
783
784
785
  {
    return iterated_simulations_<true>(t);
  }

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