gtec.cc 12 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
// Copyright (C) 2003, 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie.
//
// 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 "gtec.hh"
23
#include "ce.hh"
24
25
26
27
28
29
30
31

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

32
33
  couvreur99_check::couvreur99_check(const tgba* a,
				     const numbered_state_heap_factory* nshf)
34
  {
35
    ecs_ = new couvreur99_check_status(a, nshf);
36
37
  }

38
  couvreur99_check::~couvreur99_check()
39
40
41
42
43
  {
    delete ecs_;
  }

  void
44
  couvreur99_check::remove_component(const state* from)
45
46
47
48
49
50
51
52
53
54
  {
    // Remove from H all states which are reachable from state FROM.

    // Stack of iterators towards states to remove.
    std::stack<tgba_succ_iterator*> to_remove;

    // 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.)
55
56
57
58
    numbered_state_heap::state_index_p spi = ecs_->h->index(from);
    assert(spi.first);
    assert(*spi.second != -1);
    *spi.second = -1;
59
60
61
62
63
64
65
66
    tgba_succ_iterator* i = ecs_->aut->succ_iter(from);

    for (;;)
      {
	// Remove each destination of this iterator.
	for (i->first(); !i->done(); i->next())
	  {
	    state* s = i->current_state();
67
	    numbered_state_heap::state_index_p spi = ecs_->h->index(s);
68
69
70
71
72
73
74
75
76

	    // This state is not necessary in H, because if we were
	    // doing inclusion checking during the emptiness-check
	    // (redefining find()), the index `s' can be included in a
	    // larger state and will not be found by index().  We can
	    // safely ignore such states.
	    if (!spi.first)
	      continue;

77
	    if (*spi.second != -1)
78
	      {
79
80
		*spi.second = -1;
		to_remove.push(ecs_->aut->succ_iter(spi.first));
81
82
83
84
85
86
87
88
89
90
	      }
	  }
	delete i;
	if (to_remove.empty())
	  break;
	i = to_remove.top();
	to_remove.pop();
      }
  }

91
92
  emptiness_check_result*
  couvreur99_check::check()
93
94
  {
    // We use five main data in this algorithm:
95
96
    // * couvreur99_check::root, a stack of strongly connected components (SCC),
    // * couvreur99_check::h, a hash of all visited nodes, with their order,
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
    //   (it is called "Hash" in Couvreur's paper)
    // * arc, a stack of acceptance conditions between each of these SCC,
    std::stack<bdd> arc;
    // * 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
    //   form (STATE, ITERATOR) where ITERATOR is a tgba_succ_iterator
    //   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();
113
      ecs_->h->insert(init, 1);
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
      ecs_->root.push(1);
      arc.push(bddfalse);
      tgba_succ_iterator* iter = ecs_->aut->succ_iter(init);
      iter->first();
      todo.push(pair_state_iter(init, iter));
    }

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

	// We are looking at the next successor in SUCC.
	tgba_succ_iterator* succ = todo.top().second;

	// 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();

	    // 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.
140
141
	    numbered_state_heap::state_index_p spi = ecs_->h->index(curr);
	    assert(spi.first);
142
	    assert(!ecs_->root.empty());
143
	    if (ecs_->root.top().index == *spi.second)
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
	      {
		assert(!arc.empty());
		arc.pop();
		ecs_->root.pop();
		remove_component(curr);
	      }

	    delete succ;
	    // Do not delete CURR: it is a key in H.
	    continue;
	  }

	// We have a successor to look at.  Fetch the values
	// (destination state, acceptance conditions of the arc)
	// we are interested in...
	const state* dest = succ->current_state();
	bdd acc = succ->current_acceptance_conditions();
	// ... 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?
167
168
	numbered_state_heap::state_index_p spi = ecs_->h->find(dest);
	if (!spi.first)
169
170
171
	  {
	    // Yes.  Number it, stack it, and register its successors
	    // for later processing.
172
	    ecs_->h->insert(dest, ++num);
173
174
175
176
177
178
179
180
181
	    ecs_->root.push(num);
	    arc.push(acc);
	    tgba_succ_iterator* iter = ecs_->aut->succ_iter(dest);
	    iter->first();
	    todo.push(pair_state_iter(dest, iter));
	    continue;
	  }

	// If we have reached a dead component, ignore it.
182
	if (*spi.second == -1)
183
184
185
186
187
188
189
190
191
192
193
194
195
	  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").
196
	int threshold = *spi.second;
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
	while (threshold < ecs_->root.top().index)
	  {
	    assert(!ecs_->root.empty());
	    assert(!arc.empty());
	    acc |= ecs_->root.top().condition;
	    acc |= arc.top();
	    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;

	if (ecs_->root.top().condition
	    == ecs_->aut->all_acceptance_conditions())
	  {
	    // We have found an accepting SCC.
	    // Release all iterators in TODO.
	    while (!todo.empty())
	      {
		delete todo.top().second;
		todo.pop();
	      }
224
            set_states(ecs_->states());
225
	    return new couvreur99_check_result(ecs_);
226
227
228
	  }
      }
    // This automaton recognizes no word.
