ce.cc 12.1 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
23
24
25
26
27
28
29
30
// Copyright (C) 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 "ce.hh"
#include "tgba/bddprint.hh"
#include <map>

namespace spot
{
  namespace
  {
    typedef std::pair<const spot::state*, tgba_succ_iterator*> pair_state_iter;
31
    typedef std::pair<const state*, bdd> state_proposition;
32
33
  }

34
35
36
37
  couvreur99_check_result::couvreur99_check_result
  (const couvreur99_check_status* ecs,
   const explicit_connected_component_factory* eccf)
    : ecs_(ecs), eccf_(eccf)
38
  {
39
40
41
42
43
44
45
  }

  tgba_run*
  couvreur99_check_result::accepting_run()
  {
    run_ = new tgba_run;

46
47
48
49
50
51
    assert(!ecs_->root.empty());

    scc_stack::stack_type root = ecs_->root.s;
    int comp_size = root.size();
    // Transform the stack of connected component into an array.
    explicit_connected_component** scc =
52
      new explicit_connected_component*[comp_size];
53
54
    for (int j = comp_size - 1; 0 <= j; --j)
      {
55
	scc[j] = eccf_->build();
56
57
58
59
60
61
62
	scc[j]->index = root.top().index;
	scc[j]->condition = root.top().condition;
	root.pop();
      }
    assert(root.empty());

    // Build the set of states for all SCCs.
63
    numbered_state_heap_const_iterator* i = ecs_->h->iterator();
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
    for (i->first(); !i->done(); i->next())
      {
	int index = i->get_index();
	// Skip states from dead SCCs.
	if (index < 0)
	  continue;
	assert(index != 0);

	// Find the SCC this state belongs to.
	int j;
	for (j = 1; j < comp_size; ++j)
	  if (index < scc[j]->index)
	    break;
	scc[j - 1]->insert(i->get_state());
      }
    delete i;

81
82
83
    numbered_state_heap::state_index_p spi =
      ecs_->h->index(ecs_->aut->get_init_state());
    assert(spi.first);
84
85
86
    /// FIXME: Should compute label and acceptance condition.
    tgba_run::step s = { spi.first, bddtrue, bddfalse };
    run_->prefix.push_front(s);
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104

    // We build a path trough each SCC in the stack.  For the
    // first SCC, the starting state is the initial state of the
    // automaton.  The destination state is the closest state
    // from the next SCC.  This destination state becomes the
    // starting state when building a path though the next SCC.
    for (int k = 0; k < comp_size - 1; ++k)
      {
	// FIFO for the breadth-first search.
	// (we are looking for the closest state in the next SCC.)
	std::deque<pair_state_iter> todo;

	// Record the father of each state, while performing the BFS.
	typedef std::map<const state*, const state*,
	                 state_ptr_less_than> father_map;
	father_map father;

	// Initial state of the BFS.
105
	const state* start = run_->prefix.back().s;
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
	{
	  tgba_succ_iterator* i = ecs_->aut->succ_iter(start);
	  todo.push_back(pair_state_iter(start, i));
	}

	while (!todo.empty())
	  {
	    const state* src = todo.front().first;
	    tgba_succ_iterator* i = todo.front().second;
	    todo.pop_front();

	    for (i->first(); !i->done(); i->next())
	      {
		const state* dest = i->current_state();

		// Are we leaving this SCC?
		const state* h_dest = scc[k]->has_state(dest);
		if (!h_dest)
		  {
125
		    // If we have found a state in the next SCC.
126
		    // Unwind the path and populate RUN_->PREFIX.
127
128
129
		    h_dest = scc[k+1]->has_state(dest);
		    if (h_dest)
		      {
130
			tgba_run::steps seq;
131

132
133
134
135
			/// FIXME: Should compute label and acceptance
			/// condition.
			tgba_run::step s = { h_dest, bddtrue, bddfalse };
			seq.push_front(s);
136
137
			while (src->compare(start))
			  {
138
139
140
141
			    /// FIXME: Should compute label and acceptance
			    /// condition.
			    tgba_run::step s = { h_dest, bddtrue, bddfalse };
			    seq.push_front(s);
142
143
			    src = father[src];
			  }
144
145
			// Append SEQ to RUN_->PREFIX.
			run_->prefix.splice(run_->prefix.end(), seq);
146
147
148
149
150
151
152
153
154
			// Exit this BFS for this SCC.
			while (!todo.empty())
			  {
			    delete todo.front().second;
			    todo.pop_front();
			  }
			break;
		      }
		    // Restrict the BFS to state inside the SCC.
155
		    delete dest;
156
157
158
159
160
161
162
163
164
165
166
167
168
169
		    continue;
		  }

		if (father.find(h_dest) == father.end())
		  {
		    todo.push_back
		      (pair_state_iter(h_dest, ecs_->aut->succ_iter(h_dest)));
		    father[h_dest] = src;
		  }
	      }
	    delete i;
	  }
      }

170
    accepting_path(scc[comp_size - 1], run_->prefix.back().s,
171
		   scc[comp_size - 1]->condition);
172
    run_->prefix.pop_back(); // this state belongs to the cycle.
173
174
175
176

    for (int j = comp_size - 1; 0 <= j; --j)
      delete scc[j];
    delete[] scc;
177
178
179
180
181
182
183
184
185
186
187
188

    // Clone every state in the run before returning it.  (We didn't
    // do that before in the algorithm, because it's easier to follow
    // if every state manipulated is the instance in the hash table.)
    for (tgba_run::steps::iterator i = run_->prefix.begin();
	 i != run_->prefix.end(); ++i)
      i->s = i->s->clone();
    for (tgba_run::steps::iterator i = run_->cycle.begin();
	 i != run_->cycle.end(); ++i)
      i->s = i->s->clone();

    return run_;
189
190
191
  }

