From 50c7a69f94830e5626490b538e2625c58a8fc9fe Mon Sep 17 00:00:00 2001 From: Lukas Posch Date: Mon, 8 Mar 2021 12:41:14 +0100 Subject: [PATCH] added bounds to computeBoundedGlobally Probabilities and parse upperBound to the game vi helper, additional little changes --- .../rpatl/helper/SparseSmgRpatlHelper.cpp | 36 ++++++++++++++----- .../rpatl/helper/SparseSmgRpatlHelper.h | 2 +- 2 files changed, 28 insertions(+), 10 deletions(-) diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp index 263b131d6..094f36f18 100644 --- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp @@ -107,7 +107,7 @@ namespace storm { } template - MDPSparseModelCheckingHelperReturnType 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) { + MDPSparseModelCheckingHelperReturnType 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); @@ -117,30 +117,48 @@ namespace storm { // Relevant states are safe states - the psiStates. storm::storage::BitVector relevantStates = psiStates; - std::vector b = transitionMatrix.getConstrainedRowGroupSumVector(psiStates, psiStates); + std::vector b = transitionMatrix.getConstrainedRowGroupSumVector(relevantStates, relevantStates); // Reduce the matrix to relevant states - storm::storage::SparseMatrix submatrix = transitionMatrix.getSubmatrix(true, psiStates, psiStates, false); + storm::storage::SparseMatrix submatrix = transitionMatrix.getSubmatrix(true, relevantStates, relevantStates, true); - storm::storage::BitVector clippedStatesOfCoalition(psiStates.getNumberOfSetBits()); - clippedStatesOfCoalition.setClippedStatesOfCoalition(psiStates, statesOfCoalition); + storm::storage::BitVector clippedStatesOfCoalition(relevantStates.getNumberOfSetBits()); + clippedStatesOfCoalition.setClippedStatesOfCoalition(relevantStates, statesOfCoalition); clippedStatesOfCoalition.complement(); - // here is the bounded globally game vi helper used + // Use the bounded globally game vi helper storm::modelchecker::helper::internal::BoundedGloballyGameViHelper viHelper(submatrix, clippedStatesOfCoalition); std::unique_ptr> scheduler; if (produceScheduler) { viHelper.setProduceScheduler(true); } - viHelper.performValueIteration(env, x, b, goal.direction()); - viHelper.fillResultVector(x, psiStates); + // TODO: the lower bounds are not used at the moment + if(lowerBound != 0) + { + STORM_LOG_WARN("The use of lower bounds is not implemented for bounded globally formulas."); + } + + STORM_LOG_DEBUG("upperBound = " << upperBound); + + // in case of 'G<1' or 'G<=0' the states with are initially 'safe' are filled with ones + if(upperBound == 0) + { + x = std::vector(relevantStates.size(), storm::utility::one()); + } else { + viHelper.performValueIteration(env, x, b, goal.direction(), upperBound); + } + + 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(), psiStates, ~psiStates)); + 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/SparseSmgRpatlHelper.h b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.h index 5c39767f7..e6a36f2af 100644 --- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.h +++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.h @@ -39,7 +39,7 @@ namespace storm { static MDPSparseModelCheckingHelperReturnType 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 = ModelCheckerHint()); static MDPSparseModelCheckingHelperReturnType 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 MDPSparseModelCheckingHelperReturnType 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 MDPSparseModelCheckingHelperReturnType 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); + static MDPSparseModelCheckingHelperReturnType 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); private: static storm::storage::Scheduler expandScheduler(storm::storage::Scheduler scheduler, storm::storage::BitVector psiStates, storm::storage::BitVector notPhiStates);