simulation.cc 22.9 KB
Newer Older
Thomas Badie's avatar
Thomas Badie committed
1
// -*- coding: utf-8 -*-
2
3
// Copyright (C) 2012, 2013, 2014, 2015 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>
Thomas Badie's avatar
Thomas Badie committed
25
26
27
28
#include "simulation.hh"
#include "misc/minato.hh"
#include "tgba/bddprint.hh"
#include "tgbaalgos/reachiter.hh"
29
#include "tgbaalgos/sccfilter.hh"
30
#include "tgbaalgos/sccinfo.hh"
31
#include "misc/bddlt.hh"
Thomas Badie's avatar
Thomas Badie committed
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63

// 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
// simplification if the condition of the transition A implies the
// transition of B, and if the acceptance condition of A is included
// in the acceptance condition of B. To let the bdd makes the job, we
// revert them.

// Then, to check if a transition i-dominates another, we'll use the bdd:
// "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
//      'relation_' accordingly. This function is `update_po'.
64
// 3. Rename the class (to actualize the name in the previous_class and
Thomas Badie's avatar
Thomas Badie committed
65
66
67
68
69
70
71
72
//    in relation_).
// 4. Building an automaton with the result, with the condition:
// "a transition in the original automaton appears in the simulated one
// iff this transition is included in the set of i-maximal neighbour."
// This function is `build_output'.
// The automaton simulated is recomplemented to come back to its initial
// state when the object Simulation is destroyed.
//
73
// Obviously these functions are possibly cut into several little ones.
Thomas Badie's avatar
Thomas Badie committed
74
75
// This is just the general development idea.

Thomas Badie's avatar
Thomas Badie committed
76

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

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

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

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


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

103
104
105
106
107
108
109
110
111
112
113
114
      automaton_size(const tgba_digraph_ptr& a)
        : transitions(a->num_transitions()),
          states(a->num_states())
      {
      }

      void set_size(const tgba_digraph_ptr& a)
      {
	states = a->num_states();
	transitions = a->num_transitions();
      }

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

Thomas Badie's avatar
Thomas Badie committed
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
      inline bool operator<(const automaton_size& r)
      {
        if (states < r.states)
          return true;
        if (states > r.states)
          return false;

        if (transitions < r.transitions)
          return true;
        if (transitions > r.transitions)
          return false;

        return false;
      }

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

        if (transitions < r.transitions)
          return false;
        if (transitions > r.transitions)
          return true;

        return false;
      }

150
151
152
      int transitions;
      int states;
    };
Thomas Badie's avatar
Thomas Badie committed
153

Thomas Badie's avatar
Thomas Badie committed
154
    // The direct_simulation. If Cosimulation is true, we are doing a
155
156
    // cosimulation.
    template <bool Cosimulation, bool Sba>
157
    class direct_simulation
