alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

game: let highlight_strategy work for non-parity games

Browse source 
This is required by an upcoming patch by Jérôme, solving reachability
games.

* spot/misc/game.cc (highlight_strategy): Do not require parity
acceptance.
This commit is contained in:
Alexandre Duret-Lutz 2020-09-24 13:28:29 +02:00
parent 392c1a0ec3
commit 324b0872a4
1 changed files with 22 additions and 18 deletions
Download patch file Download diff file Expand all files Collapse all files

40
spot/misc/game.cc
View file

@ -28,6 +28,19 @@ namespace spot
{ {
namespace namespace
{ {
static const std::vector<bool>*
ensure_game(const const_twa_graph_ptr& arena, const char* fnname)
{
auto owner = arena->get_named_prop<std::vector<bool>>("state-player");
if (!owner)
throw std::runtime_error
(std::string(fnname) + ": automaton should define \"state-player\"");
if (owner->size() != arena->num_states())
throw std::runtime_error
(std::string(fnname) + ": \"state-player\" should have "
"as many states as the automaton");
return owner;
}
static const std::vector<bool>* static const std::vector<bool>*
ensure_parity_game(const const_twa_graph_ptr& arena, const char* fnname) ensure_parity_game(const const_twa_graph_ptr& arena, const char* fnname)
@ -38,26 +51,13 @@ namespace spot
throw std::runtime_error throw std::runtime_error
(std::string(fnname) + (std::string(fnname) +
": arena must have max-odd acceptance condition"); ": arena must have max-odd acceptance condition");
for (const auto& e : arena->edges()) for (const auto& e : arena->edges())
if (!e.acc) if (!e.acc)
throw std::runtime_error throw std::runtime_error
(std::string(fnname) + ": arena must be colorized"); (std::string(fnname) + ": arena must be colorized");
return ensure_game(arena, fnname);
auto owner = arena->get_named_prop<std::vector<bool>>("state-player");
if (!owner)
throw std::runtime_error
(std::string(fnname) + ": automaton should define \"state-player\"");
if (owner->size() != arena->num_states())
throw
(std::string(fnname) + ": \"state-player\" should have "
"as many states as the automaton");
return owner;
} }
// Internal structs // Internal structs
// winning regions for env and player // winning regions for env and player
struct winner_t struct winner_t
@ -869,12 +869,16 @@ namespace spot
int player0_color, int player0_color,
int player1_color) int player1_color)
{ {
auto owner = ensure_parity_game(aut, "highlight_strategy()"); auto owner = ensure_game(aut, "highlight_strategy()");
region_t* w = aut->get_named_prop<region_t>("state-winner"); region_t* w = aut->get_named_prop<region_t>("state-winner");
strategy_t* s = aut->get_named_prop<strategy_t>("strategy"); strategy_t* s = aut->get_named_prop<strategy_t>("strategy");
if (!w || !s) if (!w)
throw std::runtime_error("highlight_strategy(): " throw std::runtime_error
"strategy not available, solve the game first"); ("highlight_strategy(): "
"winning region unavailable, solve the game first");
if (!s)
throw std::runtime_error
("highlight_strategy(): strategy unavailable, solve the game first");
unsigned ns = aut->num_states(); unsigned ns = aut->num_states();
auto* hl_edges = aut->get_or_set_named_prop<std::map<unsigned, unsigned>> auto* hl_edges = aut->get_or_set_named_prop<std::map<unsigned, unsigned>>