spot  2.7.1
Public Types | Public Member Functions | List of all members
spot::parity_game Class Reference
Collaboration diagram for spot::parity_game:

Public Types

typedef std::unordered_set< unsigned > region_t
 
typedef std::unordered_map< unsigned, unsigned > strategy_t
 

Public Member Functions

 parity_game (const twa_graph_ptr &arena, const std::vector< bool > &owner)
 
unsigned num_states () const
 
unsigned get_init_state_number () const
 
internal::state_out< const twa_graph::graph_tout (unsigned src) const
 
internal::state_out< const twa_graph::graph_tout (unsigned src)
 
bool owner (unsigned src) const
 
unsigned max_parity () const
 
void print (std::ostream &os)
 Print the parity game in PGSolver's format. More...
 
void solve (region_t(&w)[2], strategy_t(&s)[2]) const
 

Constructor & Destructor Documentation

◆ parity_game()

spot::parity_game::parity_game ( const twa_graph_ptr &  arena,
const std::vector< bool > &  owner 
)

parity_game provides an interface to manipulate a colorized parity automaton as a parity game, including methods to solve the game. The input automaton (arena) should be colorized and have a max-odd parity acceptance condition.

Parameters
arenathe underlying parity automaton
ownera vector of Booleans indicating the owner of each state: true stands for Player 1, false stands for Player 0.

Member Function Documentation

◆ print()

void spot::parity_game::print ( std::ostream &  os)

Print the parity game in PGSolver's format.

◆ solve()

void spot::parity_game::solve ( region_t(&)  w[2],
strategy_t(&)  s[2] 
) const

Compute the winning strategy and winning region of this game for player 1 using Zielonka's recursive algorithm.

@article{ zielonka.98.tcs
  title = "Infinite games on finitely coloured graphs with applications to
  automata on infinite trees",
  journal = "Theoretical Computer Science",
  volume = "200",
  number = "1",
  pages = "135 - 183",
  year = "1998",
  author = "Wieslaw Zielonka",
}

The documentation for this class was generated from the following file:

Please direct any question, comment, or bug report to the Spot mailing list at spot@lrde.epita.fr.
Generated on Fri Feb 27 2015 10:00:07 for spot by doxygen 1.8.13