Extended functionality of game solver: repeated multiply, scheduler hints

src/storm/solver/AbstractGameSolver.cpp

@@ -61,6 +61,27 @@ namespace storm {
             return relative;
         }
     
+        template <typename ValueType>
+        void AbstractGameSolver<ValueType>::setSchedulerHint(storm::storage::TotalScheduler&& player1Scheduler, storm::storage::TotalScheduler&& player2Scheduler) {
+            player1SchedulerHint = player1Scheduler;
+            player2SchedulerHint = player2Scheduler;
+        }
+    
+        template <typename ValueType>
+        bool AbstractGameSolver<ValueType>::hasSchedulerHints() const {
+            return player1SchedulerHint.is_initialized() && player2SchedulerHint.is_initialized();
+        }
+    
+        template <typename ValueType>
+        void AbstractGameSolver<ValueType>::setLowerBound(ValueType const& value) {
+            this->lowerBound = value;
+        }
+    
+        template <typename ValueType>
+        void AbstractGameSolver<ValueType>::setUpperBound(ValueType const& value) {
+            this->upperBound = value;
+        }
+    
         template class AbstractGameSolver<double>;
         
     }

src/storm/solver/AbstractGameSolver.h

@@ -33,6 +33,15 @@ namespace storm {
              */
             AbstractGameSolver(double precision, uint_fast64_t maximalNumberOfIterations, bool relative);
             
+            /*!
+             * Sets schedulers that might be considered by the solver as an initial guess
+             */
+            void setSchedulerHint(storm::storage::TotalScheduler&& player1Scheduler, storm::storage::TotalScheduler&& player2Scheduler);
+            bool hasSchedulerHints() const;
+            
+            void setLowerBound(ValueType const& value);
+            void setUpperBound(ValueType const& value);
+            
             void setTrackScheduler(bool trackScheduler = true);
             bool isTrackSchedulerSet() const;
             bool hasScheduler() const;
@@ -59,6 +68,16 @@ namespace storm {
             // The scheduler for the corresponding players (if it could be successfully generated).
             mutable boost::optional<std::unique_ptr<storm::storage::TotalScheduler>> player1Scheduler;
             mutable boost::optional<std::unique_ptr<storm::storage::TotalScheduler>> player2Scheduler;
+            
+            // schedulers that might be considered by the solver as an initial guess
+            boost::optional<storm::storage::TotalScheduler> player1SchedulerHint;
+            boost::optional<storm::storage::TotalScheduler> player2SchedulerHint;
+            
+            boost::optional<ValueType> lowerBound;
+            boost::optional<ValueType> upperBound;
+            
+            
+            
         };
     }
 }

src/storm/solver/GameSolver.cpp

