sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Removed obsolete constructors of sparse matrix class as the new matrix builder is supposed to be used anyway. Fixed some minor issues. 

Former-commit-id: ee8a7cc440
tempestpy_adaptions
dehnert 11 years ago
parent
5e12a65d67
commit
f684ce7799
7 changed files with 37 additions and 65 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 10
      src/modelchecker/prctl/SparseMdpPrctlModelChecker.h
  2. 9
      src/models/AbstractNondeterministicModel.h
  3. 34
      src/storage/SparseMatrix.cpp
  4. 20
      src/storage/SparseMatrix.h
  5. 13
      src/utility/solver.cpp
  6. 5
      src/utility/solver.h
  7. 11
      test/functional/storage/SparseMatrixTest.cpp

10
src/modelchecker/prctl/SparseMdpPrctlModelChecker.h
View File

@ -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<Type> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, std::vector<Type> const& result, std::vector<Type> const* stateRewardVector = nullptr, storm::storage::SparseMatrix<Type> const* transitionRewardMatrix = nullptr) {
std::vector<Type> temporaryResult(nondeterministicChoiceIndices.size() - 1);
std::vector<Type> nondeterministicResult(result);
storm::solver::GmmxxLinearEquationSolver<Type> solver;
solver.performMatrixVectorMultiplication(transitionMatrix, nondeterministicResult, nullptr, 1);
std::vector<Type> temporaryResult(result.size());
std::vector<Type> nondeterministicResult(transitionMatrix.getRowCount());
transitionMatrix.multiplyWithVector(result, nondeterministicResult);
if (stateRewardVector != nullptr || transitionRewardMatrix != nullptr) {
std::vector<Type> totalRewardVector;
if (transitionRewardMatrix != nullptr) {

9
src/models/AbstractNondeterministicModel.h
View File

@ -127,8 +127,7 @@ namespace storm {
uint_fast64_t numberOfTransitions = this->getNumberOfTransitions();
std::vector<uint_fast64_t> rowIndications(numberOfStates + 1);
std::vector<uint_fast64_t> columnIndications(numberOfTransitions);
std::vector<T> values(numberOfTransitions, T());
std::vector<std::pair<uint_fast64_t, T>> columnsAndValues(numberOfTransitions, std::make_pair(0, storm::utility::constantZero<T>()));
// 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<T>::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<T> backwardTransitionMatrix(numberOfStates, std::move(rowIndications), std::move(columnIndications), std::move(values));
storm::storage::SparseMatrix<T> backwardTransitionMatrix(numberOfStates, std::move(rowIndications), std::move(columnsAndValues));
return backwardTransitionMatrix;
}

34
src/storage/SparseMatrix.cpp
View File

@ -184,43 +184,11 @@ namespace storm {
// Intentionally left empty.
}
template<typename T>
SparseMatrix<T>::SparseMatrix(uint_fast64_t columnCount, std::vector<uint_fast64_t> const& rowIndications, std::vector<uint_fast64_t> const& columnIndications, std::vector<T> 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<uint_fast64_t>::const_iterator columnIt = columnIndications.begin();
for (typename std::vector<T>::const_iterator valueIt = values.begin(), valueIte = values.end(); valueIt != valueIte; ++valueIt, ++columnIt) {
columnsAndValues.emplace_back(*columnIt, *valueIt);
}
}
template<typename T>
SparseMatrix<T>::SparseMatrix(uint_fast64_t columnCount, std::vector<uint_fast64_t>&& rowIndications, std::vector<std::pair<uint_fast64_t, T>>&& columnsAndValues) : rowCount(rowIndications.size() - 1), columnCount(columnCount), entryCount(columnsAndValues.size()), columnsAndValues(std::move(columnsAndValues)), rowIndications(std::move(rowIndications)) {
// Intentionally left empty.
}
template<typename T>
SparseMatrix<T>::SparseMatrix(uint_fast64_t columnCount, std::vector<uint_fast64_t>&& rowIndications, std::vector<uint_fast64_t>&& columnIndications, std::vector<T>&& 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<uint_fast64_t>::const_iterator columnIt = columnIndications.begin();
for (typename std::vector<T>::const_iterator valueIt = values.begin(), valueIte = values.end(); valueIt != valueIte; ++valueIt, ++columnIt) {
columnsAndValues.emplace_back(*columnIt, *valueIt);
}
}
template<typename T>
SparseMatrix<T>& SparseMatrix<T>::operator=(SparseMatrix<T> const& other) {
// Only perform assignment if source and target are not the same.

20
src/storage/SparseMatrix.h
View File

@ -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<uint_fast64_t> const& rowIndications, std::vector<std::pair<uint_fast64_t, T>> 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<uint_fast64_t> const& rowIndications, std::vector<uint_fast64_t> const& columnIndications, std::vector<T> 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<uint_fast64_t>&& rowIndications, std::vector<uint_fast64_t>&& columnIndications, std::vector<T>&& values);
/*!
* Constructs a sparse matrix by moving the given contents.

13
src/utility/solver.cpp
View File

@ -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<typename ValueType>
std::shared_ptr<storm::solver::AbstractLinearEquationSolver<ValueType>> getLinearEquationSolver() {
std::string const& matrixLibrary = storm::settings::Settings::getInstance()->getOptionByLongName("matrixLibrary").getArgument(0).getValueAsString();
if (matrixLibrary == "gmm++") {
return std::shared_ptr<storm::solver::AbstractLinearEquationSolver<ValueType>>(new storm::solver::GmmxxLinearEquationSolver<ValueType>());
}
throw storm::exceptions::InvalidSettingsException() << "No suitable linear equation solver selected.";
}
template<typename ValueType>
std::shared_ptr<storm::solver::AbstractNondeterministicLinearEquationSolver<ValueType>> 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<storm::solver::AbstractLinearEquationSolver<double>> getLinearEquationSolver();
template std::shared_ptr<storm::solver::AbstractNondeterministicLinearEquationSolver<double>> getNondeterministicLinearEquationSolver();
}
}

5
src/utility/solver.h
View File

@ -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<storm::solver::LpSolver> getLpSolver(std::string const& name);
template<typename ValueType>
std::shared_ptr<storm::solver::AbstractLinearEquationSolver<ValueType>> getLinearEquationSolver();
template<typename ValueType>
std::shared_ptr<storm::solver::AbstractNondeterministicLinearEquationSolver<ValueType>> getNondeterministicLinearEquationSolver();
}
}
}

11
test/functional/storage/SparseMatrixTest.cpp
View File

@ -147,8 +147,15 @@ TEST(SparseMatrix, Build) {
}
TEST(SparseMatrix, CreationWithMovingContents) {
ASSERT_NO_THROW(storm::storage::SparseMatrix<double> matrix(4, {0, 2, 5, 5}, {1, 2, 0, 1, 3}, {1.0, 1.2, 0.5, 0.7, 0.2}));
storm::storage::SparseMatrix<double> matrix(4, {0, 2, 5, 5}, {1, 2, 0, 1, 3}, {1.0, 1.2, 0.5, 0.7, 0.2});
std::vector<std::pair<uint_fast64_t, double>> 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<double> matrix(4, {0, 2, 5, 5}, columnsAndValues));
storm::storage::SparseMatrix<double> matrix(4, {0, 2, 5, 5}, columnsAndValues);
ASSERT_EQ(3, matrix.getRowCount());
ASSERT_EQ(4, matrix.getColumnCount());
ASSERT_EQ(5, matrix.getEntryCount());
Write Preview
Loading…
Cancel
Save