Thomas Badie's avatar
Thomas Badie committed
158
    {
Thomas Badie's avatar
Thomas Badie committed
159
    protected:
160
161
      // Shortcut used in update_po and go_to_next_it.
      typedef std::map<bdd, bdd, bdd_less_than> map_bdd_bdd;
162
      int acc_vars;
163
    public:
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185

      bdd mark_to_bdd(acc_cond::mark_t m)
      {
	// FIXME: Use a cache.
	bdd res = bddtrue;
	for (auto n: a_->acc().sets(m))
	  res &= bdd_ithvar(acc_vars + n);
	return res;
      }

      acc_cond::mark_t bdd_to_mark(const tgba_digraph_ptr& aut, bdd b)
      {
	// FIXME: Use a cache.
	std::vector<unsigned> res;
	while (b != bddtrue)
	  {
	    res.push_back(bdd_var(b) - acc_vars);
	    b = bdd_high(b);
	  }
	return aut->acc().marks(res.begin(), res.end());
      }

186
187
      direct_simulation(const const_tgba_digraph_ptr& in)
        : po_size_(0),
Thomas Badie's avatar
Thomas Badie committed
188
          all_class_var_(bddtrue),
189
          original_(in)
190
      {
191
192
193
194
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();
        scc_info_.reset(new scc_info(in));

	unsigned ns = in->num_states();
	assert(ns > 0);
	size_a_ = ns;
Thomas Badie's avatar
Thomas Badie committed
199

200
201
	// Replace all the acceptance conditions by their complements.
	// (In the case of Cosimulation, we also flip the transitions.)
202
203
204
205
206
	if (Cosimulation)
	  {
	    a_ = make_tgba_digraph(in->get_dict());
	    a_->copy_ap_of(in);
	    a_->copy_acceptance_conditions_of(in);
207
	    a_->new_states(ns);
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
	    auto& acccond = in->acc();

	    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 = acccond.comp(td.acc);
			    break;
			  }
		      }
		    else
		      {
			acc = acccond.comp(t.acc);
		      }
234
		    a_->new_transition(t.dst, s, t.cond, acc);
235
236
237
238
239
240
241
242
243
244
245
246
		  }
		a_->set_init_state(init_state_number);
	      }
	  }
	else
	  {
	    a_ = make_tgba_digraph(in, tgba::prop_set::all());
	    auto& acccond = a_->acc();
	    for (auto& t: a_->transitions())
	      t.acc = acccond.comp(t.acc);
	  }
	assert(a_->num_states() == size_a_);
247
248
249
250
251

	// 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()
252
	  ->register_anonymous_variables(size_a_ + 1, this);
253

254
255
256
257
258
259
260
	unsigned n_acc = a_->acc().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
261

Thomas Badie's avatar
Thomas Badie committed
262
263
        bdd_initial = bdd_ithvar(set_num++);
	bdd init = bdd_ithvar(set_num++);
264
265
266

	used_var_.push_back(init);

267
268
269
270
	// 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
271

272
273
274
275
	// 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.
276
	all_class_var_ = init;
277
	for (unsigned i = set_num; i < set_num + size_a_ - 1; ++i)
Thomas Badie's avatar
Thomas Badie committed
278
279
280
281
282
          {
            free_var_.push(i);
            all_class_var_ &= bdd_ithvar(i);
          }

283
284
	relation_[init] = init;
      }
Thomas Badie's avatar
Thomas Badie committed
285
286


287
288
289
      // 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
290
      virtual ~direct_simulation()
291
      {
292
	a_->get_dict()->unregister_all_my_variables(this);
293
      }
Thomas Badie's avatar
Thomas Badie committed
294

295
      // Update the name of the classes.
296
297
298
299
300
301
      void update_previous_class()
      {
	std::list<bdd>::iterator it_bdd = used_var_.begin();

	// We run through the map bdd/list<state>, and we update
	// the previous_class_ with the new data.
302
	for (auto& p: bdd_lstate_)
Thomas Badie's avatar
Thomas Badie committed
303
          {
304
305
306
307
308
309
310
311
	    // If the signature of a state is bddfalse (no
	    // transitions) the class of this state is bddfalse
	    // instead of an anonymous variable. It allows
	    // simplifications in the signature by removing a
	    // transition which has as a destination a state with
	    // no outgoing transition.
	    if (p.first == bddfalse)
	      for (auto s: p.second)
312
		previous_class_[s] = bddfalse;
313
314
	    else
	      for (auto s: p.second)
315
		previous_class_[s] = *it_bdd;
316
	    ++it_bdd;
Thomas Badie's avatar
Thomas Badie committed
317
          }
318
319
      }

Thomas Badie's avatar
Thomas Badie committed
320
      void main_loop()
