From 8f187f46f12ae95ee50b31a725766361af0cd236 Mon Sep 17 00:00:00 2001 From: Fabian Russold Date: Wed, 9 Oct 2024 21:10:52 +0200 Subject: [PATCH] debug: Sound Game VI now fully debugged (fixed Find_MSEC), WIP: produce scheduler --- .../rpatl/SparseSmgRpatlModelChecker.cpp | 1 - .../rpatl/helper/SparseSmgRpatlHelper.cpp | 50 +++++------ .../helper/internal/SoundGameViHelper.cpp | 90 ++++++++----------- .../rpatl/helper/internal/SoundGameViHelper.h | 6 +- 4 files changed, 63 insertions(+), 84 deletions(-) diff --git a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp index 6cd0a5560..9239f0578 100644 --- a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp +++ b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp @@ -154,7 +154,6 @@ namespace storm { if (checkTask.isProduceSchedulersSet() && ret.scheduler) { result->asExplicitQuantitativeCheckResult().setScheduler(std::move(ret.scheduler)); } - //STORM_LOG_DEBUG(result); return result; } diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp index 88f2bd1a2..31dc8cea7 100644 --- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp @@ -61,29 +61,30 @@ 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_LOG_DEBUG("statesOfCoalition: " << statesOfCoalition << std::endl); - storm::storage::BitVector prob1 = storm::utility::graph::performProb1(backwardTransitions, phiStates, psiStates); storm::storage::BitVector probGreater0 = storm::utility::graph::performProbGreater0(backwardTransitions, phiStates, psiStates); - STORM_LOG_DEBUG("probGreater0: " << probGreater0 << std::endl); - - - std::unique_ptr> scheduler; - storm::storage::BitVector relevantStates = storm::storage::BitVector(transitionMatrix.getRowGroupCount(), true); // TODO Fabian + storm::storage::BitVector relevantStates = phiStates; storm::storage::SparseMatrix submatrix = transitionMatrix.getSubmatrix(true, relevantStates, relevantStates, false); // Initialize the x vector and solution vector result. - std::vector xL = std::vector(relevantStates.getNumberOfSetBits(), storm::utility::zero()); + std::vector xL = std::vector(transitionMatrix.getRowGroupCount(), storm::utility::zero()); + // assigning 1s to the xL vector for all Goal states auto xL_begin = xL.begin(); - std::for_each(xL.begin(), xL.end(), [&prob1, &xL_begin](ValueType &it) + std::for_each(xL.begin(), xL.end(), [&psiStates, &xL_begin](ValueType &it) { - if (prob1[&it - &(*xL_begin)]) + if (psiStates[&it - &(*xL_begin)]) it = 1; }); - // std::transform(xL.begin(), xL.end(), psiStates.begin(), xL, [](double& a) { a *= 3; }) // TODO Fabian - // assigning 1s to the xL vector for all Goal states + size_t i = 0; + auto new_end = std::remove_if(xL.begin(), xL.end(), [&relevantStates, &i](const auto& item) { + bool ret = !(relevantStates[i]); + i++; + return ret; + }); + xL.erase(new_end, xL.end()); + xL.resize(relevantStates.getNumberOfSetBits()); std::vector xU = std::vector(transitionMatrix.getRowGroupCount(), storm::utility::zero()); // assigning 1s to the xU vector for all states except the states s where Prob(sEf) = 0 for all goal states f auto xU_begin = xU.begin(); @@ -92,33 +93,32 @@ namespace storm { if (probGreater0[&it - &(*xU_begin)]) it = 1; }); - /*size_t i = 0; - auto new_end = std::remove_if(xU.begin(), xU.end(), [&relevantStates, &i](const auto& item) { + i = 0; + auto new_end_U = std::remove_if(xU.begin(), xU.end(), [&relevantStates, &i](const auto& item) { bool ret = !(relevantStates[i]); i++; return ret; }); - xU.erase(new_end, xU.end()); - xU.resize(relevantStates.getNumberOfSetBits()); */ + xU.erase(new_end_U, xU.end()); + xU.resize(relevantStates.getNumberOfSetBits()); + + storm::storage::BitVector clippedPsiStates(relevantStates.getNumberOfSetBits()); + clippedPsiStates.setClippedStatesOfCoalition(relevantStates, psiStates); - std::vector result = std::vector(transitionMatrix.getRowGroupCount(), storm::utility::zero()); std::vector b = transitionMatrix.getConstrainedRowGroupSumVector(relevantStates, psiStates); + std::vector result = std::vector(transitionMatrix.getRowGroupCount(), storm::utility::zero()); - // STORM_LOG_DEBUG(transitionMatrix); - STORM_LOG_DEBUG("b: " << b); storm::storage::BitVector clippedStatesOfCoalition(relevantStates.getNumberOfSetBits()); clippedStatesOfCoalition.setClippedStatesOfCoalition(relevantStates, statesOfCoalition); - // std::vector constrainedChoiceValues = std::vector(b.size(), storm::utility::zero()); // TODO Fabian: do I need this? - std::vector constrainedChoiceValues; + std::vector constrainedChoiceValues = std::vector(b.size(), storm::utility::zero()); - storm::modelchecker::helper::internal::SoundGameViHelper viHelper(transitionMatrix, backwardTransitions, b, statesOfCoalition, psiStates, goal.direction()); + storm::modelchecker::helper::internal::SoundGameViHelper viHelper(submatrix, submatrix.transpose(), b, clippedStatesOfCoalition, clippedPsiStates, goal.direction()); viHelper.performValueIteration(env, xL, xU, goal.direction(), constrainedChoiceValues); - storm::utility::vector::setVectorValues(result, relevantStates, xU); - storm::utility::vector::setVectorValues(result, psiStates, storm::utility::one()); + viHelper.fillChoiceValuesVector(constrainedChoiceValues, relevantStates, transitionMatrix.getRowGroupIndices()); + storm::utility::vector::setVectorValues(result, relevantStates, xL); - STORM_LOG_DEBUG(xU); return SMGSparseModelCheckingHelperReturnType(std::move(result), std::move(relevantStates), std::move(scheduler), std::move(constrainedChoiceValues)); } diff --git a/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp b/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp index 41dc61b50..4cea25c18 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp @@ -20,7 +20,6 @@ namespace storm { template void SoundGameViHelper::prepareSolversAndMultipliers(const Environment& env) { - STORM_LOG_DEBUG("\n" << _transitionMatrix); _multiplier = storm::solver::MultiplierFactory().create(env, _transitionMatrix); _x1IsCurrent = false; _minimizerStates = _optimizationDirection == OptimizationDirection::Maximize ? _statesOfCoalition : ~_statesOfCoalition; @@ -39,13 +38,11 @@ namespace storm { //_x1.assign(_transitionMatrix.getRowGroupCount(), storm::utility::zero()); _x1L = xL; _x2L = _x1L; - _x1Test = _x1L; - _x2Test = _x1L; _x1U = xU; _x2U = _x1U; - if (this->isProduceSchedulerSet()) { + if (this->isProduceSchedulerSet()) { // TODO Fabian scheduler !!! if (!this->_producedOptimalChoices.is_initialized()) { this->_producedOptimalChoices.emplace(); } @@ -53,12 +50,19 @@ namespace storm { } uint64_t iter = 0; - constrainedChoiceValues = std::vector(xL.size(), storm::utility::zero()); // ?? + constrainedChoiceValues = std::vector(xL.size(), storm::utility::zero()); while (iter < maxIter) { performIterationStep(env, dir); if (checkConvergence(precision)) { - //_multiplier->multiply(env, xNewL(), nullptr, constrainedChoiceValues); // TODO Fabian: ??? + // one last iteration for shield + _multiplier->multiply(env, xNewL(), nullptr, constrainedChoiceValues); + 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; + }); break; } if (storm::utility::resources::isTerminate()) { @@ -69,13 +73,10 @@ namespace storm { xL = xNewL(); xU = xNewU(); - // for profiling - STORM_PRINT(_timing[0] << ", " << _timing[1] << ", " << _timing[2] << ", " << _timing[3] << ", " << _timing[4] << std::endl); - - if (isProduceSchedulerSet()) { + /* if (isProduceSchedulerSet()) { // We will be doing one more iteration step and track scheduler choices this time. performIterationStep(env, dir, &_producedOptimalChoices.get()); - } + } */ } template @@ -92,21 +93,25 @@ namespace storm { _multiplier->multiply(env, xOldL(), nullptr, choiceValuesL); reduceChoiceValues(choiceValuesL, &reducedMinimizerActions, xNewL()); - - - // just for debugging - _multiplier->multiplyAndReduce(env, _optimizationDirection, xOldTest(), nullptr, xNewTest(), nullptr, &_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; + }); // over_approximation std::vector choiceValuesU = std::vector(this->_transitionMatrix.getRowCount(), storm::utility::zero()); _multiplier->multiply(env, xOldU(), nullptr, choiceValuesU); reduceChoiceValues(choiceValuesU, nullptr, xNewU()); - - auto finish = std::chrono::steady_clock::now(); - double elapsed_seconds = std::chrono::duration_cast< - std::chrono::duration>(finish - start).count(); - _timing[0] += elapsed_seconds; + auto xU_begin = xNewU().begin(); + std::for_each(xNewU().begin(), xNewU().end(), [&psiStates, &xU_begin](ValueType &it) + { + if (psiStates[&it - &(*xU_begin)]) + it = 1; + }); if (reducedMinimizerActions != _oldPolicy) { // new MECs only if Policy changed start = std::chrono::steady_clock::now(); @@ -114,21 +119,10 @@ namespace storm { // restricting the none optimal minimizer choices _restrictedTransitions = this->_transitionMatrix.restrictRows(reducedMinimizerActions); - 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) { @@ -137,31 +131,28 @@ 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 - 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 void SoundGameViHelper::deflate(storm::storage::MaximalEndComponentDecomposition const MSEC, storage::SparseMatrix const restrictedMatrix, std::vector& xU, std::vector choiceValues) { + auto rowGroupIndices = restrictedMatrix.getRowGroupIndices(); auto choice_begin = choiceValues.begin(); // iterating over all MSECs for (auto smec_it : MSEC) { ValueType bestExit = 0; - if (smec_it.isErgodic(restrictedMatrix)) continue; + // if (smec_it.isErgodic(restrictedMatrix)) continue; auto stateSet = smec_it.getStateSet(); for (uint state : stateSet) { + if (_psiStates[state]) { + bestExit = 1; + break; + } if (_minimizerStates[state]) continue; uint rowGroupIndex = rowGroupIndices[state]; auto exitingCompare = [&state, &smec_it, &choice_begin](const ValueType &lhs, const ValueType &rhs) @@ -176,13 +167,16 @@ namespace storm { uint rowGroupSize = rowGroupIndices[state + 1] - rowGroupIndex; auto choice_it = choice_begin + rowGroupIndex; - ValueType newBestExit = *std::max_element(choice_it, choice_it + rowGroupSize, exitingCompare); + auto it = std::max_element(choice_it, choice_it + rowGroupSize, exitingCompare); + ValueType newBestExit = 0; + if (!smec_it.containsChoice(state, it - choice_begin)) { + newBestExit = *it; + } if (newBestExit > bestExit) bestExit = newBestExit; } // deflating the states of the current MSEC for (uint state : stateSet) { - if (_psiStates[state]) continue; xU[state] = std::min(xU[state], bestExit); } } @@ -361,16 +355,6 @@ 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 ad78bee56..45d583b7b 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.h +++ b/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.h @@ -97,10 +97,6 @@ namespace storm { std::vector& xOldU(); std::vector const& xOldU() const; - std::vector& xNewTest(); - - std::vector& xOldTest(); - bool _x1IsCurrent; storm::storage::BitVector _minimizerStates; @@ -123,7 +119,7 @@ namespace storm { storm::storage::BitVector _oldPolicy; storm::storage::BitVector _statesOfCoalition; storm::storage::BitVector _psiStates; - std::vector _x, _x1L, _x2L, _x1U, _x2U, _x1Test, _x2Test, _b; + std::vector _x, _x1L, _x2L, _x1U, _x2U, _b; OptimizationDirection _optimizationDirection; storm::storage::MaximalEndComponentDecomposition _MSECs;