diff --git a/src/storm/logic/FragmentSpecification.cpp b/src/storm/logic/FragmentSpecification.cpp index 648dd2bf0..1e7e1f357 100644 --- a/src/storm/logic/FragmentSpecification.cpp +++ b/src/storm/logic/FragmentSpecification.cpp @@ -67,6 +67,7 @@ namespace storm { rpatl.setReachabilityProbabilityFormulasAllowed(true); rpatl.setUntilFormulasAllowed(true); rpatl.setGloballyFormulasAllowed(true); + rpatl.setNextFormulasAllowed(true); return rpatl; } diff --git a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp index bc20aadec..767df179e 100644 --- a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp +++ b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp @@ -114,6 +114,8 @@ namespace storm { return this->computeUntilProbabilities(env, checkTask.substituteFormula(formula.asUntilFormula())); } else if (formula.isGloballyFormula()) { return this->computeGloballyProbabilities(env, checkTask.substituteFormula(formula.asGloballyFormula())); + } else if (formula.isNextFormula()) { + return this->computeNextProbabilities(env, checkTask.substituteFormula(formula.asNextFormula())); } STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << formula << "' is invalid."); } @@ -136,7 +138,6 @@ namespace storm { std::unique_ptr rightResultPointer = this->check(env, pathFormula.getRightSubformula()); ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult(); ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); - storm::solver::SolveGoal foo(this->getModel(), checkTask); auto ret = storm::modelchecker::helper::SparseSmgRpatlHelper::computeUntilProbabilities(env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), statesOfCoalition, checkTask.isProduceSchedulersSet(), checkTask.getHint()); std::unique_ptr result(new ExplicitQuantitativeCheckResult(std::move(ret.values))); @@ -160,7 +161,19 @@ namespace storm { return result; } - template + template + std::unique_ptr SparseSmgRpatlModelChecker::computeNextProbabilities(Environment const& env, CheckTask const& checkTask) { + storm::logic::NextFormula 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."); + std::unique_ptr subResultPointer = this->check(env, pathFormula.getSubformula()); + ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); + + auto ret = storm::modelchecker::helper::SparseSmgRpatlHelper::computeNextProbabilities(env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), statesOfCoalition, checkTask.isProduceSchedulersSet(), checkTask.getHint()); + std::unique_ptr result(new ExplicitQuantitativeCheckResult(std::move(ret.values))); + 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 4b1dc2547..28b25f9e6 100644 --- a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.h +++ b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.h @@ -38,6 +38,8 @@ namespace storm { std::unique_ptr computeUntilProbabilities(Environment const& env, CheckTask const& checkTask) override; 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 computeLongRunAverageProbabilities(Environment const& env, CheckTask const& checkTask) override; std::unique_ptr computeLongRunAverageRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp index ff8d213af..079a193a6 100644 --- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp @@ -85,6 +85,37 @@ namespace storm { return result; } + template + MDPSparseModelCheckingHelperReturnType 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) { + + auto solverEnv = env; + solverEnv.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration, false); + + // Initialize the solution vector. + std::vector x = std::vector(transitionMatrix.getRowGroupCount(), storm::utility::zero()); + + auto allStates = storm::storage::BitVector(transitionMatrix.getRowGroupCount(), true); + + std::vector b = transitionMatrix.getConstrainedRowGroupSumVector(allStates, psiStates); + + storm::storage::BitVector clippedStatesOfCoalition(transitionMatrix.getRowGroupCount()); + clippedStatesOfCoalition.setClippedStatesOfCoalition(allStates, statesOfCoalition); + clippedStatesOfCoalition.complement(); + + storm::modelchecker::helper::internal::GameViHelper viHelper(transitionMatrix, clippedStatesOfCoalition); + std::unique_ptr> scheduler; + if (produceScheduler) { + viHelper.setProduceScheduler(true); + } + + viHelper.performNextIteration(env, x, b, goal.direction()); + + if (produceScheduler) { + scheduler = std::make_unique>(expandScheduler(viHelper.extractScheduler(), psiStates, ~allStates)); + } + return MDPSparseModelCheckingHelperReturnType(std::move(x), std::move(scheduler)); + } + template class SparseSmgRpatlHelper; #ifdef STORM_HAVE_CARL template class SparseSmgRpatlHelper; diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.h b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.h index 68dee01fb..119eec84a 100644 --- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.h +++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.h @@ -38,6 +38,7 @@ namespace storm { static MDPSparseModelCheckingHelperReturnType computeUntilProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint = ModelCheckerHint()); static MDPSparseModelCheckingHelperReturnType computeGloballyProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint = ModelCheckerHint()); + static MDPSparseModelCheckingHelperReturnType computeNextProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint); private: static storm::storage::Scheduler expandScheduler(storm::storage::Scheduler scheduler, storm::storage::BitVector psiStates, storm::storage::BitVector notPhiStates); diff --git a/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp b/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp index 8c354d945..e0c18d179 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp @@ -151,6 +151,31 @@ namespace storm { } template + void GameViHelper::performNextIteration(Environment const& env, std::vector& x, std::vector b, storm::solver::OptimizationDirection const dir) { + prepareSolversAndMultipliersReachability(env); + 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; + + if (this->isProduceSchedulerSet()) { + if (!this->_producedOptimalChoices.is_initialized()) { + this->_producedOptimalChoices.emplace(); + } + this->_producedOptimalChoices->resize(this->_transitionMatrix.getRowGroupCount()); + } + + if (isProduceSchedulerSet()) { + performIterationStep(env, dir, &_producedOptimalChoices.get()); + } else + performIterationStep(env, dir); + + x = xNew(); + } + + template void GameViHelper::setProduceScheduler(bool value) { _produceScheduler = value; } diff --git a/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.h b/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.h index f3e353665..d67c090de 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.h +++ b/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.h @@ -30,6 +30,8 @@ namespace storm { */ void fillResultVector(std::vector& result, storm::storage::BitVector relevantStates, storm::storage::BitVector psiStates); + void performNextIteration(Environment const& env, std::vector& x, std::vector b, storm::solver::OptimizationDirection const dir); + /*h * Sets whether an optimal scheduler shall be constructed during the computation */ @@ -41,6 +43,7 @@ namespace storm { bool isProduceSchedulerSet() const; storm::storage::Scheduler extractScheduler() const; + private: void performIterationStep(Environment const& env, storm::solver::OptimizationDirection const dir, std::vector* choices = nullptr);