From 8301c3dc888f687bb056618a08a5866c1c309d91 Mon Sep 17 00:00:00 2001 From: lukpo Date: Wed, 4 Aug 2021 14:30:48 +0200 Subject: [PATCH 01/21] fixed case for empty relevantStates in computeUntilProbabilities --- .../rpatl/helper/SparseSmgRpatlHelper.cpp | 28 +++++++++++-------- 1 file changed, 17 insertions(+), 11 deletions(-) diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp index 78d554346..b0b16ccc5 100644 --- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp @@ -27,26 +27,32 @@ namespace storm { std::vector b = transitionMatrix.getConstrainedRowGroupSumVector(relevantStates, psiStates); std::vector constrainedChoiceValues = std::vector(b.size(), storm::utility::zero()); - // Reduce the matrix to relevant states - storm::storage::SparseMatrix submatrix = transitionMatrix.getSubmatrix(true, relevantStates, relevantStates, false); - storm::storage::BitVector clippedStatesOfCoalition(relevantStates.getNumberOfSetBits()); clippedStatesOfCoalition.setClippedStatesOfCoalition(relevantStates, statesOfCoalition); clippedStatesOfCoalition.complement(); - storm::modelchecker::helper::internal::GameViHelper viHelper(submatrix, clippedStatesOfCoalition); - std::unique_ptr> scheduler; - if (produceScheduler) { - viHelper.setProduceScheduler(true); + storm::modelchecker::helper::internal::GameViHelper viHelper(transitionMatrix, 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); + if (produceScheduler) { + viHelper.setProduceScheduler(true); + } + // Perform value iteration. + viHelper.performValueIteration(env, x, b, goal.direction()); + if(goal.isShieldingTask()) { + viHelper.getChoiceValues(env, x, constrainedChoiceValues); + } } - 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()); + std::unique_ptr> scheduler; if (produceScheduler) { scheduler = std::make_unique>(expandScheduler(viHelper.extractScheduler(), psiStates, ~phiStates)); } From 7bdb5e11a8099817481a36b896916753da0fee2a Mon Sep 17 00:00:00 2001 From: lukpo Date: Wed, 4 Aug 2021 14:31:46 +0200 Subject: [PATCH 02/21] fixed case for empty relevantStates in computeBoundedGlobally Probabilities --- .../rpatl/helper/SparseSmgRpatlHelper.cpp | 29 ++++++++----------- 1 file changed, 12 insertions(+), 17 deletions(-) diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp index b0b16ccc5..84b756dee 100644 --- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp @@ -131,33 +131,28 @@ namespace storm { // Initialize the solution vector. std::vector x = std::vector(relevantStates.getNumberOfSetBits(), storm::utility::one()); - - // 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()); + std::vector constrainedChoiceValues = std::vector(transitionMatrix.getConstrainedRowGroupSumVector(relevantStates, psiStates).size(), storm::utility::zero()); storm::storage::BitVector clippedStatesOfCoalition(relevantStates.getNumberOfSetBits()); clippedStatesOfCoalition.setClippedStatesOfCoalition(relevantStates, statesOfCoalition); clippedStatesOfCoalition.complement(); - // Use the bounded globally game vi helper - storm::modelchecker::helper::internal::BoundedGloballyGameViHelper viHelper(submatrix, clippedStatesOfCoalition); - std::unique_ptr> scheduler; - if (produceScheduler) { - viHelper.setProduceScheduler(true); - } - - // in case of upperBound = 0 the states which are initially "safe" are filled with ones - if(upperBound > 0) - { + // Use the bounded globally game vi helper. + storm::modelchecker::helper::internal::BoundedGloballyGameViHelper 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. + storm::modelchecker::helper::internal::BoundedGloballyGameViHelper viHelper(submatrix, clippedStatesOfCoalition); + if (produceScheduler) { + viHelper.setProduceScheduler(true); + } viHelper.performValueIteration(env, x, goal.direction(), upperBound, constrainedChoiceValues); } - viHelper.fillChoiceValuesVector(constrainedChoiceValues, relevantStates, transitionMatrix.getRowGroupIndices()); viHelper.fillResultVector(x, relevantStates); viHelper.fillChoiceValuesVector(constrainedChoiceValues, relevantStates, transitionMatrix.getRowGroupIndices()); - + std::unique_ptr> scheduler; if (produceScheduler) { scheduler = std::make_unique>(expandScheduler(viHelper.extractScheduler(), relevantStates, ~relevantStates)); } From b6ffa9a6497ce300d279d5424d73f91281b27f76 Mon Sep 17 00:00:00 2001 From: lukpo Date: Wed, 4 Aug 2021 14:33:17 +0200 Subject: [PATCH 03/21] small change in the comments of computeGloballyProbabilities --- src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp index 84b756dee..b3b89688e 100644 --- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp @@ -81,9 +81,8 @@ namespace storm { template SMGSparseModelCheckingHelperReturnType SparseSmgRpatlHelper::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) { - // the idea is to implement the definition of globally as in the formula: // G psi = not(F(not psi)) = not(true U (not psi)) - // so the psiStates are flipped, then the true U part is calculated, at the end the result is flipped again + // 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(); auto result = computeUntilProbabilities(env, std::move(goal), transitionMatrix, backwardTransitions, storm::storage::BitVector(transitionMatrix.getRowGroupCount(), true), notPsiStates, qualitative, statesOfCoalition, produceScheduler, hint); From 65a5308809c29f579bbc73be87e416f1d7ceb8e1 Mon Sep 17 00:00:00 2001 From: lukpo Date: Wed, 4 Aug 2021 14:35:03 +0200 Subject: [PATCH 04/21] small change in computation in computeNextProbabilities --- .../rpatl/helper/SparseSmgRpatlHelper.cpp | 15 +++++---------- 1 file changed, 5 insertions(+), 10 deletions(-) diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp index b3b89688e..d4e06bbde 100644 --- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp @@ -97,25 +97,20 @@ namespace storm { 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 to get to state psi + // 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()); 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(); - if (produceScheduler) { STORM_LOG_WARN("Next formula does not expect that produceScheduler is set to true."); } - - // create multiplier and execute the calculation for 1 step + // Create a multiplier for reduction. auto multiplier = storm::solver::MultiplierFactory().create(env, transitionMatrix); - std::vector choiceValues = std::vector(transitionMatrix.getRowCount(), storm::utility::zero()); + multiplier->reduce(env, goal.direction(), b, transitionMatrix.getRowGroupIndices(), x, &statesOfCoalition); if (goal.isShieldingTask()) { - multiplier->multiply(env, x, &b, choiceValues); - multiplier->reduce(env, goal.direction(), choiceValues, transitionMatrix.getRowGroupIndices(), x, &statesOfCoalition); - } else { - multiplier->multiplyAndReduce(env, goal.direction(), x, &b, x, nullptr, &statesOfCoalition); + choiceValues = b; } return SMGSparseModelCheckingHelperReturnType(std::move(x), std::move(allStates), nullptr, std::move(choiceValues)); } From 6289788a6876907ac648e20263da01d79ee4223e Mon Sep 17 00:00:00 2001 From: lukpo Date: Wed, 4 Aug 2021 15:35:36 +0200 Subject: [PATCH 05/21] small changes to fit to the GameViHelper.* --- .../rpatl/helper/internal/BoundedGloballyGameViHelper.cpp | 6 +++--- .../rpatl/helper/internal/BoundedGloballyGameViHelper.h | 4 ++-- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.cpp b/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.cpp index 33bb6dfe2..6742476ef 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.cpp @@ -60,12 +60,12 @@ namespace storm { } template - void BoundedGloballyGameViHelper::fillResultVector(std::vector& result, storm::storage::BitVector psiStates) + void BoundedGloballyGameViHelper::fillResultVector(std::vector& result, storm::storage::BitVector relevantStates) { - std::vector filledVector = std::vector(psiStates.size(), storm::utility::zero()); + std::vector filledVector = std::vector(relevantStates.size(), storm::utility::zero()); uint bitIndex = 0; for(uint i = 0; i < filledVector.size(); i++) { - if (psiStates.get(i)) { + if (relevantStates.get(i)) { filledVector.at(i) = result.at(bitIndex); bitIndex++; } diff --git a/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.h b/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.h index 78d499265..8dcb8e848 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.h +++ b/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.h @@ -26,9 +26,9 @@ namespace storm { 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 + * Fills the result vector to the original size with zeros for all states except the relevantStates */ - void fillResultVector(std::vector& result, storm::storage::BitVector psiStates); + void fillResultVector(std::vector& result, storm::storage::BitVector relevantStates); /*! * Fills the choice values vector to the original size with zeros for ~psiState choices. From d22233771556c74f79a502ee17dfb5c582109c06 Mon Sep 17 00:00:00 2001 From: lukpo Date: Wed, 4 Aug 2021 15:36:47 +0200 Subject: [PATCH 06/21] added functionality of BoundedGloballyGameViHelper to GameViHelper --- .../rpatl/helper/internal/GameViHelper.cpp | 51 ++++++++++++++++++- .../rpatl/helper/internal/GameViHelper.h | 23 ++++++++- 2 files changed, 71 insertions(+), 3 deletions(-) diff --git a/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp b/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp index 58a42a397..8f4800128 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp @@ -15,22 +15,22 @@ namespace storm { template GameViHelper::GameViHelper(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector statesOfCoalition) : _transitionMatrix(transitionMatrix), _statesOfCoalition(statesOfCoalition) { + // Intentionally left empty. } template void GameViHelper::prepareSolversAndMultipliers(const Environment& env) { _multiplier = storm::solver::MultiplierFactory().create(env, _transitionMatrix); - _x1IsCurrent = false; } template void GameViHelper::performValueIteration(Environment const& env, std::vector& x, std::vector b, storm::solver::OptimizationDirection const dir) { 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()); _x2 = _x1; @@ -113,6 +113,53 @@ namespace storm { return true; } + template + void GameViHelper::performValueIterationUpperBound(Environment const& env, std::vector& x, storm::solver::OptimizationDirection const dir, uint64_t upperBound, std::vector& constrainedChoiceValues) { + prepareSolversAndMultipliers(env); + _x = x; + 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, nullptr, 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, nullptr, _x, nullptr, &_statesOfCoalition); + } else { + // Also keep track of the choices made. + _multiplier->multiplyAndReduce(env, dir, _x, nullptr, _x, choices, &_statesOfCoalition); + } + } + + template + void GameViHelper::fillResultVector(std::vector& result, storm::storage::BitVector relevantStates) { + std::vector filledVector = std::vector(relevantStates.size(), storm::utility::zero()); + uint bitIndex = 0; + for(uint i = 0; i < filledVector.size(); i++) { + if (relevantStates.get(i)) { + filledVector.at(i) = result.at(bitIndex); + bitIndex++; + } + } + result = filledVector; + } + template void GameViHelper::fillResultVector(std::vector& result, storm::storage::BitVector relevantStates, storm::storage::BitVector psiStates) { std::vector filledVector = std::vector(relevantStates.size(), storm::utility::zero()); diff --git a/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.h b/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.h index 00eca9fe6..2d1b1538a 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.h +++ b/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.h @@ -23,8 +23,21 @@ namespace storm { void prepareSolversAndMultipliers(const Environment& env); + /*! + * 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, storm::solver::OptimizationDirection const dir, uint64_t upperBound, std::vector& constrainedChoiceValues); + + /*! + * Fills the result vector to the original size with zeros for all states except the relevantStates + */ + void fillResultVector(std::vector& result, storm::storage::BitVector relevantStates); + /*! * Fills the result vector to the original size with ones for being psiStates, zeros for being not phiStates */ @@ -49,8 +62,16 @@ namespace storm { void getChoiceValues(Environment const& env, std::vector const& x, std::vector& choiceValues); private: + /*! + * Performs one iteration step for value iteration + */ 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 */ @@ -77,7 +98,7 @@ namespace storm { storm::storage::SparseMatrix _transitionMatrix; storm::storage::BitVector _statesOfCoalition; - std::vector _x1, _x2, _b; + std::vector _x, _x1, _x2, _b; std::unique_ptr> _multiplier; bool _produceScheduler = false; From f4615614c1d0c1c76352819015022a20325c7db8 Mon Sep 17 00:00:00 2001 From: lukpo Date: Wed, 4 Aug 2021 15:38:48 +0200 Subject: [PATCH 07/21] use GameViHelper instead of BoundedGloballyGameViHelper --- .../modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp index d4e06bbde..40e1c47e9 100644 --- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp @@ -132,16 +132,16 @@ namespace storm { clippedStatesOfCoalition.complement(); // Use the bounded globally game vi helper. - storm::modelchecker::helper::internal::BoundedGloballyGameViHelper viHelper(transitionMatrix, clippedStatesOfCoalition); + 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. - storm::modelchecker::helper::internal::BoundedGloballyGameViHelper viHelper(submatrix, clippedStatesOfCoalition); + storm::modelchecker::helper::internal::GameViHelper viHelper(submatrix, clippedStatesOfCoalition); if (produceScheduler) { viHelper.setProduceScheduler(true); } - viHelper.performValueIteration(env, x, goal.direction(), upperBound, constrainedChoiceValues); + viHelper.performValueIterationUpperBound(env, x, goal.direction(), upperBound, constrainedChoiceValues); } viHelper.fillResultVector(x, relevantStates); From e5dd9ab90f865ed73dc704c6f84c8f820493768a Mon Sep 17 00:00:00 2001 From: lukpo Date: Wed, 4 Aug 2021 15:40:37 +0200 Subject: [PATCH 08/21] small cleanup SparseSmgRpatlModelChecker --- .../modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp | 7 ------- src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.h | 2 +- 2 files changed, 1 insertion(+), 8 deletions(-) diff --git a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp index 1668bc440..b03d89b3c 100644 --- a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp +++ b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp @@ -39,8 +39,6 @@ namespace storm { // Intentionally left empty. } - - template bool SparseSmgRpatlModelChecker::canHandleStatic(CheckTask const& checkTask, bool* requiresSingleInitialState) { storm::logic::Formula const& formula = checkTask.getFormula(); @@ -57,8 +55,6 @@ namespace storm { } } - - template std::unique_ptr SparseSmgRpatlModelChecker::checkGameFormula(Environment const& env, CheckTask const& checkTask) { Environment solverEnv = env; @@ -97,7 +93,6 @@ namespace storm { std::unique_ptr SparseSmgRpatlModelChecker::checkRewardOperatorFormula(Environment const& env, CheckTask const& checkTask) { storm::logic::RewardOperatorFormula const& formula = checkTask.getFormula(); std::unique_ptr result = this->computeRewards(env, formula.getMeasureType(), checkTask.substituteFormula(formula.getSubformula())); - return result; } @@ -105,7 +100,6 @@ namespace storm { std::unique_ptr SparseSmgRpatlModelChecker::checkLongRunAverageOperatorFormula(Environment const& env, CheckTask const& checkTask) { storm::logic::LongRunAverageOperatorFormula const& formula = checkTask.getFormula(); std::unique_ptr result = this->computeLongRunAverageProbabilities(env, checkTask.substituteFormula(formula.getSubformula().asStateFormula())); - return result; } @@ -216,7 +210,6 @@ namespace storm { } else if (checkTask.isProduceSchedulersSet()) { result->asExplicitQuantitativeCheckResult().setScheduler(std::make_unique>(helper.extractScheduler())); } - return result; } diff --git a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.h b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.h index a27e580c5..44b55f868 100644 --- a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.h +++ b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.h @@ -28,6 +28,7 @@ namespace storm { // The implemented methods of the AbstractModelChecker interface. bool canHandle(CheckTask const& checkTask) const override; + std::unique_ptr checkGameFormula(Environment const& env, CheckTask const& checkTask) override; std::unique_ptr checkProbabilityOperatorFormula(Environment const& env, CheckTask const& checkTask) override; std::unique_ptr checkRewardOperatorFormula(Environment const& env, CheckTask const& checkTask) override; @@ -44,7 +45,6 @@ namespace storm { std::unique_ptr computeLongRunAverageProbabilities(Environment const& env, CheckTask const& checkTask) override; std::unique_ptr computeLongRunAverageRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; - //void coalitionIndicator(Environment& env, CheckTask const& checkTask); private: storm::storage::BitVector statesOfCoalition; }; From 75bacaa6b249f4a33614c556676569116bd92e04 Mon Sep 17 00:00:00 2001 From: lukpo Date: Wed, 4 Aug 2021 15:46:14 +0200 Subject: [PATCH 09/21] deleted BoundedGloballyGameViHelper --- .../internal/BoundedGloballyGameViHelper.cpp | 132 ------------------ .../internal/BoundedGloballyGameViHelper.h | 76 ---------- 2 files changed, 208 deletions(-) delete mode 100644 src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.cpp delete mode 100644 src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.h diff --git a/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.cpp b/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.cpp deleted file mode 100644 index 6742476ef..000000000 --- a/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.cpp +++ /dev/null @@ -1,132 +0,0 @@ -#include "BoundedGloballyGameViHelper.h" - -#include "storm/environment/Environment.h" -#include "storm/environment/solver/SolverEnvironment.h" -#include "storm/environment/solver/GameSolverEnvironment.h" - -#include "storm/utility/SignalHandler.h" -#include "storm/utility/vector.h" - -namespace storm { - namespace modelchecker { - namespace helper { - namespace internal { - - template - BoundedGloballyGameViHelper::BoundedGloballyGameViHelper(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector statesOfCoalition) : _transitionMatrix(transitionMatrix), _statesOfCoalition(statesOfCoalition) { - } - - template - void BoundedGloballyGameViHelper::prepareSolversAndMultipliers(const Environment& env) { - _multiplier = storm::solver::MultiplierFactory().create(env, _transitionMatrix); - } - - template - void BoundedGloballyGameViHelper::performValueIteration(Environment const& env, std::vector& x, storm::solver::OptimizationDirection const dir, uint64_t upperBound, std::vector& constrainedChoiceValues) { - prepareSolversAndMultipliers(env); - _x = x; - - 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, nullptr, constrainedChoiceValues); - } - performIterationStep(env, dir); - } - - x = _x; - } - - template - void BoundedGloballyGameViHelper::performIterationStep(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, nullptr, _x, nullptr, &_statesOfCoalition); - } else { - // Also keep track of the choices made. - _multiplier->multiplyAndReduce(env, dir, _x, nullptr, _x, choices, &_statesOfCoalition); - } - } - - template - void BoundedGloballyGameViHelper::fillResultVector(std::vector& result, storm::storage::BitVector relevantStates) - { - std::vector filledVector = std::vector(relevantStates.size(), storm::utility::zero()); - uint bitIndex = 0; - for(uint i = 0; i < filledVector.size(); i++) { - if (relevantStates.get(i)) { - filledVector.at(i) = result.at(bitIndex); - bitIndex++; - } - } - result = filledVector; - } - - template - void BoundedGloballyGameViHelper::fillChoiceValuesVector(std::vector& choiceValues, storm::storage::BitVector psiStates, std::vector::index_type> rowGroupIndices) { - std::vector allChoices = std::vector(rowGroupIndices.at(rowGroupIndices.size() - 1), storm::utility::zero()); - auto choice_it = choiceValues.begin(); - for(uint state = 0; state < rowGroupIndices.size() - 1; state++) { - uint rowGroupSize = rowGroupIndices[state + 1] - rowGroupIndices[state]; - if (psiStates.get(state)) { - for(uint choice = 0; choice < rowGroupSize; choice++, choice_it++) { - allChoices.at(rowGroupIndices.at(state) + choice) = *choice_it; - } - } - } - choiceValues = allChoices; - } - - template - void BoundedGloballyGameViHelper::setProduceScheduler(bool value) { - _produceScheduler = value; - } - - template - bool BoundedGloballyGameViHelper::isProduceSchedulerSet() const { - return _produceScheduler; - } - - template - std::vector const& BoundedGloballyGameViHelper::getProducedOptimalChoices() const { - STORM_LOG_ASSERT(this->isProduceSchedulerSet(), "Trying to get the produced optimal choices although no scheduler was requested."); - STORM_LOG_ASSERT(this->_producedOptimalChoices.is_initialized(), "Trying to get the produced optimal choices but none were available. Was there a computation call before?"); - return this->_producedOptimalChoices.get(); - } - - template - std::vector& BoundedGloballyGameViHelper::getProducedOptimalChoices() { - STORM_LOG_ASSERT(this->isProduceSchedulerSet(), "Trying to get the produced optimal choices although no scheduler was requested."); - STORM_LOG_ASSERT(this->_producedOptimalChoices.is_initialized(), "Trying to get the produced optimal choices but none were available. Was there a computation call before?"); - return this->_producedOptimalChoices.get(); - } - - template - storm::storage::Scheduler BoundedGloballyGameViHelper::extractScheduler() const{ - auto const& optimalChoices = getProducedOptimalChoices(); - storm::storage::Scheduler scheduler(optimalChoices.size()); - for (uint64_t state = 0; state < optimalChoices.size(); ++state) { - scheduler.setChoice(optimalChoices[state], state); - } - return scheduler; - } - - template class BoundedGloballyGameViHelper; -#ifdef STORM_HAVE_CARL - template class BoundedGloballyGameViHelper; -#endif - } - } - } -} diff --git a/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.h b/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.h deleted file mode 100644 index 8dcb8e848..000000000 --- a/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.h +++ /dev/null @@ -1,76 +0,0 @@ -#pragma once - -#include "storm/storage/SparseMatrix.h" -#include "storm/solver/LinearEquationSolver.h" -#include "storm/solver/MinMaxLinearEquationSolver.h" -#include "storm/solver/Multiplier.h" - -namespace storm { - class Environment; - - namespace storage { - template class Scheduler; - } - - namespace modelchecker { - namespace helper { - namespace internal { - - template - class BoundedGloballyGameViHelper { - public: - BoundedGloballyGameViHelper(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector statesOfCoalition); - - void prepareSolversAndMultipliers(const Environment& env); - - 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 zeros for all states except the relevantStates - */ - void fillResultVector(std::vector& result, storm::storage::BitVector relevantStates); - - /*! - * Fills the choice values vector to the original size with zeros for ~psiState choices. - */ - void fillChoiceValuesVector(std::vector& choiceValues, storm::storage::BitVector psiStates, std::vector::index_type> rowGroupIndices); - - /*! - * Sets whether an optimal scheduler shall be constructed during the computation - */ - void setProduceScheduler(bool value); - - /*! - * @return whether an optimal scheduler shall be constructed during the computation - */ - bool isProduceSchedulerSet() const; - - storm::storage::Scheduler extractScheduler() const; - - private: - void performIterationStep(Environment const& env, storm::solver::OptimizationDirection const dir, std::vector* choices = nullptr); - - /*! - * @pre before calling this, a computation call should have been performed during which scheduler production was enabled. - * @return the produced scheduler of the most recent call. - */ - std::vector const& getProducedOptimalChoices() const; - - /*! - * @pre before calling this, a computation call should have been performed during which scheduler production was enabled. - * @return the produced scheduler of the most recent call. - */ - std::vector& getProducedOptimalChoices(); - - storm::storage::SparseMatrix _transitionMatrix; - storm::storage::BitVector _statesOfCoalition; - std::vector _x; - std::unique_ptr> _multiplier; - - bool _produceScheduler = false; - boost::optional> _producedOptimalChoices; - }; - } - } - } -} From 3f408d059c4aa8f13a68f752c19ef50aadf170be Mon Sep 17 00:00:00 2001 From: lukpo Date: Fri, 6 Aug 2021 15:43:32 +0200 Subject: [PATCH 10/21] allow boundedUntilFormulas in rpatl --- src/storm/logic/FragmentSpecification.cpp | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/storm/logic/FragmentSpecification.cpp b/src/storm/logic/FragmentSpecification.cpp index 2272ef61f..2c4f74155 100644 --- a/src/storm/logic/FragmentSpecification.cpp +++ b/src/storm/logic/FragmentSpecification.cpp @@ -110,6 +110,9 @@ namespace storm { rpatl.setGloballyFormulasAllowed(true); rpatl.setNextFormulasAllowed(true); rpatl.setBoundedGloballyFormulasAllowed(true); + rpatl.setBoundedUntilFormulasAllowed(true); + rpatl.setStepBoundedUntilFormulasAllowed(true); + rpatl.setTimeBoundedUntilFormulasAllowed(true); return rpatl; } From 44d83b9fe026392105a27a2c07e9adeecb5cce28 Mon Sep 17 00:00:00 2001 From: lukpo Date: Fri, 6 Aug 2021 15:44:17 +0200 Subject: [PATCH 11/21] added checks for bounds in computeBoundedGloballyProbabilities --- src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp index b03d89b3c..e7d3348b8 100644 --- a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp +++ b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp @@ -181,6 +181,11 @@ namespace storm { std::unique_ptr SparseSmgRpatlModelChecker::computeBoundedGloballyProbabilities(Environment const& env, CheckTask const& checkTask) { storm::logic::BoundedGloballyFormula const& pathFormula = checkTask.getFormula(); STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); + // check for upper and lower bounds + STORM_LOG_THROW(pathFormula.hasUpperBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have (a single) upper step bound."); + STORM_LOG_THROW(!pathFormula.hasLowerBound(), storm::exceptions::InvalidPropertyException, "Formulas with lower bound are not supported."); + STORM_LOG_THROW(pathFormula.hasIntegerUpperBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have discrete upper time bound."); + std::unique_ptr subResultPointer = this->check(env, pathFormula.getSubformula()); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); From 28252a3caf5f7e811beb3378d09c97de281b2ecf Mon Sep 17 00:00:00 2001 From: lukpo Date: Fri, 6 Aug 2021 15:45:05 +0200 Subject: [PATCH 12/21] added computeBoundedUntilProbabilities to SparseSmgRpatlModelChecker --- .../rpatl/SparseSmgRpatlModelChecker.cpp | 24 +++++++++++++++++++ .../rpatl/SparseSmgRpatlModelChecker.h | 1 + 2 files changed, 25 insertions(+) diff --git a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp index e7d3348b8..cf50d10e8 100644 --- a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp +++ b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp @@ -116,6 +116,8 @@ namespace storm { return this->computeNextProbabilities(env, checkTask.substituteFormula(formula.asNextFormula())); } else if (formula.isBoundedGloballyFormula()) { return this->computeBoundedGloballyProbabilities(env, checkTask.substituteFormula(formula.asBoundedGloballyFormula())); + } else if (formula.isBoundedUntilFormula()) { + return this->computeBoundedUntilProbabilities(env, checkTask.substituteFormula(formula.asBoundedUntilFormula())); } STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << formula << "' is invalid."); } @@ -197,6 +199,28 @@ namespace storm { return result; } + template + std::unique_ptr SparseSmgRpatlModelChecker::computeBoundedUntilProbabilities(Environment const& env, CheckTask const& checkTask) { + storm::logic::BoundedUntilFormula const& pathFormula = checkTask.getFormula(); + STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); + // check for upper and lower bounds + STORM_LOG_THROW(pathFormula.hasUpperBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have (a single) upper step bound."); + STORM_LOG_THROW(pathFormula.hasIntegerLowerBound(), storm::exceptions::InvalidPropertyException, "Formula lower step bound must be discrete/integral."); + STORM_LOG_THROW(pathFormula.hasIntegerUpperBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have discrete upper time bound."); + + std::unique_ptr leftResultPointer = this->check(env, pathFormula.getLeftSubformula()); + std::unique_ptr rightResultPointer = this->check(env, pathFormula.getRightSubformula()); + ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult(); + ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); + + auto ret = storm::modelchecker::helper::SparseSmgRpatlHelper::computeBoundedUntilProbabilities(env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), statesOfCoalition, checkTask.isProduceSchedulersSet(), checkTask.getHint(), pathFormula.getNonStrictLowerBound(), pathFormula.getNonStrictUpperBound()); + std::unique_ptr result(new ExplicitQuantitativeCheckResult(std::move(ret.values))); + if(checkTask.isShieldingTask()) { + tempest::shields::createShield(std::make_shared>(this->getModel()), std::move(ret.choiceValues), checkTask.getShieldingExpression(), checkTask.getOptimizationDirection(), std::move(ret.relevantStates), ~statesOfCoalition); + } + return result; + } + template std::unique_ptr SparseSmgRpatlModelChecker::computeLongRunAverageProbabilities(Environment const& env, CheckTask const& checkTask) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "NYI"); diff --git a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.h b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.h index 44b55f868..645eeb79d 100644 --- a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.h +++ b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.h @@ -41,6 +41,7 @@ namespace storm { std::unique_ptr computeGloballyProbabilities(Environment const& env, CheckTask const& checkTask) override; std::unique_ptr computeNextProbabilities(Environment const& env, CheckTask const& checkTask) override; std::unique_ptr computeBoundedGloballyProbabilities(Environment const& env, CheckTask const& checkTask) override; + std::unique_ptr computeBoundedUntilProbabilities(Environment const& env, CheckTask const& checkTask) override; std::unique_ptr computeLongRunAverageProbabilities(Environment const& env, CheckTask const& checkTask) override; std::unique_ptr computeLongRunAverageRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; From c2d2c38c2832723e844868990d704e3e99424ecc Mon Sep 17 00:00:00 2001 From: lukpo Date: Fri, 6 Aug 2021 15:47:42 +0200 Subject: [PATCH 13/21] 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); - }; } } From fefd6b0951b0ec7c13406453ab8e1e44a66c15b7 Mon Sep 17 00:00:00 2001 From: lukpo Date: Fri, 6 Aug 2021 15:49:02 +0200 Subject: [PATCH 14/21] WIP helper functions in GameViHelper --- .../rpatl/helper/internal/GameViHelper.cpp | 85 ++++++++----------- .../rpatl/helper/internal/GameViHelper.h | 28 +++--- 2 files changed, 49 insertions(+), 64 deletions(-) diff --git a/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp b/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp index 8f4800128..2426268b5 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp @@ -114,9 +114,11 @@ namespace storm { } template - void GameViHelper::performValueIterationUpperBound(Environment const& env, std::vector& x, storm::solver::OptimizationDirection const dir, uint64_t upperBound, std::vector& constrainedChoiceValues) { + 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(); @@ -125,10 +127,21 @@ namespace storm { } for (uint64_t iter = 0; iter < upperBound; iter++) { if(iter == upperBound - 1) { - _multiplier->multiply(env, _x, nullptr, constrainedChoiceValues); + STORM_LOG_DEBUG("before multipliing ..."); + STORM_LOG_DEBUG("_x = " << _x); + STORM_LOG_DEBUG("_b = " << _b); + STORM_LOG_DEBUG("constrainedChoiceValues = " << constrainedChoiceValues); + + _multiplier->multiply(env, _x, &_b, constrainedChoiceValues); + STORM_LOG_DEBUG("before multipliing ..."); + STORM_LOG_DEBUG("_x = " << _x); + STORM_LOG_DEBUG("_b = " << _b); + STORM_LOG_DEBUG("constrainedChoiceValues = " << constrainedChoiceValues); + } performIterationStepUpperBound(env, dir); } + x = _x; } @@ -140,57 +153,13 @@ namespace storm { // multiplyandreducegaussseidel // Ax = x' if (choices == nullptr) { - _multiplier->multiplyAndReduce(env, dir, _x, nullptr, _x, nullptr, &_statesOfCoalition); + _multiplier->multiplyAndReduce(env, dir, _x, &_b, _x, nullptr, &_statesOfCoalition); } else { // Also keep track of the choices made. - _multiplier->multiplyAndReduce(env, dir, _x, nullptr, _x, choices, &_statesOfCoalition); + _multiplier->multiplyAndReduce(env, dir, _x, &_b, _x, choices, &_statesOfCoalition); } } - template - void GameViHelper::fillResultVector(std::vector& result, storm::storage::BitVector relevantStates) { - std::vector filledVector = std::vector(relevantStates.size(), storm::utility::zero()); - uint bitIndex = 0; - for(uint i = 0; i < filledVector.size(); i++) { - if (relevantStates.get(i)) { - filledVector.at(i) = result.at(bitIndex); - bitIndex++; - } - } - result = filledVector; - } - - template - void GameViHelper::fillResultVector(std::vector& result, storm::storage::BitVector relevantStates, storm::storage::BitVector psiStates) { - std::vector filledVector = std::vector(relevantStates.size(), storm::utility::zero()); - uint bitIndex = 0; - for(uint i = 0; i < filledVector.size(); i++) { - if (relevantStates.get(i)) { - filledVector.at(i) = result.at(bitIndex); - bitIndex++; - } - else if (psiStates.get(i)) { - filledVector.at(i) = 1; - } - } - result = filledVector; - } - - template - void GameViHelper::fillChoiceValuesVector(std::vector& choiceValues, storm::storage::BitVector psiStates, std::vector::index_type> rowGroupIndices) { - std::vector allChoices = std::vector(rowGroupIndices.at(rowGroupIndices.size() - 1), storm::utility::zero()); - auto choice_it = choiceValues.begin(); - for(uint state = 0; state < rowGroupIndices.size() - 1; state++) { - uint rowGroupSize = rowGroupIndices[state + 1] - rowGroupIndices[state]; - if (psiStates.get(state)) { - for(uint choice = 0; choice < rowGroupSize; choice++, choice_it++) { - allChoices.at(rowGroupIndices.at(state) + choice) = *choice_it; - } - } - } - choiceValues = allChoices; - } - template void GameViHelper::setProduceScheduler(bool value) { _produceScheduler = value; @@ -201,6 +170,11 @@ namespace storm { return _produceScheduler; } + template + void GameViHelper::updateTransitionMatrix(storm::storage::SparseMatrix newTransitionMatrix) { + _transitionMatrix = newTransitionMatrix; + } + template std::vector const& GameViHelper::getProducedOptimalChoices() const { STORM_LOG_ASSERT(this->isProduceSchedulerSet(), "Trying to get the produced optimal choices although no scheduler was requested."); @@ -230,6 +204,21 @@ namespace storm { _multiplier->multiply(env, x, &_b, choiceValues); } + template + void GameViHelper::fillChoiceValuesVector(std::vector& choiceValues, storm::storage::BitVector psiStates, std::vector::index_type> rowGroupIndices) { + std::vector allChoices = std::vector(rowGroupIndices.at(rowGroupIndices.size() - 1), storm::utility::zero()); + auto choice_it = choiceValues.begin(); + for(uint state = 0; state < rowGroupIndices.size() - 1; state++) { + uint rowGroupSize = rowGroupIndices[state + 1] - rowGroupIndices[state]; + if (psiStates.get(state)) { + for(uint choice = 0; choice < rowGroupSize; choice++, choice_it++) { + allChoices.at(rowGroupIndices.at(state) + choice) = *choice_it; + } + } + } + choiceValues = allChoices; + } + template std::vector& GameViHelper::xNew() { return _x1IsCurrent ? _x1 : _x2; diff --git a/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.h b/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.h index 2d1b1538a..8f2c8143f 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.h +++ b/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.h @@ -31,22 +31,7 @@ namespace storm { /*! * Perform value iteration until upper bound */ - void performValueIterationUpperBound(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 zeros for all states except the relevantStates - */ - void fillResultVector(std::vector& result, storm::storage::BitVector relevantStates); - - /*! - * Fills the result vector to the original size with ones for being psiStates, zeros for being not phiStates - */ - void fillResultVector(std::vector& result, storm::storage::BitVector relevantStates, storm::storage::BitVector psiStates); - - /*! - * Fills the choice values vector to the original size with zeros for ~psiState choices. - */ - void fillChoiceValuesVector(std::vector& choiceValues, storm::storage::BitVector psiStates, std::vector::index_type> rowGroupIndices); + void performValueIterationUpperBound(Environment const& env, std::vector& x, std::vector b, storm::solver::OptimizationDirection const dir, uint64_t upperBound, std::vector& constrainedChoiceValues); /*! * Sets whether an optimal scheduler shall be constructed during the computation @@ -58,9 +43,20 @@ namespace storm { */ bool isProduceSchedulerSet() const; + /*! + * Changes the transitionMatrix of the gameViHelper to the given one. + */ + void updateTransitionMatrix(storm::storage::SparseMatrix newTransitionMatrix); + storm::storage::Scheduler extractScheduler() const; void getChoiceValues(Environment const& env, std::vector const& x, std::vector& choiceValues); + + /*! + * Fills the choice values vector to the original size with zeros for ~psiState choices. + */ + void fillChoiceValuesVector(std::vector& choiceValues, storm::storage::BitVector psiStates, std::vector::index_type> rowGroupIndices); + private: /*! * Performs one iteration step for value iteration From 03ec53321ec1b82f9b02e48573dbe8570d039e46 Mon Sep 17 00:00:00 2001 From: lukpo Date: Mon, 9 Aug 2021 15:24:58 +0200 Subject: [PATCH 15/21] added updateStatesOfCoalition to GameViHelper --- .../modelchecker/rpatl/helper/internal/GameViHelper.cpp | 5 +++++ .../modelchecker/rpatl/helper/internal/GameViHelper.h | 7 ++++++- 2 files changed, 11 insertions(+), 1 deletion(-) diff --git a/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp b/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp index 2426268b5..96a2e0c81 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp @@ -175,6 +175,11 @@ namespace storm { _transitionMatrix = newTransitionMatrix; } + template + void GameViHelper::updateStatesOfCoaltion(storm::storage::BitVector newStatesOfCoaltion) { + _statesOfCoalition = newStatesOfCoaltion; + } + template std::vector const& GameViHelper::getProducedOptimalChoices() const { STORM_LOG_ASSERT(this->isProduceSchedulerSet(), "Trying to get the produced optimal choices although no scheduler was requested."); diff --git a/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.h b/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.h index 8f2c8143f..393f8a79a 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.h +++ b/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.h @@ -44,10 +44,15 @@ namespace storm { bool isProduceSchedulerSet() const; /*! - * Changes the transitionMatrix of the gameViHelper to the given one. + * Changes the transitionMatrix to the given one. */ void updateTransitionMatrix(storm::storage::SparseMatrix newTransitionMatrix); + /*! + * Changes the statesOfCoalition to the given one. + */ + void updateStatesOfCoaltion(storm::storage::BitVector newStatesOfCoaltion); + storm::storage::Scheduler extractScheduler() const; void getChoiceValues(Environment const& env, std::vector const& x, std::vector& choiceValues); From 9fea23981a575579f23a4974e6f785d8ad60f151 Mon Sep 17 00:00:00 2001 From: lukpo Date: Mon, 9 Aug 2021 15:25:47 +0200 Subject: [PATCH 16/21] finished computeBoundedUntilProbability in SparseSmgRpatlHelper --- .../rpatl/helper/SparseSmgRpatlHelper.cpp | 114 ++++++------------ 1 file changed, 38 insertions(+), 76 deletions(-) diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp index 9c302052f..9237e46b9 100644 --- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp @@ -22,19 +22,13 @@ namespace storm { // 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); @@ -177,31 +171,18 @@ namespace storm { 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); + // boundedUntil formulas look like: + // phi U [lowerBound, upperBound] psi + // -- + // We solve this by look at psiStates, finding phiStates which have paths to psiStates in the given step bounds, + // then we find all states which have a path to those phiStates in the given lower bound + // (which states the paths pass before the lower bound does not matter). + + // First initialization of relevantStates between the step bounds. 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()); @@ -212,65 +193,47 @@ namespace storm { storm::storage::BitVector clippedStatesOfCoalition(relevantStates.getNumberOfSetBits()); clippedStatesOfCoalition.setClippedStatesOfCoalition(relevantStates, statesOfCoalition); - //clippedStatesOfCoalition.complement(); - STORM_LOG_DEBUG(clippedStatesOfCoalition); + // If there are no relevantStates or the upperBound is 0, no computation is needed. 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); + // Reduce the matrix to relevant states. - relevant states are all 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); } + // If the lowerBound = 0, value iteration is done until the upperBound. 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); + // The lowerBound != 0, the first computation between the given bound steps is done. + viHelper.performValueIterationUpperBound(env, x, b, goal.direction(), upperBound - lowerBound, 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()); + storm::utility::vector::setVectorValues(subResult, relevantStates, x); + storm::utility::vector::setVectorValues(subResult, psiStates, storm::utility::one()); + + // The newPsiStates are those states which can reach the psiStates in the steps between the bounds - the !=0 values in subResult. + storm::storage::BitVector newPsiStates(subResult.size(), false); + storm::utility::vector::setNonzeroIndices(subResult, newPsiStates); + + // The relevantStates for the second part of the computation are all states. + relevantStates = storm::storage::BitVector(phiStates.size(), true); submatrix = transitionMatrix.getSubmatrix(true, relevantStates, relevantStates, false); + + // Update the viHelper for the (full-size) submatrix and statesOfCoalition. viHelper.updateTransitionMatrix(submatrix); - b = std::vector(b.size(), storm::utility::zero()); - viHelper.performValueIterationUpperBound(env, x, b, goal.direction(), lowerBound - 1, constrainedChoiceValues); -*/ + viHelper.updateStatesOfCoaltion(statesOfCoalition); + // Reset constrainedChoiceValues and b to 0-vector in the correct dimension. + constrainedChoiceValues = std::vector(transitionMatrix.getConstrainedRowGroupSumVector(relevantStates, newPsiStates).size(), storm::utility::zero()); + 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); + x = subResult; } viHelper.fillChoiceValuesVector(constrainedChoiceValues, relevantStates, transitionMatrix.getRowGroupIndices()); if (produceScheduler) { @@ -278,9 +241,8 @@ namespace storm { } storm::utility::vector::setVectorValues(result, relevantStates, x); } - if(lowerBound == 0) { - storm::utility::vector::setVectorValues(result, psiStates, storm::utility::one()); - } + + 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)); } From 4373c324f916ac223e55023d211301efa41dbf42 Mon Sep 17 00:00:00 2001 From: lukpo Date: Mon, 9 Aug 2021 15:42:50 +0200 Subject: [PATCH 17/21] checks for bounds in SparseSmgRpatlModelChecker --- .../modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp index cf50d10e8..97ddffabd 100644 --- a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp +++ b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp @@ -183,10 +183,10 @@ namespace storm { std::unique_ptr SparseSmgRpatlModelChecker::computeBoundedGloballyProbabilities(Environment const& env, CheckTask const& checkTask) { storm::logic::BoundedGloballyFormula const& pathFormula = checkTask.getFormula(); STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); - // check for upper and lower bounds + // checks for bounds STORM_LOG_THROW(pathFormula.hasUpperBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have (a single) upper step bound."); STORM_LOG_THROW(!pathFormula.hasLowerBound(), storm::exceptions::InvalidPropertyException, "Formulas with lower bound are not supported."); - STORM_LOG_THROW(pathFormula.hasIntegerUpperBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have discrete upper time bound."); + STORM_LOG_THROW(pathFormula.hasIntegerUpperBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have discrete upper bound."); std::unique_ptr subResultPointer = this->check(env, pathFormula.getSubformula()); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); @@ -203,10 +203,10 @@ namespace storm { std::unique_ptr SparseSmgRpatlModelChecker::computeBoundedUntilProbabilities(Environment const& env, CheckTask const& checkTask) { storm::logic::BoundedUntilFormula const& pathFormula = checkTask.getFormula(); STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); - // check for upper and lower bounds + // checks for bounds STORM_LOG_THROW(pathFormula.hasUpperBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have (a single) upper step bound."); - STORM_LOG_THROW(pathFormula.hasIntegerLowerBound(), storm::exceptions::InvalidPropertyException, "Formula lower step bound must be discrete/integral."); - STORM_LOG_THROW(pathFormula.hasIntegerUpperBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have discrete upper time bound."); + STORM_LOG_THROW(pathFormula.hasIntegerLowerBound(), storm::exceptions::InvalidPropertyException, "Formula lower step bound must be discrete."); + STORM_LOG_THROW(pathFormula.hasIntegerUpperBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have discrete upper bound."); std::unique_ptr leftResultPointer = this->check(env, pathFormula.getLeftSubformula()); std::unique_ptr rightResultPointer = this->check(env, pathFormula.getRightSubformula()); From 86c3b3d9c675164119403f8b9c79c707811f4597 Mon Sep 17 00:00:00 2001 From: lukpo Date: Tue, 10 Aug 2021 09:27:54 +0200 Subject: [PATCH 18/21] 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); From 679279a33909280099a385176855688221356e23 Mon Sep 17 00:00:00 2001 From: Stefan Pranger Date: Fri, 3 Sep 2021 14:56:30 +0200 Subject: [PATCH 19/21] By changing the computation we now allow lowerBounds in bounded-globally formulas Conflicts: src/storm-parsers/parser/FormulaParserGrammar.cpp --- .../parser/FormulaParserGrammar.cpp | 16 ++++++++++++++-- .../rpatl/SparseSmgRpatlModelChecker.cpp | 6 +++--- 2 files changed, 17 insertions(+), 5 deletions(-) diff --git a/src/storm-parsers/parser/FormulaParserGrammar.cpp b/src/storm-parsers/parser/FormulaParserGrammar.cpp index aa07a7961..13b56d8a9 100644 --- a/src/storm-parsers/parser/FormulaParserGrammar.cpp +++ b/src/storm-parsers/parser/FormulaParserGrammar.cpp @@ -386,8 +386,20 @@ namespace storm { } } - std::shared_ptr FormulaParserGrammar::createGloballyFormula(std::shared_ptr const& subformula) const { - return std::shared_ptr(new storm::logic::GloballyFormula(subformula)); + std::shared_ptr FormulaParserGrammar::createGloballyFormula(boost::optional, boost::optional, std::shared_ptr>>> const& timeBounds, std::shared_ptr const& subformula) const { + if (timeBounds && !timeBounds.get().empty()) { + std::vector> lowerBounds, upperBounds; + std::vector timeBoundReferences; + for (auto const& timeBound : timeBounds.get()) { + STORM_LOG_ASSERT(!std::get<0>(timeBound), "Cannot use lower time bounds (or intervals) in globally formulas."); + lowerBounds.push_back(std::get<0>(timeBound)); + upperBounds.push_back(std::get<1>(timeBound)); + timeBoundReferences.emplace_back(*std::get<2>(timeBound)); + } + return std::shared_ptr(new storm::logic::BoundedGloballyFormula(subformula, lowerBounds, upperBounds, timeBoundReferences)); + } else { + return std::shared_ptr(new storm::logic::GloballyFormula(subformula)); + } } std::shared_ptr FormulaParserGrammar::createNextFormula(std::shared_ptr const& subformula) const { diff --git a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp index 97ddffabd..bf04dc000 100644 --- a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp +++ b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp @@ -185,8 +185,8 @@ namespace storm { STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); // checks for bounds STORM_LOG_THROW(pathFormula.hasUpperBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have (a single) upper step bound."); - STORM_LOG_THROW(!pathFormula.hasLowerBound(), storm::exceptions::InvalidPropertyException, "Formulas with lower bound are not supported."); - STORM_LOG_THROW(pathFormula.hasIntegerUpperBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have discrete upper bound."); + STORM_LOG_THROW(pathFormula.hasIntegerLowerBound(), storm::exceptions::InvalidPropertyException, "Formula lower step bound must be discrete."); + STORM_LOG_THROW(pathFormula.hasIntegerUpperBound(), storm::exceptions::InvalidPropertyException, "Formula upper step bound must be discrete."); std::unique_ptr subResultPointer = this->check(env, pathFormula.getSubformula()); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); @@ -206,7 +206,7 @@ namespace storm { // checks for bounds STORM_LOG_THROW(pathFormula.hasUpperBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have (a single) upper step bound."); STORM_LOG_THROW(pathFormula.hasIntegerLowerBound(), storm::exceptions::InvalidPropertyException, "Formula lower step bound must be discrete."); - STORM_LOG_THROW(pathFormula.hasIntegerUpperBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have discrete upper bound."); + STORM_LOG_THROW(pathFormula.hasIntegerUpperBound(), storm::exceptions::InvalidPropertyException, "Formula upper step bound must be discrete."); std::unique_ptr leftResultPointer = this->check(env, pathFormula.getLeftSubformula()); std::unique_ptr rightResultPointer = this->check(env, pathFormula.getRightSubformula()); From fb84fc6af0ccd50344438c75bed484cb56ddaa39 Mon Sep 17 00:00:00 2001 From: lukpo Date: Tue, 10 Aug 2021 10:14:12 +0200 Subject: [PATCH 20/21] Added a comment why this computeBoundedGlobally check happens. --- src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp index e28d591e0..527bb07e0 100644 --- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp @@ -218,6 +218,7 @@ 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. if(!computeBoundedGlobally){ storm::utility::vector::setVectorValues(result, psiStates, storm::utility::one()); } From 1391b26e93611b315fdc880e9b139c1126ad99c0 Mon Sep 17 00:00:00 2001 From: lukpo Date: Tue, 10 Aug 2021 10:25:46 +0200 Subject: [PATCH 21/21] Removed unnecessary debug information --- .../rpatl/helper/SparseSmgRpatlHelper.cpp | 14 -------------- .../rpatl/helper/internal/GameViHelper.cpp | 10 ---------- 2 files changed, 24 deletions(-) diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp index 527bb07e0..85a08ea96 100644 --- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp @@ -32,11 +32,6 @@ namespace storm { storm::storage::BitVector clippedStatesOfCoalition(relevantStates.getNumberOfSetBits()); clippedStatesOfCoalition.setClippedStatesOfCoalition(relevantStates, statesOfCoalition); - 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); @@ -57,11 +52,9 @@ namespace storm { scheduler = std::make_unique>(expandScheduler(viHelper.extractScheduler(), psiStates, ~phiStates)); } } - // 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)); } @@ -91,7 +84,6 @@ 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) { @@ -100,7 +92,6 @@ namespace storm { for (auto& element : result.choiceValues) { element = storm::utility::one() - element; } - STORM_LOG_DEBUG(result.values); return result; } @@ -112,7 +103,6 @@ namespace storm { 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."); @@ -123,7 +113,6 @@ namespace storm { if (goal.isShieldingTask()) { choiceValues = b; } - STORM_LOG_DEBUG(result); return SMGSparseModelCheckingHelperReturnType(std::move(result), std::move(allStates), nullptr, std::move(choiceValues)); } @@ -141,7 +130,6 @@ namespace storm { for (auto& element : result.choiceValues) { element = storm::utility::one() - element; } - STORM_LOG_DEBUG(result.values); return result; } @@ -217,12 +205,10 @@ 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. 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/internal/GameViHelper.cpp b/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp index 96a2e0c81..4ddadc247 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp @@ -127,17 +127,7 @@ namespace storm { } for (uint64_t iter = 0; iter < upperBound; iter++) { if(iter == upperBound - 1) { - STORM_LOG_DEBUG("before multipliing ..."); - STORM_LOG_DEBUG("_x = " << _x); - STORM_LOG_DEBUG("_b = " << _b); - STORM_LOG_DEBUG("constrainedChoiceValues = " << constrainedChoiceValues); - _multiplier->multiply(env, _x, &_b, constrainedChoiceValues); - STORM_LOG_DEBUG("before multipliing ..."); - STORM_LOG_DEBUG("_x = " << _x); - STORM_LOG_DEBUG("_b = " << _b); - STORM_LOG_DEBUG("constrainedChoiceValues = " << constrainedChoiceValues); - } performIterationStepUpperBound(env, dir); }