Graph used for backward propagation of winning conditions in parity games.
More...
#include <spot/twaalgos/backprop.hh>
|
| | backprop_graph (bool stop_asap=true) |
| | Construct the backpropagation graph.
|
| |
| int | new_state (bool owner) |
| | Add a new state; owner is true if owned by Player 1.
|
| |
| void | set_name (unsigned state, const std::string &s) |
| | Set the name of the given state.
|
| |
| bool | new_edge (unsigned src, unsigned dst) |
| | Add an edge from src to dst.
|
| |
| bool | freeze_state (unsigned state) |
| | Mark a state as frozen (no more incoming edges).
|
| |
| bool | is_frozen (unsigned state) const |
| | Check if a state is frozen.
|
| |
| bool | is_determined (unsigned state) const |
| | Check if the winner of a state has been determined.
|
| |
| bool | winner (unsigned state) const |
| | Return the winner of a state (true = Player 0).
|
| |
| unsigned | choice (unsigned state) const |
| | Return the chosen successor for a state.
|
| |
| bool | set_winner (unsigned state, bool winner) |
| | Set the winner of a state.
|
| |
| std::ostream & | print_dot (std::ostream &os) const |
| | Print the graph in dot format.
|
| |
| unsigned | num_edges () const |
| | Return the number of edges.
|
| |
Graph used for backward propagation of winning conditions in parity games.
◆ backprop_graph()
| spot::backprop_graph::backprop_graph |
( |
bool |
stop_asap = true | ) |
|
|
inline |
Construct the backpropagation graph.
◆ choice()
| unsigned spot::backprop_graph::choice |
( |
unsigned |
state | ) |
const |
|
inline |
Return the chosen successor for a state.
◆ freeze_state()
| bool spot::backprop_graph::freeze_state |
( |
unsigned |
state | ) |
|
Mark a state as frozen (no more incoming edges).
Once a state is frozen, no more incoming edges can be added. If all successors are won by the other player, then a frozen state can be marked as won by the other player too.
◆ is_determined()
| bool spot::backprop_graph::is_determined |
( |
unsigned |
state | ) |
const |
|
inline |
Check if the winner of a state has been determined.
◆ is_frozen()
| bool spot::backprop_graph::is_frozen |
( |
unsigned |
state | ) |
const |
|
inline |
Check if a state is frozen.
Once a state is frozen, no more incoming edges can be added. If all successors are won by the other player, then a frozen state can be marked as won by the other player too.
◆ new_edge()
| bool spot::backprop_graph::new_edge |
( |
unsigned |
src, |
|
|
unsigned |
dst |
|
) |
| |
Add an edge from src to dst.
◆ new_state()
| int spot::backprop_graph::new_state |
( |
bool |
owner | ) |
|
|
inline |
Add a new state; owner is true if owned by Player 1.
◆ num_edges()
| unsigned spot::backprop_graph::num_edges |
( |
| ) |
const |
|
inline |
Return the number of edges.
◆ print_dot()
| std::ostream & spot::backprop_graph::print_dot |
( |
std::ostream & |
os | ) |
const |
Print the graph in dot format.
◆ set_name()
| void spot::backprop_graph::set_name |
( |
unsigned |
state, |
|
|
const std::string & |
s |
|
) |
| |
|
inline |
Set the name of the given state.
◆ set_winner()
| bool spot::backprop_graph::set_winner |
( |
unsigned |
state, |
|
|
bool |
winner |
|
) |
| |
|
inline |
Set the winner of a state.
◆ winner()
| bool spot::backprop_graph::winner |
( |
unsigned |
state | ) |
const |
|
inline |
Return the winner of a state (true = Player 0).
The documentation for this class was generated from the following file:
