From 2de38edbff72e97d222e4c76549117bc08321648 Mon Sep 17 00:00:00 2001 From: Fabian Russold Date: Thu, 25 Jul 2024 15:35:50 +0200 Subject: [PATCH] basic implementation done --- .../rpatl/helper/SparseSmgRpatlHelper.cpp | 2 +- .../helper/internal/SoundGameViHelper.cpp | 63 ++++++++++--------- .../rpatl/helper/internal/SoundGameViHelper.h | 4 +- 3 files changed, 39 insertions(+), 30 deletions(-) diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp index 3b824341f..29d41b45c 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, backwardTransitions, statesOfCoalition, goal.direction()); + storm::modelchecker::helper::internal::SoundGameViHelper viHelper(transitionMatrix, backwardTransitions, statesOfCoalition, psiStates, 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 198550e6f..d035f6fd7 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::SparseMatrix const& backwardTransitions, storm::storage::BitVector statesOfCoalition, OptimizationDirection const& optimizationDirection) : _transitionMatrix(transitionMatrix), _backwardTransitions(backwardTransitions), _statesOfCoalition(statesOfCoalition), _optimizationDirection(optimizationDirection) { + SoundGameViHelper::SoundGameViHelper(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector statesOfCoalition, storm::storage::BitVector psiStates, OptimizationDirection const& optimizationDirection) : _transitionMatrix(transitionMatrix), _backwardTransitions(backwardTransitions), _statesOfCoalition(statesOfCoalition), _psiStates(psiStates), _optimizationDirection(optimizationDirection) { // Intentionally left empty. } @@ -98,40 +98,47 @@ namespace storm { // restricting the none optimal minimizer choices storage::SparseMatrix restrictedTransMatrix = this->_transitionMatrix.restrictRows(reducedMinimizerActions); + _multiplierRestricted = storm::solver::MultiplierFactory().create(env, restrictedTransMatrix); - // storage::SparseMatrix restrictedBackMatrix = this->_backwardTransitions.restrictRows(reducedMinimizerActions); - STORM_LOG_DEBUG("restricted Transition: \n" << restrictedTransMatrix); + // storage::SparseMatrix restrictedBackMatrix = this->_backwardTransitions.restrictRows(reducedMinimizerActions); + // STORM_LOG_DEBUG("restricted Transition: \n" << restrictedTransMatrix); - // TODO Fabian: find_MSECs() & deflate() + // find_MSECs() & deflate() storm::storage::MaximalEndComponentDecomposition MECD = storm::storage::MaximalEndComponentDecomposition(restrictedTransMatrix, _backwardTransitions); - STORM_LOG_DEBUG("MECD: \n" << MECD); - // deflate(MECD,restrictedTransMatrix, xNewU()); + // 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); + void SoundGameViHelper::deflate(storm::storage::MaximalEndComponentDecomposition const MECD, storage::SparseMatrix const restrictedMatrix, std::vector& xU) { + auto rowGroupIndices = restrictedMatrix.getRowGroupIndices(); + + // iterating over all MSECs + for (auto smec_it : MECD) { + ValueType bestExit = 0; + for (uint state = 0; state < rowGroupIndices.size() - 1; state++) { + uint rowGroupSize = rowGroupIndices[state + 1] - rowGroupIndices[state]; + if (!_minimizerStates[state] && smec_it.containsState(state)) { // check if current state is maximizer state + // getting the optimal minimizer choice for the given state + + for (uint choice = 0; choice < rowGroupSize; choice++) { + if (!smec_it.containsChoice(state, choice + rowGroupIndices[state])) { + ValueType choiceValue = 0; + _multiplierRestricted->multiplyRow(choice + rowGroupIndices[state], xU, choiceValue); + if (choiceValue > bestExit) + bestExit = choiceValue; + } } } - // reducing the xNew() (choiceValues) vector for minimizer states - choiceValues[state] = optChoice; } - } */ + auto stateSet = smec_it.getStateSet(); + for (auto smec_state : stateSet) + { + if (!_psiStates[smec_state]) + xU[smec_state] = std::min(xU[smec_state], bestExit); + } + } } template @@ -178,9 +185,9 @@ namespace storm { STORM_LOG_ASSERT(_multiplier, "tried to check for convergence without doing an iteration first."); // Now check whether the currently produced results are precise enough STORM_LOG_ASSERT(threshold > storm::utility::zero(), "Did not expect a non-positive threshold."); - auto x1It = xOldL().begin(); - auto x1Ite = xOldL().end(); - auto x2It = xNewL().begin(); + auto x1It = xNewL().begin(); + auto x1Ite = xNewL().end(); + auto x2It = xNewU().begin(); ValueType maxDiff = (*x2It - *x1It); ValueType minDiff = maxDiff; // The difference between maxDiff and minDiff is zero at this point. Thus, it doesn't make sense to check the threshold now. diff --git a/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.h b/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.h index f140eb734..5fecd8d87 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.h +++ b/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.h @@ -20,7 +20,7 @@ namespace storm { template class SoundGameViHelper { public: - SoundGameViHelper(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector statesOfCoalition, OptimizationDirection const& optimizationDirection); + SoundGameViHelper(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector statesOfCoalition, storm::storage::BitVector psiStates, OptimizationDirection const& optimizationDirection); void prepareSolversAndMultipliers(const Environment& env); @@ -114,8 +114,10 @@ namespace storm { storm::storage::SparseMatrix _transitionMatrix; storm::storage::SparseMatrix _backwardTransitions; storm::storage::BitVector _statesOfCoalition; + storm::storage::BitVector _psiStates; std::vector _x, _x1L, _x2L, _x1U, _x2U; std::unique_ptr> _multiplier; + std::unique_ptr> _multiplierRestricted; OptimizationDirection _optimizationDirection; bool _produceScheduler = false;