  void
192
193
194
195
  couvreur99_check_result::complete_cycle(const explicit_connected_component*
					  scc,
					  const state* from,
					  const state* to)
196
  {
197
    // If by chance our cycle already ends on the state we have
198
199
    // to reach back, we are done.
    if (from == to
200
	&& !run_->cycle.empty())
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
      return;

    // Records backlinks to parent state during the BFS.
    // (This also stores the propositions of this link.)
    std::map<const state*, state_proposition, state_ptr_less_than> father;

    // BFS queue.
    std::deque<pair_state_iter> todo;

    // Initial state.
    {
      tgba_succ_iterator* i = ecs_->aut->succ_iter(from);
      todo.push_back(pair_state_iter(from, i));
    }

    while (!todo.empty())
      {
	const state* src = todo.front().first;
	tgba_succ_iterator* i = todo.front().second;
	todo.pop_front();
	for (i->first(); !i->done(); i->next())
	  {
	    const state* dest = i->current_state();

	    // Do not escape this SCC or visit a state already visited.
	    const state* h_dest = scc->has_state(dest);
	    if (!h_dest)
	      {
		delete dest;
		continue;
	      }
	    if (father.find(h_dest) != father.end())
	      continue;

	    bdd cond = i->current_condition();

	    // If we have reached our destination, unwind the path
238
	    // and populate RUN_->CYCLE.
239
240
	    if (h_dest == to)
	      {
241
242
243
244
		tgba_run::steps p;
		// FIXME: should compute acceptance condition.
		tgba_run::step s = { h_dest, cond, bddfalse };
		p.push_front(s);
245
246
247
		while (src != from)
		  {
		    const state_proposition& psi = father[src];
248
249
250
		    // FIXME: should compute acceptance condition.
		    tgba_run::step s = { src, psi.second, bddfalse };
		    p.push_front(s);
251
252
		    src = psi.first;
		  }
253
		run_->cycle.splice(run_->cycle.end(), p);
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290

		// Exit the BFS, but release all iterators first.
		while (!todo.empty())
		  {
		    delete todo.front().second;
		    todo.pop_front();
		  }
		break;
	      }

	    // Common case: record backlinks and continue BFS.
	    todo.push_back(pair_state_iter(h_dest,
					   ecs_->aut->succ_iter(h_dest)));
	    father[h_dest] = state_proposition(src, cond);
	  }
	delete i;
      }
  }


  namespace
  {
    struct triplet
    {
      const state* s;		// Current state.
      tgba_succ_iterator* iter;	// Iterator to successor of the current state.
      bdd acc;			// All acceptance conditions traversed by
				// the path so far.

