diff --git a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp index 43df463ae..af0c46121 100644 --- a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp +++ b/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 submatrix = transitionMatrix.getSubmatrix(true, player2MaybeStates, maybeStates); std::vector b = transitionMatrix.getConstrainedRowGroupSumVector(player2MaybeStates, maybeStates); -// auto multiplier = storm::solver::MultiplierFactory().create(env, submatrix); -// multiplier->repeatedMultiplyAndReduce(env, goal.direction(), subresult, &b, stepBound); -// -// -// env. + auto gameSolver = storm::solver::GameSolverFactory().create(env, player1Groups, transitionMatrix); + exit(-1); + } template diff --git a/src/storm/settings/modules/MinMaxEquationSolverSettings.cpp b/src/storm/settings/modules/MinMaxEquationSolverSettings.cpp index 186f0caf9..8ee45ab20 100644 --- a/src/storm/settings/modules/MinMaxEquationSolverSettings.cpp +++ b/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 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 multiplicationStyles = {"gaussseidel", "regular", "gs", "r"}; this->addOption(storm::settings::OptionBuilder(moduleName, valueIterationMultiplicationStyleOptionName, false, "Sets which method multiplication style to prefer for value iteration.") diff --git a/src/storm/solver/GameSolver.cpp b/src/storm/solver/GameSolver.cpp index bb27cb4fa..f5ccce0ad 100644 --- a/src/storm/solver/GameSolver.cpp +++ b/src/storm/solver/GameSolver.cpp @@ -124,6 +124,16 @@ namespace storm { return std::make_unique>(std::move(player1Matrix), std::move(player2Matrix), std::make_unique>()); } + template + std::unique_ptr> GameSolverFactory::create(Environment const& env, std::vector const& player1Grouping, storm::storage::SparseMatrix const& player2Matrix) const { + return std::make_unique>(player1Grouping, player2Matrix, std::make_unique>()); + } + + template + std::unique_ptr> GameSolverFactory::create(Environment const& env, std::vector&& player1Grouping, storm::storage::SparseMatrix&& player2Matrix) const { + return std::make_unique>(std::move(player1Grouping), std::move(player2Matrix), std::make_unique>()); + } + template class GameSolver; template class GameSolver; diff --git a/src/storm/solver/GameSolver.h b/src/storm/solver/GameSolver.h index 07cb16e88..6c724e33c 100644 --- a/src/storm/solver/GameSolver.h +++ b/src/storm/solver/GameSolver.h @@ -154,9 +154,8 @@ namespace storm { virtual std::unique_ptr> create(Environment const& env, storm::storage::SparseMatrix const& player1Matrix, storm::storage::SparseMatrix const& player2Matrix) const; virtual std::unique_ptr> create(Environment const& env, storm::storage::SparseMatrix&& player1Matrix, storm::storage::SparseMatrix&& player2Matrix) const; - private: - bool trackScheduler; - + virtual std::unique_ptr> create(Environment const& env, std::vector const& player1Grouping, storm::storage::SparseMatrix const& player2Matrix) const; + virtual std::unique_ptr> create(Environment const& env, std::vector&& player1Grouping, storm::storage::SparseMatrix&& player2Matrix) const; }; } // namespace solver diff --git a/src/storm/solver/GmmxxMultiplier.cpp b/src/storm/solver/GmmxxMultiplier.cpp index 9618e2495..939a4b61e 100644 --- a/src/storm/solver/GmmxxMultiplier.cpp +++ b/src/storm/solver/GmmxxMultiplier.cpp @@ -119,6 +119,7 @@ namespace storm { template void GmmxxMultiplier::multAddReduceHelper(storm::solver::OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices) const { + bool min = dir == OptimizationDirection::Minimize; typedef std::vector VectorType; typedef gmm::csr_matrix MatrixType; @@ -133,13 +134,13 @@ namespace storm { if (choices) { 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(); // Only multiply and reduce if the row group is not empty. @@ -150,35 +151,39 @@ namespace storm { } currentValue += vect_sp(gmm::linalg_traits::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(); newValue += vect_sp(gmm::linalg_traits::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; + + // Finally write value to target vector. + *target_it = currentValue; + if (choices && (min ? currentValue < oldSelectedChoiceValue : currentValue > oldSelectedChoiceValue)) { + *choice_it = selectedChoice; + } } - - // Write back final value. - *target_it = currentValue; } } @@ -275,7 +280,7 @@ namespace storm { template void GmmxxMultiplier::multAddReduceParallel(storm::solver::OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices) const { #ifdef STORM_HAVE_INTELTBB - tbb::parallel_for(tbb::blocked_range(0, rowGroupIndices.size() - 1, 10), TbbMultAddReduceFunctor(dir, rowGroupIndices, this->gmmMatrix, x, b, result, choices)); + tbb::parallel_for(tbb::blocked_range(0, rowGroupIndices.size() - 1, 100), TbbMultAddReduceFunctor(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); diff --git a/src/storm/solver/StandardGameSolver.h b/src/storm/solver/StandardGameSolver.h index e0a800ea2..338966d27 100644 --- a/src/storm/solver/StandardGameSolver.h +++ b/src/storm/solver/StandardGameSolver.h @@ -75,7 +75,6 @@ namespace storm { std::vector const* player1Grouping; storm::storage::SparseMatrix const* player1Matrix; storm::storage::SparseMatrix const& player2Matrix; - }; } } diff --git a/src/storm/utility/vector.h b/src/storm/utility/vector.h index ac73e48d5..c283d7495 100644 --- a/src/storm/utility/vector.h +++ b/src/storm/utility/vector.h @@ -672,28 +672,43 @@ namespace storm { typename std::vector::const_iterator sourceIt = source.begin(); typename std::vector::const_iterator sourceIte; typename std::vector::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; - ++sourceIt; - localChoice = 1; - if (choices != nullptr) { - *choiceIt = 0; + + if (choices) { + selectedChoice = 0; + if (*choiceIt == 0) { + oldSelectedChoiceValue = *targetIt; + } } - for (sourceIte = source.begin() + *(rowGroupingIt + 1); sourceIt != sourceIte; ++sourceIt, ++localChoice) { + + ++sourceIt; + for (sourceIte = source.begin() + *(rowGroupingIt + 1); sourceIt != sourceIte; ++sourceIt) { + if (choices && selectedChoice == std::distance(source.begin(), sourceIt) - *rowGroupingIt) { + oldSelectedChoiceValue = *sourceIt; + } + 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(); }