scc.cc 11 KB
Newer Older
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1
// Copyright (C) 2008, 2009  Laboratoire de Recherche et Developpement de
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
// l'Epita.
//
// 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 <queue>
#include <set>
#include <iostream>
24
#include <sstream>
25
26
27
28
29
30
31
32
33
#include "scc.hh"
#include "tgba/bddprint.hh"

namespace spot
{
  std::ostream&
  scc_stats::dump(std::ostream& out) const
  {
    out << "total SCCs: " << scc_total << std::endl;
34
35
36
37
    out << "accepting SCCs: " << acc_scc << std::endl;
    out << "dead SCCs: " << dead_scc << std::endl;
    out << "accepting paths: " << acc_paths << std::endl;
    out << "dead paths: " << dead_paths << std::endl;
38
39
40
41
42
43
44
45
46
    return out;
  }


  scc_map::scc_map(const tgba* aut)
    : aut_(aut)
  {
  }

47
  unsigned
48
49
50
  scc_map::initial() const
  {
    state* in = aut_->get_init_state();
51
    int val = scc_of_state(in);
52
53
54
55
56
    delete in;
    return val;
  }

  const scc_map::succ_type&
57
  scc_map::succ(unsigned n) const
58
  {
59
60
    assert(scc_map_.size() > n);
    return scc_map_[n].succ;
61
62
63
  }

  bool
64
  scc_map::accepting(unsigned n) const
65
  {
66
    return acc_set_of(n) == aut_->all_acceptance_conditions();
67
68
69
70
71
72
73
74
75
  }

  const tgba*
  scc_map::get_aut() const
  {
    return aut_;
  }


76
77
  int
  scc_map::relabel_component()
78
79
80
  {
    assert(!root_.front().states.empty());
    std::list<const state*>::iterator i;
81
    int n = scc_map_.size();
82
83
84
85
86
    for (i = root_.front().states.begin(); i != root_.front().states.end(); ++i)
      {
	hash_type::iterator spi = h_.find(*i);
	assert(spi != h_.end());
	assert(spi->first == *i);
87
	assert(spi->second < 0);
88
89
	spi->second = n;
      }
90
91
    scc_map_.push_back(root_.front());
    return n;
92
93
94
95
96
97
98
99
  }

