tgbareduc.cc 12.1 KB
Newer Older
1
2
// Copyright (C) 2008, 2009, 2011 Laboratoire de Recherche et
// Developpement de l'Epita (LRDE).
Guillaume Sadegh's avatar
Guillaume Sadegh committed
3
// Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
4
5
// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
// Université Pierre et Marie Curie.
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
//
// 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
// the Free Software Foundation; either version 2 of the License, or
// (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
// along with Spot; see the file COPYING.  If not, write to the Free
// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
// 02111-1307, USA.

#include "tgbareduc.hh"
#include <sstream>

namespace spot
{
  namespace
  {
    typedef std::pair<const spot::state*, tgba_succ_iterator*> pair_state_iter;
  }

34
  tgba_reduc::tgba_reduc(const tgba* a)
35
    : tgba_explicit_string(a->get_dict()),
36
      tgba_reachable_iterator_breadth_first(a)
37
  {
martinez's avatar
martinez committed
38
    dict_->register_all_variables_of(a, this);
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55

    run();
    all_acceptance_conditions_ = a->all_acceptance_conditions();
    all_acceptance_conditions_computed_ = true;
  }

  tgba_reduc::~tgba_reduc()
  {
    sp_map::iterator i;
    for (i = state_predecessor_map_.begin();
	 i!= state_predecessor_map_.end(); ++i)
      {
	delete i->second;
      }
  }

  void
martinez's avatar
martinez committed
56
  tgba_reduc::quotient_state(direct_simulation_relation* rel)
57
  {
martinez's avatar
martinez committed
58
59
    // Remember that for each state couple
    // (*i)->second simulate (*i)->first.
60

martinez's avatar
martinez committed
61
    for (direct_simulation_relation::iterator i = rel->begin();
62
63
64
65
66
67
68
69
70
	 i != rel->end(); ++i)
      {

	// All state simulate himself.
	if (((*i)->first)->compare((*i)->second) == 0)
	  continue;

	// We check if the two state are co-simulate.
	bool recip = false;
martinez's avatar
martinez committed
71
	for (direct_simulation_relation::iterator j = i;
72
73
74
75
76
	     j != rel->end(); ++j)
	  if ((((*i)->first)->compare((*j)->second) == 0) &&
	      (((*j)->first)->compare((*i)->second) == 0))
	    recip = true;

martinez's avatar
martinez committed
77
78
79
	if (recip)
	  //this->redirect_transition((*i)->first, (*i)->second);
	  this->merge_state((*i)->first, (*i)->second);
80
81
82
83
84
85
      }

    this->merge_transitions();
  }

  void
martinez's avatar
martinez committed
86
  tgba_reduc::quotient_state(delayed_simulation_relation* rel)
87
  {
martinez's avatar
martinez committed
88
89
    if (nb_set_acc_cond() > 1)
      return;
90

martinez's avatar
martinez committed
91
92
93
    //this->quotient_state(rel);

    for (delayed_simulation_relation::iterator i = rel->begin();
94
95
96
97
98
99
100
101
102
	 i != rel->end(); ++i)
      {

	// All state simulate himself.
	if (((*i)->first)->compare((*i)->second) == 0)
	  continue;

	// We check if the two state are co-simulate.
	bool recip = false;
martinez's avatar
martinez committed
103
	for (delayed_simulation_relation::iterator j = i;
104
105
106
107
108
109
110
111
112
113
114
115
	     j != rel->end(); ++j)
	  if ((((*i)->first)->compare((*j)->second) == 0) &&
	      (((*j)->first)->compare((*i)->second) == 0))
	    recip = true;

	if (recip)
	  this->merge_state((*i)->first, (*i)->second);
      }

    this->merge_transitions();
  }

martinez's avatar
martinez committed
116
117
118
119
120
121
122
123
124
125
126
127
128
  void
  tgba_reduc::delete_transitions(simulation_relation* rel)
  {
    for (simulation_relation::iterator i = rel->begin();
	 i != rel->end(); ++i)
      {
	if (((*i)->first)->compare((*i)->second) == 0)
	  continue;
	this->redirect_transition((*i)->first, (*i)->second);
      }
    this->merge_transitions();
  }

129
  ////////////////////////////////////////////
martinez's avatar
martinez committed
130
  // for build tgba_reduc
131
132
133
134

