10#ifndef MCRL2_PG_PARITY_GAME_H
11#define MCRL2_PG_PARITY_GAME_H
18namespace mcrl2 {
namespace pbes_system {
class pbes; } }
21# define ATTR_PACKED __attribute__((__packed__))
148 template<
class ForwardIterator>
150 ForwardIterator vertices_begin,
151 ForwardIterator vertices_end,
157 void make_subgame_threads(
const ParityGame &game,
183 void shuffle(
const std::vector<verti> &perm);
202 bool preserve_parity =
true );
229 void read_pbes(
const std::string &file_path,
verti *goal_vertex = 0,
231 const std::string &rewrite_strategy =
"jitty" );
245 std::ostream &os = std::cerr)
const;
269 template<
class StrategyT>
295 const std::string &rewrite_strategy =
"jitty" );
std::size_t verti
type used to number vertices
player_t opponent(const player_t p)
bool operator==(const ParityGameVertex &a, const ParityGameVertex &b)
void swap(ParityGame &a, ParityGame &b)
bool operator!=(const ParityGameVertex &a, const ParityGameVertex &b)
priority_t priority(verti v) const
verti cardinality(int p) const
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
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
void assign(const ParityGame &game)
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)
void write_dot(std::ostream &os) const
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)
ParityGameVertex * vertex_
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
void make_random(verti V, unsigned clustersize, unsigned outdeg, StaticGraph::EdgeDirection edge_dir, int d)
std::vector< verti > Strategy
const verti * const_iterator
parameterized boolean equation system
Standard exception class for reporting runtime errors.
Exception classes for use in libraries and tools.
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
player_t player
the vertex owner (i.e. next player to move)
priority_t priority
the priority of the vertex between 0 and d (exclusive).