From 9a414442171ac9b0b7babc4e777435f60241b42f Mon Sep 17 00:00:00 2001 From: Fabian Russold Date: Fri, 19 Jul 2024 17:01:01 +0200 Subject: [PATCH] finding MSECs done, in progress: deflating the MSECs --- .../rpatl/helper/SparseSmgRpatlHelper.cpp | 2 +- .../helper/internal/SoundGameViHelper.cpp | 44 ++++++++++++++++--- .../rpatl/helper/internal/SoundGameViHelper.h | 8 ++-- 3 files changed, 44 insertions(+), 10 deletions(-) diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp index 1a346333b..3b824341f 100644 --- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp @@ -63,7 +63,7 @@ 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::modelchecker::helper::internal::SoundGameViHelper viHelper(transitionMatrix, statesOfCoalition, goal.direction()); + storm::modelchecker::helper::internal::SoundGameViHelper viHelper(transitionMatrix, backwardTransitions, statesOfCoalition, goal.direction()); // Initialize the x vector and solution vector result. // TODO Fabian: maybe relevant states (later) diff --git a/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp b/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp index a3817540b..198550e6f 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp @@ -14,7 +14,7 @@ namespace storm { namespace internal { template - SoundGameViHelper::SoundGameViHelper(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector statesOfCoalition, OptimizationDirection const& optimizationDirection) : _transitionMatrix(transitionMatrix), _statesOfCoalition(statesOfCoalition), _optimizationDirection(optimizationDirection) { + SoundGameViHelper::SoundGameViHelper(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector statesOfCoalition, OptimizationDirection const& optimizationDirection) : _transitionMatrix(transitionMatrix), _backwardTransitions(backwardTransitions), _statesOfCoalition(statesOfCoalition), _optimizationDirection(optimizationDirection) { // Intentionally left empty. } @@ -34,7 +34,6 @@ namespace storm { // Get precision for convergence check. ValueType precision = storm::utility::convertNumber(env.solver().game().getPrecision()); - STORM_LOG_DEBUG("hello" << "world"); uint64_t maxIter = env.solver().game().getMaximalNumberOfIterations(); //_x1.assign(_transitionMatrix.getRowGroupCount(), storm::utility::zero()); _x1L = xL; @@ -97,14 +96,48 @@ namespace storm { _multiplier->multiplyAndReduce(env, dir, xOldU(), nullptr, xNewU(), nullptr, &_statesOfCoalition); + // restricting the none optimal minimizer choices + storage::SparseMatrix restrictedTransMatrix = this->_transitionMatrix.restrictRows(reducedMinimizerActions); + + // storage::SparseMatrix restrictedBackMatrix = this->_backwardTransitions.restrictRows(reducedMinimizerActions); + STORM_LOG_DEBUG("restricted Transition: \n" << restrictedTransMatrix); + // TODO Fabian: find_MSECs() & deflate() + storm::storage::MaximalEndComponentDecomposition MECD = storm::storage::MaximalEndComponentDecomposition(restrictedTransMatrix, _backwardTransitions); + + STORM_LOG_DEBUG("MECD: \n" << MECD); + // deflate(MECD,restrictedTransMatrix, xNewU()); + } + + template + void SoundGameViHelper::deflate(storm::storage::MaximalEndComponentDecomposition const MECD, storage::SparseMatrix const restrictedMatrix, std::vector& xU) + { + /* auto rowGroupIndices = restrictedMatrix.getRowGroupIndices(); + auto mec_it = MECD.begin(); + + + for(uint state = 0; state < rowGroupIndices.size() - 1; state++) { + uint rowGroupSize = rowGroupIndices[state + 1] - rowGroupIndices[state]; + ValueType optChoice; + if (!_minimizerStates[state]) { // check if current state is maximizer state + // getting the optimal minimizer choice for the given state + optChoice = *std::min_element(choice_it, choice_it + rowGroupSize); + + for (uint choice = 0; choice < rowGroupSize; choice++, choice_it++) { + if (*choice_it > optChoice) { + result->set(rowGroupIndices[state] + choice, 0); + } + } + // reducing the xNew() (choiceValues) vector for minimizer states + choiceValues[state] = optChoice; + } + } */ } template void SoundGameViHelper::reduceChoiceValues(std::vector& choiceValues, storm::storage::BitVector* result) { - // result BitVec should be initialized with 1s outside the function - // restrict rows + // result BitVec should be initialized with 1s outside the method auto rowGroupIndices = this->_transitionMatrix.getRowGroupIndices(); auto choice_it = choiceValues.begin(); @@ -137,8 +170,6 @@ namespace storm { } } choiceValues.resize(this->_transitionMatrix.getRowGroupCount()); - STORM_LOG_DEBUG("reduced BitVec: " << *result); - STORM_LOG_DEBUG("reduced x Vector: " << choiceValues); } @@ -177,6 +208,7 @@ namespace storm { _produceScheduler = value; } + template bool SoundGameViHelper::isProduceSchedulerSet() const { return _produceScheduler; diff --git a/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.h b/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.h index 21ec6b464..f140eb734 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.h +++ b/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.h @@ -4,6 +4,7 @@ #include "storm/solver/LinearEquationSolver.h" #include "storm/solver/MinMaxLinearEquationSolver.h" #include "storm/solver/Multiplier.h" +#include "storm/storage/MaximalEndComponentDecomposition.h" namespace storm { class Environment; @@ -19,7 +20,7 @@ namespace storm { template class SoundGameViHelper { public: - SoundGameViHelper(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector statesOfCoalition, OptimizationDirection const& optimizationDirection); + SoundGameViHelper(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector statesOfCoalition, OptimizationDirection const& optimizationDirection); void prepareSolversAndMultipliers(const Environment& env); @@ -73,9 +74,9 @@ namespace storm { */ void performIterationStep(Environment const& env, storm::solver::OptimizationDirection const dir, std::vector* choices = nullptr); + void deflate(storm::storage::MaximalEndComponentDecomposition const MECD, storage::SparseMatrix const restrictedMatrix, std::vector& xU); + void reduceChoiceValues(std::vector& choiceValues, storm::storage::BitVector* result); - // - // für alle minimizer states -> reduce zu optimal actions /*! * Checks whether the curently computed value achieves the desired precision @@ -111,6 +112,7 @@ namespace storm { std::vector& getProducedOptimalChoices(); storm::storage::SparseMatrix _transitionMatrix; + storm::storage::SparseMatrix _backwardTransitions; storm::storage::BitVector _statesOfCoalition; std::vector _x, _x1L, _x2L, _x1U, _x2U; std::unique_ptr> _multiplier;