Line data Source code
1 : // Copyright (c) 2009-2013 University of Twente
2 : // Copyright (c) 2009-2013 Michael Weber <michaelw@cs.utwente.nl>
3 : // Copyright (c) 2009-2013 Maks Verver <maksverver@geocities.com>
4 : // Copyright (c) 2009-2013 Eindhoven University of Technology
5 : //
6 : // Distributed under the Boost Software License, Version 1.0.
7 : // (See accompanying file LICENSE_1_0.txt or copy at
8 : // http://www.boost.org/LICENSE_1_0.txt)
9 :
10 : #include "mcrl2/pg/SCC.h"
11 : #include "mcrl2/pg/shuffle.h"
12 : #include "mcrl2/utilities/logger.h"
13 :
14 :
15 0 : StaticGraph::StaticGraph()
16 0 : : successors_(NULL), predecessors_(NULL),
17 0 : successor_index_(NULL), predecessor_index_(NULL)
18 : {
19 0 : reset(0, 0, EDGE_NONE);
20 0 : }
21 :
22 0 : StaticGraph::~StaticGraph()
23 : {
24 0 : delete[] successors_;
25 0 : delete[] predecessors_;
26 0 : delete[] successor_index_;
27 0 : delete[] predecessor_index_;
28 0 : }
29 :
30 0 : void StaticGraph::clear()
31 : {
32 0 : reset(0, 0, EDGE_NONE);
33 0 : }
34 :
35 0 : void StaticGraph::reset(verti V, edgei E, EdgeDirection edge_dir)
36 : {
37 0 : V_ = V;
38 0 : E_ = E;
39 0 : edge_dir_ = edge_dir;
40 :
41 0 : delete[] successors_;
42 0 : delete[] predecessors_;
43 0 : delete[] successor_index_;
44 0 : delete[] predecessor_index_;
45 :
46 0 : if ((edge_dir & EDGE_SUCCESSOR))
47 : {
48 0 : successors_ = new verti[E];
49 0 : successor_index_ = new edgei[V + 1];
50 0 : for (verti v = 0; v <= V; ++v) successor_index_[v] = 0;
51 : }
52 : else
53 : {
54 0 : successors_ = NULL;
55 0 : successor_index_ = NULL;
56 : }
57 :
58 0 : if ((edge_dir_ & EDGE_PREDECESSOR))
59 : {
60 0 : predecessors_ = new verti[E];
61 0 : predecessor_index_ = new edgei[V + 1];
62 0 : for (verti v = 0; v <= V; ++v) predecessor_index_[v] = 0;
63 : }
64 : else
65 : {
66 0 : predecessors_ = NULL;
67 0 : predecessor_index_ = NULL;
68 : }
69 0 : }
70 :
71 0 : static bool edge_cmp_forward ( const std::pair<verti, verti> &a,
72 : const std::pair<verti, verti> &b )
73 : {
74 0 : return a.first < b.first || (a.first == b.first && a.second < b.second);
75 : }
76 :
77 0 : static bool edge_cmp_backward( const std::pair<verti, verti> &a,
78 : const std::pair<verti, verti> &b )
79 : {
80 0 : return a.second < b.second || (a.second == b.second && a.first < b.first);
81 : }
82 :
83 0 : void StaticGraph::make_random_scc(edge_list &edges)
84 : {
85 0 : SCCs sccs;
86 0 : decompose_graph(*this, sccs);
87 :
88 : /* If we happen to have a single SCC by luck, we are done too: */
89 0 : if (sccs.size() <= 1) return;
90 :
91 : /* Otherwise, identify `top` and `bottom` components: */
92 0 : std::vector<verti> index(V_, NO_VERTEX);
93 0 : for (verti i = 0; i < sccs.size(); ++i)
94 : {
95 0 : const std::vector<verti> scc;
96 0 : for (verti j = 0; j < scc.size(); ++j)
97 : {
98 0 : index[scc[j]] = i;
99 : }
100 0 : }
101 0 : std::vector<char> is_top(sccs.size(), 1),
102 0 : is_bot(sccs.size(), 1);
103 0 : for (verti v = 0; v < V_; ++v)
104 : {
105 0 : for (const_iterator it = succ_begin(v); it != succ_end(v); ++it)
106 : {
107 0 : verti w = *it;
108 0 : if (index[v] != index[w])
109 : {
110 0 : is_bot[index[v]] = 0;
111 0 : is_top[index[w]] = 0;
112 : }
113 : }
114 : }
115 :
116 : /* Pick one vertex per SCC at random (excluding SCCs that are neither on top
117 : nor at the bottom of the hierarchy) and connect them in a cycle. */
118 : // FIXME: this creates more edges than strictly necessary!
119 0 : std::vector<verti> vertis;
120 0 : for (verti i = 0; i < sccs.size(); ++i)
121 : {
122 0 : if (is_top[i] || is_bot[i])
123 : {
124 0 : vertis.push_back(sccs[i][rand()%sccs[i].size()]);
125 : }
126 : }
127 0 : mCRL2log(mcrl2::log::debug) << "Connecting " << vertis.size()
128 0 : << " of " << V_ << " vertices to create an SCC." << std::endl;
129 0 : shuffle_vector(vertis);
130 0 : for (verti i = 0; i < sccs.size(); ++i)
131 : {
132 0 : const verti v = vertis[i],
133 0 : w = vertis[(i + 1)%sccs.size()];
134 0 : edges.push_back(std::make_pair(v, w));
135 : }
136 0 : }
137 :
138 0 : void StaticGraph::make_random(verti V, unsigned outdeg, EdgeDirection edge_dir,
139 : bool scc)
140 : {
141 0 : if (V < 2)
142 : {
143 0 : edge_list edges;
144 0 : assign(edges, edge_dir);
145 0 : return;
146 0 : }
147 :
148 : /* Some assumptions on the RNG output range: */
149 0 : assert(RAND_MAX >= 2*outdeg);
150 0 : assert(RAND_MAX >= V);
151 :
152 : /* Create a random edge set, with at least one outgoing edge per node,
153 : and an average outdegree `outdeg`, without any duplicate edges (but
154 : possibly with self-edges). */
155 0 : edge_list edges;
156 0 : std::vector<verti> neighbours(V);
157 0 : for (verti i = 0; i < V; ++i) neighbours[i] = i;
158 0 : for (verti i = 0; i < V; ++i)
159 : {
160 0 : unsigned N = 1 + rand()%(2*outdeg - 1);
161 0 : if (N >= V - 1) N = V - 1;
162 0 : for (unsigned n = 0; n < N; ++n)
163 : {
164 0 : std::swap(neighbours[n], neighbours[n + rand()%(V - n)]);
165 0 : if (neighbours[n] == i) // don't generate loops
166 : {
167 0 : std::swap( neighbours[n],
168 0 : neighbours[n + 1 + rand()%(V - n - 1)] );
169 : }
170 0 : edges.push_back(std::make_pair(i, neighbours[n]));
171 : }
172 : }
173 :
174 : /* Create graph from edge set */
175 0 : assign(edges, edge_dir);
176 :
177 0 : if (scc)
178 : {
179 : /* Turn graph into a single strongly connected component: */
180 0 : make_random_scc(edges);
181 0 : assign(edges, edge_dir);
182 : #ifdef DEBUG
183 : /* Check the resulting graph: */
184 : SCCs new_sccs;
185 : decompose_graph(*this, new_sccs);
186 : assert(new_sccs.size() == 1);
187 : #endif
188 : }
189 0 : }
190 :
191 0 : void StaticGraph::make_random_clustered( verti cluster_size, verti V,
192 : unsigned outdeg, EdgeDirection edge_dir)
193 : {
194 0 : assert(cluster_size > 1);
195 0 : std::size_t clusters = V/cluster_size;
196 0 : if (clusters <= 1)
197 : {
198 0 : make_random(V, outdeg, edge_dir, true);
199 0 : return;
200 : }
201 :
202 : // Build `clusters` initial random graphs of cluster_size each:
203 0 : StaticGraph *subgraphs = new StaticGraph[clusters];
204 0 : for (std::size_t i = 0; i < clusters; ++i)
205 : {
206 0 : subgraphs[i].make_random( cluster_size + (i < V%cluster_size),
207 : outdeg, edge_dir, true );
208 : }
209 :
210 : // Iteratively merge clusters:
211 0 : for (int i = 0; clusters > 1; ++i)
212 : {
213 0 : mCRL2log(mcrl2::log::verbose) << "Generating clustered random game level "
214 0 : << i << "..." << std::endl;
215 0 : std::size_t next_clusters = (clusters + cluster_size - 1)/cluster_size;
216 0 : StaticGraph *next_subgraphs = new StaticGraph[next_clusters];
217 0 : std::vector<verti> offset(clusters, 0);
218 0 : for (std::size_t c = 0; c < next_clusters; ++c)
219 : {
220 : /* Combine clusters [i:j) into one: */
221 0 : std::size_t i = c*clusters/next_clusters,
222 0 : j = (c + 1)*clusters/next_clusters;
223 0 : mCRL2log(mcrl2::log::debug) << "combining " << j-i << " subgraphs ("
224 0 : << i << " through " << j << " of "
225 0 : << clusters << ")" << std::endl;
226 :
227 : /* Calculate offsets to apply to vertex indices: */
228 0 : for (std::size_t k = i + 1; k < j; ++k)
229 : {
230 0 : offset[k] = offset[k - 1] + subgraphs[k - 1].V();
231 : }
232 :
233 : /* Build edge list of combined subgraphs: */
234 0 : edge_list edges;
235 0 : for (std::size_t k = i; k < j; ++k)
236 : {
237 0 : edge_list subedges = subgraphs[k].get_edges();
238 0 : for ( edge_list::const_iterator it = subedges.begin();
239 0 : it != subedges.end(); ++it )
240 : {
241 0 : edges.push_back(std::make_pair( it->first + offset[k],
242 0 : it->second + offset[k] ));
243 : }
244 0 : }
245 :
246 : /* Create parent graph and use its edges to connect subgraphs: */
247 0 : StaticGraph parent;
248 0 : parent.make_random(j - i, outdeg, edge_dir, true);
249 0 : edge_list paredges = parent.get_edges();
250 0 : for (std::size_t e = 0; e < paredges.size(); ++e)
251 : {
252 0 : verti v = paredges[e].first,
253 0 : w = paredges[e].second;
254 0 : edges.push_back(std::make_pair(
255 0 : offset[i + v] + rand()%subgraphs[i + v].V(),
256 0 : offset[i + w] + rand()%subgraphs[i + w].V() ));
257 : }
258 0 : next_subgraphs[c].assign(edges, edge_dir);
259 0 : }
260 0 : delete[] subgraphs;
261 0 : subgraphs = next_subgraphs;
262 0 : clusters = next_clusters;
263 0 : }
264 0 : assert(clusters == 1);
265 0 : swap(subgraphs[0]);
266 0 : delete[] subgraphs;
267 : }
268 :
269 0 : void StaticGraph::shuffle_vertices()
270 : {
271 0 : std::vector<verti> perm(V_);
272 0 : for (verti i = 0; i < V_; ++i) perm[i] = i;
273 0 : shuffle_vector(perm);
274 0 : shuffle_vertices(perm);
275 0 : }
276 :
277 0 : void StaticGraph::shuffle_vertices(const std::vector<verti> &perm)
278 : {
279 0 : edge_list edges = get_edges();
280 0 : for (edge_list::iterator it = edges.begin(); it != edges.end(); ++it)
281 : {
282 0 : it->first = perm[it->first];
283 0 : it->second = perm[it->second];
284 : }
285 0 : assign(edges, edge_dir_);
286 0 : }
287 :
288 0 : void StaticGraph::assign(const StaticGraph &graph)
289 : {
290 0 : if (&graph == this) return;
291 :
292 0 : reset(graph.V_, graph.E_, graph.edge_dir_);
293 :
294 0 : if (edge_dir_ & EDGE_SUCCESSOR)
295 : {
296 0 : std::copy(graph.successors_, graph.successors_ + E_, successors_);
297 0 : std::copy(graph.successor_index_, graph.successor_index_ + V_ + 1,
298 : successor_index_);
299 : }
300 0 : if (edge_dir_ & EDGE_PREDECESSOR)
301 : {
302 0 : std::copy(graph.predecessors_, graph.predecessors_ + E_, predecessors_);
303 0 : std::copy(graph.predecessor_index_, graph.predecessor_index_ + V_ + 1,
304 : predecessor_index_);
305 : }
306 : }
307 :
308 0 : void StaticGraph::assign(edge_list edges, EdgeDirection edge_dir)
309 : {
310 : // Find number of vertices
311 0 : verti V = 0;
312 0 : for (edge_list::iterator it = edges.begin(); it != edges.end(); ++it)
313 : {
314 0 : if (it->first >= V) V = it->first + 1;
315 0 : if (it->second >= V) V = it->second + 1;
316 : }
317 :
318 : // Count number of vertices
319 0 : edgei E = (edgei)edges.size();
320 0 : assert(E == edges.size()); /* detect integer overflow */
321 :
322 : /* Reallocate memory */
323 0 : reset(V, E, edge_dir);
324 :
325 0 : if (edge_dir_ & EDGE_SUCCESSOR)
326 : {
327 : /* Sort edges by predecessor first, successor second */
328 0 : if (!std::is_sorted(edges.begin(), edges.end(), edge_cmp_forward))
329 : {
330 0 : std::sort(edges.begin(), edges.end(), edge_cmp_forward);
331 : }
332 :
333 : /* Create successor index */
334 0 : edgei pos = 0;
335 0 : for (verti v = 0; v < V; ++v)
336 : {
337 0 : while (pos < E && edges[pos].first < v) ++pos;
338 0 : successor_index_[v] = pos;
339 : }
340 0 : successor_index_[V] = E;
341 :
342 : /* Create successor list */
343 0 : for (edgei e = 0; e < E; ++e) successors_[e] = edges[e].second;
344 : }
345 :
346 0 : if (edge_dir_ & EDGE_PREDECESSOR)
347 : {
348 : /* Sort edges by successor first, predecessor second */
349 0 : std::sort(edges.begin(), edges.end(), edge_cmp_backward);
350 :
351 : /* Create predecessor index */
352 0 : edgei pos = 0;
353 0 : for (verti v = 0; v < V; ++v)
354 : {
355 0 : while (pos < E && edges[pos].second < v) ++pos;
356 0 : predecessor_index_[v] = pos;
357 : }
358 0 : predecessor_index_[V] = E;
359 :
360 : /* Create predecessor list */
361 0 : for (edgei e = 0; e < E; ++e) predecessors_[e] = edges[e].first;
362 : }
363 0 : }
364 :
365 0 : void StaticGraph::remove_edges(StaticGraph::edge_list &edges)
366 : {
367 : // Add end-of-list marker:
368 0 : edges.push_back(std::make_pair(V_, V_));
369 :
370 0 : if (edge_dir_ & EDGE_SUCCESSOR)
371 : {
372 : // Sort edges by predecessor first, successor second
373 0 : if (!std::is_sorted(edges.begin(), edges.end(), edge_cmp_forward))
374 : {
375 0 : std::sort(edges.begin(), edges.end(), edge_cmp_forward);
376 : }
377 :
378 : // Loop over existing edges and remove those listed in `edges`:
379 0 : StaticGraph::edge_list::const_iterator it = edges.begin();
380 0 : const verti *p = successors_;
381 0 : verti v = 0;
382 0 : edgei e = 0;
383 0 : while (v < V_)
384 : {
385 0 : if (p == successors_ + successor_index_[v + 1])
386 : {
387 0 : successor_index_[++v] = e;
388 0 : continue;
389 : }
390 0 : std::pair<verti, verti> edge(v, *p++);
391 0 : while (edge_cmp_forward(*it, edge)) ++it;
392 0 : if (*it == edge) ++it; else successors_[e++] = edge.second;
393 : }
394 : }
395 :
396 0 : if (edge_dir_ & EDGE_PREDECESSOR)
397 : {
398 : // Sort edges by successor first, predecessor second
399 0 : std::sort(edges.begin(), edges.end(), edge_cmp_backward);
400 :
401 : // Loop over existing edges and remove those listed in `edges`:
402 0 : StaticGraph::edge_list::const_iterator it = edges.begin();
403 0 : const verti *p = predecessors_;
404 0 : verti v = 0;
405 0 : edgei e = 0;
406 0 : while (v < V_)
407 : {
408 0 : if (p == predecessors_ + predecessor_index_[v + 1])
409 : {
410 0 : predecessor_index_[++v] = e;
411 0 : continue;
412 : }
413 0 : std::pair<verti, verti> edge(*p++, v);
414 0 : while (edge_cmp_backward(*it, edge)) ++it;
415 0 : if (*it == edge) ++it; else predecessors_[e++] = edge.first;
416 : }
417 : }
418 :
419 : // Remove end-of-list marker:
420 0 : edges.pop_back();
421 :
422 : // Update edge count
423 0 : if (edge_dir_ & EDGE_SUCCESSOR)
424 : {
425 0 : if (edge_dir_ & EDGE_PREDECESSOR)
426 : {
427 0 : assert(successor_index_[V_] == predecessor_index_[V_]);
428 : }
429 0 : E_ = successor_index_[V_];
430 : }
431 : else
432 : {
433 0 : assert(edge_dir_ & EDGE_PREDECESSOR);
434 0 : E_ = predecessor_index_[V_];
435 : }
436 0 : }
437 :
438 0 : StaticGraph::edge_list StaticGraph::get_edges() const
439 : {
440 0 : assert(edge_dir_ & EDGE_SUCCESSOR); // successor info required for now!
441 :
442 0 : edge_list result;
443 0 : result.reserve(E_);
444 0 : for (verti v = 0; v < V_; ++v)
445 : {
446 0 : edgei begin = successor_index_[v], end = successor_index_[v + 1];
447 0 : for (edgei i = begin; i < end; ++i)
448 : {
449 0 : verti w = successors_[i];
450 0 : result.push_back(std::make_pair(v, w));
451 : }
452 : }
453 0 : assert(result.size() == E_);
454 0 : return result;
455 0 : }
456 :
457 0 : void StaticGraph::write_raw(std::ostream &os) const
458 : {
459 0 : os.write((const char*)&V_, sizeof(V_));
460 0 : os.write((const char*)&E_, sizeof(E_));
461 0 : os.write((const char*)&edge_dir_, sizeof(edge_dir_));
462 0 : if (edge_dir_ & EDGE_SUCCESSOR)
463 : {
464 0 : os.write((const char*)successors_, sizeof(verti)*E_);
465 0 : os.write((const char*)successor_index_, sizeof(edgei)*(V_ + 1));
466 : }
467 0 : if (edge_dir_ & EDGE_PREDECESSOR)
468 : {
469 0 : os.write((const char*)predecessors_, sizeof(verti)*E_);
470 0 : os.write((const char*)predecessor_index_, sizeof(edgei)*(V_ + 1));
471 : }
472 0 : }
473 :
474 0 : void StaticGraph::read_raw(std::istream &is)
475 : {
476 : verti V;
477 : edgei E;
478 : EdgeDirection edge_dir;
479 :
480 0 : is.read((char*)&V, sizeof(V));
481 0 : is.read((char*)&E, sizeof(E));
482 0 : is.read((char*)&edge_dir, sizeof(edge_dir));
483 :
484 0 : reset(V, E, edge_dir);
485 :
486 0 : if (edge_dir & EDGE_SUCCESSOR)
487 : {
488 0 : is.read((char*)successors_, sizeof(verti)*E_);
489 0 : is.read((char*)successor_index_, sizeof(edgei)*(V_ + 1));
490 : }
491 0 : if (edge_dir & EDGE_PREDECESSOR)
492 : {
493 0 : is.read((char*)predecessors_, sizeof(verti)*E_);
494 0 : is.read((char*)predecessor_index_, sizeof(edgei)*(V_ + 1));
495 : }
496 0 : }
497 :
498 0 : void StaticGraph::swap(StaticGraph &g)
499 : {
500 0 : if (this == &g) return;
501 0 : std::swap(V_, g.V_);
502 0 : std::swap(E_, g.E_);
503 0 : std::swap(successors_, g.successors_);
504 0 : std::swap(predecessors_, g.predecessors_);
505 0 : std::swap(successor_index_, g.successor_index_);
506 0 : std::swap(predecessor_index_, g.predecessor_index_);
507 0 : std::swap(edge_dir_, g.edge_dir_);
508 : }
509 :
510 : #ifdef WITH_THREADS
511 : void StaticGraph::make_subgraph_threads( const StaticGraph &graph,
512 : const verti *verts,
513 : const verti num_vertices,
514 : bool proper,
515 : EdgeDirection edge_dir )
516 : {
517 : assert(this != &graph);
518 :
519 : edgei num_edges = 0;
520 :
521 : // Create a map of old->new vertex indices:
522 : std::vector<verti> map(graph.V(), NO_VERTEX);
523 : #pragma omp parallel
524 : {
525 : #pragma omp for
526 : for (verti i = 0; i < num_vertices; ++i)
527 : {
528 : map[verts[i]] = i;
529 : }
530 :
531 : // Count number of new edges:
532 : #pragma omp for reduction(+:num_edges)
533 : for (verti i = 0; i < num_vertices; ++i)
534 : {
535 : const_iterator a = graph.succ_begin(verts[i]),
536 : b = graph.succ_end(verts[i]);
537 : while (a != b) if (map[*a++] != NO_VERTEX) ++num_edges;
538 : }
539 : }
540 :
541 : // Allocate memory:
542 : reset(num_vertices, num_edges, edge_dir ? edge_dir : graph.edge_dir());
543 :
544 : //
545 : // TODO: parallellize rest of function!
546 : //
547 :
548 : if (edge_dir_ & EDGE_SUCCESSOR)
549 : {
550 : // Assign new successors:
551 : verti v = 0;
552 : edgei e = 0;
553 : for (verti i = 0; i < num_vertices; ++i)
554 : {
555 : const verti u = verts[i];
556 : successor_index_[v++] = e;
557 : verti *begin = &successors_[e];
558 : for (const_iterator succ_it = graph.succ_begin(u),
559 : succ_end = graph.succ_end(u);
560 : succ_it != succ_end; ++succ_it)
561 : {
562 : verti w = map[*succ_it];
563 : if (w != NO_VERTEX) successors_[e++] = w;
564 : }
565 : verti *end = &successors_[e];
566 : if (!std::is_sorted(begin, end, std::less<verti>()))
567 : {
568 : std::sort(begin, end);
569 : }
570 : if (proper) assert(begin != end); /* proper parity game graph */
571 : }
572 : assert(v == V_ && e == E_);
573 : successor_index_[v] = e;
574 : }
575 :
576 : if (edge_dir_ & EDGE_PREDECESSOR)
577 : {
578 : // Assign new predecessors:
579 : verti v = 0;
580 : edgei e = 0;
581 : for (verti i = 0; i < num_vertices; ++i)
582 : {
583 : const verti u = verts[i];
584 : predecessor_index_[v++] = e;
585 : verti *begin = &predecessors_[e];
586 : for (const_iterator pred_it = graph.pred_begin(u),
587 : pred_end = graph.pred_end(u);
588 : pred_it != pred_end; ++pred_it)
589 : {
590 : verti w = map[*pred_it];
591 : if (w != NO_VERTEX) predecessors_[e++] = w;
592 : }
593 : verti *end = &predecessors_[e];
594 : if (!std::is_sorted(begin, end, std::less<verti>()))
595 : {
596 : std::sort(begin, end);
597 : }
598 : }
599 : assert(v == V_ && e == E_);
600 : predecessor_index_[v] = e;
601 : }
602 : }
603 : #endif
|
