From bb72102e501e54277ed9c3c5ef0b4b9529af7b59 Mon Sep 17 00:00:00 2001 From: Fabian Russold Date: Fri, 11 Oct 2024 16:49:31 +0200 Subject: [PATCH] produceShield: small fix, produceScheduler: implemented --- .../rpatl/helper/SparseSmgRpatlHelper.cpp | 15 +++++++++++++-- .../rpatl/helper/SparseSmgRpatlHelper.h | 2 +- .../helper/internal/SoundGameViHelper.cpp | 19 ++++++++++++------- 3 files changed, 26 insertions(+), 10 deletions(-) diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp index 31dc8cea7..ddf04ea90 100644 --- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp @@ -114,16 +114,24 @@ namespace storm { storm::modelchecker::helper::internal::SoundGameViHelper viHelper(submatrix, submatrix.transpose(), b, clippedStatesOfCoalition, clippedPsiStates, goal.direction()); + if (produceScheduler) { + viHelper.setProduceScheduler(true); + } + viHelper.performValueIteration(env, xL, xU, goal.direction(), constrainedChoiceValues); viHelper.fillChoiceValuesVector(constrainedChoiceValues, relevantStates, transitionMatrix.getRowGroupIndices()); storm::utility::vector::setVectorValues(result, relevantStates, xL); + if (produceScheduler) { + scheduler = std::make_unique>(expandScheduler(viHelper.extractScheduler(), psiStates, ~phiStates)); + } + return SMGSparseModelCheckingHelperReturnType(std::move(result), std::move(relevantStates), std::move(scheduler), std::move(constrainedChoiceValues)); } template - storm::storage::Scheduler SparseSmgRpatlHelper::expandScheduler(storm::storage::Scheduler scheduler, storm::storage::BitVector psiStates, storm::storage::BitVector notPhiStates) { + storm::storage::Scheduler SparseSmgRpatlHelper::expandScheduler(storm::storage::Scheduler scheduler, storm::storage::BitVector psiStates, storm::storage::BitVector notPhiStates, bool sound) { storm::storage::Scheduler completeScheduler(psiStates.size()); uint_fast64_t maybeStatesCounter = 0; uint schedulerSize = psiStates.size(); @@ -131,6 +139,9 @@ namespace storm { // psiStates already fulfill formulae so we can set an arbitrary action if(psiStates.get(stateCounter)) { completeScheduler.setChoice(0, stateCounter); + if (sound) { + maybeStatesCounter++; + } // ~phiStates do not fulfill formulae so we can set an arbitrary action } else if(notPhiStates.get(stateCounter)) { completeScheduler.setChoice(0, stateCounter); @@ -149,7 +160,7 @@ namespace storm { 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); + 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; } diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.h b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.h index 741d5961d..c0216d23f 100644 --- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.h +++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.h @@ -41,7 +41,7 @@ namespace storm { 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 storm::storage::Scheduler expandScheduler(storm::storage::Scheduler scheduler, storm::storage::BitVector psiStates, storm::storage::BitVector notPhiStates, bool sound = false); 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/SoundGameViHelper.cpp b/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp index 4cea25c18..e42179764 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp @@ -50,7 +50,7 @@ namespace storm { } uint64_t iter = 0; - constrainedChoiceValues = std::vector(xL.size(), storm::utility::zero()); + constrainedChoiceValues = std::vector(_transitionMatrix.getRowCount(), storm::utility::zero()); while (iter < maxIter) { performIterationStep(env, dir); @@ -73,10 +73,18 @@ namespace storm { xL = xNewL(); xU = xNewU(); - /* if (isProduceSchedulerSet()) { + if (isProduceSchedulerSet()) { // We will be doing one more iteration step and track scheduler choices this time. - performIterationStep(env, dir, &_producedOptimalChoices.get()); - } */ + _x1IsCurrent = !_x1IsCurrent; + _multiplier->multiplyAndReduce(env, dir, xOldL(), nullptr, xNewL(), &_producedOptimalChoices.get(), &_statesOfCoalition); + storm::storage::BitVector psiStates = _psiStates; + auto xL_begin = xNewL().begin(); + std::for_each(xNewL().begin(), xNewL().end(), [&psiStates, &xL_begin](ValueType &it) + { + if (psiStates[&it - &(*xL_begin)]) + it = 1; + }); + } } template @@ -84,7 +92,6 @@ namespace storm { storm::storage::BitVector reducedMinimizerActions = {storm::storage::BitVector(this->_transitionMatrix.getRowCount(), true)}; // under approximation - auto start = std::chrono::steady_clock::now(); if (!_multiplier) { prepareSolversAndMultipliers(env); } @@ -114,8 +121,6 @@ namespace storm { }); if (reducedMinimizerActions != _oldPolicy) { // new MECs only if Policy changed - start = std::chrono::steady_clock::now(); - // restricting the none optimal minimizer choices _restrictedTransitions = this->_transitionMatrix.restrictRows(reducedMinimizerActions);