emptinesscheck.cc 15.4 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
#include "emptinesscheck.hh"
#include "tgba/tgba.hh"
#include "tgba/state.hh"
#include "tgba/bddprint.hh"
#include "tgba/tgbabddfactory.hh"
#include "tgba/succiterconcrete.hh"
#include "tgba/tgbabddconcrete.hh"
#include "bdd.h"
#include <map>
#include <list>
#include <sstream>
#include <stack>
#include <queue>
#include <stdio.h>
#include <vector>
#include <set>
17
18
19
#include <iterator>
#include <utility>
#include <ostream>
20
21
22
23
24

namespace spot
{
  connected_component::connected_component()
  {
25
26
27
28
29
30
    index = 0;
    condition = bddfalse;
    transition_acc = -1;
    nb_transition = 0;
    nb_state = 1;
    not_null = false;
31
32
  }

33
  connected_component::connected_component(int i, bdd a)
34
  {
35
36
37
38
39
40
    index = i;
    condition = a;
    transition_acc = -1;
    nb_transition = 0;
    nb_state = 1;
    not_null = false;
41
42
  }

43
  connected_component::~connected_component()
44
45
46
47
48
49
50
51
52
  {
  }

  bool
  connected_component::isAccepted(tgba* aut)
  {
    return aut->all_accepting_conditions() == condition;
  }

53
54
55
56
  /// \brief Remove all the nodes accessible from the given node start_delete.
  ///
  /// The removed graph is the subgraph containing nodes stored
  /// in table state_map with order -1.
57
  void
58
59
60
  emptiness_check::remove_component(const tgba& aut, seen& state_map,
				    const spot::state* start_delete)
  {
61
62
63
64
65
    std::stack<spot::tgba_succ_iterator*> to_remove;
    state_map[start_delete] = -1;
    tgba_succ_iterator* iter_delete = aut.succ_iter(start_delete);
    iter_delete->first();
    to_remove.push(iter_delete);
66
    while (!to_remove.empty())
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
      {
	tgba_succ_iterator* succ_delete = to_remove.top();
	to_remove.pop();
	if (!succ_delete->done())
	  {
	    to_remove.push(succ_delete);
	    state* curr_state = succ_delete->current_state();
	    succ_delete->next();
	    if (state_map[curr_state] != -1)
	      {
		state_map[curr_state] = -1;
		tgba_succ_iterator* succ_delete2 = aut.succ_iter(curr_state);
		succ_delete2->first();
		to_remove.push(succ_delete2);
	      }
	  }
      }
84
  }
85

86
87
88
89
  /// \brief On-the-fly emptiness check.
  ///
  /// The algorithm used here is adapted from Jean-Michel Couvreur's
  /// Probataf tool.
90
91
92
93
  bool
  emptiness_check::tgba_emptiness_check(const spot::tgba* aut_check)
  {

94
95
96
97
    int nbstate = 1;
    state* init = aut_check->get_init_state();
    seen_state_num[init] = 1;
    root_component.push(spot::connected_component(1,bddfalse));
98
    arc_accepting.push(bddfalse);
99
100
101
    tgba_succ_iterator* iter_ = aut_check->succ_iter(init);
    iter_->first();
    todo.push(pair_state_iter(init, iter_ ));
102
    while (!todo.empty())
103
104
105
106
107
108
109
110
      {
	pair_state_iter step = todo.top();
	if ((step.second)->done())
	  {
	    todo.pop();
	    assert(!root_component.empty());
	    connected_component comp_tmp = root_component.top();
	    root_component.pop();
111
112
	    seen::iterator i_0 = seen_state_num.find(step.first);
	    assert(i_0 != seen_state_num.end());
113
114
115
	    if (comp_tmp.index == seen_state_num[step.first])
	      {
		/// The current node is a root of a Strong Connected Component.
116
117
118
		spot::emptiness_check::remove_component(*aut_check,
							seen_state_num,
							step.first);
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
		assert(!arc_accepting.empty());
		arc_accepting.pop();
		assert(root_component.size() == arc_accepting.size());
	      }
	    else
	      {
		root_component.push(comp_tmp);
		assert(root_component.size() == arc_accepting.size());
	      }
	  }
	else
	  {
	    iter_ = step.second;
	    state* current_state = iter_->current_state();
	    bdd current_accepting = iter_->current_accepting_conditions();
	    seen::iterator i = seen_state_num.find(current_state);
	    iter_->next();
	    if (i == seen_state_num.end())
	      {
138
		// New node.
139
		nbstate = nbstate + 1;
140
		assert(nbstate != 0);
141
142
143
144
145
146
147
148
149
		seen_state_num[current_state] = nbstate;
		root_component.push(connected_component(nbstate, bddfalse));
		arc_accepting.push(current_accepting);
		tgba_succ_iterator* iter2 = aut_check->succ_iter(current_state);
		iter2->first();
		todo.push(pair_state_iter(current_state, iter2 ));
	      }
	    else if (seen_state_num[current_state] != -1)
	      {
150
		// A node with order != -1 (a seen node not removed).
151
152
153
		assert(!root_component.empty());
		connected_component comp = root_component.top();
		root_component.pop();
154
		bdd new_condition = current_accepting;
155
156
157
		int current_index = seen_state_num[current_state];
		while (comp.index > current_index)
		  {
158
159
160
		    // root_component and arc_accepting are popped
		    // until the head of root_component is less or
		    // equal to the order of the current state.
161
162
163
		    assert(!root_component.empty());
		    comp = root_component.top();
		    root_component.pop();
164
		    new_condition |= comp.condition;
165
166
167
		    assert(!arc_accepting.empty());
		    bdd arc_acc = arc_accepting.top();
		    arc_accepting.pop();
168
		    new_condition |= arc_acc;
169
		  }
170
		comp.condition |= new_condition;
171
172
		if (aut_check->all_accepting_conditions() == comp.condition)
		  {
173
		    // A failure SCC was found, the automata is not empty.
174
		    root_component.push(comp);
175
      		    return false;
176
177
178
179
180
181
		  }
		root_component.push(comp);
		assert(root_component.size() == arc_accepting.size());
	      }
	  }
      }
182
    // The automata is empty.
183
184
185
186
    return true;
  }


187
188
189
  std::ostream&
  emptiness_check::print_result(std::ostream& os, const spot::tgba* aut,
				const tgba* restrict) const
190
191
192
193
  {
    os << "======================" << std::endl;
    os << "Prefix:" << std::endl;
    os << "======================" << std::endl;
194
    const bdd_dict* d = aut->get_dict();
195
    for (state_sequence::const_iterator i_se = suffix.begin();
196
	 i_se != suffix.end(); ++i_se)
197
198
199
200
201
202
203
204
205
206
207
      {
	if (restrict)
	  {
	    os << restrict->format_state(aut->project_state((*i_se), restrict))
	       << std::endl;
	  }
	else
	  {
	    os << aut->format_state((*i_se)) << std::endl;
	  }
      }
208
209
210
    os << "======================" << std::endl;
    os << "Cycle:" <<std::endl;
    os << "======================" << std::endl;
211
    for (cycle_path::const_iterator it = period.begin();
212
	 it != period.end(); ++it)
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
      {
	if (restrict)
	  {
	    os << "     | " << bdd_format_set(d, (*it).second) <<std::endl ;
	    os << restrict->format_state(aut->project_state((*it).first,
							    restrict))
	       << std::endl;
	  }
	else
	  {
	    os << "     | " << bdd_format_set(d, (*it).second) <<std::endl ;
	    os << aut->format_state((*it).first) << std::endl;
	  }
      }
    return os;
228
229
  }

230
  /// \brief Build a possible prefix and period for a counter example.
231
  void
232
233
234
235
236
237
  emptiness_check::counter_example(const spot::tgba* aut_counter)
  {
    std::deque <pair_state_iter> todo_trace;
    typedef std::map<const spot::state*, const spot::state*,
                     spot::state_ptr_less_than> path_state;
    path_state path_map;
238

239
240
241
242
243
244
245
246
247
248
249
250
251
252
    assert(!root_component.empty());

    int comp_size = root_component.size();
    typedef std::vector<connected_component> vec_compo;
    vec_compo vec_component;
    vec_component.resize(comp_size);
    vec_sequence.resize(comp_size);
    state_sequence seq;
    state_sequence tmp_lst;
    state_sequence best_lst;
    bdd tmp_acc = bddfalse;
    std::stack<pair_state_iter> todo_accept;

    for (int j = comp_size - 1; j >= 0; j--)
253
      {
254
255
256
	vec_component[j] = root_component.top();
	root_component.pop();
      }
257

258
259
260
261
262
263
264
265
266
    int q_index;
    int tmp_int = 0;
    // Fill the SCC in the stack root_component.
    for (seen::iterator iter_map = seen_state_num.begin();
	 iter_map != seen_state_num.end(); ++iter_map)
      {
	q_index = (*iter_map).second;
	tmp_int = 0;
	if (q_index > 0)
267
	  {
268
269
270
271
272
273
274
	    while ((tmp_int < comp_size)
		   && (vec_component[tmp_int].index <= q_index))
	      tmp_int = tmp_int+1;
	    if (tmp_int < comp_size)
	      vec_component[tmp_int - 1].state_set.insert((*iter_map).first);
	    else
	      vec_component[comp_size - 1].state_set.insert((*iter_map).first);
275
	  }
276
      }
277

278
279
280
281
282
    state* start_state = aut_counter->get_init_state();
    if (comp_size != 1)
      {
	tgba_succ_iterator* i = aut_counter->succ_iter(start_state);
	todo_trace.push_back(pair_state_iter(start_state, i));
283

284
	for (int k = 0; k < comp_size - 1; ++k)
285
	  {
286
287
288
	    // We build a path trought all SCC in the stack: a
	    // possible prefix for a counter example.
	    while (!todo_trace.empty())
289
	      {
290
291
292
		pair_state_iter started_from = todo_trace.front();
		todo_trace.pop_front();
		started_from.second->first();
293

294
295
296
297
298
299
300
301
302
		for (started_from.second->first();
		     !started_from.second->done();
		     started_from.second->next())
		  {
		    const state* curr_state =
		      started_from.second->current_state();
		    connected_component::set_of_state::iterator iter_set =
		      vec_component[k+1].state_set.find(curr_state);
		    if (iter_set != vec_component[k+1].state_set.end())
303
		      {
304
305
306
307
308
309
310
311
312
			const state* curr_father = started_from.first;
			seq.push_front(*iter_set);
			seq.push_front(curr_father);
			seen::iterator i_2 =
			  seen_state_num.find(curr_father);
			assert(i_2 != seen_state_num.end());
			while ((vec_component[k].index
				< seen_state_num[curr_father])
			       && (seen_state_num[curr_father] != 1))
313
			  {
314
315
316
			    seq.push_front(path_map[curr_father]);
			    curr_father = path_map[curr_father];
			    seen::iterator i_3 =
317
			      seen_state_num.find(curr_father);
318
			    assert(i_3 != seen_state_num.end());
319
			  }
320
321
322
323
324
325
326
327
328
329
			vec_sequence[k] = seq;
			seq.clear();
			todo_trace.clear();
			break;
		      }
		    else
		      {
			connected_component::set_of_state::iterator i_s =
			  vec_component[k].state_set.find(curr_state);
			if (i_s != vec_component[k].state_set.end())
330
			  {
331
332
333
334
			    path_state::iterator i_path =
			      path_map.find(curr_state);
			    seen::iterator i_seen =
			      seen_state_num.find(curr_state);
335

336
337
338
339
340
341
342
343
			    if (i_seen != seen_state_num.end()
				&& seen_state_num[curr_state] > 0
				&& i_path == path_map.end())
			      {
				todo_trace.
				  push_back(pair_state_iter(curr_state,
							    aut_counter->succ_iter(curr_state)));
				path_map[curr_state] = started_from.first;
344
345
346
347
348
			      }
			  }
		      }
		  }
	      }
349
350
351
	    todo_trace.
	      push_back(pair_state_iter(vec_sequence[k].back(),
					aut_counter->succ_iter(vec_sequence[k].back())));
352
353
	  }
      }
354
355
    else
      {
356
	suffix.push_front(start_state);
357
      }
358
359
360
361
362
363
364
365
366
    for (int n_ = 0; n_ < comp_size - 1; ++n_)
      for (state_sequence::iterator it = vec_sequence[n_].begin();
	   it != vec_sequence[n_].end(); ++it)
	suffix.push_back(*it);
    suffix.unique();
    emptiness_check::accepting_path(aut_counter,
				    vec_component[comp_size - 1],
				    suffix.back(),
				    vec_component[comp_size - 1].condition);
367
  }
368

369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
  /// \brief complete the path build by accepting_path to get the period.
  void
  emptiness_check::complete_cycle(const spot::tgba* aut_counter,
				  const connected_component& comp_path,
				  const state* from_state,
				  const state* to_state)
  {
    if (seen_state_num[from_state] != seen_state_num[to_state])
      {
	std::map<const spot::state*, state_proposition,
	         spot::state_ptr_less_than> complete_map;
	std::deque<pair_state_iter> todo_complete;
	spot::tgba_succ_iterator* ite = aut_counter->succ_iter(from_state);
	todo_complete.push_back(pair_state_iter(from_state, ite));
	cycle_path tmp_comp;
	while(!todo_complete.empty())
	  {
	    pair_state_iter started_ = todo_complete.front();
	    todo_complete.pop_front();
	    tgba_succ_iterator* iter_s = started_.second;
	    iter_s->first();
	    for (iter_s->first(); !iter_s->done(); iter_s->next())
	      {
		const state* curr_state = (started_.second)->current_state();
		connected_component::set_of_state::iterator i_set =
		  comp_path.state_set.find(curr_state);
		if (i_set != comp_path.state_set.end())
		  {
		    if (curr_state->compare(to_state) == 0)
		      {
			const state* curr_father = started_.first;
			bdd curr_condition = iter_s->current_condition();
			tmp_comp.push_front(state_proposition(curr_state, curr_condition));
			while (curr_father->compare(from_state) != 0)
			  {
			    tmp_comp.push_front(state_proposition(curr_father,
						 complete_map[curr_father].second));
			    curr_father = complete_map[curr_father].first;
			  }
408
			emptiness_check::period.splice(period.end(),
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
							tmp_comp);
			todo_complete.clear();
			break;
		      }
		    else
		      {
			todo_complete.push_back(pair_state_iter(curr_state,
								aut_counter->succ_iter(curr_state)));
			complete_map[curr_state] =
			  state_proposition(started_.first,
					    iter_s->current_condition());
		      }
		  }
	      }
	  }
      }
  }
426

427
428
429
430
431
432
433
  /// \Brief build recursively a path in the accepting SCC to get
  /// all accepting conditions. This path is the first part of the
  /// period.
  void
  emptiness_check::accepting_path(const spot::tgba* aut_counter,
				  const connected_component& comp_path,
				  const spot::state* start_path, bdd to_accept)
434
  {
435
436
437
438
    seen seen_priority;
    std::stack<triplet> todo_path;
    tgba_succ_iterator* t_s_i = aut_counter->succ_iter(start_path);
    t_s_i->first();
439
    todo_path.push(triplet(pair_state_iter(start_path, t_s_i), bddfalse));
440
441
442
443
444
445
446
447
448
    bdd tmp_acc = bddfalse;
    bdd best_acc = bddfalse;
    cycle_path tmp_lst;
    cycle_path best_lst;
    bool ok = false;
    seen_priority[start_path] = seen_state_num[start_path];
    while (!todo_path.empty())
      {
	triplet step_ = todo_path.top();
449
	tgba_succ_iterator* iter_ = step_.first.second;
450
451
452
	if (iter_->done())
	  {
	    todo_path.pop();
453
	    seen_priority.erase(step_.first.first);
454
455
456
457
458
	    tmp_lst.pop_back();
	  }
	else
	  {
	    state* curr_state = iter_->current_state();
459
460
	    connected_component::set_of_state::iterator it_set =
	      comp_path.state_set.find(curr_state);
461
462
463
464
465
	    if (it_set != comp_path.state_set.end())
	      {
		seen::iterator i = seen_priority.find(curr_state);
		if (i == seen_priority.end())
		  {
466
467
468
		    tgba_succ_iterator* c_iter =
		      aut_counter->succ_iter(curr_state);
		    bdd curr_bdd =
469
		      iter_->current_accepting_conditions() | step_.second;
470
471
472
473
474
475
		    c_iter->first();
		    todo_path.push(triplet(pair_state_iter(curr_state, c_iter),
					   curr_bdd));
		    tmp_lst.push_back(state_proposition(curr_state,
							iter_->current_condition()));
		    seen_priority[curr_state] = seen_state_num[curr_state];
476
477
478
479
480
481
482
483
		  }
		else
		  {
		    if (ok)
		      {
			bdd last_ = iter_->current_accepting_conditions();
			bdd prop_ = iter_->current_condition();
			tmp_lst.push_back(state_proposition(curr_state, prop_));
484
485
486
			tmp_acc = last_ | step_.second;
			bdd curr_in = tmp_acc & to_accept;
			bdd best_in = best_acc & to_accept;
487
488
489
490
491
492
493
494
495
496
			if (curr_in == best_in)
			  {
			    if (tmp_lst.size() < best_lst.size())
			      {
				cycle_path tmp(tmp_lst);
				best_lst = tmp;
			      }
			  }
			else
			  {
497
			    if (bddtrue == (best_in >> curr_in))
498
			      {
499
500
501
				cycle_path tmp(tmp_lst);
				best_lst = tmp;
				best_acc = tmp_acc;
502
503
504
505
506
507
508
			      }
			  }
		      }
		    else
		      {
			bdd last_ = iter_->current_accepting_conditions();
			bdd prop_ = iter_->current_condition();
509
		        tmp_acc = last_ | step_.second;
510
511
			tmp_lst.push_back(state_proposition(curr_state,
							    prop_));
512
513
514
515
516
517
518
519
520
521
			cycle_path tmp(tmp_lst);
			best_lst = tmp;
			best_acc = tmp_acc;
			ok = true;
		      }
		  }
	      }
	    iter_->next();
	  }
      }
522
    for (cycle_path::iterator it = best_lst.begin();
523
	 it != best_lst.end(); ++it)
524
      emptiness_check::period.push_back(*it);
525

526
527
    if (best_acc != to_accept)
      {
528
	bdd rec_to_acc = to_accept - best_acc;
529
	emptiness_check::accepting_path(aut_counter, comp_path,
530
					period.back().first, rec_to_acc);
531
532
533
      }
    else
      {
534
	if (!period.empty())
535
	  {
536
	    /// The path contains all accepting conditions. Then we
537
	    ///complete the cycle in this SCC by calling complete_cycle.
538
539
	    complete_cycle(aut_counter, comp_path, period.back().first,
			   suffix.back());
540
541
542
543
	  }
      }
  }
}