From 86c3b3d9c675164119403f8b9c79c707811f4597 Mon Sep 17 00:00:00 2001 From: lukpo Date: Tue, 10 Aug 2021 09:27:54 +0200 Subject: [PATCH] changed computeBoundedGloballyProbabilities computation by using computeBoundedUntilProbabilities --- .../rpatl/helper/SparseSmgRpatlHelper.cpp | 54 ++++++------------- .../rpatl/helper/SparseSmgRpatlHelper.h | 2 +- 2 files changed, 17 insertions(+), 39 deletions(-) diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp index 9237e46b9..e28d591e0 100644 --- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp @@ -129,48 +129,24 @@ namespace storm { template SMGSparseModelCheckingHelperReturnType SparseSmgRpatlHelper::computeBoundedGloballyProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint,uint64_t lowerBound, uint64_t upperBound) { - auto solverEnv = env; - solverEnv.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration, false); - - // Relevant states are safe states - the psiStates. - storm::storage::BitVector relevantStates = psiStates; - - // Initializations. - std::vector x = std::vector(relevantStates.getNumberOfSetBits(), storm::utility::one()); - std::vector b = std::vector(transitionMatrix.getConstrainedRowGroupSumVector(relevantStates, psiStates).size(), storm::utility::zero()); - std::vector result = std::vector(transitionMatrix.getRowGroupCount(), storm::utility::zero()); - std::vector constrainedChoiceValues = std::vector(transitionMatrix.getConstrainedRowGroupSumVector(relevantStates, psiStates).size(), storm::utility::zero()); - std::unique_ptr> scheduler; - - storm::storage::BitVector clippedStatesOfCoalition(relevantStates.getNumberOfSetBits()); - clippedStatesOfCoalition.setClippedStatesOfCoalition(relevantStates, statesOfCoalition); - //clippedStatesOfCoalition.complement(); - STORM_LOG_DEBUG(clippedStatesOfCoalition); - - if(!relevantStates.empty() && upperBound > 0) { - // Reduce the matrix to relevant states. - storm::storage::SparseMatrix submatrix = transitionMatrix.getSubmatrix(true, relevantStates, relevantStates, false); - // Create GameViHelper for computations. - storm::modelchecker::helper::internal::GameViHelper viHelper(submatrix, clippedStatesOfCoalition); - if (produceScheduler) { - viHelper.setProduceScheduler(true); - } + // G psi = not(F(not psi)) = not(true U (not psi)) + // The psiStates are flipped, then the true U part is calculated, at the end the result is flipped again. + storm::storage::BitVector notPsiStates = ~psiStates; + statesOfCoalition.complement(); - viHelper.performValueIterationUpperBound(env, x, b, goal.direction(), upperBound, constrainedChoiceValues); - viHelper.fillChoiceValuesVector(constrainedChoiceValues, relevantStates, transitionMatrix.getRowGroupIndices()); - if (produceScheduler) { - scheduler = std::make_unique>(expandScheduler(viHelper.extractScheduler(), relevantStates, ~relevantStates)); - } + auto result = computeBoundedUntilProbabilities(env, std::move(goal), transitionMatrix, backwardTransitions, storm::storage::BitVector(transitionMatrix.getRowGroupCount(), true), notPsiStates, qualitative, statesOfCoalition, produceScheduler, hint, lowerBound, upperBound, true); + for (auto& element : result.values) { + element = storm::utility::one() - element; } - - // Fill up the result vector with the values of x for the relevant states (0 is default) - storm::utility::vector::setVectorValues(result, relevantStates, x); - STORM_LOG_DEBUG(result); - return SMGSparseModelCheckingHelperReturnType(std::move(result), std::move(relevantStates), std::move(scheduler), std::move(constrainedChoiceValues)); + for (auto& element : result.choiceValues) { + element = storm::utility::one() - element; + } + STORM_LOG_DEBUG(result.values); + return result; } template - SMGSparseModelCheckingHelperReturnType SparseSmgRpatlHelper::computeBoundedUntilProbabilities(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,uint64_t lowerBound, uint64_t upperBound) { + SMGSparseModelCheckingHelperReturnType SparseSmgRpatlHelper::computeBoundedUntilProbabilities(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,uint64_t lowerBound, uint64_t upperBound, bool computeBoundedGlobally) { auto solverEnv = env; solverEnv.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration, false); @@ -242,7 +218,9 @@ namespace storm { storm::utility::vector::setVectorValues(result, relevantStates, x); } - storm::utility::vector::setVectorValues(result, psiStates, storm::utility::one()); + if(!computeBoundedGlobally){ + storm::utility::vector::setVectorValues(result, psiStates, storm::utility::one()); + } STORM_LOG_DEBUG(result); return SMGSparseModelCheckingHelperReturnType(std::move(result), std::move(relevantStates), std::move(scheduler), std::move(constrainedChoiceValues)); } diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.h b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.h index a17cbd653..0592c929b 100644 --- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.h +++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.h @@ -38,7 +38,7 @@ namespace storm { static SMGSparseModelCheckingHelperReturnType computeGloballyProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint = ModelCheckerHint()); static SMGSparseModelCheckingHelperReturnType computeNextProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint); static SMGSparseModelCheckingHelperReturnType computeBoundedGloballyProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint, uint64_t lowerBound, uint64_t upperBound); - static SMGSparseModelCheckingHelperReturnType computeBoundedUntilProbabilities(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, uint64_t lowerBound, uint64_t upperBound); + static SMGSparseModelCheckingHelperReturnType computeBoundedUntilProbabilities(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, uint64_t lowerBound, uint64_t upperBound, bool computeBoundedGlobally = false); private: static storm::storage::Scheduler expandScheduler(storm::storage::Scheduler scheduler, storm::storage::BitVector psiStates, storm::storage::BitVector notPhiStates); static void expandChoiceValues(std::vector const& rowGroupIndices, storm::storage::BitVector const& relevantStates, std::vector const& constrainedChoiceValues, std::vector& choiceValues);