gtec.cc 16.6 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
// Copyright (C) 2008, 2011, 2014, 2015 Laboratoire de Recherche et
3
// Développement de l'Epita (LRDE).
Guillaume Sadegh's avatar
Guillaume Sadegh committed
4
// Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de
5
6
// Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
// Université Pierre et Marie Curie.
7
8
9
10
11
//
// 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
12
// the Free Software Foundation; either version 3 of the License, or
13
14
15
16
17
18
19
20
// (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
21
// along with this program.  If not, see <http://www.gnu.org/licenses/>.
22

23
24
25
26
27
28
29
30
31
// #define TRACE

#include <iostream>
#ifdef TRACE
#define trace std::cerr
#else
#define trace while (0) std::cerr
#endif

32
#include "gtec.hh"
33
#include "ce.hh"
34
#include "misc/memusage.hh"
35
36
37
38
39

namespace spot
{
  namespace
  {
40
    typedef std::pair<const spot::state*, twa_succ_iterator*> pair_state_iter;
41
42
  }

43
  couvreur99_check::couvreur99_check(const const_twa_ptr& a, option_map o)
44
45
    : emptiness_check(a, o),
      removed_components(0)
46
  {
47
    poprem_ = o.get("poprem", 1);
48
    ecs_ = std::make_shared<couvreur99_check_status>(a);
49
50
51
    stats["removed components"] =
	static_cast<spot::unsigned_statistics::unsigned_fun>
	(&couvreur99_check::get_removed_components);
52
53
54
    stats["vmsize"] =
	static_cast<spot::unsigned_statistics::unsigned_fun>
	(&couvreur99_check::get_vmsize);
55
56
  }

57
  couvreur99_check::~couvreur99_check()
58
59
60
  {
  }

61
62
63
64
65
66
  unsigned
  couvreur99_check::get_removed_components() const
  {
    return removed_components;
  }

67
68
69
70
71
72
73
74
75
  unsigned
  couvreur99_check::get_vmsize() const
  {
    int size = memusage();
    if (size > 0)
      return size;
    return 0;
  }

76
  void
77
  couvreur99_check::remove_component(const state* from)
78
  {
79
    ++removed_components;
80
81
82
83
84
    // If rem has been updated, removing states is very easy.
    if (poprem_)
      {
	assert(!ecs_->root.rem().empty());
	dec_depth(ecs_->root.rem().size());
85
86
	for (auto i: ecs_->root.rem())
	  ecs_->h[i] = -1;
87
88
89
90
	// ecs_->root.rem().clear();
	return;
      }

91
92
93
    // Remove from H all states which are reachable from state FROM.

    // Stack of iterators towards states to remove.
94
    std::stack<twa_succ_iterator*> to_remove;
95
96
97
98
99

    // Remove FROM itself, and prepare to remove its successors.
    // (FROM should be in H, otherwise it means all reachable
    // states from FROM have already been removed and there is no
    // point in calling remove_component.)
100
    ecs_->h[from] = -1;
101
    twa_succ_iterator* i = ecs_->aut->succ_iter(from);
102
103
104
105

    for (;;)
      {
	// Remove each destination of this iterator.
106
107
108
109
110
111
	if (i->first())
	  do
	    {
	      inc_transitions();

	      state* s = i->current_state();
112
113
114
	      auto j = ecs_->h.find(s);
	      assert(j != ecs_->h.end());
	      s->destroy();
115

116
	      if (j->second != -1)
117
		{
118
119
		  j->second = -1;
		  to_remove.push(ecs_->aut->succ_iter(j->first));
120
121
122
		}
	    }
	  while (i->next());
123
	ecs_->aut->release_iter(i);
124
125
126
127
128
129
130
	if (to_remove.empty())
	  break;
	i = to_remove.top();
	to_remove.pop();
      }
  }

131
  emptiness_check_result_ptr
132
  couvreur99_check::check()
133
  {
134
135
136
137
138
139
140
141
142
    {
      auto acc = ecs_->aut->acc();
      if (acc.get_acceptance().is_false())
	return nullptr;
      if (acc.uses_fin_acceptance())
	throw std::runtime_error
	  ("Fin acceptance is not supported by couvreur99()");
    }

143
    // We use five main data in this algorithm:
144
145
    // * couvreur99_check::root, a stack of strongly connected components (SCC),
    // * couvreur99_check::h, a hash of all visited nodes, with their order,
146
147
    //   (it is called "Hash" in Couvreur's paper)
    // * arc, a stack of acceptance conditions between each of these SCC,
148
    std::stack<acc_cond::mark_t> arc;
149
150
151
152
    // * num, the number of visited nodes.  Used to set the order of each
    //   visited node,
    int num = 1;
    // * todo, the depth-first search stack.  This holds pairs of the
153
    //   form (STATE, ITERATOR) where ITERATOR is a twa_succ_iterator
154
155
156
157
158
159
160
161
    //   over the successors of STATE.  In our use, ITERATOR should
    //   always be freed when TODO is popped, but STATE should not because
    //   it is also used as a key in H.
    std::stack<pair_state_iter> todo;

    // Setup depth-first search from the initial state.
    {
      state* init = ecs_->aut->get_init_state();
162
      ecs_->h[init] = 1;
163
      ecs_->root.push(1);
164
      arc.push(0U);
165
      twa_succ_iterator* iter = ecs_->aut->succ_iter(init);
166
      iter->first();
167
      todo.emplace(init, iter);
168
      inc_depth();
169
170
171
172
173
174
175
    }

    while (!todo.empty())
      {
	assert(ecs_->root.size() == arc.size());

	// We are looking at the next successor in SUCC.
176
	twa_succ_iterator* succ = todo.top().second;
177
178
179
180
181
182
183
184
185

	// If there is no more successor, backtrack.
	if (succ->done())
	  {
	    // We have explored all successors of state CURR.
	    const state* curr = todo.top().first;

	    // Backtrack TODO.
	    todo.pop();
186
	    dec_depth();
187

188
189
190
	    // If poprem is used, fill rem with any component removed,
	    // so that remove_component() does not have to traverse
	    // the SCC again.
191
192
	    auto i = ecs_->h.find(curr);
	    assert(i != ecs_->h.end());
193
194
	    if (poprem_)
	      {
195
		ecs_->root.rem().push_front(i->first);
196
197
		inc_depth();
	      }
198
199
200
201
	    // When backtracking the root of an SCC, we must also
	    // remove that SCC from the ARC/ROOT stacks.  We must
	    // discard from H all reachable states from this SCC.
	    assert(!ecs_->root.empty());
202
	    if (ecs_->root.top().index == i->second)
203
204
205
206
	      {
		assert(!arc.empty());
		arc.pop();
		remove_component(curr);
207
		ecs_->root.pop();
208
	      }
209
	    ecs_->aut->release_iter(succ);
210
	    // Do not destroy CURR: it is a key in H.
211
212
213
	    continue;
	  }

214
215
216
217
	// We have a successor to look at.
	inc_transitions();
	// Fetch the values (destination state, acceptance conditions
	// of the arc) we are interested in...
218
	const state* dest = succ->current_state();
219
	acc_cond::mark_t acc = succ->current_acceptance_conditions();
220
221
222
223
224
225
	// ... and point the iterator to the next successor, for
	// the next iteration.
	succ->next();
	// We do not need SUCC from now on.

	// Are we going to a new state?
226
	auto p = ecs_->h.emplace(dest, num + 1);
227
	if (p.second)
228
	  {
229
230
231
	    // Yes.  Bump number, stack the stack, and register its
	    // successors for later processing.
	    ecs_->root.push(++num);
232
	    arc.push(acc);
233
	    twa_succ_iterator* iter = ecs_->aut->succ_iter(dest);
234
	    iter->first();
235
	    todo.emplace(dest, iter);
236
	    inc_depth();
237
238
	    continue;
	  }
239
	dest->destroy();
240
241

	// If we have reached a dead component, ignore it.
242
	if (p.first->second == -1)
243
244
245
246
247
248
249
250
251
252
253
254
255
	  continue;

	// Now this is the most interesting case.  We have reached a
	// state S1 which is already part of a non-dead SCC.  Any such
	// non-dead SCC has necessarily been crossed by our path to
	// this state: there is a state S2 in our path which belongs
	// to this SCC too.  We are going to merge all states between
	// this S1 and S2 into this SCC.
	//
	// This merge is easy to do because the order of the SCC in
	// ROOT is ascending: we just have to merge all SCCs from the
	// top of ROOT that have an index greater to the one of
	// the SCC of S2 (called the "threshold").
256
	int threshold = p.first->second;
257
	std::list<const state*> rem;
258
259
260
261
262
263
	while (threshold < ecs_->root.top().index)
	  {
	    assert(!ecs_->root.empty());
	    assert(!arc.empty());
	    acc |= ecs_->root.top().condition;
	    acc |= arc.top();
264
	    rem.splice(rem.end(), ecs_->root.rem());
265
266
267
268
269
270
271
272
273
274
	    ecs_->root.pop();
	    arc.pop();
	  }
	// Note that we do not always have
	//  threshold == ecs_->root.top().index
	// after this loop, the SCC whose index is threshold might have
	// been merged with a lower SCC.

	// Accumulate all acceptance conditions into the merged SCC.
	ecs_->root.top().condition |= acc;
275
	ecs_->root.rem().splice(ecs_->root.rem().end(), rem);
276

277
	if (ecs_->aut->acc().accepting(ecs_->root.top().condition))
278
279
280
281
282
	  {
	    // We have found an accepting SCC.
	    // Release all iterators in TODO.
	    while (!todo.empty())
	      {
283
		ecs_->aut->release_iter(todo.top().second);
284
		todo.pop();
285
		dec_depth();
286
	      }
287
288
	    // Use this state to start the computation of an accepting
	    // cycle.
289
	    ecs_->cycle_seed = p.first->first;
290
            set_states(ecs_->states());
291
	    return std::make_shared<couvreur99_check_result>(ecs_, options());
292
293
294
	  }
      }
    // This automaton recognizes no word.
295
    set_states(ecs_->states());
296
    return nullptr;
297
298
  }

299
  std::shared_ptr<const couvreur99_check_status>
300
  couvreur99_check::result() const
301
302
303
304
  {
    return ecs_;
  }

305
306
307
308
  std::ostream&
  couvreur99_check::print_stats(std::ostream& os) const
  {
    ecs_->print_stats(os);
309
310
    os << transitions() << " transitions explored" << std::endl;
    os << max_depth() << " items max in DFS search stack" << std::endl;
311
312
313
    return os;
  }

314
315
  //////////////////////////////////////////////////////////////////////

316
317
318
319
  couvreur99_check_shy::todo_item::todo_item(const state* s, int n,
					     couvreur99_check_shy* shy)
	: s(s), n(n)
  {
320
    for (auto iter: shy->ecs_->aut->succ(s))
321
      {
322
323
	q.emplace_back(iter->current_acceptance_conditions(),
		       iter->current_state());
324
	shy->inc_depth();
325
	shy->inc_transitions();
326
327
328
      }
  }

329
  couvreur99_check_shy::couvreur99_check_shy(const const_twa_ptr& a,
330
					     option_map o)
331
    : couvreur99_check(a, o), num(1)
332
  {
333
    group_ = o.get("group", 1);
334
335
    group2_ = o.get("group2", 0);
    group_ |= group2_;
336

337
    // Setup depth-first search from the initial state.
338
    const state* i = ecs_->aut->get_init_state();
339
    ecs_->h[i] = ++num;
340
    ecs_->root.push(num);
341
    todo.emplace_back(i, num, this);
342
    inc_depth(1);
343
344
  }

345
  couvreur99_check_shy::~couvreur99_check_shy()
346
347
348
  {
  }

349
350
351
  void
  couvreur99_check_shy::clear_todo()
  {
352
    // We must destroy all states appearing in TODO
353
354
355
356
    // unless they are used as keys in H.
    while (!todo.empty())
      {
	succ_queue& queue = todo.back().q;
357
	for (auto& q: queue)
358
	  {
359
360
361
362
363
	    // Destroy the state if it is a clone of a state in the
	    // heap or if it is an unknown state.
	    auto i = ecs_->h.find(q.s);
	    if (i == ecs_->h.end() || i->first != q.s)
	      q.s->destroy();
364
	  }
365
	dec_depth(todo.back().q.size() + 1);
366
367
	todo.pop_back();
      }
368
369
    dec_depth(ecs_->root.clear_rem());
    assert(depth() == 0);
370
371
  }

372
373
374
  void
  couvreur99_check_shy::dump_queue(std::ostream& os)
  {
375
    os << "--- TODO ---\n";
376
    unsigned pos = 0;
377
    for (auto& ti: todo)
378
379
      {
	++pos;
380
	os << '#' << pos << " s:" << ti.s << " n:" << ti.n
381
	   << " q:{";
382
	for (auto qi = ti.q.begin(); qi != ti.q.end();)
383
384
385
	  {
	    os << qi->s;
	    ++qi;
386
	    if (qi != ti.q.end())
387
388
	      os << ", ";
	  }
389
	os << "}\n";
390
391
392
      }
  }

393
  emptiness_check_result_ptr
394
  couvreur99_check_shy::check()
395
  {
396
397
398
399
400
401
402
403
    {
      auto acc = ecs_->aut->acc();
      if (acc.get_acceptance().is_false())
	return nullptr;
      if (acc.uses_fin_acceptance())
	throw std::runtime_error
	  ("Fin acceptance is not supported by couvreur99()");
    }
404
    // Position in the loop seeking known successors.
405
    pos = todo.back().q.begin();
406

407
408
    for (;;)
      {
409
410
411
412
#ifdef TRACE
	dump_queue();
#endif

413
	assert(ecs_->root.size() == 1 + arc.size());
414
415

	// Get the successors of the current state.
416
	succ_queue& queue = todo.back().q;
417

418
419
420
	// If there is no more successor, backtrack.
	if (queue.empty())
	  {
421
	    trace << "backtrack" << std::endl;
422

423
	    // We have explored all successors of state CURR.
424
425
	    const state* curr = todo.back().s;
	    int index = todo.back().n;
426

427
	    // Backtrack TODO.
428
	    todo.pop_back();
429
430
	    dec_depth();

431
	    if (todo.empty())
432
433
434
	      {
		// This automaton recognizes no word.
		set_states(ecs_->states());
435
		assert(poprem_ || depth() == 0);
436
		return nullptr;
437
	      }
438

439
440
	    pos = todo.back().q.begin();

441
442
443
444
445
	    // If poprem is used, fill rem with any component removed,
	    // so that remove_component() does not have to traverse
	    // the SCC again.
	    if (poprem_)
	      {
446
447
448
449
		auto i = ecs_->h.find(curr);
		assert(i != ecs_->h.end());
		assert(i->first == curr);
		ecs_->root.rem().push_front(i->first);
450
451
452
		inc_depth();
	      }

453
454
455
456
	    // When backtracking the root of an SCC, we must also
	    // remove that SCC from the ARC/ROOT stacks.  We must
	    // discard from H all reachable states from this SCC.
	    assert(!ecs_->root.empty());
457
	    if (ecs_->root.top().index == index)
458
459
460
461
	      {
		assert(!arc.empty());
		arc.pop();
		remove_component(curr);
462
		ecs_->root.pop();
463
464
465
466
	      }
	    continue;
	  }

467
468
469
470
471
472
473
474
475
476
477
478
	// We always make a first pass over the successors of a state
	// to check whether it contains some state we have already seen.
	// This way we hope to merge the most SCCs before stacking new
	// states.
	//
	// So are we checking for known states ?  If yes, POS tells us
	// which state we are considering.  Otherwise just pick the
	// first one.
	succ_queue::iterator old;
	if (pos == queue.end())
	  old = queue.begin();
	else
479
480
481
	  old = pos;
	if (pos != queue.end())
	  ++pos;
482
	//int* i = sip.second;
483

484
485
486
	successor succ = *old;
	trace << "picked state " << succ.s << '\n';
	auto i = ecs_->h.find(succ.s);
487

488
	if (i == ecs_->h.end())
489
490
491
492
493
	  {
	    // It's a new state.
	    // If we are seeking known states, just skip it.
	    if (pos != queue.end())
	      continue;
494

495
	    trace << "new state\n";
496

497
498
499
	    // Otherwise, number it and stack it so we recurse.
	    queue.erase(old);
	    dec_depth();
500
	    ecs_->h[succ.s] = ++num;
501
502
	    ecs_->root.push(num);
	    arc.push(succ.acc);
503
	    todo.emplace_back(succ.s, num, this);
504
505
506
507
508
	    pos = todo.back().q.begin();
	    inc_depth();
	    continue;
	  }

509
510
511
	// It's an known state.  Use i->first from now on.
	succ.s->destroy();

512
	queue.erase(old);
513
	dec_depth();
514
515

	// Skip dead states.
516
	if (i->second == -1)
517
	  {
518
	    trace << "dead state\n";
519
520
521
	    continue;
	  }

522
	trace << "merging...\n";
523

524
525
526
527
528
529
530
531
532
533
534
535
536
537
	// Now this is the most interesting case.  We have
	// reached a state S1 which is already part of a
	// non-dead SCC.  Any such non-dead SCC has
	// necessarily been crossed by our path to this
	// state: there is a state S2 in our path which
	// belongs to this SCC too.  We are going to merge
	// all states between this S1 and S2 into this
	// SCC.
	//
	// This merge is easy to do because the order of
	// the SCC in ROOT is ascending: we just have to
	// merge all SCCs from the top of ROOT that have
	// an index greater to the one of the SCC of S2
	// (called the "threshold").
538
	int threshold = i->second;
539
	std::list<const state*> rem;
540
	acc_cond::mark_t acc = succ.acc;
541
	while (threshold < ecs_->root.top().index)
542
	  {
543
544
545
546
547
548
549
550
551
552
553
554
	    assert(!ecs_->root.empty());
	    assert(!arc.empty());
	    acc |= ecs_->root.top().condition;
	    acc |= arc.top();
	    rem.splice(rem.end(), ecs_->root.rem());
	    ecs_->root.pop();
	    arc.pop();
	  }
	// Note that we do not always have
	//   threshold == ecs_->root.top().index
	// after this loop, the SCC whose index is threshold
	// might have been merged with a lower SCC.
555

556
557
558
559
	// Accumulate all acceptance conditions into the
	// merged SCC.
	ecs_->root.top().condition |= acc;
	ecs_->root.rem().splice(ecs_->root.rem().end(), rem);
560

561
	// Have we found all acceptance conditions?
562
	if (ecs_->aut->acc().accepting(ecs_->root.top().condition))
563
564
565
	  {
	    // Use this state to start the computation of an accepting
	    // cycle.
566
	    ecs_->cycle_seed = i->first;
567

568
569
570
	    // We have found an accepting SCC.  Clean up TODO.
	    clear_todo();
	    set_states(ecs_->states());
571
	    return std::make_shared<couvreur99_check_result>(ecs_, options());
572
	  }
573
574
	// Group the pending successors of formed SCC if requested.
	if (group_)
575
	  {
576
577
	    assert(todo.back().s);
	    while (ecs_->root.top().index < todo.back().n)
578
	      {
579
580
581
582
		todo_list::reverse_iterator prev = todo.rbegin();
		todo_list::reverse_iterator last = prev++;
		// If group2 is used we insert the last->q in front
		// of prev->q so that the states in prev->q are checked
583
		// for existence again after we have processed the states
584
585
586
587
588
589
		// of last->q.  Otherwise we just append to the end.
		prev->q.splice(group2_ ? prev->q.begin() : prev->q.end(),
			       last->q);

		if (poprem_)
		  {
590
591
592
593
594
		    const state* s = todo.back().s;
		    auto i = ecs_->h.find(s);
		    assert(i != ecs_->h.end());
		    assert(i->first == s);
		    ecs_->root.rem().push_front(i->first);
595
596
597
598
		    // Don't change the stack depth, since
		    // we are just moving the state from TODO to REM.
		  }
		else
599
		  {
600
		    dec_depth();
601
		  }
602
		todo.pop_back();
603
	      }
604
	    pos = todo.back().q.begin();
605
	  }
606
607
      }
  }
608

609
  emptiness_check_ptr
610
  couvreur99(const const_twa_ptr& a, option_map o)
611
612
  {
    if (o.get("shy"))
613
614
      return std::make_shared<couvreur99_check_shy>(a, o);
    return std::make_shared<couvreur99_check>(a, o);
615
616
  }

617
}