further work towards proper scheduler extraction for games

src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp

@@ -32,6 +32,7 @@
 #include "storm/logic/FragmentSpecification.h"
 
 #include "storm/solver/SymbolicGameSolver.h"
+#include "storm/solver/StandardGameSolver.h"
 
 #include "storm/settings/SettingsManager.h"
 #include "storm/settings/modules/CoreSettings.h"
@@ -410,11 +411,9 @@ namespace storm {
             storm::storage::SparseMatrix<ValueType> submatrix = transitionMatrix.getSubmatrix(true, player2MaybeStates, maybeStates);
             std::vector<ValueType> b = transitionMatrix.getConstrainedRowGroupSumVector(player2MaybeStates, maybeStates);
             
-//            auto multiplier = storm::solver::MultiplierFactory<ValueType>().create(env, submatrix);
-//            multiplier->repeatedMultiplyAndReduce(env, goal.direction(), subresult, &b, stepBound);
-//
-//
-//            env.
+            auto gameSolver = storm::solver::GameSolverFactory<ValueType>().create(env, player1Groups, transitionMatrix);
+            exit(-1);
+            
         }
         
         template<storm::dd::DdType Type, typename ModelType>

src/storm/settings/modules/MinMaxEquationSolverSettings.cpp

@@ -38,7 +38,7 @@ namespace storm {
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of a long run average computation method.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(lraMethods)).setDefaultValueString("vi").build()).build());
 
                 std::vector<std::string> maMethods = {"imca", "unifplus"};
-                this->addOption(storm::settings::OptionBuilder(moduleName, markovAutomatonBoundedReachabilityMethodOptionName, true, "The method to use to solve bounded reachability queries on MAs.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the method to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(maMethods)).setDefaultValueString("unifplus").build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, markovAutomatonBoundedReachabilityMethodOptionName, false, "The method to use to solve bounded reachability queries on MAs.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the method to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(maMethods)).setDefaultValueString("unifplus").build()).build());
                 
                 std::vector<std::string> multiplicationStyles = {"gaussseidel", "regular", "gs", "r"};
                 this->addOption(storm::settings::OptionBuilder(moduleName, valueIterationMultiplicationStyleOptionName, false, "Sets which method multiplication style to prefer for value iteration.")

src/storm/solver/GameSolver.cpp

@@ -124,6 +124,16 @@ namespace storm {
             return std::make_unique<StandardGameSolver<ValueType>>(std::move(player1Matrix), std::move(player2Matrix), std::make_unique<GeneralLinearEquationSolverFactory<ValueType>>());
         }
         
+        template<typename ValueType>
+        std::unique_ptr<GameSolver<ValueType>> GameSolverFactory<ValueType>::create(Environment const& env, std::vector<uint64_t> const& player1Grouping, storm::storage::SparseMatrix<ValueType> const& player2Matrix) const {
+            return std::make_unique<StandardGameSolver<ValueType>>(player1Grouping, player2Matrix, std::make_unique<GeneralLinearEquationSolverFactory<ValueType>>());
+        }
+        
+        template<typename ValueType>
+        std::unique_ptr<GameSolver<ValueType>> GameSolverFactory<ValueType>::create(Environment const& env, std::vector<uint64_t>&& player1Grouping, storm::storage::SparseMatrix<ValueType>&& player2Matrix) const {
+            return std::make_unique<StandardGameSolver<ValueType>>(std::move(player1Grouping), std::move(player2Matrix), std::make_unique<GeneralLinearEquationSolverFactory<ValueType>>());
+        }
+        
         template class GameSolver<double>;
         template class GameSolver<storm::RationalNumber>;
         

src/storm/solver/GameSolver.h

@@ -154,9 +154,8 @@ namespace storm {
             virtual std::unique_ptr<GameSolver<ValueType>> create(Environment const& env, storm::storage::SparseMatrix<storm::storage::sparse::state_type> const& player1Matrix, storm::storage::SparseMatrix<ValueType> const& player2Matrix) const;
             virtual std::unique_ptr<GameSolver<ValueType>> create(Environment const& env, storm::storage::SparseMatrix<storm::storage::sparse::state_type>&& player1Matrix, storm::storage::SparseMatrix<ValueType>&& player2Matrix) const;
 
-        private:
-            bool trackScheduler;
-
+            virtual std::unique_ptr<GameSolver<ValueType>> create(Environment const& env, std::vector<uint64_t> const& player1Grouping, storm::storage::SparseMatrix<ValueType> const& player2Matrix) const;
+            virtual std::unique_ptr<GameSolver<ValueType>> create(Environment const& env, std::vector<uint64_t>&& player1Grouping, storm::storage::SparseMatrix<ValueType>&& player2Matrix) const;
         };
         
     } // namespace solver