  void
  tgba_reduc::process_state(const spot::state* s, int, tgba_succ_iterator* si)
  {
135
    spot::state* init = aut_->get_init_state();
136
    if (init->compare(s) == 0)
137
      this->set_init_state(aut_->format_state(s));
138
    init->destroy();
139
140
141
142
143
144
145
146

    transition* t;
    for (si->first(); !si->done(); si->next())
      {
	init = si->current_state();
	t = this->create_transition(s, init);
	this->add_conditions(t, si->current_condition());
	this->add_acceptance_conditions(t, si->current_acceptance_conditions());
147
	init->destroy();
148
149
150
      }
  }

Pierre PARUTTO's avatar
Pierre PARUTTO committed
151
  tgba_explicit_string::transition*
152
153
154
  tgba_reduc::create_transition(const spot::state* source,
				const spot::state* dest)
  {
155
156
    const std::string ss = aut_->format_state(source);
    const std::string sd = aut_->format_state(dest);
157

Pierre PARUTTO's avatar
Pierre PARUTTO committed
158
159
    state_explicit_string* s = tgba_explicit_string::add_state(ss);
    state_explicit_string* d = tgba_explicit_string::add_state(sd);
160

161
162
    transition t;
    t.dest = d;
163
164
165
166
167
168
169
170
171
172
173
174
175

    sp_map::iterator i = state_predecessor_map_.find(d);
    if (i == state_predecessor_map_.end())
      {
	std::list<state*>* pred = new std::list<state*>;
	pred->push_back(s);
	state_predecessor_map_[d] = pred;
      }
    else
      {
	(i->second)->push_back(s);
      }

176
177
    t.condition = bddtrue;
    t.acceptance_conditions = bddfalse;
Pierre PARUTTO's avatar
Pierre PARUTTO committed
178
    state_explicit_string::transitions_t::iterator is
179
180
      = s->successors.insert(s->successors.end(), t);
    return &*is;
181
182
183
184
185
186
187
188
189
190
191
192
  }

  ///////////////////////////////////////////////////

  void
  tgba_reduc::redirect_transition(const spot::state* s,
				  const spot::state* simul)
  {
    bool belong = false;
    bdd cond_simul;
    bdd acc_simul;
    std::list<state*> ltmp;
Pierre PARUTTO's avatar
Pierre PARUTTO committed
193
194
195
196
    const state_explicit_string* s1 =
      &(ls_[tgba_explicit_string::format_state(s)]);
    const state_explicit_string* s2 =
      &(ls_[tgba_explicit_string::format_state(simul)]);
197
198
199
200
201
202
203
204
205
206
207

    sp_map::iterator i = state_predecessor_map_.find(s1);
    if (i == state_predecessor_map_.end()) // 0 predecessor
	return;

    // for all predecessor of s.
    for (std::list<state*>::iterator p = (i->second)->begin();
	 p != (i->second)->end(); ++p)
      {
	// We check if simul belong to the successor of p,
	// as s belong too.
Pierre PARUTTO's avatar
Pierre PARUTTO committed
208
	for (state_explicit_string::transitions_t::iterator
209
210
211
	       j = (*p)->successors.begin();
	     j != (*p)->successors.end(); ++j)
	  if (j->dest == s2) // simul belong to the successor of p.
212
213
	    {
	      belong = true;
214
215
	      cond_simul = j->condition;
	      acc_simul = j->acceptance_conditions;
216
217
218
219
220
221
222
223
	      break;
	    }

	// If not, we check for another predecessor of s.
	if (!belong)
	  continue;

	// for all successor of p, a predecessor of s and simul.
Pierre PARUTTO's avatar
Pierre PARUTTO committed
224
	for (state_explicit_string::transitions_t::iterator
225
226
	       j = (*p)->successors.begin();
	     j != (*p)->successors.end(); ++j)
227
228
	  {
	    // if the transition lead to s.
229
	    if ((j->dest == s1) &&
230
231
		// if the label of the transition whose lead to s implies
		// this leading to simul.
232
233
		(((!j->condition | cond_simul) == bddtrue) &&
		 ((!j->acceptance_conditions) | acc_simul) == bddtrue))
234
235
	      {
		// We can redirect transition leading to s on simul.
Pierre PARUTTO's avatar
Pierre PARUTTO committed
236
		j->dest = const_cast<state_explicit_string*>(s2);
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
267
268
269
270
271

		// We memorize that we have to remove p
		// of the predecessor of s.
		ltmp.push_back(*p);
	      }
	  }
	belong = false;
      }

    // We remove all the predecessor of s than we have memorized.
    std::list<state*>::iterator k;
    for (k = ltmp.begin();
	 k != ltmp.end(); ++k)
      this->remove_predecessor_state(i->first, *k);
  }

