added class BoundedGloballyGameViHelper

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

@@ -0,0 +1,169 @@
+#include "BoundedGloballyGameViHelper.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>
+                BoundedGloballyGameViHelper<ValueType>::GameViHelper(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector statesOfCoalition) : _transitionMatrix(transitionMatrix), _statesOfCoalition(statesOfCoalition) {
+                }
+
+                template <typename ValueType>
+                void BoundedGloballyGameViHelper<ValueType>::prepareSolversAndMultipliersReachability(const Environment& env) {
+                    _multiplier = storm::solver::MultiplierFactory<ValueType>().create(env, _transitionMatrix);
+                    _x1IsCurrent = false;
+                }
+
+                template <typename ValueType>
+                void BoundedGloballyGameViHelper<ValueType>::performValueIteration(Environment const& env, std::vector<ValueType>& x, std::vector<ValueType> b, storm::solver::OptimizationDirection const dir) {
+                    prepareSolversAndMultipliersReachability(env);
+                    // TODO: parse k from the formula
+                    uint64_t k = 3;
+                    _b = b;
+
+                    _x1.assign(_transitionMatrix.getRowGroupCount(), storm::utility::zero<ValueType>());
+                    _x2 = _x1;
+
+                    if (this->isProduceSchedulerSet()) {
+                        if (!this->_producedOptimalChoices.is_initialized()) {
+                            this->_producedOptimalChoices.emplace();
+                        }
+                        this->_producedOptimalChoices->resize(this->_transitionMatrix.getRowGroupCount());
+                    }
+
+                    uint64_t iter = 0;
+                    std::vector<ValueType> result = x;
+                    while (iter < k) {
+                        ++iter;
+                        performIterationStep(env, dir);
+
+                        if (storm::utility::resources::isTerminate()) {
+                            break;
+                        }
+                    }
+                    x = xNew();
+
+                    // TODO: do we have to do that by using boundedGlobally?
+                    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 BoundedGloballyGameViHelper<ValueType>::performIterationStep(Environment const& env, storm::solver::OptimizationDirection const dir, std::vector<uint64_t>* choices) {
+                    if (!_multiplier) {
+                        prepareSolversAndMultipliersReachability(env);
+                    }
+                    _x1IsCurrent = !_x1IsCurrent;
+
+                    // multiplyandreducegaussseidel
+                    // Ax + b
+                    if (choices == nullptr) {
+                        //STORM_LOG_DEBUG("\n" << _transitionMatrix);
+                        //STORM_LOG_DEBUG("xOld = " << storm::utility::vector::toString(xOld()));
+                        //STORM_LOG_DEBUG("b = " << storm::utility::vector::toString(_b));
+                        //STORM_LOG_DEBUG("xNew = " << storm::utility::vector::toString(xNew()));
+                        _multiplier->multiplyAndReduce(env, dir, xOld(), &_b, xNew(), nullptr, &_statesOfCoalition);
+                        //std::cin.get();
+                    } else {
+                        // Also keep track of the choices made.
+                        _multiplier->multiplyAndReduce(env, dir, xOld(), &_b, xNew(), choices, &_statesOfCoalition);
+                    }
+
+                    // compare applyPointwise
+                    storm::utility::vector::applyPointwise<ValueType, ValueType, ValueType>(xOld(), xNew(), xNew(), [&dir] (ValueType const& a, ValueType const& b) -> ValueType {
+                        if(storm::solver::maximize(dir)) {
+                            if(a > b) return a;
+                            else return b;
+                        } else {
+                            if(a > b) return a;
+                            else return b;
+                        }
+                    });
+                }
+
+                template <typename ValueType>
+                void BoundedGloballyGameViHelper<ValueType>::fillResultVector(std::vector<ValueType>& result, storm::storage::BitVector psiStates)
+                {
+                    std::vector<ValueType> filledVector = std::vector<ValueType>(relevantStates.size(), storm::utility::zero<ValueType>());
+                    uint bitIndex = 0;
+                    for(uint i = 0; i < filledVector.size(); i++) {
+                        if (psiStates.get(i)) {
+                            filledVector.at(i) = result.at(bitIndex);
+                            bitIndex++;
+                        }
+                    }
+                    result = filledVector;
+                }
+
+                template <typename ValueType>
+                void BoundedGloballyGameViHelper<ValueType>::setProduceScheduler(bool value) {
+                    _produceScheduler = value;
+                }
+
+                template <typename ValueType>
+                bool BoundedGloballyGameViHelper<ValueType>::isProduceSchedulerSet() const {
+                    return _produceScheduler;
+                }
+
+                template <typename ValueType>
+                std::vector<uint64_t> const& BoundedGloballyGameViHelper<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>& BoundedGloballyGameViHelper<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> BoundedGloballyGameViHelper<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>
+                std::vector<ValueType>& BoundedGloballyGameViHelper<ValueType>::xNew() {
+                    return _x1IsCurrent ? _x1 : _x2;
+                }
+
+                template <typename ValueType>
+                std::vector<ValueType> const& BoundedGloballyGameViHelper<ValueType>::xNew() const {
+                    return _x1IsCurrent ? _x1 : _x2;
+                }
+
+                template <typename ValueType>
+                std::vector<ValueType>& BoundedGloballyGameViHelper<ValueType>::xOld() {
+                    return _x1IsCurrent ? _x2 : _x1;
+                }
+
+                template <typename ValueType>
+                std::vector<ValueType> const& BoundedGloballyGameViHelper<ValueType>::xOld() const {
+                    return _x1IsCurrent ? _x2 : _x1;
+                }
+
+                template class BoundedGloballyGameViHelper<double>;
+#ifdef STORM_HAVE_CARL
+                template class BoundedGloballyGameViHelper<storm::RationalNumber>;
+#endif
+            }
+        }
+    }
+}

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

@@ -0,0 +1,79 @@
+#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 BoundedGloballyGameViHelper {
+                public:
+                    BoundedGloballyGameViHelper(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector statesOfCoalition);
+
+                    void prepareSolversAndMultipliersReachability(const Environment& env);
+
+                    // TODO: add 'k' as input of the method - maybe the type TimeBound from the formula
+                    void performValueIteration(Environment const& env, std::vector<ValueType>& x, std::vector<ValueType> b, storm::solver::OptimizationDirection const dir);
+
+                    /*!
+                     * Fills the result vector to the original size with ones for being psiStates, zeros for being not phiStates
+                     */
+                    void fillResultVector(std::vector<ValueType>& result, storm::storage::BitVector psiStates);
+
+                    /*h
+                     * 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;
+
+                    storm::storage::Scheduler<ValueType> extractScheduler() const;
+
+                private:
+                    void performIterationStep(Environment const& env, storm::solver::OptimizationDirection const dir, std::vector<uint64_t>* choices = nullptr);
+
+                    std::vector<ValueType>& xNew();
+                    std::vector<ValueType> const& xNew() const;
+
+                    std::vector<ValueType>& xOld();
+                    std::vector<ValueType> const& xOld() 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> _x1, _x2, _b;
+                    std::unique_ptr<storm::solver::Multiplier<ValueType>> _multiplier;
+
+                    bool _produceScheduler = false;
+                    boost::optional<std::vector<uint64_t>> _producedOptimalChoices;
+                };
+            }
+        }
+    }
+}