diff --git a/spot/twaalgos/game.cc b/spot/twaalgos/game.cc index df259b84a..17f94a7e4 100644 --- a/spot/twaalgos/game.cc +++ b/spot/twaalgos/game.cc @@ -1056,7 +1056,18 @@ namespace spot (*owners)[state] = owner; } - const region_t& get_state_players(const_twa_graph_ptr arena) + const region_t& get_state_players(const const_twa_graph_ptr& arena) + { + region_t *owners = arena->get_named_prop + ("state-player"); + if (!owners) + throw std::runtime_error + ("get_state_players(): state-player property not defined, not a game?"); + + return *owners; + } + + const region_t& get_state_players(twa_graph_ptr& arena) { region_t *owners = arena->get_named_prop ("state-player"); @@ -1081,7 +1092,7 @@ namespace spot } - const strategy_t& get_strategy(const_twa_graph_ptr arena) + const strategy_t& get_strategy(const const_twa_graph_ptr& arena) { auto strat_ptr = arena->get_named_prop("strategy"); if (!strat_ptr) @@ -1174,7 +1185,7 @@ namespace spot (*winners)[state] = winner; } - const region_t& get_state_winners(const_twa_graph_ptr arena) + const region_t& get_state_winners(const const_twa_graph_ptr& arena) { region_t *winners = arena->get_named_prop("state-winner"); if (!winners) diff --git a/spot/twaalgos/game.hh b/spot/twaalgos/game.hh index df5d27439..dbaccce75 100644 --- a/spot/twaalgos/game.hh +++ b/spot/twaalgos/game.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2017-2022 Laboratoire de Recherche et Développement +// Copyright (C) 2017-2023 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -163,14 +163,18 @@ namespace spot /// \ingroup games /// \brief Get the owner of all states + ///@{ SPOT_API - const region_t& get_state_players(const_twa_graph_ptr arena); + const region_t& get_state_players(const const_twa_graph_ptr& arena); + SPOT_API + const region_t& get_state_players(twa_graph_ptr& arena); + ///@} /// \ingroup games /// \brief Get or set the strategy /// @{ SPOT_API - const strategy_t& get_strategy(const_twa_graph_ptr arena); + const strategy_t& get_strategy(const const_twa_graph_ptr& arena); SPOT_API void set_strategy(twa_graph_ptr arena, const strategy_t& strat); SPOT_API @@ -214,5 +218,5 @@ namespace spot /// \ingroup games /// \brief Get the winner of all states SPOT_API - const region_t& get_state_winners(const_twa_graph_ptr arena); + const region_t& get_state_winners(const const_twa_graph_ptr& arena); } diff --git a/spot/twaalgos/mealy_machine.cc b/spot/twaalgos/mealy_machine.cc index e2b1523de..25bab05a9 100644 --- a/spot/twaalgos/mealy_machine.cc +++ b/spot/twaalgos/mealy_machine.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2021, 2022 Laboratoire de Recherche et Développement +// Copyright (C) 2021, 2022, 2023 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -3995,7 +3995,7 @@ namespace // 0 -> "Env" next is input props // 1 -> "Player" next is output prop - const auto& spref = get_state_players(mmw); + const region_t& spref = get_state_players(mmw); assert((spref.size() == mmw->num_states()) && "Inconsistent state players"); @@ -4146,9 +4146,9 @@ namespace spot const unsigned initl = left->get_init_state_number(); const unsigned initr = right->get_init_state_number(); - auto& spr = get_state_players(right); + const region_t& spr = get_state_players(right); #ifndef NDEBUG - auto& spl = get_state_players(left); + const region_t& spl = get_state_players(left); // todo auto check_out = [](const const_twa_graph_ptr& aut, const auto& sp) diff --git a/spot/twaalgos/synthesis.cc b/spot/twaalgos/synthesis.cc index 4e38efd5b..aef11d27b 100644 --- a/spot/twaalgos/synthesis.cc +++ b/spot/twaalgos/synthesis.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2020-2022 Laboratoire de Recherche et +// Copyright (C) 2020-2023 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -138,12 +138,12 @@ namespace{ // Note, this only deals with deterministic strategies // Note, assumes that env starts playing twa_graph_ptr - apply_strategy(const twa_graph_ptr& arena, + apply_strategy(const const_twa_graph_ptr& arena, bool unsplit, bool keep_acc) { - const auto& win = get_state_winners(arena); - const auto& strat = get_strategy(arena); - const auto& sp = get_state_players(arena); + const region_t& win = get_state_winners(arena); + const strategy_t& strat = get_strategy(arena); + const region_t& sp = get_state_players(arena); auto outs = get_synthesis_outputs(arena); if (!win[arena->get_init_state_number()]) @@ -1955,7 +1955,7 @@ namespace spot throw std::runtime_error("arena is null."); auto& arena_r = *arena; - const auto& sp = get_state_players(arena); + const region_t& sp = get_state_players(arena); bdd all_ap = arena->ap_vars(); if (std::find_if(arena->ap().cbegin(), arena->ap().cend(),