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/ParityGame_impl.h"
11 :
12 : #include <deque>
13 : #include <map>
14 : #include <cstdlib>
15 :
16 0 : ParityGame::ParityGame()
17 0 : : d_(0), vertex_(NULL), cardinality_(NULL)
18 : {
19 0 : }
20 :
21 0 : ParityGame::~ParityGame()
22 : {
23 0 : delete[] vertex_;
24 0 : delete[] cardinality_;
25 0 : }
26 :
27 0 : void ParityGame::clear()
28 : {
29 0 : delete[] vertex_;
30 0 : delete[] cardinality_;
31 :
32 0 : d_ = 0;
33 0 : graph_.clear();
34 0 : vertex_ = NULL;
35 0 : cardinality_ = NULL;
36 0 : }
37 :
38 0 : void ParityGame::assign(const ParityGame &game)
39 : {
40 0 : if (&game == this) return;
41 :
42 0 : graph_.assign(game.graph_);
43 0 : verti V = graph_.V();
44 0 : reset(V, game.d_);
45 0 : std::copy(game.vertex_, game.vertex_ + V, vertex_);
46 0 : recalculate_cardinalities(V);
47 : }
48 :
49 0 : void ParityGame::assign(const StaticGraph& g, ParityGameVertex* v)
50 : {
51 0 : delete[] vertex_;
52 0 : delete[] cardinality_;
53 :
54 0 : vertex_ = v;
55 0 : graph_.assign(g);
56 0 : d_ = 0;
57 0 : for(verti i = 0; i < g.V(); i++)
58 : {
59 0 : d_ = std::max(d_, static_cast<int>(v[i].priority + 1));
60 : }
61 0 : cardinality_ = new verti[d_];
62 0 : recalculate_cardinalities(g.V());
63 0 : }
64 :
65 0 : void ParityGame::reset(verti V, int d)
66 : {
67 0 : delete[] vertex_;
68 0 : delete[] cardinality_;
69 :
70 0 : d_ = d;
71 0 : vertex_ = new ParityGameVertex[V];
72 0 : cardinality_ = new verti[d_];
73 0 : }
74 :
75 0 : void ParityGame::recalculate_cardinalities(verti num_vertices)
76 : {
77 0 : std::fill(cardinality_, cardinality_ + d_, 0);
78 0 : for (verti v = 0; v < num_vertices; ++v)
79 : {
80 0 : cardinality_[vertex_[v].priority] += 1;
81 : }
82 0 : }
83 :
84 0 : void ParityGame::make_random( verti V, unsigned clustersize, unsigned outdeg,
85 : StaticGraph::EdgeDirection edge_dir, int d )
86 : {
87 0 : graph_.make_random_clustered(clustersize > 0 ? clustersize : V,
88 : V, outdeg, edge_dir);
89 0 : if (clustersize > 0) graph_.shuffle_vertices();
90 0 : reset(V, d);
91 0 : for (verti v = 0; v < V; ++v)
92 : {
93 0 : vertex_[v].player = (rand()%2 == 0) ? PLAYER_EVEN : PLAYER_ODD;
94 0 : vertex_[v].priority = rand()%d;
95 : }
96 0 : recalculate_cardinalities(V);
97 0 : }
98 :
99 0 : void ParityGame::make_dual()
100 : {
101 : // For each vertex, invert player and increase priority by one
102 0 : for (verti v = 0; v < graph_.V(); ++v)
103 : {
104 0 : vertex_[v].player = opponent(vertex_[v].player);
105 0 : vertex_[v].priority = vertex_[v].priority + 1;
106 : }
107 :
108 : // Update priority counts (move each on space to the right)
109 0 : verti *new_cardinality = new verti[d_ + 1];
110 0 : new_cardinality[0] = 0;
111 0 : std::copy(cardinality_, cardinality_ + d_, new_cardinality + 1);
112 0 : delete[] cardinality_;
113 0 : cardinality_ = new_cardinality;
114 0 : d_ = d_ + 1;
115 :
116 : // Try to compress priorities
117 0 : compress_priorities();
118 0 : }
119 :
120 0 : void ParityGame::shuffle(const std::vector<verti> &perm)
121 : {
122 : // N.B. maximum priority and priorities cardinalities remain unchanged.
123 :
124 : /* NOTE: shuffling could probably be done more efficiently (in-place?)
125 : if performance becomes an issue. */
126 0 : graph_.shuffle_vertices(perm);
127 :
128 : // Create new vertex info
129 0 : ParityGameVertex *new_vertex = new ParityGameVertex[graph_.V()];
130 0 : for (verti v = 0; v < graph_.V(); ++v) new_vertex[perm[v]] = vertex_[v];
131 0 : delete[] vertex_;
132 0 : vertex_ = new_vertex;
133 0 : }
134 :
135 0 : void ParityGame::compress_priorities( const verti cardinality[],
136 : bool preserve_parity )
137 : {
138 0 : if (cardinality == 0) cardinality = cardinality_;
139 :
140 : // Quickly check if we have anything to compress first:
141 0 : if ( empty() || std::find( cardinality + preserve_parity,
142 0 : cardinality + d_, 0 ) == cardinality + d_ )
143 : {
144 0 : return;
145 : }
146 :
147 : // Find out how to map old priorities to new priorities
148 0 : std::vector<int> prio_map(d_, -1);
149 0 : int first_prio = 0, last_prio = 0;
150 0 : if (!preserve_parity)
151 : {
152 : // Find lowest priority in use:
153 0 : while (cardinality[first_prio] == 0) ++first_prio;
154 0 : assert(first_prio < d_); // fails only if cardinality count is invalid!
155 : }
156 0 : int swap_players = first_prio%2;
157 0 : prio_map[first_prio] = last_prio;
158 0 : for (int p = first_prio + 1; p < d_; ++p)
159 : {
160 0 : if (cardinality[p] == 0) continue; // remove priority p
161 0 : if ((last_prio ^ p)%2 != swap_players) ++last_prio;
162 0 : prio_map[p] = last_prio;
163 : }
164 :
165 : // Update priority limit and cardinality counts
166 0 : int new_d = last_prio + 1;
167 0 : verti *new_cardinality = new verti[new_d];
168 0 : std::fill(new_cardinality, new_cardinality + new_d, 0);
169 0 : for (int p = 0; p < d_; ++p)
170 : {
171 0 : if (prio_map[p] >= 0)
172 : {
173 0 : new_cardinality[prio_map[p]] += cardinality_[p];
174 : }
175 : }
176 0 : delete[] cardinality_;
177 0 : cardinality_ = new_cardinality;
178 0 : d_ = new_d;
179 :
180 : // Remap priorities and players of all vertices
181 0 : for (verti v = 0; v < graph_.V(); ++v)
182 : {
183 0 : assert(prio_map[vertex_[v].priority] >= 0);
184 0 : vertex_[v].priority = prio_map[vertex_[v].priority];
185 0 : if (0 != swap_players) vertex_[v].player = opponent(vertex_[v].player);
186 : }
187 :
188 0 : return;
189 0 : }
190 :
191 0 : int ParityGame::propagate_priority( verti v, StaticGraph::const_iterator it,
192 : StaticGraph::const_iterator end )
193 : {
194 0 : int p = priority(v), q = 0;
195 0 : for ( ; it != end; ++it)
196 : {
197 0 : verti w = *it;
198 0 : int r = priority(w);
199 0 : if (r >= p) return 0;
200 0 : if (r > q) q = r;
201 : }
202 0 : vertex_[v].priority = q;
203 0 : --cardinality_[p];
204 0 : ++cardinality_[q];
205 0 : return p - q;
206 : }
207 :
208 : /* N.B. this method is designed to be reasonably fast and use little memory
209 : in the common case that few priorities can be propagated, which is why the
210 : algorithm starts with a first pass looking for vertices which can be
211 : updated, rather than putting them all in the initial queue, which would be
212 : simpler but require more memory up-front. */
213 0 : long long ParityGame::propagate_priorities()
214 : {
215 0 : long long res = 0;
216 0 : std::deque<verti> todo;
217 :
218 : // Make an initial pass to look for updatable vertices:
219 0 : for (verti v = 0; v < graph_.V(); ++v)
220 : {
221 0 : if (priority(v) > 0)
222 : {
223 0 : int change = propagate_priority(v, graph_.succ_begin(v),
224 : graph_.succ_end(v) )
225 0 : + propagate_priority(v, graph_.pred_begin(v),
226 0 : graph_.pred_end(v) );
227 0 : if (change > 0) {
228 0 : res += change;
229 0 : todo.push_back(v);
230 : }
231 : }
232 : }
233 :
234 : // Check neighbours of updated vertices again:
235 0 : while (!todo.empty())
236 : {
237 0 : verti w = todo.front();
238 0 : priority_t p = priority(w);
239 0 : todo.pop_front();
240 :
241 : // Perform backwards propagation on predecessors:
242 0 : for ( StaticGraph::const_iterator it = graph_.pred_begin(w);
243 0 : it != graph_.pred_end(w); ++it )
244 : {
245 0 : verti v = *it;
246 0 : if (priority(v) > p)
247 : {
248 0 : int change = propagate_priority(v, graph_.succ_begin(v),
249 : graph_.succ_end(v) );
250 0 : if (change > 0) {
251 0 : res += change;
252 0 : todo.push_back(v);
253 : }
254 : }
255 : }
256 :
257 : // Perform forwards propagation on successors:
258 0 : for ( StaticGraph::const_iterator it = graph_.succ_begin(w);
259 0 : it != graph_.succ_end(w); ++it )
260 : {
261 0 : verti v = *it;
262 0 : if (priority(v) > p)
263 : {
264 0 : int change = propagate_priority(v, graph_.pred_begin(v),
265 : graph_.pred_end(v) );
266 0 : if (change > 0) {
267 0 : res += change;
268 0 : todo.push_back(v);
269 : }
270 : }
271 : }
272 : }
273 :
274 0 : return res;
275 0 : }
276 :
277 0 : bool ParityGame::proper() const
278 : {
279 0 : for (verti v = 0; v < graph_.V(); ++v)
280 : {
281 0 : if (graph_.succ_begin(v) == graph_.succ_end(v)) return false;
282 : }
283 0 : return true;
284 : }
285 :
286 0 : void ParityGame::swap(ParityGame &pg)
287 : {
288 : using std::swap;
289 0 : swap(d_, pg.d_);
290 0 : swap(graph_, pg.graph_);
291 0 : swap(vertex_, pg.vertex_);
292 0 : swap(cardinality_, pg.cardinality_);
293 0 : }
294 :
295 : #ifdef WITH_THREADS
296 : void ParityGame::make_subgame_threads( const ParityGame &game,
297 : const verti *verts,
298 : const verti nvert,
299 : bool proper,
300 : StaticGraph::EdgeDirection edge_dir )
301 : {
302 : assert(this != &game);
303 : reset(nvert, game.d());
304 :
305 : //#pragma omp parallel for
306 : for (verti v = 0; v < nvert; ++v)
307 : {
308 : vertex_[v] = game.vertex_[verts[v]];
309 : }
310 :
311 : graph_.make_subgraph_threads(game.graph_, verts, nvert, proper, edge_dir);
312 :
313 : // FIXME: parallellize this?
314 : recalculate_cardinalities(nvert);
315 : }
316 : #endif
|