321
322
323
324
325
      {
	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
326
          {
327
            update_previous_class();
Thomas Badie's avatar
Thomas Badie committed
328
329
330
331
332
333
334
335
            nb_partition_before = bdd_lstate_.size();
            bdd_lstate_.clear();
            nb_po_before = po_size_;
            po_size_ = 0;
            update_sig();
            go_to_next_it();
          }

336
	update_previous_class();
Thomas Badie's avatar
Thomas Badie committed
337
338
339
      }

      // The core loop of the algorithm.
340
      tgba_digraph_ptr run()
Thomas Badie's avatar
Thomas Badie committed
341
342
      {
        main_loop();
343
344
	return build_result();
      }
Thomas Badie's avatar
Thomas Badie committed
345

346
      // Take a state and compute its signature.
347
      bdd compute_sig(unsigned src)
348
      {
Thomas Badie's avatar
Thomas Badie committed
349
        bdd res = bddfalse;
Thomas Badie's avatar
Thomas Badie committed
350

351
        for (auto& t: a_->out(src))
Thomas Badie's avatar
Thomas Badie committed
352
          {
353
            bdd acc = mark_to_bdd(t.acc);
354
355
356
357

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

360
361
	    res |= to_add;
	  }
Thomas Badie's avatar
Thomas Badie committed
362

Thomas Badie's avatar
Thomas Badie committed
363
        // When we Cosimulate, we add a special flag to differentiate
364
        // the initial state from the other.
365
        if (Cosimulation && src == a_->get_init_state_number())
Thomas Badie's avatar
Thomas Badie committed
366
367
368
          res |= bdd_initial;

        return res;
369
370
      }

Thomas Badie's avatar
Thomas Badie committed
371

372
373
      void update_sig()
      {
374
	for (unsigned s = 0; s < size_a_; ++s)
375
	  bdd_lstate_[compute_sig(s)].push_back(s);
376
      }
Thomas Badie's avatar
Thomas Badie committed
377
378


379
380
381
382
      // This method rename the color set, update the partial order.
      void go_to_next_it()
      {
	int nb_new_color = bdd_lstate_.size() - used_var_.size();
Thomas Badie's avatar
Thomas Badie committed
383

Thomas Badie's avatar
Thomas Badie committed
384
385
386

        // If we have created more partitions, we need to use more
        // variables.
387
	for (int i = 0; i < nb_new_color; ++i)
Thomas Badie's avatar
Thomas Badie committed
388
389
390
391
392
393
          {
            assert(!free_var_.empty());
            used_var_.push_back(bdd_ithvar(free_var_.front()));
            free_var_.pop();
          }

Thomas Badie's avatar
Thomas Badie committed
394
395
396

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


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

409
410
411
412
413
414
415
	// Now we make a temporary hash_table which links the tuple
	// "C^(i-1), N^(i-1)" to the new class coloring.  If we
	// rename the class before updating the partial order, we
	// loose the information, and if we make it after, I can't
	// figure out how to apply this renaming on rel_.
	// It adds a data structure but it solves our problem.
	map_bdd_bdd now_to_next;
Thomas Badie's avatar
Thomas Badie committed
416

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

419
	for (auto& p: bdd_lstate_)
Thomas Badie's avatar
Thomas Badie committed
420
          {
421
422
423
424
425
426
	    // If the signature of a state is bddfalse (no
	    // transitions) the class of this state is bddfalse
	    // instead of an anonymous variable. It allows
	    // simplifications in the signature by removing a
	    // transition which has as a destination a state with
	    // no outgoing transition.
427
428
429
430
	    bdd acc = bddfalse;
	    if (p.first != bddfalse)
	      acc = *it_bdd;
	    now_to_next[p.first] = acc;
431
	    ++it_bdd;
Thomas Badie's avatar
Thomas Badie committed
432
433
          }

Thomas Badie's avatar
Thomas Badie committed
434
	update_po(now_to_next, relation_);
435
436
      }

