SmgRpatlModelCheckerTest.cpp: added test for deflate method of SoundGameViHelper.cpp

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

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<ValueType> restrictedTransMatrix = this->_transitionMatrix.restrictRows(reducedMinimizerActions);
 
@@ -124,12 +122,11 @@ namespace storm {
                 template <typename ValueType>
                 void SoundGameViHelper<ValueType>::deflate(storm::storage::MaximalEndComponentDecomposition<ValueType> const MSEC, storage::SparseMatrix<ValueType> const restrictedMatrix,  std::vector<ValueType>& xU, std::vector<ValueType> 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;

src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.h

@@ -68,16 +68,18 @@ namespace storm {
                      */
                     void fillChoiceValuesVector(std::vector<ValueType>& choiceValues, storm::storage::BitVector psiStates, std::vector<storm::storage::SparseMatrix<double>::index_type> rowGroupIndices);
 
+                    void deflate(storm::storage::MaximalEndComponentDecomposition<ValueType> const MECD, storage::SparseMatrix<ValueType> const restrictedMatrix, std::vector<ValueType>& xU, std::vector<ValueType> choiceValues);
+
+                    void reduceChoiceValues(std::vector<ValueType>& choiceValues, storm::storage::BitVector* result, std::vector<ValueType>& x);
+
+                    // multiplier now public for testing
+                    std::unique_ptr<storm::solver::Multiplier<ValueType>> _multiplier;
                 private:
                     /*!
                      * Performs one iteration step for value iteration
                      */
                     void performIterationStep(Environment const& env, storm::solver::OptimizationDirection const dir, std::vector<uint64_t>* choices = nullptr);
 
-                    void deflate(storm::storage::MaximalEndComponentDecomposition<ValueType> const MECD, storage::SparseMatrix<ValueType> const restrictedMatrix, std::vector<ValueType>& xU, std::vector<ValueType> choiceValues);
-
-                    void reduceChoiceValues(std::vector<ValueType>& choiceValues, storm::storage::BitVector* result, std::vector<ValueType>& 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<ValueType> _x, _x1L, _x2L, _x1U, _x2U;
-                    std::unique_ptr<storm::solver::Multiplier<ValueType>> _multiplier;
                     OptimizationDirection _optimizationDirection;
 
                     bool _produceScheduler = false;

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

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<storm::modelchecker::CheckTask<storm::logic::Formula, ValueType>> getTasks(std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) const {
             std::vector<storm::modelchecker::CheckTask<storm::logic::Formula, ValueType>> 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 = " <<maxP>> 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<storm::modelchecker::CheckResult> result;
+        auto transitionMatrix = model->getTransitionMatrix();
+
+
+        auto formulas = std::move(modelFormulas.second);
+
+        storm::logic::GameFormula const& gameFormula = formulas[0]->asGameFormula();
+
+        storm::modelchecker::CheckTask<storm::logic::GameFormula, ValueType> 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<ValueType> backwardTransitions = model->getBackwardTransitions();
+        storm::OptimizationDirection optimizationDirection = storm::OptimizationDirection::Maximize;
+        auto minimizerStates = optimizationDirection == storm::OptimizationDirection::Maximize ? statesOfCoalition : ~statesOfCoalition;
+
+        storm::modelchecker::helper::internal::SoundGameViHelper<ValueType> viHelper(transitionMatrix, backwardTransitions, statesOfCoalition, psiStates, optimizationDirection);
+        viHelper.prepareSolversAndMultipliers(this->env());
+
+        std::vector<ValueType> xL = std::vector<ValueType>(transitionMatrix.getRowGroupCount(), storm::utility::zero<ValueType>());
+        for (size_t i = 0; i < xL.size(); i++)
+        {
+            if (psiStates[i])
+                xL[i] = 1;
+        }
+
+        std::vector<ValueType> xU = std::vector<ValueType>(transitionMatrix.getRowGroupCount(), storm::utility::zero<ValueType>());
+        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<ValueType> _x1L = xL;
+        std::vector<ValueType> _x2L = _x1L;
+
+        std::vector<ValueType> _x1U = xU;
+        std::vector<ValueType> _x2U = _x1U;
+
+        // perform first iteration step
+        storm::storage::BitVector reducedMinimizerActions = {storm::storage::BitVector(transitionMatrix.getRowCount(), true)};
+        std::vector<ValueType> choiceValuesL = std::vector<ValueType>(transitionMatrix.getRowCount(), storm::utility::zero<ValueType>());
+
+        viHelper._multiplier->multiply(this->env(), _x2L, nullptr, choiceValuesL);
+
+        viHelper.reduceChoiceValues(choiceValuesL, &reducedMinimizerActions, _x1L);
+
+
+        // over approximation
+        std::vector<ValueType> choiceValuesU = std::vector<ValueType>(transitionMatrix.getRowCount(), storm::utility::zero<ValueType>());
+
+        viHelper._multiplier->multiply(this->env(), _x2U, nullptr, choiceValuesU);
+        viHelper.reduceChoiceValues(choiceValuesU, nullptr, _x1U);
+
+        storm::storage::SparseMatrix<ValueType> restrictedTransMatrix = transitionMatrix.restrictRows(reducedMinimizerActions);
+
+        storm::storage::MaximalEndComponentDecomposition<ValueType> MSEC = storm::storage::MaximalEndComponentDecomposition<ValueType>(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<ValueType>(transitionMatrix.getRowCount(), storm::utility::zero<ValueType>());
+
+        viHelper._multiplier->multiply(this->env(), _x1L, nullptr, choiceValuesL);
+
+        viHelper.reduceChoiceValues(choiceValuesL, &reducedMinimizerActions, _x2L);
+
+
+        // over approximation
+        choiceValuesU = std::vector<ValueType>(transitionMatrix.getRowCount(), storm::utility::zero<ValueType>());
+
+        viHelper._multiplier->multiply(this->env(), _x1U, nullptr, choiceValuesU);
+        viHelper.reduceChoiceValues(choiceValuesU, nullptr, _x2U);
+
+        restrictedTransMatrix = transitionMatrix.restrictRows(reducedMinimizerActions);
+
+        MSEC = storm::storage::MaximalEndComponentDecomposition<ValueType>(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)
 }