From c2d2c38c2832723e844868990d704e3e99424ecc Mon Sep 17 00:00:00 2001 From: lukpo Date: Fri, 6 Aug 2021 15:47:42 +0200 Subject: [PATCH] WIP computeBoundedUntilProbabilities in SparseSmgRpatlHelper --- .../rpatl/helper/SparseSmgRpatlHelper.cpp | 199 +++++++++++++++--- .../rpatl/helper/SparseSmgRpatlHelper.h | 2 +- 2 files changed, 166 insertions(+), 35 deletions(-) diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp index 40e1c47e9..9c302052f 100644 --- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp @@ -1,3 +1,4 @@ +#include #include "SparseSmgRpatlHelper.h" #include "storm/environment/Environment.h" @@ -5,9 +6,8 @@ #include "storm/environment/solver/MinMaxSolverEnvironment.h" #include "storm/solver/MinMaxLinearEquationSolver.h" #include "storm/utility/vector.h" - +#include "storm/utility/graph.h" #include "storm/modelchecker/rpatl/helper/internal/GameViHelper.h" -#include "storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.h" namespace storm { namespace modelchecker { @@ -19,44 +19,56 @@ namespace storm { auto solverEnv = env; solverEnv.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration, false); - // Initialize the solution vector. - std::vector x = std::vector(transitionMatrix.getRowGroupCount() - psiStates.getNumberOfSetBits(), storm::utility::zero()); // Relevant states are those states which are phiStates and not PsiStates. storm::storage::BitVector relevantStates = phiStates & ~psiStates; + // TODO: check if relevantStates should be used for the size of x + // Initialize the x vector and solution vector result. + //std::vector x = std::vector(transitionMatrix.getRowGroupCount() - psiStates.getNumberOfSetBits(), storm::utility::zero()); + std::vector x = std::vector(relevantStates.getNumberOfSetBits(), storm::utility::zero()); + + std::vector result = std::vector(transitionMatrix.getRowGroupCount(), storm::utility::zero()); + std::vector b = transitionMatrix.getConstrainedRowGroupSumVector(relevantStates, psiStates); std::vector constrainedChoiceValues = std::vector(b.size(), storm::utility::zero()); + std::unique_ptr> scheduler; + + STORM_LOG_DEBUG("statesOfCoalition: " << statesOfCoalition); storm::storage::BitVector clippedStatesOfCoalition(relevantStates.getNumberOfSetBits()); clippedStatesOfCoalition.setClippedStatesOfCoalition(relevantStates, statesOfCoalition); - clippedStatesOfCoalition.complement(); - storm::modelchecker::helper::internal::GameViHelper viHelper(transitionMatrix, clippedStatesOfCoalition); + STORM_LOG_DEBUG("clippedStatesOfCoalition" << clippedStatesOfCoalition); + + //clippedStatesOfCoalition.complement(); + //STORM_LOG_DEBUG("clippedStatesOfCoalition" << clippedStatesOfCoalition); + if(!relevantStates.empty()) { // Reduce the matrix to relevant states. storm::storage::SparseMatrix submatrix = transitionMatrix.getSubmatrix(true, relevantStates, relevantStates, false); - // Update the GameViHelper. - viHelper = storm::modelchecker::helper::internal::GameViHelper(submatrix, clippedStatesOfCoalition); + // Create GameViHelper for computations. + storm::modelchecker::helper::internal::GameViHelper viHelper(submatrix, clippedStatesOfCoalition); if (produceScheduler) { viHelper.setProduceScheduler(true); } - // Perform value iteration. viHelper.performValueIteration(env, x, b, goal.direction()); if(goal.isShieldingTask()) { viHelper.getChoiceValues(env, x, constrainedChoiceValues); } - } - // Fill up the result x with 0s and 1s for not relevant states. - viHelper.fillResultVector(x, relevantStates, psiStates); - // Fill up the constrainedChoice Values to full size. - viHelper.fillChoiceValuesVector(constrainedChoiceValues, relevantStates, transitionMatrix.getRowGroupIndices()); + // Fill up the constrainedChoice Values to full size. + viHelper.fillChoiceValuesVector(constrainedChoiceValues, relevantStates, transitionMatrix.getRowGroupIndices()); - std::unique_ptr> scheduler; - if (produceScheduler) { - scheduler = std::make_unique>(expandScheduler(viHelper.extractScheduler(), psiStates, ~phiStates)); + if (produceScheduler) { + scheduler = std::make_unique>(expandScheduler(viHelper.extractScheduler(), psiStates, ~phiStates)); + } } - return SMGSparseModelCheckingHelperReturnType(std::move(x), std::move(relevantStates), std::move(scheduler), std::move(constrainedChoiceValues)); + + // Fill up the result vector with the values of x for the relevant states, with 1s for psi states (0 is default) + storm::utility::vector::setVectorValues(result, relevantStates, x); + 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)); } template @@ -85,6 +97,8 @@ namespace storm { // 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(); + STORM_LOG_DEBUG(statesOfCoalition); + auto result = computeUntilProbabilities(env, std::move(goal), transitionMatrix, backwardTransitions, storm::storage::BitVector(transitionMatrix.getRowGroupCount(), true), notPsiStates, qualitative, statesOfCoalition, produceScheduler, hint); for (auto& element : result.values) { element = storm::utility::one() - element; @@ -92,27 +106,31 @@ namespace storm { for (auto& element : result.choiceValues) { element = storm::utility::one() - element; } + STORM_LOG_DEBUG(result.values); return result; } template SMGSparseModelCheckingHelperReturnType SparseSmgRpatlHelper::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) { - // Create vector x for result, bitvector allStates with a true for each state and a vector b for the probability for each state to get to a psi state, choiceValues is to store choices for shielding. - std::vector x = std::vector(transitionMatrix.getRowGroupCount(), storm::utility::zero()); + // Create vector result, bitvector allStates with a true for each state and a vector b for the probability for each state to get to a psi state, choiceValues is to store choices for shielding. + std::vector result = std::vector(transitionMatrix.getRowGroupCount(), storm::utility::zero()); storm::storage::BitVector allStates = storm::storage::BitVector(transitionMatrix.getRowGroupCount(), true); std::vector b = transitionMatrix.getConstrainedRowGroupSumVector(allStates, psiStates); std::vector choiceValues = std::vector(transitionMatrix.getRowCount(), storm::utility::zero()); statesOfCoalition.complement(); + STORM_LOG_DEBUG(statesOfCoalition); + if (produceScheduler) { STORM_LOG_WARN("Next formula does not expect that produceScheduler is set to true."); } // Create a multiplier for reduction. auto multiplier = storm::solver::MultiplierFactory().create(env, transitionMatrix); - multiplier->reduce(env, goal.direction(), b, transitionMatrix.getRowGroupIndices(), x, &statesOfCoalition); + multiplier->reduce(env, goal.direction(), b, transitionMatrix.getRowGroupIndices(), result, &statesOfCoalition); if (goal.isShieldingTask()) { choiceValues = b; } - return SMGSparseModelCheckingHelperReturnType(std::move(x), std::move(allStates), nullptr, std::move(choiceValues)); + STORM_LOG_DEBUG(result); + return SMGSparseModelCheckingHelperReturnType(std::move(result), std::move(allStates), nullptr, std::move(choiceValues)); } template @@ -123,35 +141,148 @@ namespace storm { // Relevant states are safe states - the psiStates. storm::storage::BitVector relevantStates = psiStates; - // Initialize the solution vector. + // 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(); + //clippedStatesOfCoalition.complement(); + STORM_LOG_DEBUG(clippedStatesOfCoalition); - // Use the bounded globally game vi helper. - storm::modelchecker::helper::internal::GameViHelper viHelper(transitionMatrix, clippedStatesOfCoalition); if(!relevantStates.empty() && upperBound > 0) { // Reduce the matrix to relevant states. storm::storage::SparseMatrix submatrix = transitionMatrix.getSubmatrix(true, relevantStates, relevantStates, false); - // Update the BoundedGloballyViHelper. + // Create GameViHelper for computations. storm::modelchecker::helper::internal::GameViHelper viHelper(submatrix, clippedStatesOfCoalition); if (produceScheduler) { viHelper.setProduceScheduler(true); } - viHelper.performValueIterationUpperBound(env, x, goal.direction(), upperBound, constrainedChoiceValues); + + 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)); + } } - viHelper.fillResultVector(x, relevantStates); - viHelper.fillChoiceValuesVector(constrainedChoiceValues, relevantStates, transitionMatrix.getRowGroupIndices()); + // 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)); + } + + 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) { + STORM_LOG_DEBUG("lowerBound = " << lowerBound); + STORM_LOG_DEBUG("upperBound = " << upperBound); + + auto solverEnv = env; + solverEnv.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration, false); + + // relevantStates are default all set + // if the upper bound is 0 a psiState cannot be passed between 0 and the lower bound - we can reduce the relevant states and fill the psi states in the result with 1s. + //storm::storage::BitVector relevantStates(transitionMatrix.getRowGroupCount(), true); + storm::storage::BitVector relevantStates = phiStates & ~psiStates; + storm::storage::BitVector makeZeroColumns; +/* if (goal.minimize()) { + relevantStates = storm::utility::graph::performProbGreater0A(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, phiStates, psiStates, true, upperBound); + } else { + relevantStates = storm::utility::graph::performProbGreater0E(backwardTransitions, phiStates, psiStates, true, upperBound); + }*/ +/* if(lowerBound == 0) { + STORM_LOG_DEBUG("LOWER BOUND = 0, relevant states are the not-psiStates"); + relevantStates = phiStates & ~psiStates; + }*/ /*else { + STORM_LOG_DEBUG("LOWER BOUND !=0, relevant states are all states, makeZeroColumns = psiStates"); + makeZeroColumns = psiStates; + }*/ + + STORM_LOG_DEBUG("relevantStates = " << relevantStates); + + // Initializations. + std::vector x = std::vector(relevantStates.getNumberOfSetBits(), storm::utility::zero()); + std::vector b = transitionMatrix.getConstrainedRowGroupSumVector(relevantStates, psiStates); + 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; - if (produceScheduler) { - scheduler = std::make_unique>(expandScheduler(viHelper.extractScheduler(), relevantStates, ~relevantStates)); - } - return SMGSparseModelCheckingHelperReturnType(std::move(x), std::move(relevantStates), std::move(scheduler), std::move(constrainedChoiceValues)); + 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. - relevant states are all states + storm::storage::SparseMatrix submatrix = transitionMatrix.getSubmatrix(true, relevantStates, relevantStates, false, makeZeroColumns); + // Create GameViHelper for computations. + storm::modelchecker::helper::internal::GameViHelper viHelper(submatrix, clippedStatesOfCoalition); + if (produceScheduler) { + viHelper.setProduceScheduler(true); + } + if(lowerBound == 0) { + STORM_LOG_DEBUG("LOWER BOUND = 0 ..."); + STORM_LOG_DEBUG("Just peform Value Iteration with an UPPER BOUND."); + viHelper.performValueIterationUpperBound(env, x, b, goal.direction(), upperBound, constrainedChoiceValues); + } else { + STORM_LOG_DEBUG("LOWER BOUND != 0 ..."); + + // TODO: change the computation: first the diff, then till the lowerBound + + STORM_LOG_DEBUG("first multiplication ..."); + viHelper.performValueIterationUpperBound(env, x, b, goal.direction(), upperBound - lowerBound + 1, constrainedChoiceValues); + STORM_LOG_DEBUG("x = " << x); + STORM_LOG_DEBUG("b = " << b); + STORM_LOG_DEBUG("constrainedChoiceValues = " << constrainedChoiceValues); + + STORM_LOG_DEBUG("Reduction for ~phiStates ..."); + /* for(uint rowGroupIndex = 0; rowGroupIndex < submatrix.getRowGroupCount(); rowGroupIndex++) { + for(uint rowIndex = 0; rowIndex < submatrix.getRowGroupSize(rowGroupIndex); rowIndex++) { + if(!phiStates.get(rowGroupIndex)) { + constrainedChoiceValues.at(rowGroupIndex) = storm::utility::zero(); + } + } + }*/ + STORM_LOG_DEBUG("constrainedChoiceValues = " << constrainedChoiceValues); + + //storm::storage::BitVector newRelevantStates(x.size(), false); + //storm::utility::vector::setNonzeroIndices(x, newRelevantStates); + //storm::utility::vector::setVectorValues(x, ~phiStates, storm::utility::zero()); + + STORM_LOG_DEBUG("reset x ..."); + x = std::vector(x.size(), storm::utility::zero()); + STORM_LOG_DEBUG("x = " << x); + + STORM_LOG_DEBUG("second multiplication ..."); + viHelper.performValueIterationUpperBound(env, x, constrainedChoiceValues, goal.direction(), lowerBound, constrainedChoiceValues); + STORM_LOG_DEBUG("x = " << x); + STORM_LOG_DEBUG("b = " << b); + STORM_LOG_DEBUG("constrainedChoiceValues = " << constrainedChoiceValues); + + +/* + viHelper.performValueIterationUpperBound(env, x, b, goal.direction(), upperBound - lowerBound + 1, constrainedChoiceValues); + submatrix = transitionMatrix.getSubmatrix(true, relevantStates, relevantStates, false); + viHelper.updateTransitionMatrix(submatrix); + b = std::vector(b.size(), storm::utility::zero()); + viHelper.performValueIterationUpperBound(env, x, b, goal.direction(), lowerBound - 1, constrainedChoiceValues); +*/ + + } + viHelper.fillChoiceValuesVector(constrainedChoiceValues, relevantStates, transitionMatrix.getRowGroupIndices()); + if (produceScheduler) { + scheduler = std::make_unique>(expandScheduler(viHelper.extractScheduler(), relevantStates, ~relevantStates)); + } + storm::utility::vector::setVectorValues(result, relevantStates, x); + } + if(lowerBound == 0) { + 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)); } template class SparseSmgRpatlHelper; diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.h b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.h index 5258104dc..a17cbd653 100644 --- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.h +++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.h @@ -38,10 +38,10 @@ 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); 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); - }; } }