diff --git a/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp b/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp index e305c3be7..41dc61b50 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, storm::storage::BitVector psiStates, OptimizationDirection const& optimizationDirection) : _transitionMatrix(transitionMatrix), _backwardTransitions(backwardTransitions), _statesOfCoalition(statesOfCoalition), _psiStates(psiStates), _optimizationDirection(optimizationDirection) { + SoundGameViHelper::SoundGameViHelper(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector b, storm::storage::BitVector statesOfCoalition, storm::storage::BitVector psiStates, OptimizationDirection const& optimizationDirection) : _transitionMatrix(transitionMatrix), _backwardTransitions(backwardTransitions), _statesOfCoalition(statesOfCoalition), _psiStates(psiStates), _optimizationDirection(optimizationDirection), _b(b) { // Intentionally left empty. } @@ -24,6 +24,8 @@ namespace storm { _multiplier = storm::solver::MultiplierFactory().create(env, _transitionMatrix); _x1IsCurrent = false; _minimizerStates = _optimizationDirection == OptimizationDirection::Maximize ? _statesOfCoalition : ~_statesOfCoalition; + _oldPolicy = storm::storage::BitVector(_transitionMatrix.getRowCount(), false); + _timing = std::vector(5, 0); } template @@ -37,6 +39,8 @@ namespace storm { //_x1.assign(_transitionMatrix.getRowGroupCount(), storm::utility::zero()); _x1L = xL; _x2L = _x1L; + _x1Test = _x1L; + _x2Test = _x1L; _x1U = xU; _x2U = _x1U; @@ -65,8 +69,8 @@ namespace storm { xL = xNewL(); xU = xNewU(); - STORM_LOG_DEBUG("result xL: " << xL); - STORM_LOG_DEBUG("result xU: " << xU); + // for profiling + STORM_PRINT(_timing[0] << ", " << _timing[1] << ", " << _timing[2] << ", " << _timing[3] << ", " << _timing[4] << std::endl); if (isProduceSchedulerSet()) { // We will be doing one more iteration step and track scheduler choices this time. @@ -79,7 +83,7 @@ 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); } @@ -89,23 +93,42 @@ namespace storm { _multiplier->multiply(env, xOldL(), nullptr, choiceValuesL); reduceChoiceValues(choiceValuesL, &reducedMinimizerActions, xNewL()); - // over_approximation + // just for debugging + _multiplier->multiplyAndReduce(env, _optimizationDirection, xOldTest(), nullptr, xNewTest(), nullptr, &_statesOfCoalition); + + // over_approximation std::vector choiceValuesU = std::vector(this->_transitionMatrix.getRowCount(), storm::utility::zero()); _multiplier->multiply(env, xOldU(), nullptr, choiceValuesU); reduceChoiceValues(choiceValuesU, nullptr, xNewU()); - // restricting the none optimal minimizer choices - storage::SparseMatrix restrictedTransMatrix = this->_transitionMatrix.restrictRows(reducedMinimizerActions); + auto finish = std::chrono::steady_clock::now(); + double elapsed_seconds = std::chrono::duration_cast< + std::chrono::duration>(finish - start).count(); + _timing[0] += elapsed_seconds; - // STORM_LOG_DEBUG("restricted Transition: \n" << restrictedTransMatrix); + if (reducedMinimizerActions != _oldPolicy) { // new MECs only if Policy changed + start = std::chrono::steady_clock::now(); - // find_MSECs() - storm::storage::MaximalEndComponentDecomposition MSEC = storm::storage::MaximalEndComponentDecomposition(restrictedTransMatrix, _backwardTransitions); + // restricting the none optimal minimizer choices + _restrictedTransitions = this->_transitionMatrix.restrictRows(reducedMinimizerActions); - // STORM_LOG_DEBUG("MECD: \n" << MSEC); + finish = std::chrono::steady_clock::now(); + elapsed_seconds = std::chrono::duration_cast>(finish - start).count(); + _timing[1] += elapsed_seconds; + // STORM_LOG_DEBUG("restricted Transition: \n" << restrictedTransMatrix); + start = std::chrono::steady_clock::now(); + // find_MSECs() + _MSECs = storm::storage::MaximalEndComponentDecomposition(_restrictedTransitions, _restrictedTransitions.transpose(true)); + + finish = std::chrono::steady_clock::now(); + elapsed_seconds = std::chrono::duration_cast>(finish - start).count(); + _timing[2] += elapsed_seconds; + } + + start = std::chrono::steady_clock::now(); // reducing the choiceValuesU size_t i = 0; auto new_end = std::remove_if(choiceValuesU.begin(), choiceValuesU.end(), [&reducedMinimizerActions, &i](const auto& item) { @@ -114,9 +137,19 @@ namespace storm { return ret; }); choiceValuesU.erase(new_end, choiceValuesU.end()); + finish = std::chrono::steady_clock::now(); + elapsed_seconds = std::chrono::duration_cast< + std::chrono::duration>(finish - start).count(); + _timing[3] += elapsed_seconds; + _oldPolicy = reducedMinimizerActions; // deflating the MSECs - deflate(MSEC, restrictedTransMatrix, xNewU(), choiceValuesU); + start = std::chrono::steady_clock::now(); + deflate(_MSECs, _restrictedTransitions, xNewU(), choiceValuesU); + finish = std::chrono::steady_clock::now(); + elapsed_seconds = std::chrono::duration_cast< + std::chrono::duration>(finish - start).count(); + _timing[4] += elapsed_seconds; } template @@ -177,8 +210,9 @@ namespace storm { } } } - else + else { choice_it += rowGroupSize; + } // reducing the xNew() vector for minimizer states x[state] = optChoice; } @@ -201,22 +235,11 @@ namespace storm { 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. - for (++x1It, ++x2It; x1It != x1Ite; ++x1It, ++x2It) { + for (; x1It != x1Ite; x1It++, x2It++) { ValueType diff = (*x2It - *x1It); // Potentially update maxDiff or minDiff - bool skipCheck = false; - if (maxDiff < diff) { - maxDiff = diff; - } else if (minDiff > diff) { - minDiff = diff; - } else { - skipCheck = true; - } - // Check convergence - if (!skipCheck && (maxDiff - minDiff) > threshold) { + if (diff > threshold) { return false; } } @@ -338,6 +361,16 @@ namespace storm { return _x1IsCurrent ? _x2U : _x1U; } + template + std::vector& SoundGameViHelper::xOldTest() { + return _x1IsCurrent ? _x2Test : _x1Test; + } + + template + std::vector& SoundGameViHelper::xNewTest() { + return _x1IsCurrent ? _x1Test : _x2Test; + } + template class SoundGameViHelper; #ifdef STORM_HAVE_CARL template class SoundGameViHelper; diff --git a/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.h b/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.h index d8a0d7907..ad78bee56 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, storm::storage::BitVector psiStates, OptimizationDirection const& optimizationDirection); + SoundGameViHelper(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector b, storm::storage::BitVector statesOfCoalition, storm::storage::BitVector psiStates, OptimizationDirection const& optimizationDirection); void prepareSolversAndMultipliers(const Environment& env); @@ -97,6 +97,10 @@ namespace storm { std::vector& xOldU(); std::vector const& xOldU() const; + std::vector& xNewTest(); + + std::vector& xOldTest(); + bool _x1IsCurrent; storm::storage::BitVector _minimizerStates; @@ -115,14 +119,20 @@ namespace storm { storm::storage::SparseMatrix _transitionMatrix; storm::storage::SparseMatrix _backwardTransitions; + storm::storage::SparseMatrix _restrictedTransitions; + storm::storage::BitVector _oldPolicy; storm::storage::BitVector _statesOfCoalition; storm::storage::BitVector _psiStates; - std::vector _x, _x1L, _x2L, _x1U, _x2U; + std::vector _x, _x1L, _x2L, _x1U, _x2U, _x1Test, _x2Test, _b; OptimizationDirection _optimizationDirection; + storm::storage::MaximalEndComponentDecomposition _MSECs; + bool _produceScheduler = false; bool _shieldingTask = false; boost::optional> _producedOptimalChoices; + + std::vector _timing; }; } }