mCRL2
Loading...
Searching...
No Matches
ParityGame.h
Go to the documentation of this file.
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
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.
18namespace 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
32typedef std::size_t priority_t;
33
36 PLAYER_ODD = 1
38
39inline
41{
42 switch(p)
43 {
44 case PLAYER_EVEN:
45 return PLAYER_ODD;
46 case PLAYER_ODD:
47 return PLAYER_EVEN;
48 default:
49 throw mcrl2::runtime_error("unknown player");
50 }
51}
52
60{
63
66};
67
68inline bool operator== (const ParityGameVertex &a, const ParityGameVertex &b)
69{
70 return a.player == b.player && a.priority == b.priority;
71}
72
73inline bool operator!= (const ParityGameVertex &a, const ParityGameVertex &b)
74{
75 return a.player != b.player || a.priority != b.priority;
76}
77
78
85{
86public:
88
97 typedef std::vector<verti> Strategy;
98
100 ParityGame();
101
103 ~ParityGame();
104
106 void clear();
107
109 void assign(const ParityGame &game);
110
112 void assign(const StaticGraph& g, ParityGameVertex* na);
113
115 bool empty() const { return graph().empty(); }
116
118 void swap(ParityGame &pg);
119
120
123
137 void make_random( verti V, unsigned clustersize, unsigned outdeg,
138 StaticGraph::EdgeDirection edge_dir, int d );
139
148 template<class ForwardIterator>
149 void make_subgame( const ParityGame &game,
150 ForwardIterator vertices_begin,
151 ForwardIterator vertices_end,
152 bool proper,
155
156#ifdef WITH_THREADS
157 void make_subgame_threads( const ParityGame &game,
158 const verti *verts,
159 const verti nvert,
160 bool proper,
163#endif
164
166
169
175 void make_dual();
176
183 void shuffle(const std::vector<verti> &perm);
184
201 void compress_priorities( const verti cardinality[] = 0,
202 bool preserve_parity = true );
203
215 long long propagate_priorities();
217
220
222 void read_pgsolver( std::istream &is,
224
226 void write_pgsolver(std::ostream &os) const;
227
229 void read_pbes( const std::string &file_path, verti *goal_vertex = 0,
231 const std::string &rewrite_strategy = "jitty" );
232
234 void read_raw(std::istream &is);
235
237 void write_raw(std::ostream &os) const;
238
240 void write_dot(std::ostream &os) const;
241
244 void write_debug( const Strategy &s = Strategy(),
245 std::ostream &os = std::cerr) const;
246
248
251
253 priority_t d() const { return d_; }
254
256 const StaticGraph &graph() const { return graph_; }
257
259 priority_t priority(verti v) const { return vertex_[v].priority; }
260
262 Player player(verti v) const { return (Player)(signed char)vertex_[v].player; }
263
266 verti cardinality(int p) const { return cardinality_[p]; }
267
269 template<class StrategyT>
270 Player winner(const StrategyT &s, verti v) const;
271
273
276
280 bool proper() const;
281
289 bool verify(const Strategy &s, verti *error) const;
291
293 void assign_pbes( mcrl2::pbes_system::pbes &pbes, verti *goal_vertex = 0,
295 const std::string &rewrite_strategy = "jitty" );
296
297protected:
300 void reset(verti V, int d);
301
304 void recalculate_cardinalities(verti num_vertices);
305
311
312private:
313 explicit ParityGame(const ParityGame &game);
315
316private:
317 int d_;
322
326};
327
328inline 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 */
std::size_t verti
type used to number vertices
Definition Graph.h:24
std::size_t priority_t
Definition ParityGame.h:32
player_t
Definition ParityGame.h:35
@ PLAYER_ODD
Odd (1)
Definition ParityGame.h:36
@ PLAYER_EVEN
Even (0)
Definition ParityGame.h:35
player_t opponent(const player_t p)
Definition ParityGame.h:40
bool operator==(const ParityGameVertex &a, const ParityGameVertex &b)
Definition ParityGame.h:68
#define ATTR_PACKED
Definition ParityGame.h:23
void swap(ParityGame &a, ParityGame &b)
Definition ParityGame.h:328
bool operator!=(const ParityGameVertex &a, const ParityGameVertex &b)
Definition ParityGame.h:73
priority_t priority(verti v) const
Definition ParityGame.h:259
verti cardinality(int p) const
Definition ParityGame.h:266
priority_t d() const
Definition ParityGame.h:253
void clear()
void make_subgame(const ParityGame &game, ForwardIterator vertices_begin, ForwardIterator vertices_end, bool proper, StaticGraph::EdgeDirection edge_dir=StaticGraph::EDGE_NONE)
Player player(verti v) const
Definition ParityGame.h:262
bool empty() const
Definition ParityGame.h:115
ParityGame(const ParityGame &game)
void swap(ParityGame &pg)
void reset(verti V, int d)
long long propagate_priorities()
ParityGame & operator=(const ParityGame &game)
void write_pgsolver(std::ostream &os) const
StaticGraph graph_
Definition ParityGame.h:318
void assign(const ParityGame &game)
verti * cardinality_
Definition ParityGame.h:325
void assign_pbes(mcrl2::pbes_system::pbes &pbes, verti *goal_vertex=0, StaticGraph::EdgeDirection edge_dir=StaticGraph::EDGE_BIDIRECTIONAL, const std::string &rewrite_strategy="jitty")
void read_pgsolver(std::istream &is, StaticGraph::EdgeDirection edge_dir=StaticGraph::EDGE_BIDIRECTIONAL)
bool proper() const
void write_dot(std::ostream &os) const
player_t Player
Definition ParityGame.h:87
void shuffle(const std::vector< verti > &perm)
void read_raw(std::istream &is)
void write_debug(const Strategy &s=Strategy(), std::ostream &os=std::cerr) const
void write_raw(std::ostream &os) const
void recalculate_cardinalities(verti num_vertices)
bool verify(const Strategy &s, verti *error) const
Player winner(const StrategyT &s, verti v) const
int propagate_priority(verti v, StaticGraph::const_iterator it, StaticGraph::const_iterator end)
void compress_priorities(const verti cardinality[]=0, bool preserve_parity=true)
void make_dual()
ParityGameVertex * vertex_
Definition ParityGame.h:321
void read_pbes(const std::string &file_path, verti *goal_vertex=0, StaticGraph::EdgeDirection edge_dir=StaticGraph::EDGE_BIDIRECTIONAL, const std::string &rewrite_strategy="jitty")
const StaticGraph & graph() const
Definition ParityGame.h:256
void make_random(verti V, unsigned clustersize, unsigned outdeg, StaticGraph::EdgeDirection edge_dir, int d)
std::vector< verti > Strategy
Definition ParityGame.h:97
EdgeDirection
Definition Graph.h:84
@ EDGE_BIDIRECTIONAL
Definition Graph.h:88
@ EDGE_NONE
Definition Graph.h:85
bool empty() const
Definition Graph.h:176
const verti * const_iterator
Definition Graph.h:66
parameterized boolean equation system
Definition pbes.h:58
Standard exception class for reporting runtime errors.
Definition exception.h:27
Exception classes for use in libraries and tools.
@ error
Definition linearise.cpp:73
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72
player_t player
the vertex owner (i.e. next player to move)
Definition ParityGame.h:62
priority_t priority
the priority of the vertex between 0 and d (exclusive).
Definition ParityGame.h:65