Thomas Badie's avatar
Thomas Badie committed
437
438
439
440
441
442
443
444
445
      // This function computes the new po with previous_class_ and
      // the argument. `now_to_next' contains the relation between the
      // signature and the future name of the class.  We need a
      // template parameter because we use this function with a
      // map_bdd_bdd, but later, we need a list_bdd_bdd. So to
      // factorize some code we use a template.
      template <typename container_bdd_bdd>
      void update_po(const container_bdd_bdd& now_to_next,
                     map_bdd_bdd& relation)
446
447
448
449
450
451
452
453
      {
	// This loop follows the pattern given by the paper.
	// foreach class do
	// |  foreach class do
	// |  | update po if needed
	// |  od
	// od

Thomas Badie's avatar
Thomas Badie committed
454
455
	for (typename container_bdd_bdd::const_iterator it1
               = now_to_next.begin();
456
457
	     it1 != now_to_next.end();
	     ++it1)
Thomas Badie's avatar
Thomas Badie committed
458
459
          {
            bdd accu = it1->second;
Thomas Badie's avatar
Thomas Badie committed
460
461
            for (typename container_bdd_bdd::const_iterator it2
                   = now_to_next.begin();
Thomas Badie's avatar
Thomas Badie committed
462
463
                 it2 != now_to_next.end();
                 ++it2)
Thomas Badie's avatar
Thomas Badie committed
464
465
466
467
468
469
470
471
472
473
474
              {
                // Skip the case managed by the initialization of accu.
                if (it1 == it2)
                  continue;

                if (bdd_implies(it1->first, it2->first))
                  {
                    accu &= it2->second;
                    ++po_size_;
                  }
              }
Thomas Badie's avatar
Thomas Badie committed
475
            relation[it1->second] = accu;
Thomas Badie's avatar
Thomas Badie committed
476
          }
477
478
479
      }

      // Build the minimal resulting automaton.
480
      tgba_digraph_ptr build_result()
