diff --git a/spot/misc/game.cc b/spot/misc/game.cc index f2b6179d7..c1f6107cd 100644 --- a/spot/misc/game.cc +++ b/spot/misc/game.cc @@ -935,13 +935,13 @@ namespace spot const std::vector& get_state_players(const_twa_graph_ptr arena) { - std::vector *onwers = arena->get_named_prop> + std::vector *owners = arena->get_named_prop> ("state-player"); - if (!onwers) + if (!owners) throw std::runtime_error ("get_state_players(): state-player property not defined, not a game"); - return *onwers; + return *owners; } unsigned get_state_player(const_twa_graph_ptr arena, unsigned state) @@ -949,12 +949,63 @@ namespace spot if (state >= arena->num_states()) throw std::runtime_error("get_state_player(): invalid state number"); - std::vector* onwers = arena->get_named_prop> + std::vector* owners = arena->get_named_prop> ("state-player"); - if (!onwers) + if (!owners) throw std::runtime_error ("get_state_player(): state-player property not defined, not a game"); - return (*onwers)[state] ? 1 : 0; + return (*owners)[state] ? 1 : 0; + } + + bool solve_reachability_game(twa_graph_ptr game) + { + auto owners = get_state_players(game); + + auto winners = new region_t(game->num_states(), true); + game->set_named_prop("state-winner", winners); + auto strategy = new strategy_t(game->num_states(), 0); + game->set_named_prop("strategy", strategy); + + std::vector seen(game->num_states(), false); + std::vector todo; + todo.reserve(game->num_states()); + + auto& g = game->get_graph(); + todo.push_back(game->get_init_state_number()); + + while (!todo.empty()) + { + unsigned cur = todo.back(); + auto edges = game->out(cur); + + if (!seen[cur]) + { + for (const auto& e : edges) + todo.push_back(e.dst); + seen[cur] = true; + } + else + { + todo.pop_back(); + bool player = owners[cur]; + + auto it = std::find_if(edges.begin(), edges.end(), + [&winners, player](auto& e) + { + return (*winners)[e.dst] == player; + }); + + if (it != edges.end()) + { + (*strategy)[cur] = g.index_of_edge(*it); + (*winners)[cur] = player; + } + else + (*winners)[cur] = !player; + } + } + + return (*winners)[game->get_init_state_number()]; } } diff --git a/spot/misc/game.hh b/spot/misc/game.hh index 96d563c05..9e125de53 100644 --- a/spot/misc/game.hh +++ b/spot/misc/game.hh @@ -100,4 +100,8 @@ namespace spot /// \brief Get the owner of a state. SPOT_API unsigned get_state_player(const_twa_graph_ptr arena, unsigned state); + + /// \brief Solve a reachability game. + SPOT_API + bool solve_reachability_game(twa_graph_ptr game); }