      triplet (const state* s, tgba_succ_iterator* iter, bdd acc)
	: s(s), iter(iter), acc(acc)
      {
      }
    };

  }

martinez's avatar
martinez committed
291
  void
292
293
294
295
  couvreur99_check_result::accepting_path(const explicit_connected_component*
					  scc,
					  const state* start, bdd
					  acc_to_traverse)
martinez's avatar
martinez committed
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
  {
    // State seen during the DFS.
    typedef Sgi::hash_set<const state*,
                          state_ptr_hash, state_ptr_equal> set_type;
    set_type seen;
    // DFS stack.
    std::stack<triplet> todo;

    while (acc_to_traverse != bddfalse)
      {
	// Initial state.
	{
	  tgba_succ_iterator* i = ecs_->aut->succ_iter(start);
	  i->first();
	  todo.push(triplet(start, i, bddfalse));
	  seen.insert(start);
	}

	// The path being explored currently.
315
	tgba_run::steps path;
martinez's avatar
martinez committed
316
	// The best path seen so far.
317
	tgba_run::steps best_path;
martinez's avatar
martinez committed
318
319
320
321
322
323
324
325
326
327
328
329
330
331
	// The acceptance conditions traversed by BEST_PATH.
	bdd best_acc = bddfalse;

	while (!todo.empty())
	  {
	    tgba_succ_iterator* iter = todo.top().iter;
	    const state* s = todo.top().s;

	    // Nothing more to explore, backtrack.
	    if (iter->done())
	      {
		todo.pop();
		delete iter;
		seen.erase(s);
332
		if (!todo.empty())
martinez's avatar
martinez committed
333
		  {
334
		    assert(!path.empty());
martinez's avatar
martinez committed
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
		    path.pop_back();
		  }
		continue;
	      }

	    // We must not escape the current SCC.
	    const state* dest = iter->current_state();
	    const state* h_dest = scc->has_state(dest);
	    if (!h_dest)
	      {
		delete dest;
		iter->next();
		continue;
	      }

	    bdd acc = iter->current_acceptance_conditions() | todo.top().acc;
351
352
353
	    tgba_run::step st = { h_dest, iter->current_condition(),
				 iter->current_acceptance_conditions() };
	    path.push_back(st);
martinez's avatar
martinez committed
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371

	    // Advance iterator for next step.
	    iter->next();

	    if (seen.find(h_dest) == seen.end())
	      {
		// A new state: continue the DFS.
		tgba_succ_iterator* di = ecs_->aut->succ_iter(h_dest);
		di->first();
		todo.push(triplet(h_dest, di, acc));
		seen.insert(h_dest);
		continue;
	      }

	    // We have completed a full cycle.

	    // If we already have a best path, let see if the current
	    // one is better.
372
	    if (!best_path.empty())
martinez's avatar
martinez committed
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
408
409
410
411
412
413
414
	      {
		// When comparing the merits of two paths, only the
		// acceptance conditions we are trying the traverse
		// are important.
		bdd acc_restrict = acc & acc_to_traverse;
		bdd best_acc_restrict = best_acc & acc_to_traverse;

		// If the best path and the current one traverse the
		// same acceptance conditions, we keep the shorter
		// path.  Otherwise, we keep the path which has the
		// more acceptance conditions.
		if (best_acc_restrict == acc_restrict)
		  {
		    if (best_path.size() <= path.size())
		      goto backtrack_path;
		  }
		else
		  {
		    // `best_acc_restrict >> acc_restrict' is true
		    // when the set of acceptance conditions of
		    // best_acc_restrict is included in the set of
		    // acceptance conditions of acc_restrict.
		    //
		    // FIXME: It would be better to count the number
		    // of acceptance conditions.
		    if (bddtrue != (best_acc_restrict >> acc_restrict))
		      goto backtrack_path;
		  }
	      }

	    // The current path the best one.
	    best_path = path;
	    best_acc = acc;

	  backtrack_path:
	    // Continue exploration from parent to find better paths.
	    // (Do not pop PATH if ITER is done, because that will be
	    // done at the top of the loop, among other things.)
	    if (!iter->done())
	      path.pop_back();
	  }

415
416
	// Append our best path to the run_->cycle.
	for (tgba_run::steps::iterator it = best_path.begin();
martinez's avatar
martinez committed
417
	     it != best_path.end(); ++it)
418
	  run_->cycle.push_back(*it);
martinez's avatar
martinez committed
419
420
421
422

	// Prepare to find another path for the remaining acceptance
	// conditions.
	acc_to_traverse -= best_acc;
423
	start = run_->cycle.back().s;
martinez's avatar
martinez committed
424
425
426
427
      }

    // Complete the path so that it goes back to its beginning,
    // forming a cycle.
428
    complete_cycle(scc, start, run_->prefix.back().s);
429
430
431
  }

  void
432
  couvreur99_check_result::print_stats(std::ostream& os) const
433
434
  {
    ecs_->print_stats(os);
435
436
437
438
    // FIXME: This is bogusly assuming run_ exists.  (Even if we
    // created it, the user might have delete it.)
    os << run_->prefix.size() << " states in run_->prefix" << std::endl;
    os << run_->cycle.size() << " states in run_->cycle" << std::endl;
439
440
441
  }

}