229
    return 0;
230
231
  }

232
233
  const couvreur99_check_status*
  couvreur99_check::result() const
234
235
236
237
  {
    return ecs_;
  }

238
239
240
241
242
243
244
  std::ostream&
  couvreur99_check::print_stats(std::ostream& os) const
  {
    ecs_->print_stats(os);
    return os;
  }

245
246
  //////////////////////////////////////////////////////////////////////

247
248
249
250
  couvreur99_check_shy::couvreur99_check_shy(const tgba* a,
					     const numbered_state_heap_factory*
					     nshf)
    : couvreur99_check(a, nshf), num(1)
251
  {
252
253
254
255
    // Setup depth-first search from the initial state.
    todo.push(pair_state_successors(0, succ_queue()));
    todo.top().second.push_front(successor(bddtrue,
					   ecs_->aut->get_init_state()));
256
257
  }

258
  couvreur99_check_shy::~couvreur99_check_shy()
259
260
261
  {
  }

262
263
  emptiness_check_result*
  couvreur99_check_shy::check()
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
  {

    for (;;)
      {
	assert(ecs_->root.size() == arc.size());

	// Get the successors of the current state.
	succ_queue& queue = todo.top().second;

	// First, we process all successors that we have already seen.
	// This is an idea from Soheib Baarir.  It helps to merge SCCs
	// and get shorter traces faster.
	succ_queue::iterator q = queue.begin();
	while (q != queue.end())
	  {
279
	    int* i = find_state(q->s);
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
	    if (!i)
	      {
		// Skip unknown states.
		++q;
		continue;
	      }

	    // Skip states from dead SCCs.
	    if (*i != -1)
	      {
		// 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").
		int threshold = *i;
		bdd acc = q->acc;
		while (threshold < ecs_->root.top().index)
		  {
		    assert(!ecs_->root.empty());
		    assert(!arc.empty());
		    acc |= ecs_->root.top().condition;
		    acc |= arc.top();
		    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;

		if (ecs_->root.top().condition
		    == ecs_->aut->all_acceptance_conditions())
		  {
327
328
		    /// q->s has already been freed by find_state().
		    queue.erase(q);
329
330
331
332
333
334
335
336
337
		    // We have found an accepting SCC.  Clean up TODO.
		    // We must delete all states of apparing in TODO
		    // unless they are used as keys in H.
		    while (!todo.empty())
		      {
			succ_queue& queue = todo.top().second;
			for (succ_queue::iterator q = queue.begin();
			     q != queue.end(); ++q)
			  {
338
339
340
341
342
343
			    // Delete the state if it is a clone of a
			    // state in the heap...
			    numbered_state_heap::state_index_p spi
			      = ecs_->h->index(q->s);
			    // ... or if it is an unknown state.
			    if (spi.first == 0)
344
345
346
347
			      delete q->s;
			  }
			todo.pop();
		      }
348
                    set_states(ecs_->states());
349
		    return new couvreur99_check_result(ecs_);
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
		  }
	      }
	    // Remove that state from the queue, so we do not
	    // recurse into it.
	    succ_queue::iterator old = q++;
	    queue.erase(old);
	  }

	// If there is no more successor, backtrack.
	if (queue.empty())
	  {
	    // We have explored all successors of state CURR.
	    const state* curr = todo.top().first;
	    // Backtrack TODO.
	    todo.pop();
	    if (todo.empty())
	      // This automaton recognizes no word.
367
	      return 0;
368
369
370
371

	    // 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.
372
373
	    numbered_state_heap::state_index_p spi = ecs_->h->index(curr);
	    assert(spi.first);
374
	    assert(!ecs_->root.empty());
375
	    if (ecs_->root.top().index == *spi.second)
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
	      {
		assert(!arc.empty());
		arc.pop();
		ecs_->root.pop();
		remove_component(curr);
	      }
	    continue;
	  }

	// Recurse.  (Finally!)

	// Pick one successor off the list, and schedule its
	// successors first on TODO.  Update the various hashes and
	// stacks.
	successor succ = queue.front();
	queue.pop_front();
392
	ecs_->h->insert(succ.s, ++num);
393
394
395
396
397
	ecs_->root.push(num);
	arc.push(succ.acc);
	todo.push(pair_state_successors(succ.s, succ_queue()));
	succ_queue& new_queue = todo.top().second;
	tgba_succ_iterator* iter = ecs_->aut->succ_iter(succ.s);
398
	for (iter->first(); !iter->done(); iter->next())
399
400
401
402
403
	  new_queue.push_back(successor(iter->current_acceptance_conditions(),
					iter->current_state()));
	delete iter;
      }
  }
404
405

  int*
406
  couvreur99_check_shy::find_state(const state* s)
407
  {
408
    return ecs_->h->find(s).second;
409
410
  }

411
}