  void
  tgba_reduc::remove_predecessor_state(const state* s, const state* p)
  {
    sp_map::iterator i = state_predecessor_map_.find(s);
    if (i == state_predecessor_map_.end()) // 0 predecessor
      return;

    // for all predecessor of s we remove p.
    for (std::list<state*>::iterator j = (i->second)->begin();
	 j != (i->second)->end();)
      if (p == *j)
	j = (i->second)->erase(j);
      else
	++j;
  }

  void
  tgba_reduc::remove_state(const spot::state* s)
  {
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
272
273
274
    // We suppose that the state is not reachable when called by
    // merge_state => NO PREDECESSOR.  But it can be have some
    // predecessor in state_predecessor_map_.
275

Pierre PARUTTO's avatar
Pierre PARUTTO committed
276
277
278
    ls_map::iterator k =
      ls_.find(tgba_explicit_string::format_state(s));
    if (k == ls_.end()) // 0 predecessor
279
280
	return;

Pierre PARUTTO's avatar
Pierre PARUTTO committed
281
282
    state_explicit_string* st =
      &(ls_[tgba_explicit_string::format_state(s)]);
283
284

    // for all successor q of s, we remove s of the predecessor of q.
285
    // Note that the initial node can't be removed.
Pierre PARUTTO's avatar
Pierre PARUTTO committed
286
    for (state_explicit_string::transitions_t::iterator j =
287
	   st->successors.begin(); j != st->successors.end(); ++j)
Pierre PARUTTO's avatar
Pierre PARUTTO committed
288
289
      this->remove_predecessor_state(down_cast<const state_explicit_string*>
				     (j->dest), st);
290
291
292
293
294
295


    sp_map::iterator i = state_predecessor_map_.find(st);
    if (i == state_predecessor_map_.end()) // 0 predecessor
	return;

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
296
    // for all predecessor of s (none when called by merge_state)
297
298
299
300
    for (std::list<state*>::iterator p = (i->second)->begin();
	 p != (i->second)->end(); ++p)
      {
	// for all transition of p, a predecessor of s.
Pierre PARUTTO's avatar
Pierre PARUTTO committed
301
	for (state_explicit_string::transitions_t::iterator
302
303
	       j = (*p)->successors.begin();
	     j != (*p)->successors.end();)
304
	  {
305
	    if (j->dest == st)
306
307
	      {
		// Remove the transition
308
		j = (*p)->successors.erase(j);
309
310
311
312
313
314
315
316
		++j;
	      }
	    else
	      ++j;
	  }
      }

    // DESTROY THE STATE !? USELESS
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
317
    // it will be destroyed when the automaton is deleted
318
319
320
321
322
323
324
    // name_state_map_::iterator = name_state_map_[st];
    // const tgba_explicit::state* st = name_state_map_[this->format_state(s)];
  }

