diff --git a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp index 2c10f2f2d..43df463ae 100644 --- a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp +++ b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp @@ -410,11 +410,11 @@ 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 multiplier = storm::solver::MultiplierFactory().create(env, submatrix); +// multiplier->repeatedMultiplyAndReduce(env, goal.direction(), subresult, &b, stepBound); +// +// +// env. } template diff --git a/src/storm/solver/GameSolver.cpp b/src/storm/solver/GameSolver.cpp index 0710cc9f2..bb27cb4fa 100644 --- a/src/storm/solver/GameSolver.cpp +++ b/src/storm/solver/GameSolver.cpp @@ -99,6 +99,16 @@ namespace storm { // Intentionally left empty. } + template + void GameSolver::setHasUniqueSolution(bool value) { + this->uniqueSolution = value; + } + + template + bool GameSolver::hasUniqueSolution() const { + return this->uniqueSolution; + } + template GameSolverFactory::GameSolverFactory() { // Intentionally left empty. diff --git a/src/storm/solver/NativeMultiplier.cpp b/src/storm/solver/NativeMultiplier.cpp index 13b27c617..7dd2457df 100644 --- a/src/storm/solver/NativeMultiplier.cpp +++ b/src/storm/solver/NativeMultiplier.cpp @@ -97,7 +97,6 @@ namespace storm { } } - template void NativeMultiplier::multAdd(std::vector const& x, std::vector const* b, std::vector& result) const { this->matrix.multiplyWithVector(x, result, b); diff --git a/src/storm/solver/StandardGameSolver.cpp b/src/storm/solver/StandardGameSolver.cpp index 07512b23d..4d4cfd03c 100644 --- a/src/storm/solver/StandardGameSolver.cpp +++ b/src/storm/solver/StandardGameSolver.cpp @@ -240,7 +240,7 @@ namespace storm { Status status = Status::InProgress; while (status == Status::InProgress) { - multiplyAndReduce(env, player1Dir, player2Dir, *currentX, &b, *multiplierPlayer2Matrix, reducedPlayer2Result, *newX, trackSchedulersInValueIteration ? &this->getPlayer1SchedulerChoices() : nullptr, trackSchedulersInValueIteration ? &this->getPlayer2SchedulerChoices() : nullptr); + multiplyAndReduce(env, player1Dir, player2Dir, *currentX, &b, *multiplierPlayer2Matrix, reducedPlayer2Result, *newX, trackSchedulersInValueIteration ? &this->player1SchedulerChoices.get() : nullptr, trackSchedulersInValueIteration ? &this->player2SchedulerChoices.get() : nullptr); // Determine whether the method converged. if (storm::utility::vector::equalModuloPrecision(*currentX, *newX, precision, relative)) { diff --git a/src/storm/storage/SparseMatrix.h b/src/storm/storage/SparseMatrix.h index 1ec88e34e..c6b51b981 100644 --- a/src/storm/storage/SparseMatrix.h +++ b/src/storm/storage/SparseMatrix.h @@ -851,7 +851,9 @@ namespace storm { * @param vector The vector with which to multiply the matrix. * @param summand If given, this summand will be added to the result of the multiplication. * @param result The vector that is supposed to hold the result of the multiplication after the operation. - * @param choices If given, the choices made in the reduction process will be written to this vector. + * @param choices If given, the choices made in the reduction process will be written to this vector. Note + * that if the direction is maximize, the choice for a row group is only updated if the value obtained with + * the 'new' choice has a value strictly better (wrt. to the optimization direction) value. * @return The resulting vector the content of the given result vector. */ void multiplyAndReduce(storm::solver::OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* summand, std::vector& result, std::vector* choices) const;