work around gcc-snapshot warnings about dangling references
* spot/twaalgos/game.hh, spot/twaalgos/game.cc (get_state_players, get_strategy, get_state_winners): Take argument by reference, not copy. * spot/twaalgos/synthesis.cc, spot/twaalgos/mealy_machine.cc: Replace auto by actual type for readability.
This commit is contained in:
parent
2666072867
commit
5969aa4925
4 changed files with 31 additions and 16 deletions
|
|
@ -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<region_t>
|
||||
("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<region_t>
|
||||
("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_t>("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<region_t>("state-winner");
|
||||
if (!winners)
|
||||
|
|
|
|||
|
|
@ -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);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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.
|
||||
|
|
@ -3849,7 +3849,7 @@ namespace spot
|
|||
|
||||
// 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");
|
||||
|
||||
|
|
@ -3989,9 +3989,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)
|
||||
|
|
|
|||
|
|
@ -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.
|
||||
|
|
@ -137,12 +137,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()])
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue