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/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; } diff --git a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp index 1668bc440..bf04dc000 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; } @@ -122,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."); } @@ -187,6 +183,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."); + // 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 upper step bound must be discrete."); + std::unique_ptr subResultPointer = this->check(env, pathFormula.getSubformula()); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); @@ -198,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."); + // 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 upper step bound must be discrete."); + + 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"); @@ -216,7 +239,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..645eeb79d 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; @@ -40,11 +41,11 @@ 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; - //void coalitionIndicator(Environment& env, CheckTask const& checkTask); private: storm::storage::BitVector statesOfCoalition; }; diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp index 78d554346..85a08ea96 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,38 +19,43 @@ 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; + // Initialize the x vector and solution vector result. + 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()); - - // Reduce the matrix to relevant states - storm::storage::SparseMatrix submatrix = transitionMatrix.getSubmatrix(true, relevantStates, relevantStates, false); + std::unique_ptr> scheduler; 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); - } + if(!relevantStates.empty()) { + // 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); + } + 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); - } - viHelper.fillResultVector(x, relevantStates, psiStates); - viHelper.fillChoiceValuesVector(constrainedChoiceValues, relevantStates, transitionMatrix.getRowGroupIndices()); + // Fill up the constrainedChoice Values to full size. + viHelper.fillChoiceValuesVector(constrainedChoiceValues, relevantStates, transitionMatrix.getRowGroupIndices()); - 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()); + return SMGSparseModelCheckingHelperReturnType(std::move(result), std::move(relevantStates), std::move(scheduler), std::move(constrainedChoiceValues)); } template @@ -75,11 +80,11 @@ 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); for (auto& element : result.values) { element = storm::utility::one() - element; @@ -92,71 +97,119 @@ 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 - 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(); 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(), result, &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)); + return SMGSparseModelCheckingHelperReturnType(std::move(result), std::move(allStates), nullptr, std::move(choiceValues)); } 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) { + // 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(); + + 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; + } + for (auto& element : result.choiceValues) { + element = storm::utility::one() - element; + } + 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, bool computeBoundedGlobally) { auto solverEnv = env; solverEnv.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration, false); - // Relevant states are safe states - the psiStates. - storm::storage::BitVector relevantStates = psiStates; + // 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). - // 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); + // First initialization of relevantStates between the step bounds. + storm::storage::BitVector relevantStates = phiStates & ~psiStates; - std::vector constrainedChoiceValues = std::vector(submatrix.getRowCount(), storm::utility::zero()); + // 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; 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); - } + // 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); + // 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) { + viHelper.performValueIterationUpperBound(env, x, b, goal.direction(), upperBound, constrainedChoiceValues); + } else { + // The lowerBound != 0, the first computation between the given bound steps is done. + viHelper.performValueIterationUpperBound(env, x, b, goal.direction(), upperBound - lowerBound, constrainedChoiceValues); - // in case of upperBound = 0 the states which are initially "safe" are filled with ones - if(upperBound > 0) - { - viHelper.performValueIteration(env, x, goal.direction(), upperBound, constrainedChoiceValues); - } - viHelper.fillChoiceValuesVector(constrainedChoiceValues, relevantStates, transitionMatrix.getRowGroupIndices()); + // 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()); - viHelper.fillResultVector(x, relevantStates); - viHelper.fillChoiceValuesVector(constrainedChoiceValues, relevantStates, transitionMatrix.getRowGroupIndices()); + // 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); - if (produceScheduler) { - scheduler = std::make_unique>(expandScheduler(viHelper.extractScheduler(), relevantStates, ~relevantStates)); - } + // 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); - return SMGSparseModelCheckingHelperReturnType(std::move(x), std::move(relevantStates), std::move(scheduler), std::move(constrainedChoiceValues)); + // Update the viHelper for the (full-size) submatrix and statesOfCoalition. + viHelper.updateTransitionMatrix(submatrix); + 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) { + scheduler = std::make_unique>(expandScheduler(viHelper.extractScheduler(), relevantStates, ~relevantStates)); + } + 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()); + } + 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..0592c929b 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, 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); - }; } } 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 33bb6dfe2..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 psiStates) - { - std::vector filledVector = std::vector(psiStates.size(), storm::utility::zero()); - uint bitIndex = 0; - for(uint i = 0; i < filledVector.size(); i++) { - if (psiStates.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 78d499265..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 ones for being psiStates, zeros for being not phiStates - */ - void fillResultVector(std::vector& result, 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); - - /*! - * 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; - }; - } - } - } -} diff --git a/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp b/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp index 58a42a397..4ddadc247 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; @@ -114,34 +114,40 @@ namespace storm { } 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++; + 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(); } - else if (psiStates.get(i)) { - filledVector.at(i) = 1; + this->_producedOptimalChoices->resize(this->_transitionMatrix.getRowGroupCount()); + } + for (uint64_t iter = 0; iter < upperBound; iter++) { + if(iter == upperBound - 1) { + _multiplier->multiply(env, _x, &_b, constrainedChoiceValues); } + performIterationStepUpperBound(env, dir); } - result = filledVector; + + x = _x; } 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; - } - } + void GameViHelper::performIterationStepUpperBound(Environment const& env, storm::solver::OptimizationDirection const dir, std::vector* choices) { + if (!_multiplier) { + prepareSolversAndMultipliers(env); + } + // multiplyandreducegaussseidel + // Ax = x' + if (choices == nullptr) { + _multiplier->multiplyAndReduce(env, dir, _x, &_b, _x, nullptr, &_statesOfCoalition); + } else { + // Also keep track of the choices made. + _multiplier->multiplyAndReduce(env, dir, _x, &_b, _x, choices, &_statesOfCoalition); } - choiceValues = allChoices; } template @@ -154,6 +160,16 @@ namespace storm { return _produceScheduler; } + template + void GameViHelper::updateTransitionMatrix(storm::storage::SparseMatrix newTransitionMatrix) { + _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."); @@ -183,6 +199,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 00eca9fe6..393f8a79a 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.h +++ b/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.h @@ -23,17 +23,15 @@ namespace storm { void prepareSolversAndMultipliers(const Environment& env); - void performValueIteration(Environment const& env, std::vector& x, std::vector b, storm::solver::OptimizationDirection const dir); - /*! - * Fills the result vector to the original size with ones for being psiStates, zeros for being not phiStates + * Perform value iteration until convergence */ - void fillResultVector(std::vector& result, storm::storage::BitVector relevantStates, storm::storage::BitVector psiStates); + void performValueIteration(Environment const& env, std::vector& x, std::vector b, storm::solver::OptimizationDirection const dir); /*! - * Fills the choice values vector to the original size with zeros for ~psiState choices. + * Perform value iteration until upper bound */ - 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 @@ -45,12 +43,36 @@ namespace storm { */ bool isProduceSchedulerSet() const; + /*! + * 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); + + /*! + * 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 + */ 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 +99,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;