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 : #ifndef MCRL2_PG_SMALL_PROGRESS_MEASURES_H
11 : #define MCRL2_PG_SMALL_PROGRESS_MEASURES_H
12 :
13 : #include "mcrl2/pg/ParityGameSolver.h"
14 : #include "mcrl2/pg/LiftingStrategy.h"
15 : #include "mcrl2/utilities/logger.h"
16 :
17 : /*! \defgroup SmallProgressMeasures
18 :
19 : Classes related to the Small Progress Measures parity game solving algoritm.
20 : */
21 :
22 : /*! \ingroup SmallProgressMeasures
23 :
24 : Object used to collect statistics when solving using the SPM algorithm */
25 : class LiftingStatistics
26 : {
27 : public:
28 : /*! Construct a statistics object for the given game. */
29 : LiftingStatistics(const ParityGame &game, long long max_lifts = -1);
30 :
31 : #if 0
32 : /*! Merge statistics from a given object into this object, using the given
33 : vertex mapping to map vertex indices (vertex v in `other` has index
34 : mapping[v] in this object). */
35 : void merge(const LiftingStatistics &other, const verti *mapping = NULL);
36 : #endif
37 :
38 : long long lifts_attempted() const { return lifts_attempted_; }
39 : long long lifts_succeeded() const { return lifts_succeeded_; }
40 : long long lifts_attempted(verti v) const { return vertex_stats_[v].first; }
41 : long long lifts_succeeded(verti v) const { return vertex_stats_[v].second; }
42 :
43 : void add_lifts_attempted(long long count) { lifts_attempted_ += count; }
44 : void add_lifts_succeeded(long long count) { lifts_succeeded_ += count; }
45 : void add_lifts_attempted(verti v, long long count)
46 : {
47 : vertex_stats_[v].first += count;
48 : }
49 : void add_lifts_succeeded(verti v, long long count)
50 : {
51 : vertex_stats_[v].second += count;
52 : }
53 :
54 : private:
55 : void record_lift(verti v, bool success);
56 : friend class SmallProgressMeasures;
57 :
58 : private:
59 : long long lifts_attempted_, lifts_succeeded_;
60 : std::vector<std::pair<long long, long long> > vertex_stats_;
61 : long long max_lifts_;
62 : };
63 :
64 : /*! \ingroup SmallProgressMeasures
65 :
66 : Implements the core of the Small Progress Measures algorithm, which keeps
67 : track of progress measure vectors, and allows lifting at vertices.
68 :
69 : Note that besides these vectors, it tracks the current lifting strategy and
70 : (optionally) a statistics object. All public methods of this class notify
71 : the lifting strategy whenever vectors change (due to one of the solve..()
72 : lift..() methods), but only when vertices are lifted through one of the
73 : solve..() methods, are lifting attempts recording in the statistics object.
74 :
75 : As a result, the lift..() methods can be used to introduce information from
76 : external sources into the game, without affecting the statistics for updates
77 : that result from local lifting attempts. These methods are thus used in the
78 : two-way approach to propagate information from the dual game, and the MPI
79 : recursive solver.
80 :
81 : Note that this is an abstract base class: subclasses may implement different
82 : storage formats for the progress measure vectors.
83 : */
84 : class SmallProgressMeasures
85 : {
86 : public:
87 : //! Maximum number of lifting attempts in a row before checking timer.
88 : static const int work_size = 10000;
89 :
90 : SmallProgressMeasures(
91 : const ParityGame &game, ParityGame::Player player,
92 : LiftingStatistics *stats = 0,
93 : const verti *vmap = 0, verti vmap_size = 0 );
94 :
95 : virtual ~SmallProgressMeasures();
96 :
97 : /*! Performs some work on the game using the given lifting strategy (which
98 : must have been initialized).
99 :
100 : @param max_attempts Maximum number of lifts attempted.
101 : @return How many attempts remain; i.e. if the result is greater than
102 : zero, the game is succesfully solved.
103 : @see initialize_lifting_strategy
104 : */
105 : long long solve_some( LiftingStrategy &ls,
106 : long long attempts = work_size );
107 : long long solve_some( LiftingStrategy2 &ls,
108 : long long attempts = work_size );
109 :
110 : /*! Performs one lifting attempt, and returns the index of the vertex and
111 : whether lifting succeeded. Returns NO_VERTEX if no more vertices were
112 : candidates for lifting. */
113 : std::pair<verti, bool> solve_one(LiftingStrategy &ls);
114 : verti solve_one(LiftingStrategy2 &ls);
115 :
116 : /*! After the game is solved, this returns the strategy at vertex `v` for
117 : the current player, or NO_VERTEX if the vertex is controlled by his
118 : opponent (in that case, any move is winning) or if it is won by his
119 : opponent (in that case, all moves are losing). */
120 : verti get_strategy(verti v) const;
121 :
122 : /*! Takes an initialized strategy vector and updates it for the current
123 : player. The result is valid only after the game is solved. */
124 : void get_strategy(ParityGame::Strategy &strat) const;
125 :
126 : /*! Returns the winning set for the given player by assigning the vertices
127 : in the set to the given output iterator. If the game is not completely
128 : solved yet, then this returns a subset of the winning set. */
129 : template<class OutputIterator>
130 : void get_winning_set(ParityGame::Player player, OutputIterator result);
131 :
132 : /*! Sets the given vertex's progress measure to top, if it isn't already,
133 : and returns whether it changed: */
134 : inline bool lift_to_top(verti v);
135 :
136 : /*! Sets the given vertex's progress measure to the given value, if this
137 : is greater than the current value, and returns whether it changed.
138 : val[] must be an array of length len(v). If carry is set, the new
139 : value must be strictly greater (or top). */
140 : bool lift_to(verti v, const verti vec2[], bool carry = 0);
141 :
142 : /*! Returns the same result as lift_to() but without changing any
143 : progress measure vectors. */
144 : bool less_than(verti v, const verti vec2[], bool carry = 0);
145 :
146 : /*! For debugging: print current state to stdout */
147 : void debug_print() const;
148 : void debug_print_vertex(int v) const;
149 :
150 : /*! For debugging: verify that the current state describes a valid SPM */
151 : bool verify_solution();
152 :
153 : /*! Return the parity to be solved. */
154 0 : const ParityGame &game() const { return game_; }
155 :
156 : /*! Return the player to solve for. */
157 : ParityGame::Player player() const { return (ParityGame::Player)p_; }
158 :
159 : /*! Return the length of the SPM vectors (a positive integer). */
160 : int len() const { return len_; }
161 :
162 : /*! Returns the SPM vector space; an array of len() integers. */
163 : const verti *M() const { return M_; }
164 :
165 : /*! Changes the SPM vector space. `new_M` must be an array of at least
166 : `len` non-negative integers. */
167 : void set_M(const verti *new_M) { std::copy(new_M, new_M + len_, M_); }
168 :
169 : /*! Decrements the i'th element of M. */
170 0 : void decr_M(int i) { assert(M_[i] > 1); --M_[i]; }
171 :
172 : /*! Return the number of odd priorities less than or equal to the
173 : priority of v. This is the length of the SPM vector for `v`. */
174 0 : int len(verti v) const { return (game_.priority(v) + 1 + p_)/2; }
175 :
176 : /*! Return whether the given SPM vector has top value. */
177 0 : bool is_top(const verti vec[]) const { return vec[0] == NO_VERTEX; }
178 :
179 : /*! Return whether the SPM vector for vertex `v` has top value. */
180 0 : bool is_top(verti v) const { return is_top(vec(v)); }
181 :
182 : // The following functions are implemented in derived classes that
183 : // implement the actual storage of progress measure vectors:
184 :
185 : /*! Return the SPM vector for vertex `v`.
186 : This array contains only the components with odd (for Even) or even
187 : (for Odd) indices of the vector (since the reset is fixed at zero). */
188 : // virtual verti *vec(verti v) = 0;
189 : virtual const verti *vec(verti v) const = 0;
190 :
191 : /*! Assign the first `len(v)` elements of the vector for vertex `w` to the
192 : vector for `v`, or its successor if `carry` is set. */
193 : virtual void set_vec(verti v, const verti src[], bool carry) = 0;
194 :
195 : /*! Set the value for vertex `v` to top. */
196 : virtual void set_vec_to_top(verti v) = 0;
197 :
198 : /*! Recalculates the set of dirty vertices, and pushes them into the
199 : given lifting strategy (which is assumed to be freshly allocated). */
200 : void initialize_lifting_strategy(LiftingStrategy2 &ls);
201 :
202 : protected:
203 : /*! Sets odd-controlled vertices with (only) loops to top.
204 : Should be called by derived classes after allocating SPM data. */
205 : void initialize_loops();
206 :
207 : /*! Set the SPM vector for vertex `v` to top value. This can decrease the
208 : vector space, but nothing else; e.g, the lifting strategy is not
209 : notified of the lift. */
210 : inline void set_top(verti v);
211 :
212 : private:
213 : SmallProgressMeasures(const SmallProgressMeasures &);
214 : SmallProgressMeasures &operator=(const SmallProgressMeasures &);
215 :
216 : private:
217 : /*! Compares the first `N` elements of the given SPM vectors and returns
218 : -1, 0 or 1 to indicate that v is smaller than, equal to, or larger than
219 : w (respectively). */
220 : inline int vector_cmp(const verti vec1[], const verti vec2[], int N) const;
221 :
222 : /*! Compares `N` elements of the SPM vectors for the given vertices. */
223 : inline int vector_cmp(verti v, verti w, int N) const;
224 :
225 : /*! Returns whehter vertex `v` is lifted to the maximum successor (true)
226 : or minimum successor (false), which in turn depends on whether it is
227 : controlled by the player `p_` we are solving for. */
228 0 : inline bool take_max(verti v) const { return game_.player(v) != p_; }
229 :
230 : /*! Returns whether the progress measure for vertex `v` must be strictly
231 : greater than its successors or not (which is true if its priority has
232 : parity different from the current player). */
233 0 : inline bool compare_strict(verti v) const { return game_.priority(v)%2 != p_; }
234 :
235 : /*! Returns the minimum or maximum successor for vertex `v`,
236 : depending on whether take_max is false or true (respectively). */
237 : inline verti get_ext_succ(verti v, bool take_max) const;
238 :
239 : /*! Returns the minimum or maximum successor for vertex `v` depending on
240 : whether it is owned by player `p_` or not. */
241 : inline verti get_ext_succ(verti v) const;
242 :
243 : /*! Returns the minimum successor for vertex `v`. */
244 0 : inline verti get_min_succ(verti v) const { return get_ext_succ(v, false); }
245 :
246 : /*! Returns the maximum successor for vertex `v`. */
247 : inline verti get_max_succ(verti v) const { return get_ext_succ(v, true); }
248 :
249 : /*! Returns whether the succesor with the extreme progress measure for the
250 : given vertex. (`Extreme` means minimal for even-controlled vertices,
251 : and maximal for odd-controlled vertices.) */
252 0 : inline verti get_successor(verti v) const { return strategy_[v]; }
253 :
254 : /*! Returns whether the given vertex is dirty; i.e. its progress measure
255 : is less than its successor (or less than or equal to, if its priority
256 : is odd). */
257 0 : inline bool is_dirty(verti v) const { return dirty_[v]; }
258 :
259 : // Allow selected lifting strategies to access the SPM internals:
260 : friend class PredecessorLiftingStrategy;
261 : friend class MaxMeasureLiftingStrategy2;
262 : friend class OldMaxMeasureLiftingStrategy;
263 :
264 : protected:
265 : const ParityGame &game_; //!< the game being solved
266 : const std::size_t p_; //!< the player to solve for
267 : LiftingStatistics *stats_; //!< statistics object to record lifts
268 : const verti *vmap_; //!< active vertex map (if any)
269 : verti vmap_size_; //!< size of vertex map
270 : std::size_t len_; //!< length of SPM vectors
271 : verti *M_; //!< bounds on the SPM vector components
272 : ParityGame::Strategy strategy_; //!< current strategy
273 : bool *dirty_; //!< marks unstable vertices
274 : };
275 :
276 : /*! \ingroup SmallProgressMeasures
277 :
278 : A small progress measures implementation that stores progress measure vectors
279 : "densely". All `len`*`V` elements are stored in a contiguous array.
280 :
281 : This is memory efficient and allows fast access and updating of progress
282 : measure vectors. The main limitation is that it does not support concurrent
283 : access.
284 : */
285 : class DenseSPM : public SmallProgressMeasures
286 : {
287 : public:
288 : DenseSPM(
289 : const ParityGame &game, ParityGame::Player player,
290 : LiftingStatistics *stats = 0,
291 : const verti *vertex_map = 0, verti vertex_map_size = 0 );
292 : ~DenseSPM();
293 :
294 : // verti *vec(verti v) { return &spm_[(std::size_t)len_*v]; }
295 0 : const verti *vec(verti v) const { return &spm_[(std::size_t)len_*v]; }
296 : void set_vec(verti v, const verti src[], bool carry) ;
297 : void set_vec_to_top(verti v);
298 :
299 : protected:
300 : verti *spm_; //!< array storing the SPM vector data
301 : };
302 :
303 :
304 : /*! \ingroup SmallProgressMeasures
305 :
306 : A parity game solver based on Marcin Jurdzinski's small progress measures
307 : algorithm, with pluggable lifting heuristics. */
308 : class SmallProgressMeasuresSolver
309 : : public ParityGameSolver
310 : {
311 : protected:
312 : /*! Helper class which is an OutputIterator that sets vertices assigned
313 : through it to top in the given SPM representation (which in turn updates
314 : the corresponding lifting strategy). */
315 : class SetToTopIterator
316 : {
317 : public:
318 0 : SetToTopIterator(SmallProgressMeasures &spm) : spm(spm) { }
319 : SetToTopIterator& operator++() { return *this; }
320 0 : SetToTopIterator& operator++(int) { return *this; }
321 0 : SetToTopIterator& operator*() { return *this; }
322 0 : SetToTopIterator& operator=(verti v)
323 : {
324 0 : spm.lift_to_top(v);
325 0 : return *this;
326 : }
327 :
328 : private:
329 : SmallProgressMeasures &spm;
330 : };
331 :
332 : public:
333 : SmallProgressMeasuresSolver( const ParityGame &game,
334 : std::shared_ptr<LiftingStrategyFactory> lsf,
335 : bool alternate = false,
336 : LiftingStatistics *stats = 0,
337 : const verti *vmap = 0,
338 : verti vmap_size = 0 );
339 :
340 : ParityGame::Strategy solve();
341 :
342 : /*! Solves the game by applying Jurdziński's proposed algorithm that solves
343 : the game for one player only, and then solves a subgame with the
344 : remaining vertices. This algorithm is most efficient when the original
345 : game is easier to solve than its dual. */
346 : virtual ParityGame::Strategy solve_normal();
347 :
348 : /*! Solves the game using Friedmann's alternate strategy. This allocates
349 : solving algorithms for both the normal game and its dual at once, and
350 : alternates working on each, exchanging information about solved vertices
351 : in the process. */
352 : virtual ParityGame::Strategy solve_alternate();
353 :
354 : /*! Preprocess the game so that vertices with loops either have the loop
355 : removed, or have all other edges removed. In the latter case, the vertex
356 : is necessarily won by the player corresponding with its parity.
357 :
358 : This preprocessing operation speeds up solving with small progress
359 : measures considerably, though it is superseded by the DecycleSolver
360 : which does more general preprocessing. */
361 : static void preprocess_game(ParityGame &game);
362 :
363 : private:
364 : SmallProgressMeasuresSolver(const SmallProgressMeasuresSolver&);
365 : SmallProgressMeasuresSolver &operator=(const SmallProgressMeasuresSolver&);
366 :
367 : protected:
368 : std::shared_ptr<LiftingStrategyFactory> lsf_; //!< factory used to create lifting strategy
369 : bool alternate_; //!< whether to use the alternate algorithm
370 : LiftingStatistics *stats_; //!< object to record lifting statistics
371 : const verti *vmap_; //!< current vertex map
372 : const verti vmap_size_; //!< size of vertex map
373 : };
374 :
375 : /*! \ingroup SmallProgressMeasures
376 :
377 : TODO: document this class. */
378 : class SmallProgressMeasuresSolver2 : public SmallProgressMeasuresSolver
379 : {
380 : public:
381 : SmallProgressMeasuresSolver2( const ParityGame &game,
382 : std::shared_ptr<LiftingStrategyFactory> lsf,
383 : bool alternate = false,
384 : LiftingStatistics *stats = 0,
385 : const verti *vmap = 0,
386 : verti vmap_size = 0 );
387 :
388 : ParityGame::Strategy solve_normal();
389 : ParityGame::Strategy solve_alternate();
390 :
391 : private:
392 : SmallProgressMeasuresSolver2(const SmallProgressMeasuresSolver2&);
393 : SmallProgressMeasuresSolver2 &operator=(const SmallProgressMeasuresSolver2&);
394 : };
395 :
396 : /*! \ingroup SmallProgressMeasures
397 :
398 : Factory class for SmallProgressMeasuresSolver instances */
399 : class SmallProgressMeasuresSolverFactory : public ParityGameSolverFactory
400 : {
401 : public:
402 : SmallProgressMeasuresSolverFactory(std::shared_ptr<LiftingStrategyFactory> lsf,
403 : int version = 1, bool alt = false, LiftingStatistics *stats = 0 );
404 :
405 : ParityGameSolver *create( const ParityGame &game,
406 : const verti *vmap,
407 : verti vmap_size );
408 :
409 : private:
410 : std::shared_ptr<LiftingStrategyFactory> lsf_;
411 : int version_;
412 : bool alt_;
413 : LiftingStatistics *stats_;
414 : };
415 :
416 : #include "SmallProgressMeasures_impl.h"
417 :
418 : #endif /* ndef MCRL2_PG_SMALL_PROGRESS_MEASURES_H */
|