481
      {
482
	tgba_digraph_ptr res = make_tgba_digraph(a_->get_dict());
483
	res->copy_ap_of(a_);
484
	res->copy_acceptance_conditions_of(a_);
485
	if (Sba)
486
	  res->prop_state_based_acc();
487
488

	// Non atomic propositions variables (= acc and class)
489
	bdd nonapvars = all_proms_ & bdd_support(all_class_var_);
490

491
492
	auto* gb = res->create_namer<int>();

493
	// Create one state per partition.
494
	for (auto& p: bdd_lstate_)
Thomas Badie's avatar
Thomas Badie committed
495
          {
496
497
498
499
500
            bdd cl = previous_class_[p.second.front()];
	    // 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());
Thomas Badie's avatar
Thomas Badie committed
501
502
          }

503
	// Acceptance of states.  Only used if Sba && Cosimulation.
504
	std::vector<acc_cond::mark_t> accst;
505
	if (Sba && Cosimulation)
506
	  accst.resize(res->num_states(), 0U);
507

508
509
510
        stat.states = bdd_lstate_.size();
        stat.transitions = 0;

Thomas Badie's avatar
Thomas Badie committed
511
512
513
        unsigned nb_satoneset = 0;
        unsigned nb_minato = 0;

514
	// For each class, we will create
515
	// all the transitions between the states.
516
	for (auto& p: bdd_lstate_)
Thomas Badie's avatar
Thomas Badie committed
517
          {
518
519
520
521
522
	    // 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()];

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

Thomas Badie's avatar
Thomas Badie committed
525
526
527
            if (Cosimulation)
              sig = bdd_compose(sig, bddfalse, bdd_var(bdd_initial));

Thomas Badie's avatar
Thomas Badie committed
528
529
530
531
532
533
534
535
536
537
538
539
540
            // 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);

	    // First loop over all possible valuations atomic properties.
            while (all_atomic_prop != bddfalse)
541
542
543
544
545
546
	      {
		bdd one = bdd_satoneset(all_atomic_prop,
					sup_all_atomic_prop,
					bddtrue);
		all_atomic_prop -= one;

547
		// For each possible valuation, iterate over all possible
548
549
550
551
552
553
554
555
556
		// 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);

Thomas Badie's avatar
Thomas Badie committed
557
558
                ++nb_satoneset;

559
560
561
		bdd cond_acc_dest;
		while ((cond_acc_dest = isop.next()) != bddfalse)
		  {
562
563
                    ++stat.transitions;

Thomas Badie's avatar
Thomas Badie committed
564
565
                    ++nb_minato;

566
567
		    // Take the transition, and keep only the variable which
		    // are used to represent the class.
568
		    bdd dst = bdd_existcomp(cond_acc_dest,
569
570
571
					     all_class_var_);

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

575
		    // Keep the other!
576
577
578
579
		    bdd cond = bdd_existcomp(cond_acc_dest,
					     sup_all_atomic_prop);

		    // Because we have complemented all the acceptance
580
581
		    // conditions on the input automaton, we must
		    // revert them to create a new transition.
582
		    acc = res->acc().comp(acc);
583

584
585
586
		    if (Cosimulation)
		      {
			if (Sba)
587
588
589
590
591
592
593
			  {
			    // acc should be attached to src, or rather,
			    // in our transition-based representation)
			    // to all transitions 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;
594
			    acc = 0U;
595
596
			  }
			gb->new_transition(dst.id(), src.id(), cond, acc);
597
		      }
598
		    else
599
600
601
		      {
			gb->new_transition(src.id(), dst.id(), cond, acc);
		      }
602
603
		  }
	      }
Thomas Badie's avatar
Thomas Badie committed
604
605
          }

606
607
	res->set_init_state(gb->get_state(previous_class_
					  [a_->get_init_state_number()].id()));
Thomas Badie's avatar
Thomas Badie committed
608

609
	res->merge_transitions(); // FIXME: is this really needed?
Thomas Badie's avatar
Thomas Badie committed
610

611
612
613
	// Mark all accepting state in a second pass, when
	// dealing with SBA in cosimulation.
	if (Sba && Cosimulation)
614
615
616
617
	  {
	    unsigned ns = res->num_states();
	    for (unsigned s = 0; s < ns; ++s)
	      {
618
619
		acc_cond::mark_t acc = accst[s];
		if (acc == 0U)
620
		  continue;
621
		for (auto& t: res->out(s))
622
623
624
		  t.acc = acc;
	      }
	  }
625

626
627
	res->purge_unreachable_states();

628
	delete gb;
629
	res->prop_copy(original_,
630
		       { false, // state-based acc forced below
631
			 false, // single acc set by set_generalized_buchi
632
633
634
		         true,  // weakness preserved,
			 false, // determinism checked and set below
		       });
635
        if (nb_minato == nb_satoneset && !Cosimulation)
636
637
638
	  res->prop_deterministic();
	if (Sba)
	  res->prop_state_based_acc();
639
640
641
642
643
644
645
646
647
648
649
	return res;
      }


      // 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()
      {
650
	for (auto& p: bdd_lstate_)
Thomas Badie's avatar
Thomas Badie committed
651
652
          {
            std::cerr << "partition: "
653
                      << bdd_format_isop(a_->get_dict(), p.first)
Thomas Badie's avatar
Thomas Badie committed
654
                      << std::endl;
655
            for (auto s: p.second)
656
657
658
	      std::cerr << "  - "
			<< a_->format_state(a_->state_from_number(s))
			<< '\n';
Thomas Badie's avatar
Thomas Badie committed
659
660
          }

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

663
664
	unsigned ps = previous_class_.size();
	for (unsigned p = 0; p < ps; ++p)
Thomas Badie's avatar
Thomas Badie committed
665
          {
666
            std::cerr << a_->format_state(a_->state_from_number(p))
Thomas Badie's avatar
Thomas Badie committed
667
                      << " was in "
668
                      << bdd_format_set(a_->get_dict(), previous_class_[p])
669
                      << '\n';
Thomas Badie's avatar
Thomas Badie committed
670
          }
671
      }
Thomas Badie's avatar
Thomas Badie committed
672

Thomas Badie's avatar
Thomas Badie committed
673
    protected:
674
      // The automaton which is simulated.
675
      tgba_digraph_ptr a_;
Thomas Badie's avatar
Thomas Badie committed
676

677
678
679
680
681
682
683
      // Relation is aimed to represent the same thing than
      // rel_. The difference is in the way it does.
      // If A => A /\ A => B, rel will be (!A U B), but relation_
      // will have A /\ B at the key A. This trick is due to a problem
      // with the computation of the resulting automaton with the signature.
      // rel_ will pollute the meaning of the signature.
      map_bdd_bdd relation_;
Thomas Badie's avatar
Thomas Badie committed
684

685
      // Represent the class of each state at the previous iteration.
686
      vector_state_bdd previous_class_;
Thomas Badie's avatar
Thomas Badie committed
687

688
689
690
      // 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
691

692
693
694
      // 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
695

696
697
      // 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
698

699
700
      // Size of the automaton.
      unsigned int size_a_;
Thomas Badie's avatar
Thomas Badie committed
701

702
703
704
      // Used to know when there is no evolution in the po. Updated
      // in the `update_po' method.
      unsigned int po_size_;
Thomas Badie's avatar
Thomas Badie committed
705

706
707
      // All the class variable:
      bdd all_class_var_;
Thomas Badie's avatar
Thomas Badie committed
708
709
710
711

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

Thomas Badie's avatar
Thomas Badie committed
712
713
      bdd all_proms_;

714
      automaton_size stat;
715

716
      std::unique_ptr<scc_info> scc_info_;
Thomas Badie's avatar
Thomas Badie committed
717

718
      const const_tgba_digraph_ptr& original_;
Thomas Badie's avatar
Thomas Badie committed
719
720
    };

Thomas Badie's avatar
Thomas Badie committed
721
722
  } // End namespace anonymous.

Thomas Badie's avatar
Thomas Badie committed
723

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

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

738
  tgba_digraph_ptr
739
  cosimulation(const const_tgba_digraph_ptr& t)
Thomas Badie's avatar
Thomas Badie committed
740
  {
741
742
743
    direct_simulation<true, false> simul(t);
    return simul.run();
  }
Thomas Badie's avatar
Thomas Badie committed
744

745
  tgba_digraph_ptr
746
  cosimulation_sba(const const_tgba_digraph_ptr& t)
747
748
  {
    direct_simulation<true, true> simul(t);
Thomas Badie's avatar
Thomas Badie committed
749
750
751
    return simul.run();
  }

752
753

  template<bool Sba>
754
  tgba_digraph_ptr
755
  iterated_simulations_(const const_tgba_digraph_ptr& t)
756
  {
757
    tgba_digraph_ptr res = 0;
758
759
760
761
762
763
    automaton_size prev;
    automaton_size next;

    do
      {
        prev = next;
764
        direct_simulation<false, Sba> simul(res ? res : t);
765
        res = simul.run();
766
        if (res->is_deterministic())
767
	  break;
Thomas Badie's avatar
Thomas Badie committed
768

769
770
        direct_simulation<true, Sba> cosimul(res);
	res = cosimul.run();
771

772
	if (Sba)
773
	  res = scc_filter_states(res);
774
	else
775
	  res = scc_filter(res, false);
776
777

        next.set_size(res);
778
779
780
781
782
      }
    while (prev != next);
    return res;
  }

783
  tgba_digraph_ptr
784
  iterated_simulations(const const_tgba_digraph_ptr& t)
785
786
787
788
  {
    return iterated_simulations_<false>(t);
  }

789
  tgba_digraph_ptr
790
  iterated_simulations_sba(const const_tgba_digraph_ptr& t)
791
792
793
794
  {
    return iterated_simulations_<true>(t);
  }

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