From 1e40b9e5a3ca642b0ba5c092e6b1088392171d80 Mon Sep 17 00:00:00 2001 From: Fabian Russold Date: Tue, 20 Aug 2024 11:27:43 +0200 Subject: [PATCH] SmgRpatlModelCheckerTest.cpp: added test for deflate method of SoundGameViHelper.cpp --- .../examples/testfiles/smg/example_smg.nm | 28 ++++ .../helper/internal/SoundGameViHelper.cpp | 5 +- .../rpatl/helper/internal/SoundGameViHelper.h | 11 +- src/storm/storage/MaximalEndComponent.h | 2 +- .../rpatl/smg/SmgRpatlModelCheckerTest.cpp | 153 ++++++++++++++++++ 5 files changed, 189 insertions(+), 10 deletions(-) create mode 100644 resources/examples/testfiles/smg/example_smg.nm diff --git a/resources/examples/testfiles/smg/example_smg.nm b/resources/examples/testfiles/smg/example_smg.nm new file mode 100644 index 000000000..0050b1028 --- /dev/null +++ b/resources/examples/testfiles/smg/example_smg.nm @@ -0,0 +1,28 @@ +smg + +const double p = 2/3; + +player maxP + [q_action1], [q_action2] +endplayer + +player minP + [p_action1] +endplayer + +player sinkstates + state_space +endplayer + + +module state_space + s : [0..3]; + + [p_action1] s=0 -> (s'=1); + + [q_action1] s=1 -> (s'=0); + [q_action2] s=1 -> (1-p) : (s'=1) + (p/2) : (s'=2) + (p/2) : (s'=3); + + [] s=2 -> true; + [] s=3 -> true; +endmodule diff --git a/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp b/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp index 732127ce9..e305c3be7 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp @@ -96,8 +96,6 @@ namespace storm { _multiplier->multiply(env, xOldU(), nullptr, choiceValuesU); reduceChoiceValues(choiceValuesU, nullptr, xNewU()); - //_multiplier->multiplyAndReduce(env, dir, xOldU(), nullptr, xNewU(), nullptr, &_statesOfCoalition); - // restricting the none optimal minimizer choices storage::SparseMatrix restrictedTransMatrix = this->_transitionMatrix.restrictRows(reducedMinimizerActions); @@ -124,12 +122,11 @@ namespace storm { 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; // TODO Fabian: ?? isErgodic undefined ref + if (smec_it.isErgodic(restrictedMatrix)) continue; auto stateSet = smec_it.getStateSet(); for (uint state : stateSet) { if (_minimizerStates[state]) continue; diff --git a/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.h b/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.h index f738958ca..d8a0d7907 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.h +++ b/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.h @@ -68,16 +68,18 @@ namespace storm { */ void fillChoiceValuesVector(std::vector& choiceValues, storm::storage::BitVector psiStates, std::vector::index_type> rowGroupIndices); + void deflate(storm::storage::MaximalEndComponentDecomposition const MECD, storage::SparseMatrix const restrictedMatrix, std::vector& xU, std::vector choiceValues); + + void reduceChoiceValues(std::vector& choiceValues, storm::storage::BitVector* result, std::vector& x); + + // multiplier now public for testing + std::unique_ptr> _multiplier; private: /*! * Performs one iteration step for value iteration */ 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, std::vector choiceValues); - - void reduceChoiceValues(std::vector& choiceValues, storm::storage::BitVector* result, std::vector& x); - /*! * Checks whether the curently computed value achieves the desired precision */ @@ -116,7 +118,6 @@ namespace storm { storm::storage::BitVector _statesOfCoalition; storm::storage::BitVector _psiStates; std::vector _x, _x1L, _x2L, _x1U, _x2U; - std::unique_ptr> _multiplier; OptimizationDirection _optimizationDirection; bool _produceScheduler = false; diff --git a/src/storm/storage/MaximalEndComponent.h b/src/storm/storage/MaximalEndComponent.h index 66c1d1c4a..448159804 100644 --- a/src/storm/storage/MaximalEndComponent.h +++ b/src/storm/storage/MaximalEndComponent.h @@ -128,7 +128,7 @@ namespace storm { bool containsChoice(uint_fast64_t state, uint_fast64_t choice) const; /*! - * Retrieves wether the MEC is ergodic or not i.e. wether the MEC is exitable or not + * Retrieves whether the MEC is ergodic or not i.e. wether the MEC is exitable or not * * @param transitionMatrix the given transition matrix * @return True if the MEC is ergodic diff --git a/src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp b/src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp index 79217c614..d634ec6b2 100644 --- a/src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp @@ -17,6 +17,11 @@ #include "storm/settings/modules/CoreSettings.h" #include "storm/logic/Formulas.h" #include "storm/exceptions/UncheckedRequirementException.h" +#include "storm/solver/Multiplier.h" +#include "storm/storage/SparseMatrix.h" +#include "storm/utility/graph.h" +#include "storm/storage/MaximalEndComponentDecomposition.h" +#include "storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.h" namespace { @@ -114,6 +119,7 @@ namespace { std::vector> getTasks(std::vector> const& formulas) const { std::vector> result; for (auto const& f : formulas) { + std::cout << *f << std::endl; result.emplace_back(*f); } return result; @@ -345,5 +351,152 @@ namespace { EXPECT_NEAR(this->parseNumber("1"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); } + TYPED_TEST(SmgRpatlModelCheckerTest, Deflate) { + typedef double ValueType; + std::string formulasString = " <> Pmax=? [F (s=2)]"; + + auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/smg/example_smg.nm", formulasString); + auto model = std::move(modelFormulas.first); + auto tasks = this->getTasks(modelFormulas.second); + auto checker = this->createModelChecker(model); + std::unique_ptr result; + auto transitionMatrix = model->getTransitionMatrix(); + + + auto formulas = std::move(modelFormulas.second); + + storm::logic::GameFormula const& gameFormula = formulas[0]->asGameFormula(); + + storm::modelchecker::CheckTask checkTask(gameFormula); + + storm::storage::BitVector statesOfCoalition = model->computeStatesOfCoalition(gameFormula.getCoalition()); + statesOfCoalition.complement(); + + // TODO Fabian: get optimization direction + + storm::storage::BitVector psiStates = checker->check(this->env(), gameFormula.getSubformula().asProbabilityOperatorFormula().getSubformula().asEventuallyFormula().getSubformula().asStateFormula())->asExplicitQualitativeCheckResult().getTruthValuesVector(); + storm::storage::BitVector phiStates(model->getNumberOfStates(), true); + + storm::storage::SparseMatrix backwardTransitions = model->getBackwardTransitions(); + storm::OptimizationDirection optimizationDirection = storm::OptimizationDirection::Maximize; + auto minimizerStates = optimizationDirection == storm::OptimizationDirection::Maximize ? statesOfCoalition : ~statesOfCoalition; + + storm::modelchecker::helper::internal::SoundGameViHelper viHelper(transitionMatrix, backwardTransitions, statesOfCoalition, psiStates, optimizationDirection); + viHelper.prepareSolversAndMultipliers(this->env()); + + std::vector xL = std::vector(transitionMatrix.getRowGroupCount(), storm::utility::zero()); + for (size_t i = 0; i < xL.size(); i++) + { + if (psiStates[i]) + xL[i] = 1; + } + + std::vector xU = std::vector(transitionMatrix.getRowGroupCount(), storm::utility::zero()); + storm::storage::BitVector probGreater0 = storm::utility::graph::performProbGreater0(backwardTransitions, phiStates, psiStates); + auto xU_begin = xU.begin(); + std::for_each(xU.begin(), xU.end(), [&probGreater0, &xU_begin](ValueType &it) + { + if (probGreater0[&it - &(*xU_begin)]) + it = 1; + }); + + // performValueIteration + std::vector _x1L = xL; + std::vector _x2L = _x1L; + + std::vector _x1U = xU; + std::vector _x2U = _x1U; + + // perform first iteration step + storm::storage::BitVector reducedMinimizerActions = {storm::storage::BitVector(transitionMatrix.getRowCount(), true)}; + std::vector choiceValuesL = std::vector(transitionMatrix.getRowCount(), storm::utility::zero()); + + viHelper._multiplier->multiply(this->env(), _x2L, nullptr, choiceValuesL); + + viHelper.reduceChoiceValues(choiceValuesL, &reducedMinimizerActions, _x1L); + + + // over approximation + std::vector choiceValuesU = std::vector(transitionMatrix.getRowCount(), storm::utility::zero()); + + viHelper._multiplier->multiply(this->env(), _x2U, nullptr, choiceValuesU); + viHelper.reduceChoiceValues(choiceValuesU, nullptr, _x1U); + + storm::storage::SparseMatrix restrictedTransMatrix = transitionMatrix.restrictRows(reducedMinimizerActions); + + storm::storage::MaximalEndComponentDecomposition MSEC = storm::storage::MaximalEndComponentDecomposition(restrictedTransMatrix, backwardTransitions); + + // reducing the choiceValuesU + size_t i = 0; + auto new_end = std::remove_if(choiceValuesU.begin(), choiceValuesU.end(), [&reducedMinimizerActions, &i](const auto& item) { + bool ret = !(reducedMinimizerActions[i]); + i++; + return ret; + }); + choiceValuesU.erase(new_end, choiceValuesU.end()); + + // deflating the MSECs + viHelper.deflate(MSEC, restrictedTransMatrix, _x1U, choiceValuesU); + + xL = _x1L; + xU = _x1U; + + EXPECT_NEAR(this->parseNumber("0"), xL[0], this->precision()); + EXPECT_NEAR(this->parseNumber("0.333333"), xL[1], this->precision()); + EXPECT_NEAR(this->parseNumber("1"), xL[2], this->precision()); + EXPECT_NEAR(this->parseNumber("0"), xL[3], this->precision()); + + EXPECT_NEAR(this->parseNumber("0.666666"), xU[0], this->precision()); + EXPECT_NEAR(this->parseNumber("0.666666"), xU[1], this->precision()); + EXPECT_NEAR(this->parseNumber("1"), xU[2], this->precision()); + EXPECT_NEAR(this->parseNumber("0"), xU[3], this->precision()); + + // second iteration step + + reducedMinimizerActions = {storm::storage::BitVector(transitionMatrix.getRowCount(), true)}; + choiceValuesL = std::vector(transitionMatrix.getRowCount(), storm::utility::zero()); + + viHelper._multiplier->multiply(this->env(), _x1L, nullptr, choiceValuesL); + + viHelper.reduceChoiceValues(choiceValuesL, &reducedMinimizerActions, _x2L); + + + // over approximation + choiceValuesU = std::vector(transitionMatrix.getRowCount(), storm::utility::zero()); + + viHelper._multiplier->multiply(this->env(), _x1U, nullptr, choiceValuesU); + viHelper.reduceChoiceValues(choiceValuesU, nullptr, _x2U); + + restrictedTransMatrix = transitionMatrix.restrictRows(reducedMinimizerActions); + + MSEC = storm::storage::MaximalEndComponentDecomposition(restrictedTransMatrix, backwardTransitions); + + // reducing the choiceValuesU + i = 0; + new_end = std::remove_if(choiceValuesU.begin(), choiceValuesU.end(), [&reducedMinimizerActions, &i](const auto& item) { + bool ret = !(reducedMinimizerActions[i]); + i++; + return ret; + }); + choiceValuesU.erase(new_end, choiceValuesU.end()); + + // deflating the MSECs + viHelper.deflate(MSEC, restrictedTransMatrix, _x2U, choiceValuesU); + + xL = _x2L; + xU = _x2U; + + EXPECT_NEAR(this->parseNumber("0.333333"), xL[0], this->precision()); + EXPECT_NEAR(this->parseNumber("0.444444"), xL[1], this->precision()); + EXPECT_NEAR(this->parseNumber("1"), xL[2], this->precision()); + EXPECT_NEAR(this->parseNumber("0"), xL[3], this->precision()); + + EXPECT_NEAR(this->parseNumber("0.555555"), xU[0], this->precision()); + EXPECT_NEAR(this->parseNumber("0.555555"), xU[1], this->precision()); + EXPECT_NEAR(this->parseNumber("1"), xU[2], this->precision()); + EXPECT_NEAR(this->parseNumber("0"), xU[3], this->precision()); + + } + // TODO: create more test cases (files) }