  void
  tgba_reduc::merge_state(const spot::state* sim1, const spot::state* sim2)
  {
Pierre PARUTTO's avatar
Pierre PARUTTO committed
325
326
327
328
329
    const state_explicit_string* s1 =
      &(ls_[tgba_explicit_string::format_state(sim1)]);
    const state_explicit_string* s2 =
      &(ls_[tgba_explicit_string::format_state(sim2)]);
    const state_explicit_string* stmp = s1;
330
331
332
333
334
335
336
337
338
339
340
    const spot::state* simtmp = sim1;

    // if sim1 is the init state, we remove sim2.
    spot::state* init = this->get_init_state();
    if (sim1->compare(init) == 0)
      {
	s1 = s2;
	s2 = stmp;
	sim1 = sim2;
	sim2 = simtmp;
      }
341
    init->destroy();
342
343
344
345

    sp_map::iterator i = state_predecessor_map_.find(s1);
    if (i == state_predecessor_map_.end()) // 0 predecessor
      {
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
346
	// We can remove s1 safely, without changing the language
347
348
349
350
351
352
	// of the automaton.
	this->remove_state(sim1);
	return;
      }

    // for all predecessor of s1, not the initial state,
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
353
    // we redirect to s2 the transitions that lead to s1.
354
355
356
357
    for (std::list<state*>::iterator p = (i->second)->begin();
	 p != (i->second)->end(); ++p)
      {
	// for all successor of p, a predecessor of s1.
Pierre PARUTTO's avatar
Pierre PARUTTO committed
358
	for (state_explicit_string::transitions_t::iterator
359
360
	       j = (*p)->successors.begin();
	     j != (*p)->successors.end(); ++j)
361
	  {
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
362
	    // if the successor was s1...
363
	    if (j->dest == s1)
364
	      {
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
365
		// ... make it s2.
Pierre PARUTTO's avatar
Pierre PARUTTO committed
366
		j->dest = const_cast<state_explicit_string*>(s2);
367
368
369
370
	      }
	  }
      }

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
371
372
373
374
375
376
    // FIXME: The following justification sounds really dubious.
    //
    // We have to stock on s2 the acceptance condition of the arc
    // leaving s1 (possible when the simulation is delayed). Since s2
    // simulates s1, s2 has some labels that imply these of s1, so we
    // can put the acceptance conditions on its arcs.
Pierre PARUTTO's avatar
Pierre PARUTTO committed
377
    for (state_explicit_string::transitions_t::const_iterator
378
379
	   j = s1->successors.begin();
	 j != s1->successors.end(); ++j)
martinez's avatar
martinez committed
380
      {
381
382
383
384
	transition t;
	t.dest = j->dest;
	t.condition = j->condition;
	t.acceptance_conditions = j->acceptance_conditions;
Pierre PARUTTO's avatar
Pierre PARUTTO committed
385
	const_cast<state_explicit_string*>(s2)->successors.push_back(t);
martinez's avatar
martinez committed
386
387
      }

388
389
390
    // We remove all the predecessor of s1.
    (i->second)->clear();

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
391
    // then we can remove s1 safely, without changing the language
392
393
394
395
    // of the automaton.
    this->remove_state(sim1);
  }

martinez's avatar
martinez committed
396
397
398
399
  void
  tgba_reduc::merge_state_delayed(const spot::state*,
				  const spot::state*)
  {
martinez's avatar
martinez committed
400
    // TO DO
martinez's avatar
martinez committed
401
402
  }

martinez's avatar
martinez committed
403
404
405
406
407
408
409
410
411
  int
  tgba_reduc::nb_set_acc_cond() const
  {
    bdd acc, all;
    acc = all = this->all_acceptance_conditions();
    int count = 0;
    while (all != bddfalse)
      {
	all -= bdd_satone(all);
412
	++count;
martinez's avatar
martinez committed
413
414
415
      }
    return count;
  }
416

417
418
419
420
421
422
423
424
425
426
427
428
429
  //////// JUST FOR DEBUG //////////

  void
  tgba_reduc::display_rel_sim(simulation_relation* rel,
			      std::ostream& os)
  {
    int n = 0;
    simulation_relation::iterator i;
    for (i = rel->begin(); i != rel->end(); ++i)
      {
	if (((*i)->first)->compare((*i)->second) == 0)
	  continue;

430
	  ++n;
431
432
433
434
435
436
437
438
439
440
441
442
443
	  os << "couple " << n
	     << std::endl
	     << "  " << " [label=\""
	     << this->format_state((*i)->first) << "\"]"
	     << std::endl
	     << "  " << " [label=\""
	     << this->format_state((*i)->second) << "\"]"
	     << std::endl
	     << std::endl;
      }
  }

}