diff --git a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp index 9239f0578..7fa177d2c 100644 --- a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp +++ b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp @@ -143,7 +143,28 @@ namespace storm { ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult(); ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); - auto ret = storm::modelchecker::helper::SparseSmgRpatlHelper::computeUntilProbabilitiesSound(env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), statesOfCoalition, checkTask.isProduceSchedulersSet(), checkTask.getHint()); + if (env.solver().isForceSoundness()) { + auto ret = storm::modelchecker::helper::SparseSmgRpatlHelper::computeUntilProbabilitiesSound( + 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))); + if(checkTask.isShieldingTask()) { + storm::storage::BitVector allStatesBv = storm::storage::BitVector(this->getModel().getTransitionMatrix().getRowGroupCount(), true); + auto shield = tempest::shields::createShield(std::make_shared>(this->getModel()), std::move(ret.choiceValues), checkTask.getShieldingExpression(), checkTask.getOptimizationDirection(), allStatesBv, ~statesOfCoalition); + result->asExplicitQuantitativeCheckResult().setShield(std::move(shield)); + } + if (checkTask.isProduceSchedulersSet() && ret.scheduler) { + result->asExplicitQuantitativeCheckResult().setScheduler(std::move(ret.scheduler)); + } + return result; + } + + 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()); STORM_LOG_DEBUG(ret.values); std::unique_ptr result(new ExplicitQuantitativeCheckResult(std::move(ret.values))); if(checkTask.isShieldingTask()) { @@ -241,12 +262,28 @@ namespace storm { template std::unique_ptr SparseSmgRpatlModelChecker::computeLongRunAverageRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { auto rewardModel = storm::utility::createFilteredRewardModel(this->getModel(), checkTask); - storm::modelchecker::helper::internal::SparseSmgLraHelper helper(this->getModel().getTransitionMatrix(), statesOfCoalition); - storm::modelchecker::helper::setInformationFromCheckTaskNondeterministic(helper, checkTask, this->getModel()); - auto values = helper.computeLongRunAverageRewardsSound(env, rewardModel.get()); + if (env.solver().isForceSoundness()) { + storm::modelchecker::helper::internal::SparseSmgLraHelper helper(this->getModel().getTransitionMatrix(), statesOfCoalition); + auto values = helper.computeLongRunAverageRewardsSound(env, rewardModel.get()); + storm::modelchecker::helper::setInformationFromCheckTaskNondeterministic(helper, checkTask, this->getModel()); + std::unique_ptr result(new ExplicitQuantitativeCheckResult(std::move(values))); + + if(checkTask.isShieldingTask()) { + storm::storage::BitVector allStatesBv = storm::storage::BitVector(this->getModel().getTransitionMatrix().getRowGroupCount(), true); + auto shield = tempest::shields::createQuantitativeShield(std::make_shared>(this->getModel()), helper.getChoiceValues(), checkTask.getShieldingExpression(), checkTask.getOptimizationDirection(), allStatesBv, statesOfCoalition); + result->asExplicitQuantitativeCheckResult().setShield(std::move(shield)); + } + if (checkTask.isProduceSchedulersSet()) { + result->asExplicitQuantitativeCheckResult().setScheduler(std::make_unique>(helper.extractScheduler())); + } + return result; + } + + storm::modelchecker::helper::SparseNondeterministicGameInfiniteHorizonHelper helper(this->getModel().getTransitionMatrix(), statesOfCoalition); + auto values = helper.computeLongRunAverageRewards(env, rewardModel.get()); + storm::modelchecker::helper::setInformationFromCheckTaskNondeterministic(helper, checkTask, this->getModel()); std::unique_ptr result(new ExplicitQuantitativeCheckResult(std::move(values))); - /* if(checkTask.isShieldingTask()) { storm::storage::BitVector allStatesBv = storm::storage::BitVector(this->getModel().getTransitionMatrix().getRowGroupCount(), true); auto shield = tempest::shields::createQuantitativeShield(std::make_shared>(this->getModel()), helper.getChoiceValues(), checkTask.getShieldingExpression(), checkTask.getOptimizationDirection(), allStatesBv, statesOfCoalition); @@ -255,7 +292,6 @@ namespace storm { if (checkTask.isProduceSchedulersSet()) { result->asExplicitQuantitativeCheckResult().setScheduler(std::make_unique>(helper.extractScheduler())); } - */ return result; } diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp index ddf04ea90..e2a349a50 100644 --- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp @@ -61,13 +61,10 @@ namespace storm { template SMGSparseModelCheckingHelperReturnType SparseSmgRpatlHelper::computeUntilProbabilitiesSound(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) { - storm::storage::BitVector probGreater0 = storm::utility::graph::performProbGreater0(backwardTransitions, phiStates, psiStates); std::unique_ptr> scheduler; storm::storage::BitVector relevantStates = phiStates; - storm::storage::SparseMatrix submatrix = transitionMatrix.getSubmatrix(true, relevantStates, relevantStates, false); - // Initialize the x vector and solution vector result. std::vector xL = std::vector(transitionMatrix.getRowGroupCount(), storm::utility::zero()); // assigning 1s to the xL vector for all Goal states @@ -112,19 +109,24 @@ namespace storm { clippedStatesOfCoalition.setClippedStatesOfCoalition(relevantStates, statesOfCoalition); std::vector constrainedChoiceValues = std::vector(b.size(), storm::utility::zero()); - storm::modelchecker::helper::internal::SoundGameViHelper viHelper(submatrix, submatrix.transpose(), b, clippedStatesOfCoalition, clippedPsiStates, goal.direction()); + if (!relevantStates.empty()) { + storm::storage::SparseMatrix submatrix = transitionMatrix.getSubmatrix(true, relevantStates, relevantStates, false); + storm::modelchecker::helper::internal::SoundGameViHelper viHelper(submatrix, submatrix.transpose(), b, clippedStatesOfCoalition, + clippedPsiStates, goal.direction()); - if (produceScheduler) { - viHelper.setProduceScheduler(true); - } + if (produceScheduler) { + viHelper.setProduceScheduler(true); + } - viHelper.performValueIteration(env, xL, xU, goal.direction(), constrainedChoiceValues); + viHelper.performValueIteration(env, xL, xU, goal.direction(), constrainedChoiceValues); - viHelper.fillChoiceValuesVector(constrainedChoiceValues, relevantStates, transitionMatrix.getRowGroupIndices()); - storm::utility::vector::setVectorValues(result, relevantStates, xL); + viHelper.fillChoiceValuesVector(constrainedChoiceValues, relevantStates, transitionMatrix.getRowGroupIndices()); + storm::utility::vector::setVectorValues(result, relevantStates, xL); - if (produceScheduler) { - scheduler = std::make_unique>(expandScheduler(viHelper.extractScheduler(), psiStates, ~phiStates)); + if (produceScheduler) { + scheduler = + std::make_unique>(expandScheduler(viHelper.extractScheduler(), psiStates, ~phiStates, true)); + } } return SMGSparseModelCheckingHelperReturnType(std::move(result), std::move(relevantStates), std::move(scheduler), std::move(constrainedChoiceValues)); @@ -160,7 +162,22 @@ namespace storm { storm::storage::BitVector notPsiStates = ~psiStates; statesOfCoalition.complement(); - auto result = computeUntilProbabilitiesSound(env, std::move(goal), transitionMatrix, backwardTransitions, storm::storage::BitVector(transitionMatrix.getRowGroupCount(), true), notPsiStates, qualitative, statesOfCoalition, produceScheduler, hint); + if (env.solver().isForceSoundness()) { + auto result = computeUntilProbabilitiesSound(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; + } + for (auto& element : result.choiceValues) { + element = storm::utility::one() - element; + } + return result; + } + + 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; } diff --git a/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp b/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp index e42179764..a91fc03b6 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp @@ -42,7 +42,7 @@ namespace storm { _x1U = xU; _x2U = _x1U; - if (this->isProduceSchedulerSet()) { // TODO Fabian scheduler !!! + if (this->isProduceSchedulerSet()) { if (!this->_producedOptimalChoices.is_initialized()) { this->_producedOptimalChoices.emplace(); }