smg vi methods now return all choice values

src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp

@@ -48,6 +48,7 @@ namespace storm {
                     viHelper.getChoiceValues(env, x, constrainedChoiceValues);
                 }
                 viHelper.fillResultVector(x, relevantStates, psiStates);
+                viHelper.fillChoiceValuesVector(constrainedChoiceValues, relevantStates, transitionMatrix.getRowGroupIndices());
 
                 if (produceScheduler) {
                     scheduler = std::make_unique<storm::storage::Scheduler<ValueType>>(expandScheduler(viHelper.extractScheduler(), psiStates, ~phiStates));
@@ -86,6 +87,9 @@ namespace storm {
                 for (auto& element : result.values) {
                     element = storm::utility::one<ValueType>() - element;
                 }
+                for (auto& element : result.choiceValues) {
+                    element = storm::utility::one<ValueType>() - element;
+                }
                 return result;
             }
 
@@ -120,6 +124,7 @@ namespace storm {
 
                 // Relevant states are safe states - the psiStates.
                 storm::storage::BitVector relevantStates = psiStates;
+                STORM_LOG_DEBUG(relevantStates);
 
                 // Initialize the solution vector.
                 std::vector<ValueType> x = std::vector<ValueType>(relevantStates.getNumberOfSetBits(), storm::utility::one<ValueType>());
@@ -149,9 +154,11 @@ namespace storm {
 
                     }*/
                 }
+                viHelper.fillChoiceValuesVector(constrainedChoiceValues, relevantStates, transitionMatrix.getRowGroupIndices());
 
                 viHelper.fillResultVector(x, relevantStates);
-
+                viHelper.fillChoiceValuesVector(constrainedChoiceValues, relevantStates, transitionMatrix.getRowGroupIndices());
+                STORM_LOG_DEBUG(x);
                 return SMGSparseModelCheckingHelperReturnType<ValueType>(std::move(x), std::move(relevantStates), std::move(scheduler), std::move(constrainedChoiceValues));
             }
 

src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.cpp

@@ -73,6 +73,21 @@ namespace storm {
                     result = filledVector;
                 }
 
+                template <typename ValueType>
+                void BoundedGloballyGameViHelper<ValueType>::fillChoiceValuesVector(std::vector<ValueType>& choiceValues, storm::storage::BitVector psiStates, std::vector<storm::storage::SparseMatrix<double>::index_type> rowGroupIndices) {
+                    std::vector<ValueType> allChoices = std::vector<ValueType>(rowGroupIndices.at(rowGroupIndices.size() - 1), storm::utility::zero<ValueType>());
+                    auto choice_it = choiceValues.begin();
+                    for(uint state = 0; state < rowGroupIndices.size() - 1; state++) {
+                        uint rowGroupSize = rowGroupIndices[state + 1] - rowGroupIndices[state];
+                        if (psiStates.get(state)) {
+                            for(uint choice = 0; choice < rowGroupSize; choice++, choice_it++) {
+                                allChoices.at(rowGroupIndices.at(state) + choice) = *choice_it;
+                            }
+                        }
+                    }
+                    choiceValues = allChoices;
+                }
+
                 template <typename ValueType>
                 void BoundedGloballyGameViHelper<ValueType>::setProduceScheduler(bool value) {
                     _produceScheduler = value;

src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.h

@@ -30,6 +30,11 @@ namespace storm {
                      */
                     void fillResultVector(std::vector<ValueType>& result, storm::storage::BitVector psiStates);
 
+                    /*!
+                     * Fills the choice values vector to the original size with zeros for ~psiState choices.
+                     */
+                    void fillChoiceValuesVector(std::vector<ValueType>& choiceValues, storm::storage::BitVector psiStates, std::vector<storm::storage::SparseMatrix<double>::index_type> rowGroupIndices);
+
                     /*!
                      * Sets whether an optimal scheduler shall be constructed during the computation
                      */

src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp

@@ -149,6 +149,21 @@ namespace storm {
                     result = filledVector;
                 }
 
+                template <typename ValueType>
+                void GameViHelper<ValueType>::fillChoiceValuesVector(std::vector<ValueType>& choiceValues, storm::storage::BitVector psiStates, std::vector<storm::storage::SparseMatrix<double>::index_type> rowGroupIndices) {
+                    std::vector<ValueType> allChoices = std::vector<ValueType>(rowGroupIndices.at(rowGroupIndices.size() - 1), storm::utility::zero<ValueType>());
+                    auto choice_it = choiceValues.begin();
+                    for(uint state = 0; state < rowGroupIndices.size() - 1; state++) {
+                        uint rowGroupSize = rowGroupIndices[state + 1] - rowGroupIndices[state];
+                        if (psiStates.get(state)) {
+                            for(uint choice = 0; choice < rowGroupSize; choice++, choice_it++) {
+                                allChoices.at(rowGroupIndices.at(state) + choice) = *choice_it;
+                            }
+                        }
+                    }
+                    choiceValues = allChoices;
+                }
+
                 template <typename ValueType>
                 void GameViHelper<ValueType>::setProduceScheduler(bool value) {
                     _produceScheduler = value;

src/storm/modelchecker/rpatl/helper/internal/GameViHelper.h

@@ -30,6 +30,11 @@ namespace storm {
                      */
                     void fillResultVector(std::vector<ValueType>& result, storm::storage::BitVector relevantStates, storm::storage::BitVector psiStates);
 
+                    /*!
+                     * Fills the choice values vector to the original size with zeros for ~psiState choices.
+                     */
+                    void fillChoiceValuesVector(std::vector<ValueType>& choiceValues, storm::storage::BitVector psiStates, std::vector<storm::storage::SparseMatrix<double>::index_type> rowGroupIndices);
+
                     /*!
                      * Sets whether an optimal scheduler shall be constructed during the computation
                      */