diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp index c02f393d0..ca6e53ea2 100644 --- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp @@ -120,6 +120,8 @@ namespace storm { // Reduce the matrix to relevant states storm::storage::SparseMatrix submatrix = transitionMatrix.getSubmatrix(true, relevantStates, relevantStates, false); + std::vector constrainedChoiceValues = std::vector(submatrix.getRowCount(), storm::utility::zero()); + storm::storage::BitVector clippedStatesOfCoalition(relevantStates.getNumberOfSetBits()); clippedStatesOfCoalition.setClippedStatesOfCoalition(relevantStates, statesOfCoalition); clippedStatesOfCoalition.complement(); @@ -134,17 +136,15 @@ namespace storm { // in case of upperBound = 0 the states which are initially "safe" are filled with ones if(upperBound > 0) { - viHelper.performValueIteration(env, x, goal.direction(), upperBound); + viHelper.performValueIteration(env, x, goal.direction(), upperBound, constrainedChoiceValues); +/* if (produceScheduler) { + scheduler = std::make_unique>(expandScheduler(viHelper.extractScheduler(), relevantStates, ~relevantStates)); + + }*/ } viHelper.fillResultVector(x, relevantStates); - // TODO: i am not sure about that ~psiStates are correct - but I think (~psiStates are unsafe like the ~phiStates before) - // maybe I should create another method for this case - if (produceScheduler) { - scheduler = std::make_unique>(expandScheduler(viHelper.extractScheduler(), relevantStates, ~relevantStates)); - } - STORM_LOG_DEBUG("x = " << x); return MDPSparseModelCheckingHelperReturnType(std::move(x), std::move(scheduler)); diff --git a/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.cpp b/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.cpp index 37a04da9c..9a4db040e 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.cpp @@ -22,7 +22,7 @@ namespace storm { } template - void BoundedGloballyGameViHelper::performValueIteration(Environment const& env, std::vector& x, storm::solver::OptimizationDirection const dir, uint64_t upperBound) { + void BoundedGloballyGameViHelper::performValueIteration(Environment const& env, std::vector& x, storm::solver::OptimizationDirection const dir, uint64_t upperBound, std::vector& constrainedChoiceValues) { prepareSolversAndMultipliers(env); _x = x; @@ -34,6 +34,9 @@ namespace storm { } for (uint64_t iter = 0; iter < upperBound; iter++) { + if(iter == upperBound - 1) { + _multiplier->multiply(env, _x, nullptr, constrainedChoiceValues); + } performIterationStep(env, dir); } @@ -47,7 +50,7 @@ namespace storm { } // multiplyandreducegaussseidel - // Ax + b + // Ax = x' if (choices == nullptr) { _multiplier->multiplyAndReduce(env, dir, _x, nullptr, _x, nullptr, &_statesOfCoalition); } else { diff --git a/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.h b/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.h index c13286e41..d2eb985dc 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.h +++ b/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.h @@ -23,7 +23,7 @@ namespace storm { void prepareSolversAndMultipliers(const Environment& env); - void performValueIteration(Environment const& env, std::vector& x, storm::solver::OptimizationDirection const dir, uint64_t upperBound); + void performValueIteration(Environment const& env, std::vector& x, storm::solver::OptimizationDirection const dir, uint64_t upperBound, std::vector& constrainedChoiceValues); /*! * Fills the result vector to the original size with ones for being psiStates, zeros for being not phiStates