@@ -20,6 +20,7 @@ namespace storm {
 
         template <typename ValueType>
         void GameSolver<ValueType>::solveGame(OptimizationDirection player1Goal, OptimizationDirection player2Goal, std::vector<ValueType>& x, std::vector<ValueType> const& b) const {
+                        
             // Set up the environment for value iteration.
             bool converged = false;
             uint_fast64_t numberOfPlayer1States = x.size();
@@ -27,6 +28,27 @@ namespace storm {
             std::vector<ValueType> nondetResult(player2Matrix.getRowCount());
             std::vector<ValueType> player2Result(player2Matrix.getRowGroupCount());
             
+            // check if we have a scheduler hint to apply
+            if(this->hasSchedulerHints()) {
+                //Get the rows of the player2matrix that are selected by the schedulers
+                //Note that rows can be selected more then once and in an arbitrary order.
+                std::vector<storm::storage::sparse::state_type> selectedRows(numberOfPlayer1States);
+                for (uint_fast64_t pl1State = 0; pl1State < numberOfPlayer1States; ++pl1State){
+                    auto const& pl1Row = player1Matrix.getRow(pl1State, this->player1SchedulerHint->getChoice(pl1State));
+                    STORM_LOG_ASSERT(pl1Row.getNumberOfEntries()==1, "We assume that rows of player one have one entry.");
+                    uint_fast64_t pl2State = pl1Row.begin()->getColumn();
+                    selectedRows[pl1State] = player2Matrix.getRowGroupIndices()[pl2State] + this->player2SchedulerHint->getChoice(pl1State);
+                }
+                //Get the matrix and the vector induced by this selection
+                auto inducedMatrix = player2Matrix.selectRowsFromRowIndexSequence(selectedRows, true);
+                inducedMatrix.convertToEquationSystem();
+                storm::utility::vector::selectVectorValues<ValueType>(tmpResult, selectedRows, b);
+                auto submatrixSolver = storm::solver::GeneralLinearEquationSolverFactory<ValueType>().create(std::move(inducedMatrix));
+                if (this->lowerBound) { submatrixSolver->setLowerBound(this->lowerBound.get()); }
+                if (this->upperBound) { submatrixSolver->setUpperBound(this->upperBound.get()); }
+                submatrixSolver->solveEquations(x, tmpResult);
+            }
+
             // Now perform the actual value iteration.
             uint_fast64_t iterations = 0;
             do {
@@ -112,6 +134,51 @@ namespace storm {
             }
         }
     
+        template <typename ValueType>
+        void GameSolver<ValueType>::repeatedMultiply(OptimizationDirection player1Goal, OptimizationDirection player2Goal, std::vector<ValueType>& x, std::vector<ValueType> const* b, uint_fast64_t n) const {
+            // Set up the environment for iterations
+            uint_fast64_t numberOfPlayer1States = x.size();
+            std::vector<ValueType> tmpResult(numberOfPlayer1States);
+            std::vector<ValueType> nondetResult(player2Matrix.getRowCount());
+            std::vector<ValueType> player2Result(player2Matrix.getRowGroupCount());
+            
+            for (uint_fast64_t iteration = 0; iteration < n; ++iteration) {
+                player2Matrix.multiplyWithVector(x, nondetResult);
+                
+                if(b != nullptr) {
+                    storm::utility::vector::addVectors(*b, nondetResult, nondetResult);
+                }
+                
+                storm::utility::vector::reduceVectorMinOrMax(player2Goal, nondetResult, player2Result, player2Matrix.getRowGroupIndices());
+
+                for (uint_fast64_t pl1State = 0; pl1State < numberOfPlayer1States; ++pl1State) {
+                    storm::storage::SparseMatrix<storm::storage::sparse::state_type>::const_rows relevantRows = player1Matrix.getRowGroup(pl1State);
+                    if (relevantRows.getNumberOfEntries() > 0) {
+                        storm::storage::SparseMatrix<storm::storage::sparse::state_type>::const_iterator it = relevantRows.begin();
+                        storm::storage::SparseMatrix<storm::storage::sparse::state_type>::const_iterator ite = relevantRows.end();
+
+                        // Set the first value.
+                        tmpResult[pl1State] = player2Result[it->getColumn()];
+                        ++it;
+
+                        // Now iterate through the different values and pick the extremal one.
+                        if (player1Goal == OptimizationDirection::Minimize) {
+                            for (; it != ite; ++it) {
+                                tmpResult[pl1State] = std::min(tmpResult[pl1State], player2Result[it->getColumn()]);
+                            }
+                        } else {
+                            for (; it != ite; ++it) {
+                                tmpResult[pl1State] = std::max(tmpResult[pl1State], player2Result[it->getColumn()]);
+                            }
+                        }
+                    } else {
+                        tmpResult[pl1State] = storm::utility::zero<ValueType>();
+                    }
+                }
+                std::swap(x, tmpResult);
+            }
+        }
+        
         template <typename ValueType>
         storm::storage::SparseMatrix<storm::storage::sparse::state_type> const& GameSolver<ValueType>::getPlayer1Matrix() const {
             return player1Matrix;

src/storm/solver/GameSolver.h

@@ -50,6 +50,17 @@ namespace storm {
              */
             virtual void solveGame(OptimizationDirection player1Goal, OptimizationDirection player2Goal, std::vector<ValueType>& x, std::vector<ValueType> const& b) const;
             
+            /*!
+             * Performs n multiplications of the form
+             *  reduce(player1Matrix * reduce(player2Matrix * x + b))
+             *
+            * @param player1Goal Sets whether player 1 wants to minimize or maximize.
+             * @param player2Goal Sets whether player 2 wants to minimize or maximize.
+             * @param x The initial guess of the solution. For correctness, the guess has to be less (or equal) to the final solution (unless both players minimize)
+             * @param b The vector to add after matrix-vector multiplication.
+             * @param n The number of times we perform the multiplication
+             */
+            virtual void repeatedMultiply(OptimizationDirection player1Goal, OptimizationDirection player2Goal, std::vector<ValueType>& x, std::vector<ValueType> const* b, uint_fast64_t n) const;
 
             storm::storage::SparseMatrix<ValueType> const& getPlayer2Matrix() const;
             storm::storage::SparseMatrix<storm::storage::sparse::state_type> const& getPlayer1Matrix() const;