L(S) and G(S) (from paper)

src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp

@@ -141,8 +141,7 @@ namespace storm {
             ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult();
             ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult();
 
-
-            auto ret = storm::modelchecker::helper::SparseSmgRpatlHelper<ValueType>::computeUntilProbabilities(env, storm::solver::SolveGoal<ValueType>(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), statesOfCoalition, checkTask.isProduceSchedulersSet(), checkTask.getHint());
+            auto ret = storm::modelchecker::helper::SparseSmgRpatlHelper<ValueType>::computeUntilProbabilitiesSound(env, storm::solver::SolveGoal<ValueType>(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), statesOfCoalition, checkTask.isProduceSchedulersSet(), checkTask.getHint());
             std::unique_ptr<CheckResult> result(new ExplicitQuantitativeCheckResult<ValueType>(std::move(ret.values)));
             if(checkTask.isShieldingTask()) {
                 storm::storage::BitVector allStatesBv = storm::storage::BitVector(this->getModel().getTransitionMatrix().getRowGroupCount(), true);

src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp

@@ -9,6 +9,7 @@
 #include "storm/utility/vector.h"
 #include "storm/utility/graph.h"
 #include "storm/modelchecker/rpatl/helper/internal/GameViHelper.h"
+#include "storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.h"
 
 namespace storm {
     namespace modelchecker {
@@ -59,6 +60,43 @@ namespace storm {
                 return SMGSparseModelCheckingHelperReturnType<ValueType>(std::move(result), std::move(relevantStates), std::move(scheduler), std::move(constrainedChoiceValues));
             }
 
+            template<typename ValueType>
+            SMGSparseModelCheckingHelperReturnType<ValueType> SparseSmgRpatlHelper<ValueType>::computeUntilProbabilitiesSound(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> 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<ValueType> viHelper(transitionMatrix, statesOfCoalition);
+
+                // Initialize the x vector and solution vector result.
+                // TODO Fabian: maybe relevant states (later)
+                std::vector<ValueType> xL = std::vector<ValueType>(transitionMatrix.getRowGroupCount(), storm::utility::zero<ValueType>());
+                // 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
+                assert(xL.size() == psiStates.size());
+                for (size_t i = 0; i < xL.size(); i++)
+                {
+                    if (psiStates[xL.size() - i])
+                        xL[i] = 1;
+                }
+                STORM_LOG_DEBUG("xL " << xL);
+                std::vector<ValueType> xU = std::vector<ValueType>(transitionMatrix.getRowGroupCount(), storm::utility::zero<ValueType>());
+                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++)
+                {
+                    if (probGreater0[i])
+                        xU[i] = 1;
+                }
+                STORM_LOG_DEBUG("xU " << xU);
+
+                std::vector<ValueType> result = std::vector<ValueType>(transitionMatrix.getRowGroupCount(), storm::utility::zero<ValueType>());
+                // std::vector<ValueType> constrainedChoiceValues = std::vector<ValueType>(b.size(), storm::utility::zero<ValueType>()); // TODO Fabian: do I need this?
+                std::vector<ValueType> constrainedChoiceValues;
+
+                viHelper.performValueIteration(env, xL, xU, goal.direction(), constrainedChoiceValues);
+
+                assert(false);
+            }
+
             template<typename ValueType>
             storm::storage::Scheduler<ValueType> SparseSmgRpatlHelper<ValueType>::expandScheduler(storm::storage::Scheduler<ValueType> scheduler, storm::storage::BitVector psiStates, storm::storage::BitVector notPhiStates) {
                 storm::storage::Scheduler<ValueType> completeScheduler(psiStates.size());

src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.h

@@ -35,6 +35,7 @@ namespace storm {
             class SparseSmgRpatlHelper {
             public:
                 static SMGSparseModelCheckingHelperReturnType<ValueType> computeUntilProbabilities(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint = ModelCheckerHint());
+                static SMGSparseModelCheckingHelperReturnType<ValueType> computeUntilProbabilitiesSound(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint);
                 static SMGSparseModelCheckingHelperReturnType<ValueType> computeGloballyProbabilities(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint = ModelCheckerHint());
                 static SMGSparseModelCheckingHelperReturnType<ValueType> computeNextProbabilities(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint);
                 static SMGSparseModelCheckingHelperReturnType<ValueType> computeBoundedGloballyProbabilities(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint, uint64_t lowerBound, uint64_t upperBound);

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

@@ -0,0 +1,255 @@
+#include "SoundGameViHelper.h"
+
+#include "storm/environment/Environment.h"
+#include "storm/environment/solver/SolverEnvironment.h"
+#include "storm/environment/solver/GameSolverEnvironment.h"
+
+
+#include "storm/utility/SignalHandler.h"
+#include "storm/utility/vector.h"
+
+namespace storm {
+    namespace modelchecker {
+        namespace helper {
+            namespace internal {
+
+                template <typename ValueType>
+                SoundGameViHelper<ValueType>::SoundGameViHelper(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector statesOfCoalition) : _transitionMatrix(transitionMatrix), _statesOfCoalition(statesOfCoalition) {
+                    // Intentionally left empty.
+                }
+
+                template <typename ValueType>
+                void SoundGameViHelper<ValueType>::prepareSolversAndMultipliers(const Environment& env) {
+                    STORM_LOG_DEBUG("\n" << _transitionMatrix);
+                    _multiplier = storm::solver::MultiplierFactory<ValueType>().create(env, _transitionMatrix);
+                    _x1IsCurrent = false;
+                }
+
+                template <typename ValueType>
+                void SoundGameViHelper<ValueType>::performValueIteration(Environment const& env, std::vector<ValueType>& xL, std::vector<ValueType>& xU, storm::solver::OptimizationDirection const dir, std::vector<ValueType>& constrainedChoiceValues) {
+                    // new pair (x_old, x_new) for over_approximation()
+
+                    prepareSolversAndMultipliers(env);
+                    // Get precision for convergence check.
+                    ValueType precision = storm::utility::convertNumber<ValueType>(env.solver().game().getPrecision());
+
+                    STORM_LOG_DEBUG("hello" << "world");
+                    uint64_t maxIter = env.solver().game().getMaximalNumberOfIterations();
+                    //_x1.assign(_transitionMatrix.getRowGroupCount(), storm::utility::zero<ValueType>());
+                    _x1L = xL;
+                    _x2L = _x1L;
+
+                    _x1U = xU;
+                    _x2U = _x1U;
+
+                    if (this->isProduceSchedulerSet()) {
+                        if (!this->_producedOptimalChoices.is_initialized()) {
+                            this->_producedOptimalChoices.emplace();
+                        }
+                        this->_producedOptimalChoices->resize(this->_transitionMatrix.getRowGroupCount());
+                    }
+
+                    uint64_t iter = 0;
+                    constrainedChoiceValues = std::vector<ValueType>(xL.size(), storm::utility::zero<ValueType>()); // ??
+
+                    while (iter < maxIter) {
+                        performIterationStep(env, dir);
+                        if (checkConvergence(precision)) {
+                            //_multiplier->multiply(env, xNewL(), nullptr, constrainedChoiceValues); // TODO Fabian: ???
+                            break;
+                        }
+                        if (storm::utility::resources::isTerminate()) {
+                            break;
+                        }
+                        ++iter;
+                    }
+                    xL = xNewL();
+                    xU = xNewU();
+
+                    STORM_LOG_DEBUG("result xL: " << xL);
+                    STORM_LOG_DEBUG("result xU: " << xU);
+
+                    if (isProduceSchedulerSet()) {
+                        // We will be doing one more iteration step and track scheduler choices this time.
+                        performIterationStep(env, dir, &_producedOptimalChoices.get());
+                    }
+                }
+
+                template <typename ValueType>
+                void SoundGameViHelper<ValueType>::performIterationStep(Environment const& env, storm::solver::OptimizationDirection const dir, std::vector<uint64_t>* choices) {
+                    // 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);
+                    }
+
+                    // over_approximation
+
+                    if (choices == nullptr) {
+                        _multiplier->multiplyAndReduce(env, dir, xOldU(), nullptr, xNewU(), nullptr, &_statesOfCoalition);
+                    } else {
+                        _multiplier->multiplyAndReduce(env, dir, xOldU(), nullptr, xNewU(), choices, &_statesOfCoalition);
+                    }
+
+                    // TODO Fabian: find_MSECs() & deflate()
+
+                }
+
+                template <typename ValueType>
+                bool SoundGameViHelper<ValueType>::checkConvergence(ValueType threshold) const {
+                    STORM_LOG_ASSERT(_multiplier, "tried to check for convergence without doing an iteration first.");
+                    // Now check whether the currently produced results are precise enough
+                    STORM_LOG_ASSERT(threshold > storm::utility::zero<ValueType>(), "Did not expect a non-positive threshold.");
+                    auto x1It = xOldL().begin();
+                    auto x1Ite = xOldL().end();
+                    auto x2It = xNewL().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) {
+                        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) {
+                            return false;
+                        }
+                    }
+                    return true;
+                }
+
+                template <typename ValueType>
+                void SoundGameViHelper<ValueType>::setProduceScheduler(bool value) {
+                    _produceScheduler = value;
+                }
+
+                template <typename ValueType>
+                bool SoundGameViHelper<ValueType>::isProduceSchedulerSet() const {
+                    return _produceScheduler;
+                }
+
+                template <typename ValueType>
+                void SoundGameViHelper<ValueType>::setShieldingTask(bool value) {
+                    _shieldingTask = value;
+                }
+
+                template <typename ValueType>
+                bool SoundGameViHelper<ValueType>::isShieldingTask() const {
+                    return _shieldingTask;
+                }
+
+                template <typename ValueType>
+                void SoundGameViHelper<ValueType>::updateTransitionMatrix(storm::storage::SparseMatrix<ValueType> newTransitionMatrix) {
+                    _transitionMatrix = newTransitionMatrix;
+                }
+
+                template <typename ValueType>
+                void SoundGameViHelper<ValueType>::updateStatesOfCoalition(storm::storage::BitVector newStatesOfCoalition) {
+                    _statesOfCoalition = newStatesOfCoalition;
+                }
+
+                template <typename ValueType>
+                std::vector<uint64_t> const& SoundGameViHelper<ValueType>::getProducedOptimalChoices() const {
+                    STORM_LOG_ASSERT(this->isProduceSchedulerSet(), "Trying to get the produced optimal choices although no scheduler was requested.");
+                    STORM_LOG_ASSERT(this->_producedOptimalChoices.is_initialized(), "Trying to get the produced optimal choices but none were available. Was there a computation call before?");
+                    return this->_producedOptimalChoices.get();
+                }
+
+                template <typename ValueType>
+                std::vector<uint64_t>& SoundGameViHelper<ValueType>::getProducedOptimalChoices() {
+                    STORM_LOG_ASSERT(this->isProduceSchedulerSet(), "Trying to get the produced optimal choices although no scheduler was requested.");
+                    STORM_LOG_ASSERT(this->_producedOptimalChoices.is_initialized(), "Trying to get the produced optimal choices but none were available. Was there a computation call before?");
+                    return this->_producedOptimalChoices.get();
+                }
+
+                template <typename ValueType>
+                storm::storage::Scheduler<ValueType> SoundGameViHelper<ValueType>::extractScheduler() const{
+                    auto const& optimalChoices = getProducedOptimalChoices();
+                    storm::storage::Scheduler<ValueType> scheduler(optimalChoices.size());
+                    for (uint64_t state = 0; state < optimalChoices.size(); ++state) {
+                        scheduler.setChoice(optimalChoices[state], state);
+                    }
+                    return scheduler;
+                }
+
+                template <typename ValueType>
+                void SoundGameViHelper<ValueType>::getChoiceValues(Environment const& env, std::vector<ValueType> const& x, std::vector<ValueType>& choiceValues) {
+                    _multiplier->multiply(env, x, nullptr, choiceValues);
+                }
+
+                template <typename ValueType>
+                void SoundGameViHelper<ValueType>::fillChoiceValuesVector(std::vector<ValueType>& choiceValues, storm::storage::BitVector psiStates, std::vector<storm::storage::SparseMatrix<double>::index_type> rowGroupIndices) {
+                    std::vector<ValueType> allChoices = std::vector<ValueType>(rowGroupIndices.at(rowGroupIndices.size() - 1), storm::utility::zero<ValueType>());
+                    auto choice_it = choiceValues.begin();
+                    for(uint state = 0; state < rowGroupIndices.size() - 1; state++) {
+                        uint rowGroupSize = rowGroupIndices[state + 1] - rowGroupIndices[state];
+                        if (psiStates.get(state)) {
+                            for(uint choice = 0; choice < rowGroupSize; choice++, choice_it++) {
+                                allChoices.at(rowGroupIndices.at(state) + choice) = *choice_it;
+                            }
+                        }
+                    }
+                    choiceValues = allChoices;
+                }
+
+                template <typename ValueType>
+                std::vector<ValueType>& SoundGameViHelper<ValueType>::xNewL() {
+                    return _x1IsCurrent ? _x1L : _x2L;
+                }
+
+                template <typename ValueType>
+                std::vector<ValueType> const& SoundGameViHelper<ValueType>::xNewL() const {
+                    return _x1IsCurrent ? _x1L : _x2L;
+                }
+
+                template <typename ValueType>
+                std::vector<ValueType>& SoundGameViHelper<ValueType>::xOldL() {
+                    return _x1IsCurrent ? _x2L : _x1L;
+                }
+
+                template <typename ValueType>
+                std::vector<ValueType> const& SoundGameViHelper<ValueType>::xOldL() const {
+                    return _x1IsCurrent ? _x2L : _x1L;
+                }
+
+                template <typename ValueType>
+                std::vector<ValueType>& SoundGameViHelper<ValueType>::xNewU() {
+                    return _x1IsCurrent ? _x1U : _x2U;
+                }
+
+                template <typename ValueType>
+                std::vector<ValueType> const& SoundGameViHelper<ValueType>::xNewU() const {
+                    return _x1IsCurrent ? _x1U : _x2U;
+                }
+
+                template <typename ValueType>
+                std::vector<ValueType>& SoundGameViHelper<ValueType>::xOldU() {
+                    return _x1IsCurrent ? _x2U : _x1U;
+                }
+
+                template <typename ValueType>
+                std::vector<ValueType> const& SoundGameViHelper<ValueType>::xOldU() const {
+                    return _x1IsCurrent ? _x2U : _x1U;
+                }
+
+                template class SoundGameViHelper<double>;
+#ifdef STORM_HAVE_CARL
+                template class SoundGameViHelper<storm::RationalNumber>;
+#endif
+            }
+        }
+    }
+}

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

@@ -0,0 +1,119 @@
+#pragma once
+
+#include "storm/storage/SparseMatrix.h"
+#include "storm/solver/LinearEquationSolver.h"
+#include "storm/solver/MinMaxLinearEquationSolver.h"
+#include "storm/solver/Multiplier.h"
+
+namespace storm {
+    class Environment;
+
+    namespace storage {
+        template <typename VT> class Scheduler;
+    }
+
+    namespace modelchecker {
+        namespace helper {
+            namespace internal {
+
+                template <typename ValueType>
+                class SoundGameViHelper {
+                public:
+                    SoundGameViHelper(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector statesOfCoalition);
+
+                    void prepareSolversAndMultipliers(const Environment& env);
+
+                    /*!
+                     * Perform value iteration until convergence
+                     */
+                    void performValueIteration(Environment const& env, std::vector<ValueType>& xL, std::vector<ValueType>& xU, storm::solver::OptimizationDirection const dir, std::vector<ValueType>& constrainedChoiceValues);
+
+                    /*!
+                     * Sets whether an optimal scheduler shall be constructed during the computation
+                     */
+                    void setProduceScheduler(bool value);
+
+                    /*!
+                     * @return whether an optimal scheduler shall be constructed during the computation
+                     */
+                    bool isProduceSchedulerSet() const;
+
+                    /*!
+                     * Sets whether an optimal scheduler shall be constructed during the computation
+                     */
+                    void setShieldingTask(bool value);
+
+                    /*!
+                     * @return whether an optimal scheduler shall be constructed during the computation
+                     */
+                    bool isShieldingTask() const;
+
+                    /*!
+                     * Changes the transitionMatrix to the given one.
+                     */
+                    void updateTransitionMatrix(storm::storage::SparseMatrix<ValueType> newTransitionMatrix);
+
+                    /*!
+                     * Changes the statesOfCoalition to the given one.
+                     */
+                    void updateStatesOfCoalition(storm::storage::BitVector newStatesOfCoalition);
+
+                    storm::storage::Scheduler<ValueType> extractScheduler() const;
+
+                    void getChoiceValues(Environment const& env, std::vector<ValueType> const& x, std::vector<ValueType>& choiceValues);
+
+                    /*!
+                     * Fills the choice values vector to the original size with zeros for ~psiState choices.
+                     */
+                    void fillChoiceValuesVector(std::vector<ValueType>& choiceValues, storm::storage::BitVector psiStates, std::vector<storm::storage::SparseMatrix<double>::index_type> rowGroupIndices);
+
+                private:
+                    /*!
+                     * Performs one iteration step for value iteration
+                     */
+                    void performIterationStep(Environment const& env, storm::solver::OptimizationDirection const dir, std::vector<uint64_t>* choices = nullptr);
+
+                    /*!
+                     * Checks whether the curently computed value achieves the desired precision
+                     */
+                    bool checkConvergence(ValueType precision) const;
+
+                    std::vector<ValueType>& xNewL();
+                    std::vector<ValueType> const& xNewL() const;
+
+                    std::vector<ValueType>& xOldL();
+                    std::vector<ValueType> const& xOldL() const;
+
+                    std::vector<ValueType>& xNewU();
+                    std::vector<ValueType> const& xNewU() const;
+
+                    std::vector<ValueType>& xOldU();
+                    std::vector<ValueType> const& xOldU() const;
+
+                    bool _x1IsCurrent;
+
+                    /*!
+                     * @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.
+                     */
+                    std::vector<uint64_t> const& getProducedOptimalChoices() const;
+
+                    /*!
+                     * @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.
+                     */
+                    std::vector<uint64_t>& getProducedOptimalChoices();
+
+                    storm::storage::SparseMatrix<ValueType> _transitionMatrix;
+                    storm::storage::BitVector _statesOfCoalition;
+                    std::vector<ValueType> _x, _x1L, _x2L, _x1U, _x2U;
+                    std::unique_ptr<storm::solver::Multiplier<ValueType>> _multiplier;
+
+                    bool _produceScheduler = false;
+                    bool _shieldingTask = false;
+                    boost::optional<std::vector<uint64_t>> _producedOptimalChoices;
+                };
+            }
+        }
+    }
+}