Graph used for backward propagation of winning conditions in parity games.
More...
#include <spot/twaalgos/backprop.hh>
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:
