Commit ae7d4504 authored by Jérôme Dubois's avatar Jérôme Dubois
Browse files

game: Add set_state_player() and get_state_player()

Fixes #424.

* python/spot/impl.i: Add implicit convertion for vector<bool>.
* spot/misc/game.cc, spot/misc/game.hh: Add set_state_player()
  and get_state_player().
* tests/python/parity.py: Test them.
parent 0339e1fe
......@@ -458,6 +458,7 @@ static void handle_any_exception()
%implicitconv std::vector<spot::formula>;
%implicitconv spot::formula;
%implicitconv std::vector<bool>;
%include <spot/tl/formula.hh>
......
......@@ -349,4 +349,60 @@ namespace spot
return spot::highlight_strategy(aut, winning_strategy[!!player], color);
}
void set_state_players(twa_graph_ptr arena, std::vector<bool> owners)
{
std::vector<bool>* owners_ptr = new std::vector<bool>(owners);
set_state_players(arena, owners_ptr);
}
void set_state_players(twa_graph_ptr arena, std::vector<bool>* owners)
{
if (owners->size() != arena->num_states())
throw std::runtime_error
("set_state_players(): There must be as many owners as states");
arena->set_named_prop<std::vector<bool>>("state-player", owners);
}
void set_state_player(twa_graph_ptr arena, unsigned state, unsigned owner)
{
if (state >= arena->num_states())
throw std::runtime_error("set_state_player(): invalid state number");
std::vector<bool> *owners = arena->get_named_prop<std::vector<bool>>
("state-player");
if (!owners)
{
owners = new std::vector<bool>(arena->num_states(), false);
arena->set_named_prop<std::vector<bool>>("state-player", owners);
}
(*owners)[state] = owner;
}
const std::vector<bool>& get_state_players(const_twa_graph_ptr arena)
{
std::vector<bool> *onwers = arena->get_named_prop<std::vector<bool>>
("state-player");
if (!onwers)
throw std::runtime_error
("get_state_players(): state-player property not defined, not a game");
return *onwers;
}
unsigned get_state_player(const_twa_graph_ptr arena, unsigned state)
{
if (state >= arena->num_states())
throw std::runtime_error("get_state_player(): invalid state number");
std::vector<bool>* onwers = arena->get_named_prop<std::vector<bool>>
("state-player");
if (!onwers)
throw std::runtime_error
("get_state_player(): state-player property not defined, not a game");
return (*onwers)[state] ? 1 : 0;
}
}
......@@ -89,4 +89,22 @@ namespace spot
twa_graph_ptr highlight_strategy(twa_graph_ptr& arena,
const strategy_t& s,
unsigned color);
/// \brief Set the owner for all the states.
SPOT_API
void set_state_players(twa_graph_ptr arena, std::vector<bool> owners);
SPOT_API
void set_state_players(twa_graph_ptr arena, std::vector<bool>* owners);
/// \brief Set the owner of a state.
SPOT_API
void set_state_player(twa_graph_ptr arena, unsigned state, unsigned owner);
/// \brief Get the owner of all the state.
SPOT_API
const std::vector<bool>& get_state_players(const_twa_graph_ptr arena);
/// \brief Get the owner of a state.
SPOT_API
unsigned get_state_player(const_twa_graph_ptr arena, unsigned state);
}
......@@ -101,3 +101,51 @@ properties: deterministic
State: 0
[t] 0
--END--"""
a = spot.automaton("""HOA: v1
States: 3
Start: 0
AP: 1 "a"
acc-name: all
Acceptance: 0 t
properties: trans-labels explicit-labels state-acc deterministic
--BODY--
State: 0
[0] 1
State: 1
[0] 2
State: 2
--END--""")
try:
spot.get_state_players(a)
except RuntimeError as e:
assert "not a game" in str(e)
else:
report_missing_exception()
spot.set_state_player(a, 1, 1)
assert spot.get_state_players(a) == (False, True, False)
assert spot.get_state_player(a, 0) == 0
assert spot.get_state_player(a, 1) == 1
try:
spot.set_state_players(a, [True, False, False, False])
except RuntimeError as e:
assert "many owners as states" in str(e)
else:
report_missing_exception()
try:
spot.get_state_player(a, 4)
except RuntimeError as e:
assert "invalid state number" in str(e)
else:
report_missing_exception()
try:
spot.set_state_player(a, 4, 1)
except RuntimeError as e:
assert "invalid state number" in str(e)
else:
report_missing_exception()
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment