diff --git a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h index 482c8d9ce..1b21804b8 100644 --- a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h +++ b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h @@ -14,7 +14,7 @@ #include "src/modelchecker/prctl/AbstractModelChecker.h" #include "src/solver/AbstractNondeterministicLinearEquationSolver.h" -#include "src/solver/GmmxxLinearEquationSolver.h" +#include "src/solver/AbstractLinearEquationSolver.h" #include "src/models/Mdp.h" #include "src/utility/vector.h" #include "src/utility/graph.h" @@ -550,10 +550,10 @@ namespace storm { * @param nondeterministicChoiceIndices The assignment of states to their nondeterministic choices in the matrix. */ static storm::storage::TotalScheduler computeExtremalScheduler(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, std::vector const& result, std::vector const* stateRewardVector = nullptr, storm::storage::SparseMatrix const* transitionRewardMatrix = nullptr) { - std::vector temporaryResult(nondeterministicChoiceIndices.size() - 1); - std::vector nondeterministicResult(result); - storm::solver::GmmxxLinearEquationSolver solver; - solver.performMatrixVectorMultiplication(transitionMatrix, nondeterministicResult, nullptr, 1); + std::vector temporaryResult(result.size()); + std::vector nondeterministicResult(transitionMatrix.getRowCount()); + transitionMatrix.multiplyWithVector(result, nondeterministicResult); + if (stateRewardVector != nullptr || transitionRewardMatrix != nullptr) { std::vector totalRewardVector; if (transitionRewardMatrix != nullptr) { diff --git a/src/models/AbstractNondeterministicModel.h b/src/models/AbstractNondeterministicModel.h index f2a515bc2..e474ae0b5 100644 --- a/src/models/AbstractNondeterministicModel.h +++ b/src/models/AbstractNondeterministicModel.h @@ -127,8 +127,7 @@ namespace storm { uint_fast64_t numberOfTransitions = this->getNumberOfTransitions(); std::vector rowIndications(numberOfStates + 1); - std::vector columnIndications(numberOfTransitions); - std::vector values(numberOfTransitions, T()); + std::vector> columnsAndValues(numberOfTransitions, std::make_pair(0, storm::utility::constantZero())); // First, we need to count how many backward transitions each state has. for (uint_fast64_t i = 0; i < numberOfStates; ++i) { @@ -155,13 +154,13 @@ namespace storm { typename storm::storage::SparseMatrix::const_rows rows = this->getRows(i); for (auto const& transition : rows) { if (transition.second > 0) { - values[nextIndices[transition.first]] = transition.second; - columnIndications[nextIndices[transition.first]++] = i; + columnsAndValues[nextIndices[transition.first]] = std::make_pair(i, transition.second); + ++nextIndices[transition.first]; } } } - storm::storage::SparseMatrix backwardTransitionMatrix(numberOfStates, std::move(rowIndications), std::move(columnIndications), std::move(values)); + storm::storage::SparseMatrix backwardTransitionMatrix(numberOfStates, std::move(rowIndications), std::move(columnsAndValues)); return backwardTransitionMatrix; } diff --git a/src/storage/SparseMatrix.cpp b/src/storage/SparseMatrix.cpp index 398b3d78a..87f19e538 100644 --- a/src/storage/SparseMatrix.cpp +++ b/src/storage/SparseMatrix.cpp @@ -184,43 +184,11 @@ namespace storm { // Intentionally left empty. } - template - SparseMatrix::SparseMatrix(uint_fast64_t columnCount, std::vector const& rowIndications, std::vector const& columnIndications, std::vector const& values) : rowCount(rowIndications.size() - 1), columnCount(columnCount), entryCount(values.size()), columnsAndValues(), rowIndications(rowIndications) { - if (columnIndications.size() != values.size()) { - throw storm::exceptions::InvalidArgumentException() << "Illegal call to SparseMatrix::SparseMatrix: value and column vector length mismatch."; - } - - // Preserve enough storage to avoid reallocations. - columnsAndValues.reserve(values.size()); - - // Now zip the two vectors for columns and values. - typename std::vector::const_iterator columnIt = columnIndications.begin(); - for (typename std::vector::const_iterator valueIt = values.begin(), valueIte = values.end(); valueIt != valueIte; ++valueIt, ++columnIt) { - columnsAndValues.emplace_back(*columnIt, *valueIt); - } - } - template SparseMatrix::SparseMatrix(uint_fast64_t columnCount, std::vector&& rowIndications, std::vector>&& columnsAndValues) : rowCount(rowIndications.size() - 1), columnCount(columnCount), entryCount(columnsAndValues.size()), columnsAndValues(std::move(columnsAndValues)), rowIndications(std::move(rowIndications)) { // Intentionally left empty. } - - template - SparseMatrix::SparseMatrix(uint_fast64_t columnCount, std::vector&& rowIndications, std::vector&& columnIndications, std::vector&& values) : rowCount(rowIndications.size() - 1), columnCount(columnCount), entryCount(values.size()), columnsAndValues(), rowIndications(std::move(rowIndications)) { - if (columnIndications.size() != values.size()) { - throw storm::exceptions::InvalidArgumentException() << "Illegal call to SparseMatrix::SparseMatrix: value and column vector length mismatch."; - } - - // Preserve enough storage to avoid reallocations. - columnsAndValues.reserve(values.size()); - - // Now zip the two vectors for columns and values. - typename std::vector::const_iterator columnIt = columnIndications.begin(); - for (typename std::vector::const_iterator valueIt = values.begin(), valueIte = values.end(); valueIt != valueIte; ++valueIt, ++columnIt) { - columnsAndValues.emplace_back(*columnIt, *valueIt); - } - } - + template SparseMatrix& SparseMatrix::operator=(SparseMatrix const& other) { // Only perform assignment if source and target are not the same. diff --git a/src/storage/SparseMatrix.h b/src/storage/SparseMatrix.h index 9e996366a..0ddcbf8e6 100644 --- a/src/storage/SparseMatrix.h +++ b/src/storage/SparseMatrix.h @@ -274,26 +274,6 @@ namespace storm { * @param columnsAndValues The vector containing the columns and values of the entries in the matrix. */ SparseMatrix(uint_fast64_t columnCount, std::vector const& rowIndications, std::vector> const& columnsAndValues); - - /*! - * Constructs a sparse matrix by copying the given contents. - * - * @param columnCount The number of columns of the matrix. - * @param rowIndications The row indications vector of the matrix to be constructed. - * @param columnIndications The column indications vector of the matrix to be constructed. - * @param values The vector containing the values of the entries in the matrix. - */ - SparseMatrix(uint_fast64_t columnCount, std::vector const& rowIndications, std::vector const& columnIndications, std::vector const& values); - - /*! - * Constructs a sparse matrix by moving the given contents. - * - * @param columnCount The number of columns of the matrix. - * @param rowIndications The row indications vector of the matrix to be constructed. - * @param columnIndications The column indications vector of the matrix to be constructed. - * @param values The vector containing the values of the entries in the matrix. - */ - SparseMatrix(uint_fast64_t columnCount, std::vector&& rowIndications, std::vector&& columnIndications, std::vector&& values); /*! * Constructs a sparse matrix by moving the given contents. diff --git a/src/utility/solver.cpp b/src/utility/solver.cpp index b6036ae58..762cc360b 100644 --- a/src/utility/solver.cpp +++ b/src/utility/solver.cpp @@ -1,5 +1,6 @@ #include "src/utility/solver.h" +#include "src/solver/GmmxxLinearEquationSolver.h" #include "src/solver/GmmxxNondeterministicLinearEquationSolver.h" #include "src/solver/GurobiLpSolver.h" #include "src/solver/GlpkLpSolver.h" @@ -18,6 +19,16 @@ namespace storm { throw storm::exceptions::InvalidSettingsException() << "No suitable LP-solver selected."; } + template + std::shared_ptr> getLinearEquationSolver() { + std::string const& matrixLibrary = storm::settings::Settings::getInstance()->getOptionByLongName("matrixLibrary").getArgument(0).getValueAsString(); + if (matrixLibrary == "gmm++") { + return std::shared_ptr>(new storm::solver::GmmxxLinearEquationSolver()); + } + + throw storm::exceptions::InvalidSettingsException() << "No suitable linear equation solver selected."; + } + template std::shared_ptr> getNondeterministicLinearEquationSolver() { std::string const& matrixLibrary = storm::settings::Settings::getInstance()->getOptionByLongName("matrixLibrary").getArgument(0).getValueAsString(); @@ -30,6 +41,8 @@ namespace storm { throw storm::exceptions::InvalidSettingsException() << "No suitable nondeterministic linear equation solver selected."; } + template std::shared_ptr> getLinearEquationSolver(); + template std::shared_ptr> getNondeterministicLinearEquationSolver(); } } diff --git a/src/utility/solver.h b/src/utility/solver.h index 0122a49f3..2475456d9 100644 --- a/src/utility/solver.h +++ b/src/utility/solver.h @@ -1,6 +1,7 @@ #ifndef STORM_UTILITY_SOLVER_H_ #define STORM_UTILITY_SOLVER_H_ +#include "src/solver/AbstractLinearEquationSolver.h" #include "src/solver/AbstractNondeterministicLinearEquationSolver.h" #include "src/solver/LpSolver.h" @@ -12,8 +13,12 @@ namespace storm { std::shared_ptr getLpSolver(std::string const& name); + template + std::shared_ptr> getLinearEquationSolver(); + template std::shared_ptr> getNondeterministicLinearEquationSolver(); + } } } diff --git a/test/functional/storage/SparseMatrixTest.cpp b/test/functional/storage/SparseMatrixTest.cpp index ad7e134d8..82fd9ec5c 100644 --- a/test/functional/storage/SparseMatrixTest.cpp +++ b/test/functional/storage/SparseMatrixTest.cpp @@ -147,8 +147,15 @@ TEST(SparseMatrix, Build) { } TEST(SparseMatrix, CreationWithMovingContents) { - ASSERT_NO_THROW(storm::storage::SparseMatrix matrix(4, {0, 2, 5, 5}, {1, 2, 0, 1, 3}, {1.0, 1.2, 0.5, 0.7, 0.2})); - storm::storage::SparseMatrix matrix(4, {0, 2, 5, 5}, {1, 2, 0, 1, 3}, {1.0, 1.2, 0.5, 0.7, 0.2}); + std::vector> columnsAndValues; + columnsAndValues.emplace_back(1, 1.0); + columnsAndValues.emplace_back(2, 1.2); + columnsAndValues.emplace_back(0, 0.5); + columnsAndValues.emplace_back(1, 0.7); + columnsAndValues.emplace_back(3, 0.2); + + ASSERT_NO_THROW(storm::storage::SparseMatrix matrix(4, {0, 2, 5, 5}, columnsAndValues)); + storm::storage::SparseMatrix matrix(4, {0, 2, 5, 5}, columnsAndValues); ASSERT_EQ(3, matrix.getRowCount()); ASSERT_EQ(4, matrix.getColumnCount()); ASSERT_EQ(5, matrix.getEntryCount());