From ae7d4504cda577f1612fbeceb992ee508bf0b5a8 Mon Sep 17 00:00:00 2001
From: Jerome Dubois <jdubois@lrde.epita.fr>
Date: Tue, 15 Sep 2020 14:26:11 +0200
Subject: [PATCH] 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.
---
 python/spot/impl.i     |  1 +
 spot/misc/game.cc      | 56 ++++++++++++++++++++++++++++++++++++++++++
 spot/misc/game.hh      | 18 ++++++++++++++
 tests/python/parity.py | 48 ++++++++++++++++++++++++++++++++++++
 4 files changed, 123 insertions(+)

diff --git a/python/spot/impl.i b/python/spot/impl.i
index 44fe1f480..3604014ab 100644
--- a/python/spot/impl.i
+++ b/python/spot/impl.i
@@ -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>
 
diff --git a/spot/misc/game.cc b/spot/misc/game.cc
index 5751ecd4f..93815069e 100644
--- a/spot/misc/game.cc
+++ b/spot/misc/game.cc
@@ -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;
+  }
 }
diff --git a/spot/misc/game.hh b/spot/misc/game.hh
index 5b133a206..1f3bfd27b 100644
--- a/spot/misc/game.hh
+++ b/spot/misc/game.hh
@@ -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);
 }
diff --git a/tests/python/parity.py b/tests/python/parity.py
index 84a3437aa..96affc116 100644
--- a/tests/python/parity.py
+++ b/tests/python/parity.py
@@ -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()