simulation.cc 22.8 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>
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
64
// "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'.
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
      {
	states = a->num_states();
113
	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
Thomas Badie's avatar
Thomas Badie committed
159
    {
Thomas Badie's avatar
Thomas Badie committed
160
    protected:
161
162
      // Shortcut used in update_po and go_to_next_it.
      typedef std::map<bdd, bdd, bdd_less_than> map_bdd_bdd;
163
      int acc_vars;
164
      acc_cond::mark_t all_inf_;
165
    public:
166
167
168
169
170
171
172
173
174
175

      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;
      }

176
      acc_cond::mark_t bdd_to_mark(const twa_graph_ptr& aut, bdd b)
177
178
179
180
181
182
183
184
185
186
187
      {
	// 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());
      }

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

197
198
199
200
201
202
203
204
	// 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
205

206
207
208
	auto all_inf = in->get_acceptance().used_inf_fin_sets().first;
	all_inf_ = all_inf;

209
	// Replace all the acceptance conditions by their complements.
210
	// (In the case of Cosimulation, we also flip the edges.)
211
212
	if (Cosimulation)
	  {
213
	    a_ = make_twa_graph(in->get_dict());
214
	    a_->copy_ap_of(in);
215
	    a_->copy_acceptance_of(in);
216
	    a_->new_states(ns);
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233

	    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))
			  {
234
			    acc = td.acc ^ all_inf;
235
236
237
238
239
			    break;
			  }
		      }
		    else
		      {
240
			acc = t.acc ^ all_inf;
241
		      }
242
		    a_->new_edge(t.dst, s, t.cond, acc);
243
244
245
246
247
248
		  }
		a_->set_init_state(init_state_number);
	      }
	  }
	else
	  {
249
	    a_ = make_twa_graph(in, twa::prop_set::all());
250
	    for (auto& t: a_->edges())
251
	      t.acc ^= all_inf;
252
253
	  }
	assert(a_->num_states() == size_a_);
254
255
256
257
258

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

261
	unsigned n_acc = a_->num_sets();
262
263
264
265
266
267
	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
268

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

	used_var_.push_back(init);

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

279
280
281
282
	// 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.
283
	all_class_var_ = init;
284
	for (unsigned i = set_num; i < set_num + size_a_ - 1; ++i)
Thomas Badie's avatar
Thomas Badie committed
285
286
287
288
289
          {
            free_var_.push(i);
            all_class_var_ &= bdd_ithvar(i);
          }

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


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

302
      // Update the name of the classes.
303
304
305
306
307
308
      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.
309
	for (auto& p: bdd_lstate_)
Thomas Badie's avatar
Thomas Badie committed
310
          {
311
	    // If the signature of a state is bddfalse (no
312
	    // edges) the class of this state is bddfalse
313
314
	    // instead of an anonymous variable. It allows
	    // simplifications in the signature by removing a
315
316
	    // edge which has as a destination a state with
	    // no outgoing edge.
317
318
	    if (p.first == bddfalse)
	      for (auto s: p.second)
319
		previous_class_[s] = bddfalse;
320
321
	    else
	      for (auto s: p.second)
322
		previous_class_[s] = *it_bdd;
323
	    ++it_bdd;
Thomas Badie's avatar
Thomas Badie committed
324
          }
325
326
      }

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

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

      // The core loop of the algorithm.
347
      twa_graph_ptr run()
Thomas Badie's avatar
Thomas Badie committed
348
349
      {
        main_loop();
350
351
	return build_result();
      }
Thomas Badie's avatar
Thomas Badie committed
352

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

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

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

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

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

        return res;
376
377
      }

Thomas Badie's avatar
Thomas Badie committed
378

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


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

Thomas Badie's avatar
Thomas Badie committed
391
392
393

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

Thomas Badie's avatar
Thomas Badie committed
401
402
403

        // If we have reduced the number of partition, we 'free' them
        // in the free_var_ list.
404
405
406
407
408
409
410
411
412
413
414
	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
415

416
417
418
419
420
421
422
	// 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
423

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

426
	for (auto& p: bdd_lstate_)
Thomas Badie's avatar
Thomas Badie committed
427
          {
428
	    // If the signature of a state is bddfalse (no
429
	    // edges) the class of this state is bddfalse
430
431
	    // instead of an anonymous variable. It allows
	    // simplifications in the signature by removing a
432
433
	    // edge which has as a destination a state with
	    // no outgoing edge.
434
435
436
437
	    bdd acc = bddfalse;
	    if (p.first != bddfalse)
	      acc = *it_bdd;
	    now_to_next[p.first] = acc;
438
	    ++it_bdd;
Thomas Badie's avatar
Thomas Badie committed
439
440
          }

Thomas Badie's avatar
Thomas Badie committed
441
	update_po(now_to_next, relation_);
442
443
      }

Thomas Badie's avatar
Thomas Badie committed
444
445
446
447
448
449
450
451
452
      // 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)
453
454
455
456
457
458
459
460
      {
	// 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
461
462
	for (typename container_bdd_bdd::const_iterator it1
               = now_to_next.begin();
463
464
	     it1 != now_to_next.end();
	     ++it1)
Thomas Badie's avatar
Thomas Badie committed
465
466
          {
            bdd accu = it1->second;
Thomas Badie's avatar
Thomas Badie committed
467
468
            for (typename container_bdd_bdd::const_iterator it2
                   = now_to_next.begin();
Thomas Badie's avatar
Thomas Badie committed
469
470
                 it2 != now_to_next.end();
                 ++it2)
Thomas Badie's avatar
Thomas Badie committed
471
472
473
474
475
476
477
478
479
480
481
              {
                // 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
482
            relation[it1->second] = accu;
Thomas Badie's avatar
Thomas Badie committed
483
          }
484
485
486
      }

      // Build the minimal resulting automaton.
487
      twa_graph_ptr build_result()
488
      {
489
	twa_graph_ptr res = make_twa_graph(a_->get_dict());
490
	res->copy_ap_of(a_);
491
	res->copy_acceptance_of(a_);
492
493

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

496
497
	auto* gb = res->create_namer<int>();

498
	// Create one state per partition.
499
	for (auto& p: bdd_lstate_)
Thomas Badie's avatar
Thomas Badie committed
500
          {
501
502
503
504
505
            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
506
507
          }

508
	// Acceptance of states.  Only used if Sba && Cosimulation.
509
	std::vector<acc_cond::mark_t> accst;
510
	if (Sba && Cosimulation)
511
	  accst.resize(res->num_states(), 0U);
512

513
        stat.states = bdd_lstate_.size();
514
        stat.edges = 0;
515

Thomas Badie's avatar
Thomas Badie committed
516
517
518
        unsigned nb_satoneset = 0;
        unsigned nb_minato = 0;

519
	auto all_inf = all_inf_;
520
	// For each class, we will create
521
	// all the edges between the states.
522
	for (auto& p: bdd_lstate_)
Thomas Badie's avatar
Thomas Badie committed
523
          {
524
525
526
527
528
	    // 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.
529
            bdd sig = compute_sig(p.second.front());
Thomas Badie's avatar
Thomas Badie committed
530

Thomas Badie's avatar
Thomas Badie committed
531
532
533
            if (Cosimulation)
              sig = bdd_compose(sig, bddfalse, bdd_var(bdd_initial));

Thomas Badie's avatar
Thomas Badie committed
534
535
536
537
538
539
540
541
542
543
544
545
546
            // 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)
547
548
549
550
551
552
	      {
		bdd one = bdd_satoneset(all_atomic_prop,
					sup_all_atomic_prop,
					bddtrue);
		all_atomic_prop -= one;

553
		// For each possible valuation, iterate over all possible
554
555
556
557
558
559
560
561
562
		// 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
563
564
                ++nb_satoneset;

565
566
567
		bdd cond_acc_dest;
		while ((cond_acc_dest = isop.next()) != bddfalse)
		  {
568
                    ++stat.edges;
569

Thomas Badie's avatar
Thomas Badie committed
570
571
                    ++nb_minato;

572
		    // Take the edge, and keep only the variable which
573
		    // are used to represent the class.
574
		    bdd dst = bdd_existcomp(cond_acc_dest,
575
576
577
					     all_class_var_);

		    // Keep only ones who are acceptance condition.
578
579
		    auto acc = bdd_to_mark(res, bdd_existcomp(cond_acc_dest,
							      all_proms_));
580

581
		    // Keep the other!
582
583
584
		    bdd cond = bdd_existcomp(cond_acc_dest,
					     sup_all_atomic_prop);

585
586
		    // Because we have complemented all the Inf
		    // acceptance conditions on the input automaton,
587
		    // we must revert them to create a new edge.
588
		    acc ^= all_inf;
589

590
591
592
		    if (Cosimulation)
		      {
			if (Sba)
593
594
			  {
			    // acc should be attached to src, or rather,
595
596
			    // in our edge-based representation)
			    // to all edges leaving src.  As we
597
598
599
			    // can't do this here, store this in a table
			    // so we can fix it later.
			    accst[gb->get_state(src.id())] = acc;
600
			    acc = 0U;
601
			  }
602
			gb->new_edge(dst.id(), src.id(), cond, acc);
603
		      }
604
		    else
605
		      {
606
			gb->new_edge(src.id(), dst.id(), cond, acc);
607
		      }
608
609
		  }
	      }
Thomas Badie's avatar
Thomas Badie committed
610
611
          }

612
613
	res->set_init_state(gb->get_state(previous_class_
					  [a_->get_init_state_number()].id()));
Thomas Badie's avatar
Thomas Badie committed
614

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

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

632
633
	res->purge_unreachable_states();

634
	delete gb;
635
	res->prop_copy(original_,
636
637
		       { false, // state-based acc forced below
		         true,  // weakness preserved,
638
639
			 true, // determinism checked and overridden below
			       // and "unambiguous" property preserved
640
			 true, // stutter inv.
641
		       });
642
        if (nb_minato == nb_satoneset && !Cosimulation)
643
	  res->prop_deterministic(true);
644
	if (Sba)
645
	  res->prop_state_acc(true);
646
647
648
649
650
651
652
653
654
655
656
	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()
      {
657
	for (auto& p: bdd_lstate_)
Thomas Badie's avatar
Thomas Badie committed
658
659
          {
            std::cerr << "partition: "
660
                      << bdd_format_isop(a_->get_dict(), p.first)
Thomas Badie's avatar
Thomas Badie committed
661
                      << std::endl;
662
            for (auto s: p.second)
663
664
665
	      std::cerr << "  - "
			<< a_->format_state(a_->state_from_number(s))
			<< '\n';
Thomas Badie's avatar
Thomas Badie committed
666
667
          }

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

670
671
	unsigned ps = previous_class_.size();
	for (unsigned p = 0; p < ps; ++p)
Thomas Badie's avatar
Thomas Badie committed
672
          {
673
            std::cerr << a_->format_state(a_->state_from_number(p))
Thomas Badie's avatar
Thomas Badie committed
674
                      << " was in "
675
                      << bdd_format_set(a_->get_dict(), previous_class_[p])
676
                      << '\n';
Thomas Badie's avatar
Thomas Badie committed
677
          }
678
      }
Thomas Badie's avatar
Thomas Badie committed
679

Thomas Badie's avatar
Thomas Badie committed
680
    protected:
681
      // The automaton which is simulated.
682
      twa_graph_ptr a_;
Thomas Badie's avatar
Thomas Badie committed
683

684
685
686
687
688
689
690
      // 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
691

692
      // Represent the class of each state at the previous iteration.
693
      vector_state_bdd previous_class_;
Thomas Badie's avatar
Thomas Badie committed
694

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

699
700
701
      // 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
702

703
704
      // 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
705

706
707
      // Size of the automaton.
      unsigned int size_a_;
Thomas Badie's avatar
Thomas Badie committed
708

709
710
711
      // 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
712

713
714
      // All the class variable:
      bdd all_class_var_;
Thomas Badie's avatar
Thomas Badie committed
715
716
717
718

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

Thomas Badie's avatar
Thomas Badie committed
719
720
      bdd all_proms_;

721
      automaton_size stat;
722

723
      std::unique_ptr<scc_info> scc_info_;
Thomas Badie's avatar
Thomas Badie committed
724

725
      const const_twa_graph_ptr original_;
Thomas Badie's avatar
Thomas Badie committed
726
727
    };

Thomas Badie's avatar
Thomas Badie committed
728
729
  } // End namespace anonymous.

