From a723cfca141b8b600ccfc089a9acdd31ea3e1750 Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@rwth-aachen.de>
Date: Wed, 4 Nov 2015 11:17:59 +0100
Subject: [PATCH] Made sampling for MDPs correct again
Former-commit-id: 7917200f4e75b0e48bdd7faa5957b389ce7aadf1
---
src/modelchecker/region/SamplingModel.cpp | 4 ++++
1 file changed, 4 insertions(+)
diff --git a/src/modelchecker/region/SamplingModel.cpp b/src/modelchecker/region/SamplingModel.cpp
index 9539c2bde..2df9c63fd 100644
--- a/src/modelchecker/region/SamplingModel.cpp
+++ b/src/modelchecker/region/SamplingModel.cpp
@@ -252,6 +252,10 @@ namespace storm {
template<>
void SamplingModel<storm::models::sparse::Mdp<storm::RationalFunction>, double>::invokeSolver(){
std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<double>> solver = storm::solver::configureMinMaxLinearEquationSolver(this->solveGoal, storm::utility::solver::MinMaxLinearEquationSolverFactory<double>(), this->matrixData.matrix);
+ if(!this->solveGoal.minimize()){
+ //The value iteration method is not correct if the value is maximized and the initial x-vector is not <= the actual probability/reward.
+ this->eqSysResult.assign(this->eqSysResult.size(), storm::utility::zero<double>());
+ }
solver->solveEquationSystem(this->eqSysResult, this->vectorData.vector);
}