diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp index 139165ee3..cffe35987 100644 --- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp @@ -1,4 +1,5 @@ #include +#include #include "SparseSmgRpatlHelper.h" #include "storm/environment/Environment.h" @@ -15,7 +16,6 @@ namespace storm { template SMGSparseModelCheckingHelperReturnType SparseSmgRpatlHelper::computeUntilProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix 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 auto solverEnv = env; solverEnv.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration, false); @@ -40,7 +40,7 @@ namespace storm { if (produceScheduler) { viHelper.setProduceScheduler(true); } - viHelper.performValueIteration(env, x, b, goal.direction()); + viHelper.performValueIteration(env, x, b, goal.direction(), constrainedChoiceValues); if(goal.isShieldingTask()) { viHelper.getChoiceValues(env, x, constrainedChoiceValues); } @@ -172,10 +172,12 @@ namespace storm { } // If the lowerBound = 0, value iteration is done until the upperBound. if(lowerBound == 0) { - viHelper.performValueIterationUpperBound(env, x, b, goal.direction(), upperBound, constrainedChoiceValues); + solverEnv.solver().game().setMaximalNumberOfIterations(upperBound); + viHelper.performValueIteration(solverEnv, x, b, goal.direction(), constrainedChoiceValues); } else { // The lowerBound != 0, the first computation between the given bound steps is done. - viHelper.performValueIterationUpperBound(env, x, b, goal.direction(), upperBound - lowerBound, constrainedChoiceValues); + solverEnv.solver().game().setMaximalNumberOfIterations(upperBound - lowerBound); + viHelper.performValueIteration(solverEnv, x, b, goal.direction(), constrainedChoiceValues); // Initialization of subResult, fill it with the result of the first computation and 1s for the psiStates in full range. std::vector subResult = std::vector(transitionMatrix.getRowGroupCount(), storm::utility::zero()); @@ -199,7 +201,9 @@ namespace storm { b = std::vector(transitionMatrix.getConstrainedRowGroupSumVector(relevantStates, newPsiStates).size(), storm::utility::zero()); // The second computation is done between step 0 and the lowerBound - viHelper.performValueIterationUpperBound(env, subResult, b, goal.direction(), lowerBound, constrainedChoiceValues); + solverEnv.solver().game().setMaximalNumberOfIterations(lowerBound); + viHelper.performValueIteration(solverEnv, subResult, b, goal.direction(), constrainedChoiceValues); + x = subResult; } viHelper.fillChoiceValuesVector(constrainedChoiceValues, relevantStates, transitionMatrix.getRowGroupIndices()); @@ -208,7 +212,11 @@ namespace storm { } storm::utility::vector::setVectorValues(result, relevantStates, x); } - // In bounded-globally formulas we not only to reach a psiState on the path but also want to stay in a set of psiStates in the given step bounds. + // In bounded until and bounded eventually formula the psiStates have probability 1 to satisfy the formula, + // because once reaching a state where psi holds those formulas are satisfied. + // In bounded globally formulas we cannot set those states to 1 because it is possible to leave a set of safe states after reaching a psiState + // and in globally the formula has to hold in every time step (between the bounds). + // e.g. phiState -> phiState -> psiState -> unsafeState if(!computeBoundedGlobally){ storm::utility::vector::setVectorValues(result, psiStates, storm::utility::one()); } diff --git a/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp b/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp index 4ddadc247..5b644e23d 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp @@ -25,13 +25,14 @@ namespace storm { } template - void GameViHelper::performValueIteration(Environment const& env, std::vector& x, std::vector b, storm::solver::OptimizationDirection const dir) { + void GameViHelper::performValueIteration(Environment const& env, std::vector& x, std::vector b, storm::solver::OptimizationDirection const dir, std::vector& constrainedChoiceValues) { prepareSolversAndMultipliers(env); // Get precision for convergence check. ValueType precision = storm::utility::convertNumber(env.solver().game().getPrecision()); uint64_t maxIter = env.solver().game().getMaximalNumberOfIterations(); _b = b; - _x1.assign(_transitionMatrix.getRowGroupCount(), storm::utility::zero()); + //_x1.assign(_transitionMatrix.getRowGroupCount(), storm::utility::zero()); + _x1 = x; _x2 = _x1; if (this->isProduceSchedulerSet()) { @@ -42,17 +43,25 @@ namespace storm { } uint64_t iter = 0; - std::vector result = x; + constrainedChoiceValues = std::vector(b.size(), storm::utility::zero()); + while (iter < maxIter) { - ++iter; + if(iter == maxIter - 1) { + _multiplier->multiply(env, xNew(), &_b, constrainedChoiceValues); + auto rowGroupIndices = this->_transitionMatrix.getRowGroupIndices(); + rowGroupIndices.erase(rowGroupIndices.begin()); + _multiplier->reduce(env, dir, constrainedChoiceValues, rowGroupIndices, xNew()); + break; + } performIterationStep(env, dir); - if (checkConvergence(precision)) { + _multiplier->multiply(env, xNew(), &_b, constrainedChoiceValues); break; } if (storm::utility::resources::isTerminate()) { break; } + ++iter; } x = xNew(); @@ -74,18 +83,11 @@ namespace storm { } else { _multiplier->multiplyAndReduce(env, dir, xOld(), &_b, xNew(), choices, &_statesOfCoalition); } - - // compare applyPointwise - storm::utility::vector::applyPointwise(xOld(), xNew(), xNew(), [&dir] (ValueType const& a, ValueType const& b) -> ValueType { - if(a > b) return a; - else return b; - }); } template bool GameViHelper::checkConvergence(ValueType threshold) const { STORM_LOG_ASSERT(_multiplier, "tried to check for convergence without doing an iteration first."); - // Now check whether the currently produced results are precise enough STORM_LOG_ASSERT(threshold > storm::utility::zero(), "Did not expect a non-positive threshold."); auto x1It = xOld().begin(); @@ -113,43 +115,6 @@ namespace storm { return true; } - template - void GameViHelper::performValueIterationUpperBound(Environment const& env, std::vector& x, std::vector b, storm::solver::OptimizationDirection const dir, uint64_t upperBound, std::vector& constrainedChoiceValues) { - prepareSolversAndMultipliers(env); - _x = x; - _b = b; - - if (this->isProduceSchedulerSet()) { - if (!this->_producedOptimalChoices.is_initialized()) { - this->_producedOptimalChoices.emplace(); - } - this->_producedOptimalChoices->resize(this->_transitionMatrix.getRowGroupCount()); - } - for (uint64_t iter = 0; iter < upperBound; iter++) { - if(iter == upperBound - 1) { - _multiplier->multiply(env, _x, &_b, constrainedChoiceValues); - } - performIterationStepUpperBound(env, dir); - } - - x = _x; - } - - template - void GameViHelper::performIterationStepUpperBound(Environment const& env, storm::solver::OptimizationDirection const dir, std::vector* choices) { - if (!_multiplier) { - prepareSolversAndMultipliers(env); - } - // multiplyandreducegaussseidel - // Ax = x' - if (choices == nullptr) { - _multiplier->multiplyAndReduce(env, dir, _x, &_b, _x, nullptr, &_statesOfCoalition); - } else { - // Also keep track of the choices made. - _multiplier->multiplyAndReduce(env, dir, _x, &_b, _x, choices, &_statesOfCoalition); - } - } - template void GameViHelper::setProduceScheduler(bool value) { _produceScheduler = value; diff --git a/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.h b/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.h index 393f8a79a..db4b2939f 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.h +++ b/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.h @@ -26,12 +26,7 @@ namespace storm { /*! * Perform value iteration until convergence */ - void performValueIteration(Environment const& env, std::vector& x, std::vector b, storm::solver::OptimizationDirection const dir); - - /*! - * Perform value iteration until upper bound - */ - void performValueIterationUpperBound(Environment const& env, std::vector& x, std::vector b, storm::solver::OptimizationDirection const dir, uint64_t upperBound, std::vector& constrainedChoiceValues); + void performValueIteration(Environment const& env, std::vector& x, std::vector b, storm::solver::OptimizationDirection const dir, std::vector& constrainedChoiceValues); /*! * Sets whether an optimal scheduler shall be constructed during the computation @@ -68,11 +63,6 @@ namespace storm { */ void performIterationStep(Environment const& env, storm::solver::OptimizationDirection const dir, std::vector* choices = nullptr); - /*! - * Performs one iteration step for value iteration with upper bound - */ - void performIterationStepUpperBound(Environment const& env, storm::solver::OptimizationDirection const dir, std::vector* choices = nullptr); - /*! * Checks whether the curently computed value achieves the desired precision */