From b9dc2cd670f8e8eacedfd247a802cd311e5a761a Mon Sep 17 00:00:00 2001
From: Roman Andriushchenko <iandri@fit.vut.cz>
Date: Fri, 29 Nov 2024 15:35:48 +0100
Subject: [PATCH] fix SMG solution value vector

---
 .../src/synthesis/pomdp_family/GameAbstractionSolver.cpp      | 3 ++-
 payntbind/src/synthesis/pomdp_family/GameAbstractionSolver.h  | 4 ++--
 2 files changed, 4 insertions(+), 3 deletions(-)

diff --git a/payntbind/src/synthesis/pomdp_family/GameAbstractionSolver.cpp b/payntbind/src/synthesis/pomdp_family/GameAbstractionSolver.cpp
index 2c62e470..19bb183b 100644
--- a/payntbind/src/synthesis/pomdp_family/GameAbstractionSolver.cpp
+++ b/payntbind/src/synthesis/pomdp_family/GameAbstractionSolver.cpp
@@ -260,8 +260,8 @@ namespace synthesis {
         }
         storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType> const& result_quan = result->asExplicitQuantitativeCheckResult<ValueType>();
         storm::storage::Scheduler<ValueType> const& scheduler = result_quan.getScheduler();
-        this->solution_state_values = result_quan.getValueVector();
 
+        std::fill(this->solution_state_values.begin(),this->solution_state_values.end(),0);
         std::fill(this->solution_state_to_player1_action.begin(),this->solution_state_to_player1_action.end(),this->quotient_num_actions);
         std::fill(this->solution_state_to_quotient_choice.begin(),this->solution_state_to_quotient_choice.end(),this->quotient.getNumberOfChoices());
         std::vector<uint64_t> const& game_row_groups = abstraction.smg->getTransitionMatrix().getRowGroupIndices();
@@ -272,6 +272,7 @@ namespace synthesis {
                 continue;
             }
             auto [state,_] = abstraction.state_to_quotient_state_action[game_state];
+            this->solution_state_values[state] = result_quan[game_state];
             uint64_t game_choice = game_row_groups[game_state]+scheduler.getChoice(game_state).getDeterministicChoice();
             uint64_t player1_action = choice_to_action[abstraction.choice_to_quotient_choice[game_choice]];
             this->solution_state_to_player1_action[state] = player1_action;
diff --git a/payntbind/src/synthesis/pomdp_family/GameAbstractionSolver.h b/payntbind/src/synthesis/pomdp_family/GameAbstractionSolver.h
index 9b812749..d035102b 100644
--- a/payntbind/src/synthesis/pomdp_family/GameAbstractionSolver.h
+++ b/payntbind/src/synthesis/pomdp_family/GameAbstractionSolver.h
@@ -49,9 +49,9 @@ namespace synthesis {
         void solveSg(storm::storage::BitVector const& quotient_choice_mask);
         void solveSmg(storm::storage::BitVector const& quotient_choice_mask);
 
-        /** State values for the solution. */
+        /** For each state, the value of the game. */
         std::vector<double> solution_state_values;
-        /** Solution value of the game. */
+        /** Value of the game in the initial state. */
         double solution_value;
         
         /**