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/MaxMeasureLiftingStrategy.h"
11 :
12 : /* TODO: write short description of how this works! */
13 :
14 0 : MaxMeasureLiftingStrategy2::MaxMeasureLiftingStrategy2(
15 : const ParityGame &game, const SmallProgressMeasures &spm,
16 0 : Order order, Metric metric )
17 0 : : LiftingStrategy2(), spm_(spm), order_(order), metric_(metric),
18 0 : next_id_(0),
19 0 : insert_id_(order < HEAP ? new uint64_t[game.graph().V()] : 0),
20 0 : pq_pos_(new verti[game.graph().V()]),
21 0 : pq_(new verti[game.graph().V()]), pq_size_(0)
22 : {
23 0 : std::fill(&pq_pos_[0], &pq_pos_[game.graph().V()], NO_VERTEX);
24 0 : }
25 :
26 0 : MaxMeasureLiftingStrategy2::~MaxMeasureLiftingStrategy2()
27 : {
28 0 : delete[] insert_id_;
29 0 : delete[] pq_pos_;
30 0 : delete[] pq_;
31 0 : }
32 :
33 0 : void MaxMeasureLiftingStrategy2::move_up(verti i)
34 : {
35 : // FIXME: this can be implemented with less swapping if I think harder.
36 0 : for (verti j; i > 0 && cmp(i, j = (i - 1)/2) > 0; i = j) swap(i, j);
37 0 : }
38 :
39 0 : void MaxMeasureLiftingStrategy2::move_down(verti i)
40 : {
41 : // FIXME: this can be implemented with less swapping if I think harder.
42 : for (;;)
43 : {
44 0 : verti j = 2*i + 1;
45 0 : verti k = 2*i + 2;
46 0 : int d = j < pq_size_ ? cmp(i, j) : 1;
47 0 : int e = k < pq_size_ ? cmp(i, k) : 1;
48 :
49 0 : if (d < 0 && e < 0)
50 : {
51 : // both children are larger than current node
52 0 : if (cmp(j, k) >= 0)
53 : {
54 : // left child is largest
55 0 : swap(i, j);
56 0 : i = j;
57 : }
58 : else
59 : {
60 : // right child is largest;
61 0 : swap(i, k);
62 0 : i = k;
63 : }
64 : }
65 : else
66 0 : if (d < 0)
67 : {
68 : // left child is larger
69 0 : swap(i, j);
70 0 : i = j;
71 : }
72 : else
73 0 : if (e < 0)
74 : {
75 : // right child is larger
76 0 : swap(i, k);
77 0 : i = k;
78 : }
79 : else
80 : {
81 : // both children are smaller; we're done
82 0 : break;
83 : }
84 0 : }
85 0 : }
86 :
87 0 : void MaxMeasureLiftingStrategy2::swap(verti i, verti j)
88 : {
89 0 : verti v = pq_[i], w = pq_[j];
90 0 : pq_[i] = w;
91 0 : pq_[j] = v;
92 0 : pq_pos_[w] = i;
93 0 : pq_pos_[v] = j;
94 0 : }
95 :
96 0 : void MaxMeasureLiftingStrategy2::push(verti v)
97 : {
98 0 : mCRL2log(mcrl2::log::debug) <<"push(" << v << ")" << std::endl;
99 0 : assert(pq_pos_[v] == NO_VERTEX);
100 0 : pq_[pq_size_] = v;
101 0 : pq_pos_[v] = pq_size_;
102 0 : ++pq_size_;
103 0 : if (insert_id_) insert_id_[v] = next_id_++;
104 0 : bumped_.push_back(pq_pos_[v]);
105 0 : }
106 :
107 0 : void MaxMeasureLiftingStrategy2::bump(verti v)
108 : {
109 0 : mCRL2log(mcrl2::log::debug) << "bump(" << v << ")" << std::endl;
110 0 : bumped_.push_back(pq_pos_[v]);
111 0 : }
112 :
113 0 : verti MaxMeasureLiftingStrategy2::pop()
114 : {
115 : #ifdef DEBUG
116 : static long long ops;
117 : ops += bumped_.size() + 1;
118 : #endif
119 :
120 0 : if (!bumped_.empty())
121 : {
122 : // Move bumped vertices up the heap.
123 0 : std::sort(bumped_.begin(), bumped_.end());
124 0 : bumped_.erase( std::unique(bumped_.begin(), bumped_.end()),
125 0 : bumped_.end() );
126 0 : for (std::vector<verti>::iterator it = bumped_.begin();
127 0 : it != bumped_.end(); ++it) move_up(*it);
128 :
129 : // CHECKME: why is this necessary for MAX_STEP too?
130 : // shouldn't this just be for MIN_STEP?
131 0 : if (metric_ != MAX_VALUE)
132 : {
133 : /* Note: minimization is a bit trickier than maximization, since
134 : we need to move bumped vertices down the heap (rather than up
135 : when maximizing) but pushed vertices still need to move up.
136 :
137 : Unfortunately, we can't easily distinguish between bumped or
138 : pushed or pushed-and-then-bumped vertices, so the easiest safe
139 : way to handle the situation is to move up first, and then down.
140 :
141 : FIXME: optimize this?
142 : */
143 :
144 : // Move bumped vertices down the heap.
145 0 : for (std::vector<verti>::reverse_iterator it = bumped_.rbegin();
146 0 : it != bumped_.rend(); ++it) move_down(*it);
147 : }
148 0 : bumped_.clear();
149 : }
150 :
151 0 : if (pq_size_ == 0) return NO_VERTEX;
152 :
153 : #ifdef DEBUG
154 : if (ops >= pq_size_)
155 : {
156 : Logger::debug("checking heap integrity");
157 : assert(check());
158 : ops -= pq_size_;
159 : }
160 : #endif
161 :
162 : // Extract top element from the heap.
163 0 : verti v = pq_[0];
164 0 : mCRL2log(mcrl2::log::debug) << "pop() -> " << v << std::endl;
165 0 : pq_pos_[v] = NO_VERTEX;
166 0 : if (--pq_size_ > 0)
167 : {
168 0 : pq_[0] = pq_[pq_size_];
169 0 : pq_pos_[pq_[0]] = 0;
170 0 : move_down(0);
171 : }
172 0 : return v;
173 : }
174 :
175 0 : static int cmp_ids(uint64_t x, uint64_t y)
176 : {
177 0 : return (x > y) - (x < y);
178 : }
179 :
180 : /* This returns +1 if lifting v1 to v2 would increase the progress measure
181 : by a larger difference than lifting w1 to w2.
182 :
183 : Assumes v1 >= v2 and w1 >= w2 (for the first v_len and w_len elements
184 : respectively) and that all vectors are within bounds. (If they are not,
185 : the results are still somewhat sensible, but it may be possible that two
186 : vectors compare unequal even though their steps are equally large.)
187 : */
188 0 : static int cmp_step( const verti *v1, const verti *v2, int v_len, bool v_carry,
189 : const verti *w1, const verti *w2, int w_len, bool w_carry )
190 : {
191 0 : for (int i = 0; i < v_len || i < w_len; ++i)
192 : {
193 0 : int a = i < v_len ? v2[i] - v1[i] : 0;
194 0 : int b = i < w_len ? w2[i] - w1[i] : 0;
195 0 : if (a != b) return (a > b) - (a < b);
196 : }
197 0 : if (v_carry || w_carry)
198 : {
199 0 : if (!w_carry) return +1;
200 0 : if (!v_carry) return -1;
201 0 : if (v_len < w_len) return +1;
202 0 : if (v_len > w_len) return -1;
203 : }
204 0 : return 0;
205 : }
206 :
207 0 : int MaxMeasureLiftingStrategy2::cmp(verti i, verti j)
208 : {
209 0 : verti v = pq_[i], w = pq_[j];
210 0 : int d = 0;
211 :
212 0 : switch (metric_)
213 : {
214 0 : case MAX_VALUE:
215 0 : d = spm_.vector_cmp( spm_.get_successor(v),
216 0 : spm_.get_successor(w), spm_.len_ );
217 0 : break;
218 :
219 0 : case MIN_VALUE:
220 0 : d = -spm_.vector_cmp( spm_.get_successor(v),
221 0 : spm_.get_successor(w), spm_.len_ );
222 0 : break;
223 :
224 0 : case MAX_STEP:
225 : #ifdef DEBUG
226 : // We assume vertices are only queued when they can be lifted;
227 : // i.e. their value is less than (or equal to) their successor:
228 : assert(spm_.vector_cmp(v, spm_.get_successor(v), spm_.len(v))
229 : < spm_.compare_strict(v));
230 : assert(spm_.vector_cmp(w, spm_.get_successor(w), spm_.len(w))
231 : < spm_.compare_strict(w));
232 : #endif
233 0 : d = cmp_step( spm_.vec(v), spm_.vec(spm_.get_successor(v)),
234 0 : spm_.len(v), spm_.compare_strict(v),
235 0 : spm_.vec(w), spm_.vec(spm_.get_successor(w)),
236 0 : spm_.len(w), spm_.compare_strict(w) );
237 0 : break;
238 : }
239 :
240 0 : if (d == 0)
241 : {
242 : // Tie-break on insertion order: smallest insert-id first in queue
243 : // mode, or largest insert-id first in stack mode.
244 0 : switch (order_)
245 : {
246 0 : case QUEUE: d = cmp_ids(insert_id_[w], insert_id_[v]); break;
247 0 : case STACK: d = cmp_ids(insert_id_[v], insert_id_[w]); break;
248 0 : default: break;
249 : }
250 : }
251 :
252 0 : return d;
253 : }
254 :
255 0 : bool MaxMeasureLiftingStrategy2::check()
256 : {
257 0 : for (verti i = 1; i < pq_size_; ++i)
258 : {
259 0 : if (cmp(i, (i - 1)/2) > 0) return false;
260 : }
261 :
262 0 : for (verti i = 0; i < pq_size_; ++i)
263 : {
264 0 : if (pq_pos_[pq_[i]] != i) return false;
265 : }
266 :
267 0 : const verti V = spm_.game().graph().V();
268 0 : for (verti v = 0; v < V; ++v)
269 : {
270 0 : if (pq_pos_[v] != NO_VERTEX)
271 : {
272 0 : if (pq_[pq_pos_[v]] != v) return false;
273 : }
274 : }
275 :
276 0 : return true;
277 : }
278 :
279 0 : bool MaxMeasureLiftingStrategyFactory::supports_version(int version)
280 : {
281 0 : return version == 2;
282 : }
283 :
284 0 : LiftingStrategy *MaxMeasureLiftingStrategyFactory::create(
285 : const ParityGame& /*game*/, const SmallProgressMeasures &/*spm*/ )
286 : {
287 0 : return nullptr;
288 : }
289 :
290 0 : LiftingStrategy2 *MaxMeasureLiftingStrategyFactory::create2(
291 : const ParityGame &game, const SmallProgressMeasures &spm )
292 : {
293 0 : return new MaxMeasureLiftingStrategy2(game, spm, order_, metric_);
294 : }
|
