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_PARITY_GAME_H
11 : #define MCRL2_PG_PARITY_GAME_H
12 :
13 : #include "mcrl2/utilities/exception.h"
14 : #include "mcrl2/pg/Graph.h"
15 :
16 : // Forward declaration of mcrl2::pbes_system::pbes, which may or may not be
17 : // defined later depending on whether mCRL2 support is compiled in.
18 : namespace mcrl2 { namespace pbes_system { class pbes; } }
19 :
20 : #if __GNUC__ >= 3
21 : # define ATTR_PACKED __attribute__((__packed__))
22 : #else
23 : # define ATTR_PACKED
24 : #endif
25 :
26 : /*! \defgroup ParityGameData
27 :
28 : Data structures used to represent parity games in memory.
29 : */
30 :
31 : /*! Type of priorities in the game */
32 : typedef std::size_t priority_t;
33 :
34 : /*! The two players in a parity game (Even and Odd) */
35 : enum player_t { PLAYER_EVEN = 0, //!< Even (0)
36 : PLAYER_ODD = 1 //!< Odd (1)
37 : } ATTR_PACKED;
38 :
39 : inline
40 0 : player_t opponent(const player_t p)
41 : {
42 0 : switch(p)
43 : {
44 0 : case PLAYER_EVEN:
45 0 : return PLAYER_ODD;
46 0 : case PLAYER_ODD:
47 0 : return PLAYER_EVEN;
48 0 : default:
49 0 : throw mcrl2::runtime_error("unknown player");
50 : }
51 : }
52 :
53 : /*! \ingroup ParityGameData
54 :
55 : Parity Game data associated with each vertex in the game graph.
56 :
57 : \sa ParityGame::Player
58 : */
59 : struct ParityGameVertex
60 : {
61 : //! the vertex owner (i.e. next player to move)
62 : player_t player;
63 :
64 : //! the priority of the vertex between 0 and `d` (exclusive).
65 : priority_t priority;
66 : };
67 :
68 0 : inline bool operator== (const ParityGameVertex &a, const ParityGameVertex &b)
69 : {
70 0 : return a.player == b.player && a.priority == b.priority;
71 : }
72 :
73 0 : inline bool operator!= (const ParityGameVertex &a, const ParityGameVertex &b)
74 : {
75 0 : return a.player != b.player || a.priority != b.priority;
76 : }
77 :
78 :
79 : /*! \ingroup ParityGameData
80 :
81 : A parity game extends a directed graph by assigning a player
82 : (Even or Odd) and an integer priority to every vertex.
83 : Priorities are between 0 and `d` (exclusive). */
84 : class ParityGame
85 : {
86 : public:
87 : typedef player_t Player;
88 :
89 : /*! A strategy determines the partitioning of the game's vertices into
90 : winning sets for both players and provides a deterministic strategy for
91 : the vertices controlled by a player in its winning set.
92 :
93 : For each vertex v owned by player p:
94 : - strategy[v] == NO_VERTEX if vertex v is not in p's winning set
95 : - strategy[v] == w if vertex v is in p's winning set, (v,w) is an edge
96 : in the game graph, and (v,w) is a winning move for player p. */
97 : typedef std::vector<verti> Strategy;
98 :
99 : /*! Construct an empty parity game */
100 : ParityGame();
101 :
102 : /*! Destroy a parity game */
103 : ~ParityGame();
104 :
105 : /*! Reset to an empty game. */
106 : void clear();
107 :
108 : /*! Reset the game to a copy of `game`. */
109 : void assign(const ParityGame &game);
110 :
111 : /*! Reset the game with the given graph and node attributes. */
112 : void assign(const StaticGraph& g, ParityGameVertex* na);
113 :
114 : /*! Returns whether the game is empty. */
115 0 : bool empty() const { return graph().empty(); }
116 :
117 : /*! Efficiently swaps the contents of this parity game with another one. */
118 : void swap(ParityGame &pg);
119 :
120 :
121 : //!\name Generation
122 : //!@{
123 :
124 : /*! Generate a random parity game, with vertices assigned uniformly at
125 : random to players, and priority assigned uniformly between 0 and d-1.
126 :
127 : The generated game is a clustered random game if clustersize > 0, or
128 : an unclustered random game otherwise.
129 :
130 : \param V number of game vertices
131 : \param clustersize cluster size (or 0 for no clustering)
132 : \param outdeg average outdegree (at least 1)
133 : \param edge_dir part of edges to store
134 : \param d number of priorities (at least 1)
135 : \sa void StaticGraph::make_random()
136 : */
137 : void make_random( verti V, unsigned clustersize, unsigned outdeg,
138 : StaticGraph::EdgeDirection edge_dir, int d );
139 :
140 : /*! Create a subgame containing only the given vertices from the original
141 : game. Vertices are renumbered to be in range [0..num_vertices).
142 : Edges going out of the vertex subset specified by `vertices` are
143 : removed, so every vertex must have at least one outgoing edge that stays
144 : within the vertex subset, or the result is not a valid parity game.
145 :
146 : \sa make_subgame(const ParityGame &, const verti *, verti, const Strategy &)
147 : */
148 : template<class ForwardIterator>
149 : void make_subgame( const ParityGame &game,
150 : ForwardIterator vertices_begin,
151 : ForwardIterator vertices_end,
152 : bool proper,
153 : StaticGraph::EdgeDirection edge_dir
154 : = StaticGraph::EDGE_NONE );
155 :
156 : #ifdef WITH_THREADS
157 : void make_subgame_threads( const ParityGame &game,
158 : const verti *verts,
159 : const verti nvert,
160 : bool proper,
161 : StaticGraph::EdgeDirection edge_dir
162 : = StaticGraph::EDGE_NONE );
163 : #endif
164 :
165 : //!@}
166 :
167 : //!\name Transformation
168 : //!@{
169 :
170 : /*! Replaces the current game by its dual game, which uses the same game
171 : graph, but swaps players and changes priorities, such that the solution
172 : to the game is the same except with winners reversed. (A node won by
173 : even in the old game, is won by odd in the dual game, and vice versa.)
174 : */
175 : void make_dual();
176 :
177 : /*! Shuffles the nodes in the game. Node n becomes node perm[n], for all n.
178 : Requires that perm contains a permuation of 0 through graph().V()-1.
179 :
180 : NOTE: this is the reverse of what is normally understood to be a
181 : permutation! i.e. (2 3 1) maps 1->2, 2->3, 3->1 (instead of the
182 : usual interpretation of 1->3, 2->1, 3->2) */
183 : void shuffle(const std::vector<verti> &perm);
184 :
185 : /*! Compresses the range of priorities such that after compression,
186 : cardinality(p) > 0, for 0 < p < d.
187 :
188 : If `cardinality` is 0, then the priorities for the game itself are used.
189 : Otherwise, `cardinality` must be an array of length `d` and the caller
190 : must ensure that all priorities that occur in the game have a positive
191 : cardinality count.
192 :
193 : If `preserve_parity` is true, then remapping preserves the parity of
194 : priorities and thus players of vertices. In this case, cardinality(0)
195 : may be zero afterwards.
196 :
197 : If `preserve_parity` is false, then players as well as priorities are
198 : remapped to preserve winning sets. The function returns the parity of
199 : the priority that was mapped to zero.
200 : */
201 : void compress_priorities( const verti cardinality[] = 0,
202 : bool preserve_parity = true );
203 :
204 : /*! Propagate priorities in the graph, by changing the priority for a vertex
205 : to the maximum of the priorities of its successors, if this is less than
206 : the vertex's current priority value, and similarly for its predecessors.
207 :
208 : This preserves winners and optimal strategies, but usually shifts the
209 : distribution of priorities towards lower values, which benefits the
210 : performance in some solvers.
211 :
212 : Returns the sum of differences between old and new priority values
213 : for all vertices.
214 : */
215 : long long propagate_priorities();
216 : //!@}
217 :
218 : //!\name Input/Output
219 : //!@{
220 :
221 : /*! Read a game description in PGSolver format. */
222 : void read_pgsolver( std::istream &is,
223 : StaticGraph::EdgeDirection edge_dir = StaticGraph::EDGE_BIDIRECTIONAL );
224 :
225 : /*! Write a game description in PGSolver format. */
226 : void write_pgsolver(std::ostream &os) const;
227 :
228 : /*! Read a game description from an mCRL2 PBES. */
229 : void read_pbes( const std::string &file_path, verti *goal_vertex = 0,
230 : StaticGraph::EdgeDirection edge_dir = StaticGraph::EDGE_BIDIRECTIONAL,
231 : const std::string &rewrite_strategy = "jitty" );
232 :
233 : /*! Read raw parity game data from input stream */
234 : void read_raw(std::istream &is);
235 :
236 : /*! Write raw parity game data to output stream */
237 : void write_raw(std::ostream &os) const;
238 :
239 : /*! Write a game description in Graphviz DOT format */
240 : void write_dot(std::ostream &os) const;
241 :
242 : /*! Write human-readable description of game to error stream (intended to
243 : be used while debugging only) with optional strategy. */
244 : void write_debug( const Strategy &s = Strategy(),
245 : std::ostream &os = std::cerr) const;
246 :
247 : //!@}
248 :
249 : //! \name Data access
250 : //!@{
251 :
252 : /*! Returns the priority limit d; all priorities must be in range [0:d). */
253 0 : priority_t d() const { return d_; }
254 :
255 : /*! Returns the game graph */
256 0 : const StaticGraph &graph() const { return graph_; }
257 :
258 : /*! Returns the priority associated with vertex v */
259 0 : priority_t priority(verti v) const { return vertex_[v].priority; }
260 :
261 : /*! Returns the player associated with vertex v */
262 0 : Player player(verti v) const { return (Player)(signed char)vertex_[v].player; }
263 :
264 : /*! Returns the number of vertices with priority `p`.
265 : `p` must be between 0 and `d` (exclusive). */
266 0 : verti cardinality(int p) const { return cardinality_[p]; }
267 :
268 : /*! Returns the winner for vertex v according to strategy s. */
269 : template<class StrategyT>
270 : Player winner(const StrategyT &s, verti v) const;
271 :
272 : //!@}
273 :
274 : //!\name Verification
275 : //!@{
276 :
277 : /*! Checks if this is a proper game.
278 :
279 : A game is proper if every vertex has a successor in the game graph. */
280 : bool proper() const;
281 :
282 : /*! Verifies that the given strategy is valid in this game.
283 :
284 : \param s the strategy to be verified
285 : \param error if non-NULL, then *error is set NO_VERTEX if the strategy is
286 : correct, and to the index of an incorrectly classified
287 : vertex if the strategy is incorrect.
288 : */
289 : bool verify(const Strategy &s, verti *error) const;
290 : //!@}
291 :
292 : /*! Generate a parity game from an mCRL2 PBES. */
293 : void assign_pbes( mcrl2::pbes_system::pbes &pbes, verti *goal_vertex = 0,
294 : StaticGraph::EdgeDirection edge_dir = StaticGraph::EDGE_BIDIRECTIONAL,
295 : const std::string &rewrite_strategy = "jitty" );
296 :
297 : protected:
298 : /*! Re-allocate memory to store information on V vertices with priorities
299 : between 0 and `d` (exclusive). */
300 : void reset(verti V, int d);
301 :
302 : /*! Recalculate cardinalities (priority frequencies) from the first
303 : `num_vertices` elements of `vertex_`. */
304 : void recalculate_cardinalities(verti num_vertices);
305 :
306 : /*! Helper function for ParityGame::propagate_priorities() that decreases
307 : the priority for `v` to the maximum of those in range [begin:end), if
308 : this is less than its current value, and returns the absolute change. */
309 : int propagate_priority( verti v, StaticGraph::const_iterator it,
310 : StaticGraph::const_iterator end );
311 :
312 : private:
313 : explicit ParityGame(const ParityGame &game);
314 : ParityGame &operator=(const ParityGame &game);
315 :
316 : private:
317 : int d_; /*!< priority limit (max. priority + 1) */
318 : StaticGraph graph_; /*!< game graph */
319 :
320 : /*! Assignment of players and priorities to vertices (size graph_.V()) */
321 : ParityGameVertex *vertex_;
322 :
323 : /*! Cardinality counts for priorities.
324 : cardinality_[p] is equal to the number of vertices with priority p. */
325 : verti *cardinality_;
326 : };
327 :
328 : inline void swap(ParityGame &a, ParityGame &b)
329 : {
330 : a.swap(b);
331 : }
332 :
333 : #include "ParityGame_impl.h"
334 :
335 : #endif /* ndef MCRL2_PG_PARITY_GAME_H */
|