src/storm/solver/GmmxxMultiplier.cpp

@@ -119,6 +119,7 @@ namespace storm {
         
         template<typename ValueType>
         void GmmxxMultiplier<ValueType>::multAddReduceHelper(storm::solver::OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType> const& x, std::vector<ValueType> const* b, std::vector<ValueType>& result, std::vector<uint64_t>* choices) const {
+            bool min = dir == OptimizationDirection::Minimize;
             typedef std::vector<ValueType> VectorType;
             typedef gmm::csr_matrix<ValueType> MatrixType;
             
@@ -134,12 +135,12 @@ namespace storm {
                 choice_it = choices->end() - 1;
             }
 
-            uint64_t choice;
-            for (auto row_group_it = rowGroupIndices.end() - 2, row_group_ite = rowGroupIndices.begin() - 1; row_group_it != row_group_ite; --row_group_it, --choice_it, --target_it) {
-                if (choices) {
-                    *choice_it = 0;
-                }
+            // Variables for correctly tracking choices (only update if new choice is strictly better).
+            ValueType oldSelectedChoiceValue;
+            uint64_t selectedChoice;
 
+            uint64_t currentRow = gmmMatrix.nrows() - 1;
+            for (auto row_group_it = rowGroupIndices.end() - 2, row_group_ite = rowGroupIndices.begin() - 1; row_group_it != row_group_ite; --row_group_it, --choice_it, --target_it) {
                 ValueType currentValue = storm::utility::zero<ValueType>();
                 
                 // Only multiply and reduce if the row group is not empty.
@@ -152,33 +153,37 @@ namespace storm {
                     currentValue += vect_sp(gmm::linalg_traits<MatrixType>::row(itr), x);
 
                     if (choices) {
-                        choice = *(row_group_it + 1) - 1 - *row_group_it;
-                        *choice_it = choice;
+                        selectedChoice = currentRow - *row_group_it;
+                        if (*choice_it == selectedChoice) {
+                            oldSelectedChoiceValue = currentValue;
+                        }
                     }
 
                     --itr;
+                    --currentRow;
                     
-                    for (uint64_t row = *row_group_it + 1, rowEnd = *(row_group_it + 1); row < rowEnd; ++row, --itr, --add_it) {
+                    for (uint64_t row = *row_group_it + 1, rowEnd = *(row_group_it + 1); row < rowEnd; ++row, ++currentRow, --itr, --add_it) {
                         ValueType newValue = b ? *add_it : storm::utility::zero<ValueType>();
                         newValue += vect_sp(gmm::linalg_traits<MatrixType>::row(itr), x);
                         
-                        if (choices) {
-                            --choice;
+                        if (choices && currentRow == *choice_it + *row_group_it) {
+                            oldSelectedChoiceValue = newValue;
                         }
 
-                        if ((dir == OptimizationDirection::Minimize && newValue < currentValue) || (dir == OptimizationDirection::Maximize && newValue > currentValue)) {
+                        if (min ? currentValue < oldSelectedChoiceValue : currentValue > oldSelectedChoiceValue) {
                             currentValue = newValue;
                             if (choices) {
-                                *choice_it = choice;
-                            }
+                                selectedChoice = currentRow - *row_group_it;
                             }
                         }
-                } else if (choices) {
-                    *choice_it = 0;
                     }
                     
-                // Write back final value.
+                    // Finally write value to target vector.
                     *target_it = currentValue;
+                    if (choices && (min ? currentValue < oldSelectedChoiceValue : currentValue > oldSelectedChoiceValue)) {
+                        *choice_it = selectedChoice;
+                    }
+                }
             }
         }
         
@@ -275,7 +280,7 @@ namespace storm {
         template<typename ValueType>
         void GmmxxMultiplier<ValueType>::multAddReduceParallel(storm::solver::OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType> const& x, std::vector<ValueType> const* b, std::vector<ValueType>& result, std::vector<uint64_t>* choices) const {
 #ifdef STORM_HAVE_INTELTBB
-            tbb::parallel_for(tbb::blocked_range<unsigned long>(0, rowGroupIndices.size() - 1, 10), TbbMultAddReduceFunctor<ValueType>(dir, rowGroupIndices, this->gmmMatrix, x, b, result, choices));
+            tbb::parallel_for(tbb::blocked_range<unsigned long>(0, rowGroupIndices.size() - 1, 100), TbbMultAddReduceFunctor<ValueType>(dir, rowGroupIndices, this->gmmMatrix, x, b, result, choices));
 #else
             STORM_LOG_WARN("Storm was built without support for Intel TBB, defaulting to sequential version.");
             multAddReduceHelper(dir, rowGroupIndices, x, b, result, choices);

src/storm/solver/StandardGameSolver.h

@@ -75,7 +75,6 @@ namespace storm {
             std::vector<uint64_t> const* player1Grouping;
             storm::storage::SparseMatrix<storm::storage::sparse::state_type> const* player1Matrix;
             storm::storage::SparseMatrix<ValueType> const& player2Matrix;
-            
         };
     }
 }

src/storm/utility/vector.h

@@ -672,28 +672,43 @@ namespace storm {
                 typename std::vector<T>::const_iterator sourceIt = source.begin();
                 typename std::vector<T>::const_iterator sourceIte;
                 typename std::vector<uint_fast64_t>::iterator choiceIt;
-                uint_fast64_t localChoice;
-                if (choices != nullptr) {
+                if (choices) {
                     choiceIt = choices->begin();
                 }
                 
+                // Variables for correctly tracking choices (only update if new choice is strictly better).
+                T oldSelectedChoiceValue;
+                uint64_t selectedChoice;
+                
                 for (; targetIt != targetIte; ++targetIt, ++rowGroupingIt, ++choiceIt) {
                     // Only traverse elements if the row group is non-empty.
                     if (*rowGroupingIt != *(rowGroupingIt + 1)) {
                         *targetIt = *sourceIt;
+                        
+                        if (choices) {
+                            selectedChoice = 0;
+                            if (*choiceIt == 0) {
+                                oldSelectedChoiceValue = *targetIt;
+                            }
+                        }
+
                         ++sourceIt;
-                        localChoice = 1;
-                        if (choices != nullptr) {
-                            *choiceIt = 0;
+                        for (sourceIte = source.begin() + *(rowGroupingIt + 1); sourceIt != sourceIte; ++sourceIt) {
+                            if (choices && selectedChoice == std::distance(source.begin(), sourceIt) - *rowGroupingIt) {
+                                oldSelectedChoiceValue = *sourceIt;
                             }
-                        for (sourceIte = source.begin() + *(rowGroupingIt + 1); sourceIt != sourceIte; ++sourceIt, ++localChoice) {
+                            
                             if (f(*sourceIt, *targetIt)) {
                                 *targetIt = *sourceIt;
-                                if (choices != nullptr) {
-                                    *choiceIt = localChoice;
+                                if (choices) {
+                                    selectedChoice = std::distance(source.begin(), sourceIt) - *rowGroupingIt;
                                 }
                             }
                         }
+                        
+                        if (choices && f(*targetIt, oldSelectedChoiceValue)) {
+                            *choiceIt = selectedChoice;
+                        }
                     } else {
                         *targetIt = storm::utility::zero<T>();
                     }