Thomas Badie's avatar
Thomas Badie committed
730

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

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

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

752
753
  twa_graph_ptr
  cosimulation_sba(const const_twa_graph_ptr& t)
754
755
  {
    direct_simulation<true, true> simul(t);
Thomas Badie's avatar
Thomas Badie committed
756
757
758
    return simul.run();
  }

759
760

  template<bool Sba>
761
762
  twa_graph_ptr
  iterated_simulations_(const const_twa_graph_ptr& t)
763
  {
764
    twa_graph_ptr res = nullptr;
765
766
767
768
769
770
    automaton_size prev;
    automaton_size next;

    do
      {
        prev = next;
771
        direct_simulation<false, Sba> simul(res ? res : t);
772
        res = simul.run();
773
        if (res->prop_deterministic())
774
	  break;
Thomas Badie's avatar
Thomas Badie committed
775

776
777
        direct_simulation<true, Sba> cosimul(res);
	res = cosimul.run();
778

779
	if (Sba)
780
	  res = scc_filter_states(res, false);
781
	else
782
	  res = scc_filter(res, false);
783
784

        next.set_size(res);
785
786
787
788
789
      }
    while (prev != next);
    return res;
  }

790
791
  twa_graph_ptr
  iterated_simulations(const const_twa_graph_ptr& t)
792
793
794
795
  {
    return iterated_simulations_<false>(t);
  }

796
797
  twa_graph_ptr
  iterated_simulations_sba(const const_twa_graph_ptr& t)
798
799
800
801
  {
    return iterated_simulations_<true>(t);
  }

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