fetch choice values from until vi computation

- added an SMGModelCheckingHelperReturnType

src/storm/modelchecker/prctl/helper/MDPModelCheckingHelperReturnType.h

@@ -29,9 +29,6 @@ namespace storm {
                 // The values computed for the states.
                 std::vector<ValueType> values;
 
-                // The values computed for the available choices.
-                std::vector<ValueType> choiceValues;
-
                 // A scheduler, if it was computed.
                 std::unique_ptr<storm::storage::Scheduler<ValueType>> scheduler;
             };

src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp

@@ -72,6 +72,8 @@ namespace storm {
 
             statesOfCoalition = this->getModel().computeStatesOfCoalition(gameFormula.getCoalition());
 
+            STORM_LOG_DEBUG("\n" << this->getModel().getTransitionMatrix());
+
             if (subFormula.isRewardOperatorFormula()) {
                 return this->checkRewardOperatorFormula(solverEnv, checkTask.substituteFormula(subFormula.asRewardOperatorFormula()));
             } else if (subFormula.isLongRunAverageOperatorFormula()) {
@@ -148,12 +150,9 @@ namespace storm {
             ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult();
 
             auto ret = storm::modelchecker::helper::SparseSmgRpatlHelper<ValueType>::computeUntilProbabilities(env, storm::solver::SolveGoal<ValueType>(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), statesOfCoalition, checkTask.isProduceSchedulersSet(), checkTask.getHint());
-            for(auto const& x : ret.values) {
-                STORM_LOG_DEBUG("v: " << x);
-            }
             std::unique_ptr<CheckResult> result(new ExplicitQuantitativeCheckResult<ValueType>(std::move(ret.values)));
             if(checkTask.isShieldingTask()) {
-                result->asExplicitQuantitativeCheckResult<ValueType>().setScheduler(std::make_unique<storm::storage::Scheduler<ValueType>>(tempest::shields::createShield<ValueType>(this->getModel().getTransitionMatrix().getRowGroupIndices(), {}, checkTask.getShieldingExpression(), statesOfCoalition)));
+                result->asExplicitQuantitativeCheckResult<ValueType>().setScheduler(std::make_unique<storm::storage::Scheduler<ValueType>>(tempest::shields::createShield<ValueType>(this->getModel().getTransitionMatrix().getRowGroupIndices(), std::move(ret.choiceValues), checkTask.getShieldingExpression(), std::move(ret.relevantStates), statesOfCoalition)));
             } else if (checkTask.isProduceSchedulersSet() && ret.scheduler) {
                 result->asExplicitQuantitativeCheckResult<ValueType>().setScheduler(std::move(ret.scheduler));
             }
@@ -215,7 +214,7 @@ namespace storm {
 
             std::unique_ptr<CheckResult> result(new ExplicitQuantitativeCheckResult<ValueType>(std::move(values)));
             if(checkTask.isShieldingTask()) {
-                result->asExplicitQuantitativeCheckResult<ValueType>().setScheduler(std::make_unique<storm::storage::Scheduler<ValueType>>(tempest::shields::createShield<ValueType>(this->getModel().getTransitionMatrix().getRowGroupIndices(), {}, checkTask.getShieldingExpression(), coalitionStates)));
+                //result->asExplicitQuantitativeCheckResult<ValueType>().setScheduler(std::make_unique<storm::storage::Scheduler<ValueType>>(tempest::shields::createShield<ValueType>(this->getModel().getTransitionMatrix().getRowGroupIndices(), {}, checkTask.getShieldingExpression(), coalitionStates)));
             } else if (checkTask.isProduceSchedulersSet()) {
                 result->asExplicitQuantitativeCheckResult<ValueType>().setScheduler(std::make_unique<storm::storage::Scheduler<ValueType>>(helper.extractScheduler()));
             }

src/storm/modelchecker/rpatl/helper/SMGModelCheckingHelperReturnType.h

@@ -0,0 +1,43 @@
+#pragma once
+
+#include <vector>
+#include <memory>
+#include "storm/storage/Scheduler.h"
+
+namespace storm {
+    namespace storage {
+        class BitVector;
+    }
+
+    namespace modelchecker {
+        namespace helper {
+            template<typename ValueType>
+            struct SMGSparseModelCheckingHelperReturnType {
+
+                SMGSparseModelCheckingHelperReturnType(SMGSparseModelCheckingHelperReturnType const&) = delete;
+                SMGSparseModelCheckingHelperReturnType(SMGSparseModelCheckingHelperReturnType&&) = default;
+
+                SMGSparseModelCheckingHelperReturnType(std::vector<ValueType>&& values, storm::storage::BitVector& relevantStates, std::unique_ptr<storm::storage::Scheduler<ValueType>>&& scheduler = nullptr, std::vector<ValueType>&& choiceValues = nullptr) : values(std::move(values)), relevantStates(relevantStates), scheduler(std::move(scheduler)), choiceValues(std::move(choiceValues)) {
+                    // Intentionally left empty.
+                }
+
+                virtual ~SMGSparseModelCheckingHelperReturnType() {
+                    // Intentionally left empty.
+                }
+
+                // The values computed for the states.
+                std::vector<ValueType> values;
+
+                // The relevant states for which choice values have been computed.
+                storm::storage::BitVector relevantStates;
+
+                // A scheduler, if it was computed.
+                std::unique_ptr<storm::storage::Scheduler<ValueType>> scheduler;
+
+                // The values computed for the available choices.
+                std::vector<ValueType> choiceValues;
+            };
+        }
+
+    }
+}

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

@@ -14,7 +14,7 @@ namespace storm {
         namespace helper {
 
             template<typename ValueType>
-            MDPSparseModelCheckingHelperReturnType<ValueType> SparseSmgRpatlHelper<ValueType>::computeUntilProbabilities(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint) {
+            SMGSparseModelCheckingHelperReturnType<ValueType> SparseSmgRpatlHelper<ValueType>::computeUntilProbabilities(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint) {
                 // TODO add Kwiatkowska original reference
                 // TODO FIX solver min max mess
 
@@ -28,6 +28,7 @@ namespace storm {
                 storm::storage::BitVector relevantStates = phiStates & ~psiStates;
 
                 std::vector<ValueType> b = transitionMatrix.getConstrainedRowGroupSumVector(relevantStates, psiStates);
+                std::vector<ValueType> constrainedChoiceValues = std::vector<ValueType>(b.size(), storm::utility::zero<ValueType>());
 
                 // Reduce the matrix to relevant states
                 storm::storage::SparseMatrix<ValueType> submatrix = transitionMatrix.getSubmatrix(true, relevantStates, relevantStates, false);
@@ -43,12 +44,15 @@ namespace storm {
                 }
 
                 viHelper.performValueIteration(env, x, b, goal.direction());
+                if(true) {
+                    viHelper.getChoiceValues(env, x, constrainedChoiceValues);
+                }
                 viHelper.fillResultVector(x, relevantStates, psiStates);
 
                 if (produceScheduler) {
                     scheduler = std::make_unique<storm::storage::Scheduler<ValueType>>(expandScheduler(viHelper.extractScheduler(), psiStates, ~phiStates));
                 }
-                return MDPSparseModelCheckingHelperReturnType<ValueType>(std::move(x), std::move(scheduler));
+                return SMGSparseModelCheckingHelperReturnType<ValueType>(std::move(x), relevantStates, std::move(scheduler), std::move(constrainedChoiceValues));
             }
 
             template<typename ValueType>

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

@@ -10,6 +10,7 @@
 #include "storm/solver/SolveGoal.h"
 
 #include "storm/modelchecker/prctl/helper/MDPModelCheckingHelperReturnType.h"
+#include "storm/modelchecker/rpatl/helper/SMGModelCheckingHelperReturnType.h"
 
 namespace storm {
 
@@ -36,13 +37,14 @@ namespace storm {
             public:
                 // TODO should probably be renamed in the future:
 
-                static MDPSparseModelCheckingHelperReturnType<ValueType> computeUntilProbabilities(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint = ModelCheckerHint());
+                static SMGSparseModelCheckingHelperReturnType<ValueType> computeUntilProbabilities(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint = ModelCheckerHint());
                 static MDPSparseModelCheckingHelperReturnType<ValueType> computeGloballyProbabilities(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint = ModelCheckerHint());
                 static MDPSparseModelCheckingHelperReturnType<ValueType> computeNextProbabilities(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint);
                 static MDPSparseModelCheckingHelperReturnType<ValueType> computeBoundedGloballyProbabilities(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint, uint64_t lowerBound, uint64_t upperBound);
 
             private:
                 static storm::storage::Scheduler<ValueType> expandScheduler(storm::storage::Scheduler<ValueType> scheduler, storm::storage::BitVector psiStates, storm::storage::BitVector notPhiStates);
+                static void expandChoiceValues(std::vector<uint_fast64_t> const& rowGroupIndices, storm::storage::BitVector const& relevantStates, std::vector<ValueType> const& constrainedChoiceValues, std::vector<ValueType>& choiceValues);
 
             };
         }

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

@@ -134,8 +134,7 @@ namespace storm {
                 }
 
                 template <typename ValueType>
-                void GameViHelper<ValueType>::fillResultVector(std::vector<ValueType>& result, storm::storage::BitVector relevantStates, storm::storage::BitVector psiStates)
-                {
+                void GameViHelper<ValueType>::fillResultVector(std::vector<ValueType>& result, storm::storage::BitVector relevantStates, storm::storage::BitVector psiStates) {
                     std::vector<ValueType> filledVector = std::vector<ValueType>(relevantStates.size(), storm::utility::zero<ValueType>());
                     uint bitIndex = 0;
                     for(uint i = 0; i < filledVector.size(); i++) {
@@ -184,6 +183,11 @@ namespace storm {
                     return scheduler;
                 }
 
+                template <typename ValueType>
+                void GameViHelper<ValueType>::getChoiceValues(Environment const& env, std::vector<ValueType> const& x, std::vector<ValueType>& choiceValues) {
+                    _multiplier->multiply(env, x, &_b, choiceValues);
+                }
+
                 template <typename ValueType>
                 std::vector<ValueType>& GameViHelper<ValueType>::xNew() {
                     return _x1IsCurrent ? _x1 : _x2;

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

@@ -42,6 +42,7 @@ namespace storm {
 
                     storm::storage::Scheduler<ValueType> extractScheduler() const;
 
+                    void getChoiceValues(Environment const& env, std::vector<ValueType> const& x, std::vector<ValueType>& choiceValues);
                 private:
                     void performIterationStep(Environment const& env, storm::solver::OptimizationDirection const dir, std::vector<uint64_t>* choices = nullptr);