From e8f5865fb8c80251882442a714ab0658f7cdf691 Mon Sep 17 00:00:00 2001
From: philipp <philipp@lrde.epita.fr>
Date: Mon, 12 Jul 2021 08:09:11 +0200
Subject: [PATCH] Add setter and getter for synthesis-outputs

* spot/twaalgos/game.cc, spot/twaalgos/game.hh: Here
---
 spot/twaalgos/game.cc | 19 +++++++++++++++++--
 spot/twaalgos/game.hh |  7 +++++++
 2 files changed, 24 insertions(+), 2 deletions(-)

diff --git a/spot/twaalgos/game.cc b/spot/twaalgos/game.cc
index 1f47da445..2c6fafdc7 100644
--- a/spot/twaalgos/game.cc
+++ b/spot/twaalgos/game.cc
@@ -809,9 +809,9 @@ namespace spot
                          bool first_player, bool complete0)
   {
     auto um = arena->acc().unsat_mark();
-    if (!um.first)
+    if (!um.first && complete0)
       throw std::runtime_error
-        ("alternate_players(): game winning condition is a tautology");
+        ("alternate_players(): Can not complete monitor!");
 
     unsigned sink_env = 0;
     unsigned sink_con = 0;
@@ -957,6 +957,21 @@ namespace spot
     return (*owners)[state] ? 1 : 0;
   }
 
+  void set_synthesis_outputs(const twa_graph_ptr& arena, const bdd& outs)
+  {
+    arena->set_named_prop<bdd>("synthesis-outputs", new bdd(outs));
+  }
+
+  bdd get_synthesis_outputs(const const_twa_graph_ptr& arena)
+  {
+    if (auto outptr = arena->get_named_prop<bdd>("synthesis-outputs"))
+      return *outptr;
+    else
+      throw std::runtime_error
+          ("get_synthesis_outputs(): synthesis-outputs not defined");
+  }
+
+
   bool solve_safety_game(twa_graph_ptr game)
   {
     if (!game->acc().is_t())
diff --git a/spot/twaalgos/game.hh b/spot/twaalgos/game.hh
index 58adfeb14..fd079f733 100644
--- a/spot/twaalgos/game.hh
+++ b/spot/twaalgos/game.hh
@@ -118,4 +118,11 @@ namespace spot
   /// \brief Get the owner of a state.
   SPOT_API
   unsigned get_state_player(const_twa_graph_ptr arena, unsigned state);
+
+  /// \brief Set all synthesis outputs as a conjunction
+  SPOT_API
+  void set_synthesis_outputs(const twa_graph_ptr& arena, const bdd& outs);
+
+  SPOT_API
+  bdd get_synthesis_outputs(const const_twa_graph_ptr& arena);
 }