diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp index 784fc27d5..1a346333b 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); + storm::modelchecker::helper::internal::SoundGameViHelper viHelper(transitionMatrix, statesOfCoalition, goal.direction()); // Initialize the x vector and solution vector result. // TODO Fabian: maybe relevant states (later) @@ -73,7 +73,7 @@ namespace storm { assert(xL.size() == psiStates.size()); for (size_t i = 0; i < xL.size(); i++) { - if (psiStates[xL.size() - i]) + if (psiStates[i]) xL[i] = 1; } STORM_LOG_DEBUG("xL " << xL); @@ -81,7 +81,7 @@ namespace storm { storm::storage::BitVector probGreater0 = storm::utility::graph::performProbGreater0(backwardTransitions, phiStates, psiStates); // assigning 1s to the xU vector for all states except the states s where Prob(sEf) = 0 for all goal states f assert(xU.size() == probGreater0.size()); - for (size_t i = 0; i < xL.size(); i++) + for (size_t i = 0; i < xL.size(); i++) // TODO Fabian: do this more efficient { if (probGreater0[i]) xU[i] = 1; diff --git a/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp b/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp index 239a89d31..a3817540b 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) : _transitionMatrix(transitionMatrix), _statesOfCoalition(statesOfCoalition) { + SoundGameViHelper::SoundGameViHelper(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector statesOfCoalition, OptimizationDirection const& optimizationDirection) : _transitionMatrix(transitionMatrix), _statesOfCoalition(statesOfCoalition), _optimizationDirection(optimizationDirection) { // Intentionally left empty. } @@ -23,6 +23,7 @@ namespace storm { STORM_LOG_DEBUG("\n" << _transitionMatrix); _multiplier = storm::solver::MultiplierFactory().create(env, _transitionMatrix); _x1IsCurrent = false; + _minimizerStates = _optimizationDirection == OptimizationDirection::Maximize ? _statesOfCoalition : ~_statesOfCoalition; } template @@ -77,30 +78,70 @@ namespace storm { template void SoundGameViHelper::performIterationStep(Environment const& env, storm::solver::OptimizationDirection const dir, std::vector* choices) { + storm::storage::BitVector reducedMinimizerActions = {storm::storage::BitVector(this->_transitionMatrix.getRowCount(), true)}; + // under approximation if (!_multiplier) { prepareSolversAndMultipliers(env); } _x1IsCurrent = !_x1IsCurrent; - if (choices == nullptr) { - _multiplier->multiplyAndReduce(env, dir, xOldL(), nullptr, xNewL(), nullptr, &_statesOfCoalition); - } else { - _multiplier->multiplyAndReduce(env, dir, xOldL(), nullptr, xNewL(), choices, &_statesOfCoalition); - } + std::vector choiceValues = xNewL(); + choiceValues.resize(this->_transitionMatrix.getRowCount()); + + _multiplier->multiply(env, xOldL(), nullptr, choiceValues); + reduceChoiceValues(choiceValues, &reducedMinimizerActions); + xNewL() = choiceValues; // over_approximation - if (choices == nullptr) { - _multiplier->multiplyAndReduce(env, dir, xOldU(), nullptr, xNewU(), nullptr, &_statesOfCoalition); - } else { - _multiplier->multiplyAndReduce(env, dir, xOldU(), nullptr, xNewU(), choices, &_statesOfCoalition); - } + _multiplier->multiplyAndReduce(env, dir, xOldU(), nullptr, xNewU(), nullptr, &_statesOfCoalition); // TODO Fabian: find_MSECs() & deflate() + } + + template + void SoundGameViHelper::reduceChoiceValues(std::vector& choiceValues, storm::storage::BitVector* result) + { + // result BitVec should be initialized with 1s outside the function + // restrict rows + + auto rowGroupIndices = this->_transitionMatrix.getRowGroupIndices(); + auto choice_it = choiceValues.begin(); + STORM_LOG_DEBUG("MinStates " << _minimizerStates); + STORM_LOG_DEBUG("init choiceVal " << choiceValues); + + + 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 minimizer 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; + } + else + { + optChoice = *std::max_element(choice_it, choice_it + rowGroupSize); + // reducing the xNew() (choiceValues) vector for maximizer states + choiceValues[state] = optChoice; + choice_it += rowGroupSize; + } + } + choiceValues.resize(this->_transitionMatrix.getRowGroupCount()); + STORM_LOG_DEBUG("reduced BitVec: " << *result); + STORM_LOG_DEBUG("reduced x Vector: " << choiceValues); } + template bool SoundGameViHelper::checkConvergence(ValueType threshold) const { STORM_LOG_ASSERT(_multiplier, "tried to check for convergence without doing an iteration first."); diff --git a/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.h b/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.h index f4e3d5b35..21ec6b464 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.h +++ b/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.h @@ -19,7 +19,7 @@ namespace storm { template class SoundGameViHelper { public: - SoundGameViHelper(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector statesOfCoalition); + SoundGameViHelper(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector statesOfCoalition, OptimizationDirection const& optimizationDirection); void prepareSolversAndMultipliers(const Environment& env); @@ -73,6 +73,10 @@ namespace storm { */ void performIterationStep(Environment const& env, storm::solver::OptimizationDirection const dir, std::vector* choices = nullptr); + 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 */ @@ -92,6 +96,8 @@ namespace storm { bool _x1IsCurrent; + storm::storage::BitVector _minimizerStates; + /*! * @pre before calling this, a computation call should have been performed during which scheduler production was enabled. * @return the produced scheduler of the most recent call. @@ -108,6 +114,7 @@ namespace storm { storm::storage::BitVector _statesOfCoalition; std::vector _x, _x1L, _x2L, _x1U, _x2U; std::unique_ptr> _multiplier; + OptimizationDirection _optimizationDirection; bool _produceScheduler = false; bool _shieldingTask = false;