  void
  scc_map::build_map()
  {
    // Setup depth-first search from the initial state.
    {
      state* init = aut_->get_init_state();
100
101
102
      num_ = -1;
      h_.insert(std::make_pair(init, num_));
      root_.push_front(scc(num_));
103
104
      arc_acc_.push(bddfalse);
      arc_cond_.push(bddfalse);
105
106
107
108
109
110
111
      tgba_succ_iterator* iter = aut_->succ_iter(init);
      iter->first();
      todo_.push(pair_state_iter(init, iter));
    }

    while (!todo_.empty())
      {
112
113
	assert(root_.size() == arc_acc_.size());
	assert(root_.size() == arc_cond_.size());
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

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

	    // Fill rem with any component removed, so that
	    // remove_component() does not have to traverse the SCC
	    // again.
	    hash_type::const_iterator spi = h_.find(curr);
	    assert(spi != h_.end());
	    root_.front().states.push_front(spi->first);

	    // 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(!root_.empty());
	    if (root_.front().index == spi->second)
	      {
140
141
142
143
144
		assert(!arc_acc_.empty());
		assert(arc_cond_.size() == arc_acc_.size());
		bdd cond = arc_cond_.top();
		arc_cond_.pop();
		arc_acc_.pop();
145
		int num = relabel_component();
146
		root_.pop_front();
147
148
149
150

		// Record the transition between the SCC being popped
		// and the previous SCC.
		if (!root_.empty())
151
		  root_.front().succ.insert(std::make_pair(num, cond));
152
153
154
155
156
157
158
159
	      }

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

	// We have a successor to look at.
160
	// Fetch the values we are interested in...
161
162
163
164
165
166
167
168
169
170
171
172
173
174
	const state* dest = succ->current_state();
	bdd acc = succ->current_acceptance_conditions();
	bdd cond = succ->current_condition();
	// ... 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?
	hash_type::const_iterator spi = h_.find(dest);
	if (spi == h_.end())
	  {
	    // Yes.  Number it, stack it, and register its successors
	    // for later processing.
175
	    h_.insert(std::make_pair(dest, --num_));
176
	    root_.push_front(scc(num_));
177
178
	    arc_acc_.push(acc);
	    arc_cond_.push(cond);
179
180
181
182
183
184
	    tgba_succ_iterator* iter = aut_->succ_iter(dest);
	    iter->first();
	    todo_.push(pair_state_iter(dest, iter));
	    continue;
	  }

185
	// Have we reached a maximal SCC?
186
	if (spi->second >= 0)
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
	  {
	    int dest = spi->second;
	    // Record that there is a transition from this SCC to the
	    // dest SCC labelled with cond.
	    succ_type::iterator i = root_.front().succ.find(dest);
	    if (i == root_.front().succ.end())
	      root_.front().succ.insert(std::make_pair(dest, cond));
	    else
	      i->second |= cond;

	    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
208
209
	// ROOT is descending: we just have to merge all SCCs from the
	// top of ROOT that have an index lesser than the one of
210
211
212
213
	// the SCC of S2 (called the "threshold").
	int threshold = spi->second;
	std::list<const state*> states;
	succ_type succs;
214
215
	cond_set conds;
	conds.insert(cond);
216
	while (threshold > root_.front().index)
217
218
	  {
	    assert(!root_.empty());
219
220
	    assert(!arc_acc_.empty());
	    assert(arc_acc_.size() == arc_cond_.size());
221
	    acc |= root_.front().acc;
222
	    acc |= arc_acc_.top();
223
224
225
	    states.splice(states.end(), root_.front().states);
	    succs.insert(root_.front().succ.begin(),
			 root_.front().succ.end());
226
227
228
	    conds.insert(arc_cond_.top());
	    conds.insert(root_.front().conds.begin(),
			 root_.front().conds.end());
229
	    root_.pop_front();
230
231
	    arc_acc_.pop();
	    arc_cond_.pop();
232
	  }
233

234
235
236
	// Note that we do not always have
	//  threshold == root_.front().index
	// after this loop, the SCC whose index is threshold might have
237
	// been merged with a higher SCC.
238

239
240
	// Accumulate all acceptance conditions, states, SCC
	// successors, and conditions into the merged SCC.
241
242
243
	root_.front().acc |= acc;
	root_.front().states.splice(root_.front().states.end(), states);
	root_.front().succ.insert(succs.begin(), succs.end());
244
	root_.front().conds.insert(conds.begin(), conds.end());
245
246
247
      }
  }

248
  unsigned scc_map::scc_of_state(const state* s) const
249
250
251
252
253
254
  {
    hash_type::const_iterator i = h_.find(s);
    assert(i != h_.end());
    return i->second;
  }

255
  const scc_map::cond_set& scc_map::cond_set_of(unsigned n) const
256
  {
257
258
    assert(scc_map_.size() > n);
    return scc_map_[n].conds;
259
260
  }

261
  bdd scc_map::acc_set_of(unsigned n) const
262
  {
263
264
    assert(scc_map_.size() > n);
    return scc_map_[n].acc;
265
266
  }

267
  const std::list<const state*>& scc_map::states_of(unsigned n) const
268
  {
269
270
    assert(scc_map_.size() > n);
    return scc_map_[n].states;
271
272
  }

273
  unsigned scc_map::scc_count() const
274
  {
275
    return scc_map_.size();
276
277
  }

278
279
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
327
328
329
330
  namespace
  {
    struct scc_recurse_data
    {
      scc_recurse_data() : acc_scc(0), dead_scc(0) {};
      typedef std::map<int, unsigned> graph_counter;
      graph_counter acc_paths;
      graph_counter dead_paths;
      unsigned acc_scc;
      unsigned dead_scc;
    };

    bool scc_recurse(const scc_map& m, int state, scc_recurse_data& data)
    {
      const scc_map::succ_type& succ = m.succ(state);

      bool accepting = m.accepting(state);
      scc_map::succ_type::const_iterator it;
      int acc_paths = 0;
      int dead_paths = 0;

      bool paths_accepting = false;
      for (it = succ.begin(); it != succ.end(); ++it)
	{
	  int dest = it->first;
	  bool path_accepting = scc_recurse(m, dest, data);
	  paths_accepting |= path_accepting;

	  if (path_accepting)
	    acc_paths += data.acc_paths[dest];
	  else
	    dead_paths += data.dead_paths[dest];
	}

      if (accepting)
	{
	  ++data.acc_scc;
	  if (!paths_accepting)
	    acc_paths = 1;
	}
      else if (!paths_accepting)
	{
	  ++data.dead_scc;
	}

      data.acc_paths[state] = acc_paths;
      data.dead_paths[state] = dead_paths;

      return accepting | paths_accepting;
    }

  }

331
332
333
334
  scc_stats build_scc_stats(const scc_map& m)
  {
    scc_stats res;
    res.scc_total = m.scc_count();
335
336
337
338
339
340
341
342
343
344

    scc_recurse_data d;
    int init = m.initial();
    scc_recurse(m, init, d);

    res.acc_scc = d.acc_scc;
    res.dead_scc = d.dead_scc;
    res.acc_paths = d.acc_paths[init];
    res.dead_paths = d.dead_paths[init];

345
346
347
348
349
350
351
352
353
354
355
356
    return res;
  }

  scc_stats
  build_scc_stats(const tgba* a)
  {
    scc_map m(a);
    m.build_map();
    return build_scc_stats(m);
  }

  std::ostream&
357
  dump_scc_dot(const scc_map& m, std::ostream& out, bool verbose)
358
  {
359
    out << "digraph G {\n  i [label=\"\", style=invis, height=0]" << std::endl;
360
    int start = m.initial();
361
    out << "  i -> " << start << std::endl;
362
363
364
365
366
367
368
369
370
371
372
373

    typedef std::set<int> seen_map;
    seen_map seen;
    seen.insert(start);

    std::queue<int> q;
    q.push(start);
    while (!q.empty())
      {
	int state = q.front();
	q.pop();

374
375
376
	const scc_map::cond_set& cs = m.cond_set_of(state);

	std::ostringstream ostr;
377
	ostr << state;
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
	if (verbose)
	  {
	    size_t n = m.states_of(state).size();
	    ostr << " (" << n << " state";
	    if (n > 1)
	      ostr << "s";
	    ostr << ")\\naccs=";
	    bdd_print_accset(ostr, m.get_aut()->get_dict(),
			     m.acc_set_of(state));
	    ostr << "\\nconds=[";
	    for (scc_map::cond_set::const_iterator i = cs.begin();
		 i != cs.end(); ++i)
	      {
		if (i != cs.begin())
		  ostr << ", ";
		bdd_print_formula(ostr, m.get_aut()->get_dict(), *i);
	      }
	    ostr << "]";
	  }

398
	std::cout << "  " << state << " [shape=box,"
399
400
		  << (m.accepting(state) ? "style=bold," : "")
		  << "label=\"" << ostr.str() << "\"]" << std::endl;
401
402
403
404
405
406
407
408
409

	const scc_map::succ_type& succ = m.succ(state);

	scc_map::succ_type::const_iterator it;
	for (it = succ.begin(); it != succ.end(); ++it)
	  {
	    int dest = it->first;
	    bdd label = it->second;

410
	    out << "  " << state << " -> " << dest
411
412
413
		<< " [label=\"";
	    bdd_print_formula(out, m.get_aut()->get_dict(), label);
	    out << "\"]" << std::endl;
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429

	    seen_map::const_iterator it = seen.find(dest);
	    if (it != seen.end())
	      continue;

	    seen.insert(dest);
	    q.push(dest);
	  }
      }

    out << "}" << std::endl;

    return out;
  }

  std::ostream&
430
  dump_scc_dot(const tgba* a, std::ostream& out, bool verbose)
431
432
433
  {
    scc_map m(a);
    m.build_map();
434
    return dump_scc_dot(m, out, verbose);
435
436
437
  }

}