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
d16183c053
commit
bdaa31ef21
4 changed files with 32 additions and 17 deletions
|
|
@ -1056,7 +1056,18 @@ namespace spot
|
||||||
(*owners)[state] = owner;
|
(*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>
|
region_t *owners = arena->get_named_prop<region_t>
|
||||||
("state-player");
|
("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");
|
auto strat_ptr = arena->get_named_prop<strategy_t>("strategy");
|
||||||
if (!strat_ptr)
|
if (!strat_ptr)
|
||||||
|
|
@ -1174,7 +1185,7 @@ namespace spot
|
||||||
(*winners)[state] = winner;
|
(*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");
|
region_t *winners = arena->get_named_prop<region_t>("state-winner");
|
||||||
if (!winners)
|
if (!winners)
|
||||||
|
|
|
||||||
|
|
@ -1,5 +1,5 @@
|
||||||
// -*- coding: utf-8 -*-
|
// -*- 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).
|
// de l'Epita (LRDE).
|
||||||
//
|
//
|
||||||
// This file is part of Spot, a model checking library.
|
// This file is part of Spot, a model checking library.
|
||||||
|
|
@ -163,14 +163,18 @@ namespace spot
|
||||||
|
|
||||||
/// \ingroup games
|
/// \ingroup games
|
||||||
/// \brief Get the owner of all states
|
/// \brief Get the owner of all states
|
||||||
|
///@{
|
||||||
SPOT_API
|
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
|
/// \ingroup games
|
||||||
/// \brief Get or set the strategy
|
/// \brief Get or set the strategy
|
||||||
/// @{
|
/// @{
|
||||||
SPOT_API
|
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
|
SPOT_API
|
||||||
void set_strategy(twa_graph_ptr arena, const strategy_t& strat);
|
void set_strategy(twa_graph_ptr arena, const strategy_t& strat);
|
||||||
SPOT_API
|
SPOT_API
|
||||||
|
|
@ -214,5 +218,5 @@ namespace spot
|
||||||
/// \ingroup games
|
/// \ingroup games
|
||||||
/// \brief Get the winner of all states
|
/// \brief Get the winner of all states
|
||||||
SPOT_API
|
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 -*-
|
// -*- 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).
|
// de l'Epita (LRDE).
|
||||||
//
|
//
|
||||||
// This file is part of Spot, a model checking library.
|
// This file is part of Spot, a model checking library.
|
||||||
|
|
@ -3995,7 +3995,7 @@ namespace
|
||||||
|
|
||||||
// 0 -> "Env" next is input props
|
// 0 -> "Env" next is input props
|
||||||
// 1 -> "Player" next is output prop
|
// 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())
|
assert((spref.size() == mmw->num_states())
|
||||||
&& "Inconsistent state players");
|
&& "Inconsistent state players");
|
||||||
|
|
||||||
|
|
@ -4146,9 +4146,9 @@ namespace spot
|
||||||
const unsigned initl = left->get_init_state_number();
|
const unsigned initl = left->get_init_state_number();
|
||||||
const unsigned initr = right->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
|
#ifndef NDEBUG
|
||||||
auto& spl = get_state_players(left);
|
const region_t& spl = get_state_players(left);
|
||||||
// todo
|
// todo
|
||||||
auto check_out = [](const const_twa_graph_ptr& aut,
|
auto check_out = [](const const_twa_graph_ptr& aut,
|
||||||
const auto& sp)
|
const auto& sp)
|
||||||
|
|
|
||||||
|
|
@ -1,5 +1,5 @@
|
||||||
// -*- coding: utf-8 -*-
|
// -*- 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).
|
// Développement de l'Epita (LRDE).
|
||||||
//
|
//
|
||||||
// This file is part of Spot, a model checking library.
|
// This file is part of Spot, a model checking library.
|
||||||
|
|
@ -138,12 +138,12 @@ namespace{
|
||||||
// Note, this only deals with deterministic strategies
|
// Note, this only deals with deterministic strategies
|
||||||
// Note, assumes that env starts playing
|
// Note, assumes that env starts playing
|
||||||
twa_graph_ptr
|
twa_graph_ptr
|
||||||
apply_strategy(const twa_graph_ptr& arena,
|
apply_strategy(const const_twa_graph_ptr& arena,
|
||||||
bool unsplit, bool keep_acc)
|
bool unsplit, bool keep_acc)
|
||||||
{
|
{
|
||||||
const auto& win = get_state_winners(arena);
|
const region_t& win = get_state_winners(arena);
|
||||||
const auto& strat = get_strategy(arena);
|
const strategy_t& strat = get_strategy(arena);
|
||||||
const auto& sp = get_state_players(arena);
|
const region_t& sp = get_state_players(arena);
|
||||||
auto outs = get_synthesis_outputs(arena);
|
auto outs = get_synthesis_outputs(arena);
|
||||||
|
|
||||||
if (!win[arena->get_init_state_number()])
|
if (!win[arena->get_init_state_number()])
|
||||||
|
|
@ -1955,7 +1955,7 @@ namespace spot
|
||||||
throw std::runtime_error("arena is null.");
|
throw std::runtime_error("arena is null.");
|
||||||
auto& arena_r = *arena;
|
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();
|
bdd all_ap = arena->ap_vars();
|
||||||
|
|
||||||
if (std::find_if(arena->ap().cbegin(), arena->ap().cend(),
|
if (std::find_if(arena->ap().cbegin(), arena->ap().cend(),
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue