Browse Source

Fixed MDP Parser, removed parsing of STATES/TRANSITIONS, see #10

Refactored the Sparse Adapters, see #17
tempestpy_adaptions
PBerger 12 years ago
parent
commit
06d78967df
  1. 6
      src/adapters/EigenAdapter.h
  2. 220
      src/adapters/StormAdapter.h
  3. 20
      src/parser/NondeterministicSparseTransitionParser.cpp
  4. 247
      src/storage/SparseMatrix.h
  5. 4
      test/parser/ParseMdpTest.cpp
  6. 33
      test/storage/SparseMatrixTest.cpp
  7. 0
      test/storage/adapters/EigenAdapterTest.cpp
  8. 111
      test/storage/adapters/GmmAdapterTest.cpp
  9. 104
      test/storage/adapters/StormAdapterTest.cpp

6
src/adapters/EigenAdapter.h

@ -32,9 +32,9 @@ public:
LOG4CPLUS_DEBUG(logger, "Converting matrix with " << realNonZeros << " non-zeros to Eigen format."); LOG4CPLUS_DEBUG(logger, "Converting matrix with " << realNonZeros << " non-zeros to Eigen format.");
// Prepare the resulting matrix. // Prepare the resulting matrix.
Eigen::SparseMatrix<T, Eigen::RowMajor, int_fast32_t>* result = new Eigen::SparseMatrix<T, Eigen::RowMajor, int_fast32_t>(matrix.rowCount, matrix.colCount);
Eigen::SparseMatrix<T, Eigen::RowMajor, int_fast32_t>* result = new Eigen::SparseMatrix<T, Eigen::RowMajor, int_fast32_t>(static_cast<int>(matrix.rowCount), static_cast<int>(matrix.colCount));
result->resizeNonZeros(realNonZeros);
result->resizeNonZeros(static_cast<int>(realNonZeros));
//result->reserve(realNonZeros); //result->reserve(realNonZeros);
// Copy Row Indications // Copy Row Indications
@ -54,4 +54,4 @@ public:
} //namespace storm } //namespace storm
#endif /* STORM_ADAPTERS_GMMXXADAPTER_H_ */
#endif /* STORM_ADAPTERS_EIGENADAPTER_H_ */

220
src/adapters/StormAdapter.h

@ -0,0 +1,220 @@
/*
* StormAdapter.h
*
* Created on: 02.03.2013
* Author: Philipp Berger
*/
#ifndef STORM_ADAPTERS_STORMADAPTER_H_
#define STORM_ADAPTERS_STORMADAPTER_H_
#include "src/storage/SparseMatrix.h"
#include "log4cplus/logger.h"
#include "log4cplus/loggingmacros.h"
extern log4cplus::Logger logger;
namespace storm {
namespace adapters {
class StormAdapter {
public:
/*!
* Converts a sparse matrix into a sparse matrix in the storm format.
* @return A pointer to a row-major sparse matrix in storm format.
*/
template<class T>
static storm::storage::SparseMatrix<T>* toStormSparseMatrix(gmm::csr_matrix<T> const& matrix) {
uint_fast64_t realNonZeros = gmm::nnz(matrix);
LOG4CPLUS_DEBUG(logger, "Converting matrix with " << realNonZeros << " non-zeros from gmm++ format into Storm.");
// Prepare the resulting matrix.
storm::storage::SparseMatrix<T>* result = new storm::storage::SparseMatrix<T>(matrix.nrows(), matrix.ncols());
// Set internal NonZero Counter
result->nonZeroEntryCount = realNonZeros;
result->setState(result->Initialized);
if (!result->prepareInternalStorage(false)) {
LOG4CPLUS_ERROR(logger, "Unable to allocate internal storage while converting GMM++ Matrix to Storm.");
delete result;
return nullptr;
} else {
// Copy Row Indications
std::copy(matrix.jc.begin(), matrix.jc.end(), std::back_inserter(result->rowIndications));
// Copy Columns Indications
std::copy(matrix.ir.begin(), matrix.ir.end(), std::back_inserter(result->columnIndications));
// And do the same thing with the actual values.
std::copy(matrix.pr.begin(), matrix.pr.end(), std::back_inserter(result->valueStorage));
result->currentSize = realNonZeros;
result->lastRow = matrix.nrows() - 1;
}
result->finalize();
LOG4CPLUS_DEBUG(logger, "Done converting matrix to storm format.");
return result;
}
/*!
* Helper function to determine whether the given Eigen matrix is in RowMajor
* format. Always returns true, but is overloaded, so the compiler will
* only call it in case the Eigen matrix is in RowMajor format.
* @return True.
*/
template<typename _Scalar, typename _Index>
static bool isEigenRowMajor(Eigen::SparseMatrix<_Scalar, Eigen::RowMajor, _Index>) {
return true;
}
/*!
* Helper function to determine whether the given Eigen matrix is in RowMajor
* format. Always returns false, but is overloaded, so the compiler will
* only call it in case the Eigen matrix is in ColMajor format.
* @return False.
*/
template<typename _Scalar, typename _Index>
static bool isEigenRowMajor(
Eigen::SparseMatrix<_Scalar, Eigen::ColMajor, _Index>) {
return false;
}
/*!
* Converts a sparse matrix in the eigen format to Storm Sparse Matrix format.
* @return A pointer to a row-major sparse matrix in our format.
*/
template<class T, int _Options, typename _Index>
static storm::storage::SparseMatrix<T>* toStormSparseMatrix(Eigen::SparseMatrix<T, _Options, _Index> const& matrix) {
uint_fast64_t realNonZeros = matrix.nonZeros();
LOG4CPLUS_DEBUG(logger, "Converting matrix with " << realNonZeros << " non-zeros from Eigen3 format into Storm.");
// Throw an error in case the matrix is not in compressed format.
if (!matrix.isCompressed()) {
LOG4CPLUS_ERROR(logger, "Trying to convert from an Eigen matrix that is not in compressed form.");
return nullptr;
}
/*
* Try to prepare the internal storage and throw an error in case of
* failure.
*/
// Get necessary pointers to the contents of the Eigen matrix.
const T* valuePtr = matrix.valuePtr();
const _Index* indexPtr = matrix.innerIndexPtr();
const _Index* outerPtr = matrix.outerIndexPtr();
const uint_fast64_t outerSize = matrix.outerSize();
storm::storage::SparseMatrix<T>* result = nullptr;
// If the given matrix is in RowMajor format, copying can simply
// be done by adding all values in order.
// Direct copying is, however, prevented because we have to
// separate the diagonal entries from others.
if (isEigenRowMajor(matrix)) {
/* Because of the RowMajor format outerSize evaluates to the
* number of rows.
* Prepare the resulting matrix.
*/
result = new storm::storage::SparseMatrix<T>(matrix.outerSize(), matrix.innerSize());
// Set internal NonZero Counter
result->nonZeroEntryCount = realNonZeros;
result->setState(result->Initialized);
if (!result->prepareInternalStorage(false)) {
LOG4CPLUS_ERROR(logger, "Unable to allocate internal storage while converting Eigen3 RM Matrix to Storm.");
delete result;
return nullptr;
} else {
// Copy Row Indications
std::copy(outerPtr, outerPtr + outerSize, std::back_inserter(result->rowIndications));
// Copy Columns Indications
std::copy(indexPtr, indexPtr + realNonZeros, std::back_inserter(result->columnIndications));
// And do the same thing with the actual values.
std::copy(valuePtr, valuePtr + realNonZeros, std::back_inserter(result->valueStorage));
// This is our Sentinel Element.
result->rowIndications.push_back(realNonZeros);
result->currentSize = realNonZeros;
result->lastRow = outerSize - 1;
}
} else {
/* Because of the RowMajor format outerSize evaluates to the
* number of columns.
* Prepare the resulting matrix.
*/
const uint_fast64_t colCount = matrix.outerSize();
result = new storm::storage::SparseMatrix<T>(matrix.innerSize(), colCount);
// Set internal NonZero Counter
result->nonZeroEntryCount = realNonZeros;
result->setState(result->Initialized);
if (!result->prepareInternalStorage()) {
LOG4CPLUS_ERROR(logger, "Unable to allocate internal storage while converting Eigen3 CM Matrix to Storm.");
delete result;
return nullptr;
} else {
// Set internal NonZero Counter
result->nonZeroEntryCount = realNonZeros;
result->setState(result->Initialized);
// Create an array to remember which elements have to still
// be searched in each column and initialize it with the starting
// index for every column.
_Index* positions = new _Index[colCount]();
for (_Index i = 0; i < colCount; ++i) {
positions[i] = outerPtr[i];
}
// Now copy the elements. As the matrix is in ColMajor format,
// we need to iterate over the columns to find the next non-zero
// entry.
uint_fast64_t i = 0;
int currentRow = 0;
int currentColumn = 0;
while (i < realNonZeros) {
// If the current element belongs the the current column,
// add it in case it is also in the current row.
if ((positions[currentColumn] < outerPtr[currentColumn + 1])
&& (indexPtr[positions[currentColumn]] == currentRow)) {
result->addNextValue(currentRow, currentColumn, valuePtr[positions[currentColumn]]);
// Remember that we found one more non-zero element.
++i;
// Mark this position as "used".
++positions[currentColumn];
}
// Now we can advance to the next column and also row,
// in case we just iterated through the last column.
++currentColumn;
if (currentColumn == colCount) {
currentColumn = 0;
++currentRow;
}
}
delete[] positions;
}
}
result->setState(result->Initialized);
result->finalize();
LOG4CPLUS_DEBUG(logger, "Done converting matrix to storm format.");
return result;
}
};
} //namespace adapters
} //namespace storm
#endif /* STORM_ADAPTERS_STORMADAPTER_H_ */

20
src/parser/NondeterministicSparseTransitionParser.cpp

@ -55,14 +55,6 @@ uint_fast64_t NondeterministicSparseTransitionParser::firstPass(char* buf, uint_
*/ */
buf = strchr(buf, '\n') + 1; // skip format hint buf = strchr(buf, '\n') + 1; // skip format hint
/*
* Parse number of transitions.
* We will not actually use this value, but we will compare it to the
* number of transitions we count and issue a warning if this parsed
* value is wrong.
*/
uint_fast64_t parsed_nonzero = strtol(buf, &buf, 10);
/* /*
* Read all transitions. * Read all transitions.
*/ */
@ -91,7 +83,6 @@ uint_fast64_t NondeterministicSparseTransitionParser::firstPass(char* buf, uint_
if (source > lastsource + 1) { if (source > lastsource + 1) {
nonzero += source - lastsource - 1; nonzero += source - lastsource - 1;
choices += source - lastsource - 1; choices += source - lastsource - 1;
parsed_nonzero += source - lastsource - 1;
} else if (source != lastsource || choice != lastchoice) { } else if (source != lastsource || choice != lastchoice) {
// If we have switched the source state or the nondeterministic choice, we need to // If we have switched the source state or the nondeterministic choice, we need to
// reserve one row more. // reserve one row more.
@ -136,12 +127,6 @@ uint_fast64_t NondeterministicSparseTransitionParser::firstPass(char* buf, uint_
buf = trimWhitespaces(buf); buf = trimWhitespaces(buf);
} }
/*
* Check if the number of transitions given in the file is correct.
*/
if (nonzero != parsed_nonzero) {
LOG4CPLUS_WARN(logger, "File states to have " << parsed_nonzero << " transitions, but I counted " << nonzero << ". Maybe want to fix your file?");
}
return nonzero; return nonzero;
} }
@ -193,11 +178,6 @@ NondeterministicSparseTransitionParser::NondeterministicSparseTransitionParser(s
* Read file header, ignore values within. * Read file header, ignore values within.
*/ */
buf = strchr(buf, '\n') + 1; // skip format hint buf = strchr(buf, '\n') + 1; // skip format hint
buf += 7; // skip "STATES "
checked_strtol(buf, &buf);
buf = trimWhitespaces(buf);
buf += 12; // skip "TRANSITIONS "
checked_strtol(buf, &buf);
/* /*
* Create and initialize matrix. * Create and initialize matrix.

247
src/storage/SparseMatrix.h

@ -29,6 +29,7 @@ namespace storm {
namespace adapters{ namespace adapters{
class GmmxxAdapter; class GmmxxAdapter;
class EigenAdapter; class EigenAdapter;
class StormAdapter;
} }
} }
@ -48,6 +49,7 @@ public:
*/ */
friend class storm::adapters::GmmxxAdapter; friend class storm::adapters::GmmxxAdapter;
friend class storm::adapters::EigenAdapter; friend class storm::adapters::EigenAdapter;
friend class storm::adapters::StormAdapter;
/*! /*!
* If we only want to iterate over the columns of the non-zero entries of * If we only want to iterate over the columns of the non-zero entries of
@ -145,8 +147,7 @@ public:
* Initializes the sparse matrix with the given number of non-zero entries * Initializes the sparse matrix with the given number of non-zero entries
* and prepares it for use with addNextValue() and finalize(). * and prepares it for use with addNextValue() and finalize().
* NOTE: Calling this method before any other member function is mandatory. * NOTE: Calling this method before any other member function is mandatory.
* This version is to be used together with addNextValue(). For
* initialization from an Eigen SparseMatrix, use initialize(Eigen::SparseMatrix<T> &).
* This version is to be used together with addNextValue().
* @param nonZeroEntries The number of non-zero entries that are not on the * @param nonZeroEntries The number of non-zero entries that are not on the
* diagonal. * diagonal.
*/ */
@ -179,135 +180,6 @@ public:
} }
} }
/*!
* Initializes the sparse matrix with the given Eigen sparse matrix.
* NOTE: Calling this method before any other member function is mandatory.
* This version is only to be used when copying an Eigen sparse matrix. For
* initialization with addNextValue() and finalize() use initialize(uint_fast32_t)
* instead.
* @param eigenSparseMatrix The Eigen sparse matrix to be copied.
* *NOTE* Has to be in compressed form!
*/
template<int _Options, typename _Index>
void initialize(const Eigen::SparseMatrix<T, _Options, _Index>& eigenSparseMatrix) {
// Throw an error in case the matrix is not in compressed format.
if (!eigenSparseMatrix.isCompressed()) {
triggerErrorState();
LOG4CPLUS_ERROR(logger, "Trying to initialize from an Eigen matrix that is not in compressed form.");
throw storm::exceptions::InvalidArgumentException("Trying to initialize from an Eigen matrix that is not in compressed form.");
}
if (static_cast<uint_fast64_t>(eigenSparseMatrix.rows()) > this->rowCount) {
triggerErrorState();
LOG4CPLUS_ERROR(logger, "Trying to initialize from an Eigen matrix that has more rows than the target matrix.");
throw storm::exceptions::InvalidArgumentException("Trying to initialize from an Eigen matrix that has more rows than the target matrix.");
}
if (static_cast<uint_fast64_t>(eigenSparseMatrix.cols()) > this->colCount) {
triggerErrorState();
LOG4CPLUS_ERROR(logger, "Trying to initialize from an Eigen matrix that has more columns than the target matrix.");
throw storm::exceptions::InvalidArgumentException("Trying to initialize from an Eigen matrix that has more columns than the target matrix.");
}
const uint_fast64_t entryCount = eigenSparseMatrix.nonZeros();
nonZeroEntryCount = entryCount;
lastRow = 0;
// Try to prepare the internal storage and throw an error in case of
// failure.
// Get necessary pointers to the contents of the Eigen matrix.
const T* valuePtr = eigenSparseMatrix.valuePtr();
const _Index* indexPtr = eigenSparseMatrix.innerIndexPtr();
const _Index* outerPtr = eigenSparseMatrix.outerIndexPtr();
// If the given matrix is in RowMajor format, copying can simply
// be done by adding all values in order.
// Direct copying is, however, prevented because we have to
// separate the diagonal entries from others.
if (isEigenRowMajor(eigenSparseMatrix)) {
// Because of the RowMajor format outerSize evaluates to the
// number of rows.
if (!prepareInternalStorage(false)) {
triggerErrorState();
LOG4CPLUS_ERROR(logger, "Unable to allocate internal storage.");
throw std::bad_alloc();
} else {
if ((static_cast<uint_fast64_t>(eigenSparseMatrix.innerSize()) > nonZeroEntryCount) || (static_cast<uint_fast64_t>(entryCount) > nonZeroEntryCount)) {
triggerErrorState();
LOG4CPLUS_ERROR(logger, "Invalid internal composition of Eigen Sparse Matrix");
throw storm::exceptions::InvalidArgumentException("Invalid internal composition of Eigen Sparse Matrix");
}
std::vector<uint_fast64_t> eigenColumnTemp;
std::vector<uint_fast64_t> eigenRowTemp;
std::vector<T> eigenValueTemp;
uint_fast64_t outerSize = eigenSparseMatrix.outerSize() + 1;
uint_fast64_t entryCountUnsigned = static_cast<uint_fast64_t>(entryCount);
for (uint_fast64_t i = 0; i < entryCountUnsigned; ++i) {
eigenColumnTemp.push_back(indexPtr[i]);
eigenValueTemp.push_back(valuePtr[i]);
}
for (uint_fast64_t i = 0; i < outerSize; ++i) {
eigenRowTemp.push_back(outerPtr[i]);
}
std::copy(eigenRowTemp.begin(), eigenRowTemp.end(), std::back_inserter(this->rowIndications));
std::copy(eigenColumnTemp.begin(), eigenColumnTemp.end(), std::back_inserter(this->columnIndications));
std::copy(eigenValueTemp.begin(), eigenValueTemp.end(), std::back_inserter(this->valueStorage));
currentSize = entryCount;
lastRow = rowCount;
}
} else {
if (!prepareInternalStorage()) {
triggerErrorState();
LOG4CPLUS_ERROR(logger, "Unable to allocate internal storage.");
throw std::bad_alloc();
} else {
// Because of the ColMajor format outerSize evaluates to the
// number of columns.
const _Index colCount = eigenSparseMatrix.outerSize();
// Create an array to remember which elements have to still
// be searched in each column and initialize it with the starting
// index for every column.
_Index* positions = new _Index[colCount]();
for (_Index i = 0; i < colCount; ++i) {
positions[i] = outerPtr[i];
}
// Now copy the elements. As the matrix is in ColMajor format,
// we need to iterate over the columns to find the next non-zero
// entry.
uint_fast64_t i = 0;
int currentRow = 0;
int currentColumn = 0;
while (i < entryCount) {
// If the current element belongs the the current column,
// add it in case it is also in the current row.
if ((positions[currentColumn] < outerPtr[currentColumn + 1])
&& (indexPtr[positions[currentColumn]] == currentRow)) {
addNextValue(currentRow, currentColumn, valuePtr[positions[currentColumn]]);
// Remember that we found one more non-zero element.
++i;
// Mark this position as "used".
++positions[currentColumn];
}
// Now we can advance to the next column and also row,
// in case we just iterated through the last column.
++currentColumn;
if (currentColumn == colCount) {
currentColumn = 0;
++currentRow;
}
}
delete[] positions;
}
}
setState(MatrixStatus::Initialized);
}
/*! /*!
* Sets the matrix element at the given row and column to the given value. * Sets the matrix element at the given row and column to the given value.
* NOTE: This is a linear setter. It must be called consecutively for each element, * NOTE: This is a linear setter. It must be called consecutively for each element,
@ -535,96 +407,6 @@ public:
return (internalStatus == MatrixStatus::Error); return (internalStatus == MatrixStatus::Error);
} }
/*!
* Exports this sparse matrix to Eigens sparse matrix format.
* NOTE: this requires this matrix to be in the ReadReady state.
* @return The sparse matrix in Eigen format.
*/
Eigen::SparseMatrix<T, Eigen::RowMajor, int_fast32_t>* toEigenSparseMatrix() {
// Check whether it is safe to export this matrix.
if (!isReadReady()) {
triggerErrorState();
LOG4CPLUS_ERROR(logger, "Trying to convert a matrix that is not in a readable state to an Eigen matrix.");
throw storm::exceptions::InvalidStateException("Trying to convert a matrix that is not in a readable state to an Eigen matrix.");
} else {
// Create the resulting matrix.
int_fast32_t eigenRows = static_cast<int_fast32_t>(rowCount);
Eigen::SparseMatrix<T, Eigen::RowMajor, int_fast32_t>* mat = new Eigen::SparseMatrix<T, Eigen::RowMajor, int_fast32_t>(eigenRows, eigenRows);
// There are two ways of converting this matrix to Eigen's format.
// 1. Compute a list of triplets (row, column, value) for all
// non-zero elements and pass it to Eigen to create a sparse matrix.
// 2. Tell Eigen to reserve the average number of non-zero elements
// per row in advance and insert the values via a call to Eigen's
// insert method then. As the given reservation number is only an
// estimate, the actual number may be different and Eigen may have
// to shift a lot.
// In most cases, the second alternative is faster (about 1/2 of the
// first, but if there are "heavy" rows that are several times larger
// than an average row, the other solution might be faster.
// The desired conversion method may be set by an appropriate define.
#define STORM_USE_TRIPLETCONVERT
# ifdef STORM_USE_TRIPLETCONVERT
// Prepare the triplet storage.
typedef Eigen::Triplet<T> IntTriplet;
std::vector<IntTriplet> tripletList;
tripletList.reserve(nonZeroEntryCount + rowCount);
// First, iterate over all elements that are not on the diagonal
// and add the corresponding triplet.
uint_fast64_t rowStart;
uint_fast64_t rowEnd;
uint_fast64_t zeroCount = 0;
for (uint_fast64_t row = 0; row < rowCount; ++row) {
rowStart = rowIndications[row];
rowEnd = rowIndications[row + 1];
while (rowStart < rowEnd) {
if (valueStorage[rowStart] == 0) zeroCount++;
tripletList.push_back(IntTriplet(static_cast<int_fast32_t>(row), static_cast<int_fast32_t>(columnIndications[rowStart]), valueStorage[rowStart]));
++rowStart;
}
}
// Let Eigen create a matrix from the given list of triplets.
mat->setFromTriplets(tripletList.begin(), tripletList.end());
# else // NOT STORM_USE_TRIPLETCONVERT
// Reserve the average number of non-zero elements per row for each
// row.
mat->reserve(Eigen::VectorXi::Constant(eigenRows, static_cast<int_fast32_t>((nonZeroEntryCount + rowCount) / eigenRows)));
// Iterate over the all non-zero elements in this matrix and add
// them to the matrix individually.
uint_fast64_t rowStart;
uint_fast64_t rowEnd;
uint_fast64_t count = 0;
for (uint_fast64_t row = 0; row < rowCount; ++row) {
rowStart = rowIndications[row];
rowEnd = rowIndications[row + 1];
// Insert the elements that are not on the diagonal
while (rowStart < rowEnd) {
mat->insert(row, columnIndications[rowStart]) = valueStorage[rowStart];
count++;
++rowStart;
}
}
# endif // STORM_USE_TRIPLETCONVERT
// Make the matrix compressed, i.e. remove remaining zero-entries.
mat->makeCompressed();
return mat;
}
// This point can never be reached as both if-branches end in a return
// statement.
return nullptr;
}
/*! /*!
* Returns the number of non-zero entries that are not on the diagonal. * Returns the number of non-zero entries that are not on the diagonal.
* @returns The number of non-zero entries that are not on the diagonal. * @returns The number of non-zero entries that are not on the diagonal.
@ -1276,29 +1058,6 @@ private:
return this->prepareInternalStorage(true); return this->prepareInternalStorage(true);
} }
/*!
* Helper function to determine whether the given Eigen matrix is in RowMajor
* format. Always returns true, but is overloaded, so the compiler will
* only call it in case the Eigen matrix is in RowMajor format.
* @return True.
*/
template<typename _Scalar, typename _Index>
bool isEigenRowMajor(Eigen::SparseMatrix<_Scalar, Eigen::RowMajor, _Index>) {
return true;
}
/*!
* Helper function to determine whether the given Eigen matrix is in RowMajor
* format. Always returns false, but is overloaded, so the compiler will
* only call it in case the Eigen matrix is in ColMajor format.
* @return False.
*/
template<typename _Scalar, typename _Index>
bool isEigenRowMajor(
Eigen::SparseMatrix<_Scalar, Eigen::ColMajor, _Index>) {
return false;
}
}; };
} // namespace storage } // namespace storage

4
test/parser/ParseMdpTest.cpp

@ -13,9 +13,9 @@
TEST(ParseMdpTest, parseAndOutput) { TEST(ParseMdpTest, parseAndOutput) {
storm::parser::NondeterministicModelParser* mdpParser = nullptr; storm::parser::NondeterministicModelParser* mdpParser = nullptr;
ASSERT_NO_THROW(mdpParser = new storm::parser::NondeterministicModelParser(
/*ASSERT_NO_THROW(*/mdpParser = new storm::parser::NondeterministicModelParser(
STORM_CPP_TESTS_BASE_PATH "/parser/tra_files/mdp_general_input_01.tra", STORM_CPP_TESTS_BASE_PATH "/parser/tra_files/mdp_general_input_01.tra",
STORM_CPP_TESTS_BASE_PATH "/parser/lab_files/pctl_general_input_01.lab"));
STORM_CPP_TESTS_BASE_PATH "/parser/lab_files/pctl_general_input_01.lab")/*)*/;
std::shared_ptr<storm::models::Mdp<double>> mdp = mdpParser->getMdp(); std::shared_ptr<storm::models::Mdp<double>> mdp = mdpParser->getMdp();
std::shared_ptr<storm::storage::SparseMatrix<double>> matrix = mdp->getTransitionMatrix(); std::shared_ptr<storm::storage::SparseMatrix<double>> matrix = mdp->getTransitionMatrix();

33
test/storage/SparseMatrixTest.cpp

@ -3,6 +3,7 @@
#include "src/exceptions/InvalidArgumentException.h" #include "src/exceptions/InvalidArgumentException.h"
#include "src/exceptions/OutOfRangeException.h" #include "src/exceptions/OutOfRangeException.h"
#include "src/adapters/EigenAdapter.h" #include "src/adapters/EigenAdapter.h"
#include "src/adapters/StormAdapter.h"
TEST(SparseMatrixTest, ZeroRowsTest) { TEST(SparseMatrixTest, ZeroRowsTest) {
storm::storage::SparseMatrix<int> *ssm = new storm::storage::SparseMatrix<int>(0); storm::storage::SparseMatrix<int> *ssm = new storm::storage::SparseMatrix<int>(0);
@ -138,9 +139,6 @@ TEST(SparseMatrixTest, Test) {
TEST(SparseMatrixTest, ConversionFromDenseEigen_ColMajor_SparseMatrixTest) { TEST(SparseMatrixTest, ConversionFromDenseEigen_ColMajor_SparseMatrixTest) {
// 10 rows, 100 non zero entries // 10 rows, 100 non zero entries
storm::storage::SparseMatrix<int> *ssm = new storm::storage::SparseMatrix<int>(10);
ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix<int>::MatrixStatus::UnInitialized);
Eigen::SparseMatrix<int> esm(10, 10); Eigen::SparseMatrix<int> esm(10, 10);
for (int row = 0; row < 10; ++row) { for (int row = 0; row < 10; ++row) {
for (int col = 0; col < 10; ++col) { for (int col = 0; col < 10; ++col) {
@ -151,9 +149,8 @@ TEST(SparseMatrixTest, ConversionFromDenseEigen_ColMajor_SparseMatrixTest) {
// make compressed, important for initialize() // make compressed, important for initialize()
esm.makeCompressed(); esm.makeCompressed();
ASSERT_NO_THROW(ssm->initialize(esm));
ASSERT_NO_THROW(ssm->finalize());
storm::storage::SparseMatrix<int> *ssm = nullptr;
ASSERT_NO_THROW(ssm = storm::adapters::StormAdapter::toStormSparseMatrix(esm));
ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix<int>::MatrixStatus::ReadReady); ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix<int>::MatrixStatus::ReadReady);
@ -170,9 +167,6 @@ TEST(SparseMatrixTest, ConversionFromDenseEigen_ColMajor_SparseMatrixTest) {
TEST(SparseMatrixTest, ConversionFromDenseEigen_RowMajor_SparseMatrixTest) { TEST(SparseMatrixTest, ConversionFromDenseEigen_RowMajor_SparseMatrixTest) {
// 10 rows, 100 non zero entries // 10 rows, 100 non zero entries
storm::storage::SparseMatrix<int> *ssm = new storm::storage::SparseMatrix<int>(10);
ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix<int>::MatrixStatus::UnInitialized);
Eigen::SparseMatrix<int, Eigen::RowMajor> esm(10, 10); Eigen::SparseMatrix<int, Eigen::RowMajor> esm(10, 10);
for (int row = 0; row < 10; ++row) { for (int row = 0; row < 10; ++row) {
for (int col = 0; col < 10; ++col) { for (int col = 0; col < 10; ++col) {
@ -183,9 +177,8 @@ TEST(SparseMatrixTest, ConversionFromDenseEigen_RowMajor_SparseMatrixTest) {
// make compressed, important for initialize() // make compressed, important for initialize()
esm.makeCompressed(); esm.makeCompressed();
ASSERT_NO_THROW(ssm->initialize(esm));
ASSERT_NO_THROW(ssm->finalize());
storm::storage::SparseMatrix<int> *ssm = nullptr;
ASSERT_NO_THROW(ssm = storm::adapters::StormAdapter::toStormSparseMatrix(esm));
ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix<int>::MatrixStatus::ReadReady); ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix<int>::MatrixStatus::ReadReady);
@ -202,9 +195,6 @@ TEST(SparseMatrixTest, ConversionFromDenseEigen_RowMajor_SparseMatrixTest) {
TEST(SparseMatrixTest, ConversionFromSparseEigen_ColMajor_SparseMatrixTest) { TEST(SparseMatrixTest, ConversionFromSparseEigen_ColMajor_SparseMatrixTest) {
// 10 rows, 15 non zero entries // 10 rows, 15 non zero entries
storm::storage::SparseMatrix<int> *ssm = new storm::storage::SparseMatrix<int>(10);
ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix<int>::MatrixStatus::UnInitialized);
Eigen::SparseMatrix<int> esm(10, 10); Eigen::SparseMatrix<int> esm(10, 10);
typedef Eigen::Triplet<int> IntTriplet; typedef Eigen::Triplet<int> IntTriplet;
@ -233,9 +223,8 @@ TEST(SparseMatrixTest, ConversionFromSparseEigen_ColMajor_SparseMatrixTest) {
// make compressed, important for initialize() // make compressed, important for initialize()
esm.makeCompressed(); esm.makeCompressed();
ASSERT_NO_THROW(ssm->initialize(esm));
ASSERT_NO_THROW(ssm->finalize());
storm::storage::SparseMatrix<int> *ssm = nullptr;
ASSERT_NO_THROW(ssm = storm::adapters::StormAdapter::toStormSparseMatrix(esm));
ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix<int>::MatrixStatus::ReadReady); ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix<int>::MatrixStatus::ReadReady);
@ -251,9 +240,6 @@ TEST(SparseMatrixTest, ConversionFromSparseEigen_ColMajor_SparseMatrixTest) {
TEST(SparseMatrixTest, ConversionFromSparseEigen_RowMajor_SparseMatrixTest) { TEST(SparseMatrixTest, ConversionFromSparseEigen_RowMajor_SparseMatrixTest) {
// 10 rows, 15 non zero entries // 10 rows, 15 non zero entries
storm::storage::SparseMatrix<int> *ssm = new storm::storage::SparseMatrix<int>(10, 10);
ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix<int>::MatrixStatus::UnInitialized);
Eigen::SparseMatrix<int, Eigen::RowMajor> esm(10, 10); Eigen::SparseMatrix<int, Eigen::RowMajor> esm(10, 10);
typedef Eigen::Triplet<int> IntTriplet; typedef Eigen::Triplet<int> IntTriplet;
@ -282,9 +268,8 @@ TEST(SparseMatrixTest, ConversionFromSparseEigen_RowMajor_SparseMatrixTest) {
// make compressed, important for initialize() // make compressed, important for initialize()
esm.makeCompressed(); esm.makeCompressed();
ASSERT_NO_THROW(ssm->initialize(esm));
ASSERT_NO_THROW(ssm->finalize());
storm::storage::SparseMatrix<int> *ssm = nullptr;
ASSERT_NO_THROW(ssm = storm::adapters::StormAdapter::toStormSparseMatrix(esm));
ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix<int>::MatrixStatus::ReadReady); ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix<int>::MatrixStatus::ReadReady);

0
test/eigen/EigenAdapterTest.cpp → test/storage/adapters/EigenAdapterTest.cpp

111
test/storage/adapters/GmmAdapterTest.cpp

@ -0,0 +1,111 @@
#include "gtest/gtest.h"
#include "gmm/gmm_matrix.h"
#include "src/adapters/GmmxxAdapter.h"
#include "src/exceptions/InvalidArgumentException.h"
#include "boost/integer/integer_mask.hpp"
#define STORM_GMMADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE 5
#define STORM_GMMADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE 5
double getValue(gmm::csr_matrix<double> const& gmmSparseMatrix, uint_fast64_t row, uint_fast64_t col) {
uint_fast64_t rowStart = gmmSparseMatrix.jc.at(row);
uint_fast64_t rowEnd = gmmSparseMatrix.jc.at(row + 1);
while (rowStart < rowEnd) {
if (gmmSparseMatrix.ir.at(rowStart) == col) {
return gmmSparseMatrix.pr.at(rowStart);
}
if (gmmSparseMatrix.ir.at(rowStart) > col) {
break;
}
++rowStart;
}
return 0.0;
}
TEST(GmmAdapterTest, SimpleDenseSquareCopy) {
// 5 rows
storm::storage::SparseMatrix<double> sm(STORM_GMMADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE);
double values[STORM_GMMADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE * STORM_GMMADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE];
sm.initialize(STORM_GMMADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE * STORM_GMMADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE);
int row = 0;
int col = 0;
for (int i = 0; i < STORM_GMMADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE * STORM_GMMADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE; ++i) {
values[i] = static_cast<double>(i + 1);
sm.addNextValue(row, col, values[i]);
++col;
if (col == STORM_GMMADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE) {
++row;
col = 0;
}
}
sm.finalize();
auto gsm = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix(sm);
ASSERT_EQ(gsm->nrows(), STORM_GMMADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE);
ASSERT_EQ(gsm->ncols(), STORM_GMMADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE);
ASSERT_EQ(gmm::nnz(*gsm), STORM_GMMADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE * STORM_GMMADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE);
row = 0;
col = 0;
for (int i = 0; i < STORM_GMMADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE * STORM_GMMADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE; ++i) {
ASSERT_EQ(values[i], getValue(*gsm, row, col));
++col;
if (col == STORM_GMMADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE) {
++row;
col = 0;
}
}
}
TEST(GmmAdapterTest, SimpleSparseSquareCopy) {
// 5 rows
storm::storage::SparseMatrix<double> sm(STORM_GMMADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE);
double values[STORM_GMMADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE * STORM_GMMADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE];
sm.initialize((STORM_GMMADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE * STORM_GMMADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE + 1) / 2);
int row = 0;
int col = 0;
bool everySecondElement = true;
for (int i = 0; i < STORM_GMMADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE * STORM_GMMADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE; ++i) {
values[i] = static_cast<double>(i + 1);
if (everySecondElement) {
sm.addNextValue(row, col, values[i]);
}
everySecondElement = !everySecondElement;
++col;
if (col == STORM_GMMADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE) {
++row;
col = 0;
}
}
sm.finalize();
auto gsm = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix(sm);
ASSERT_EQ(gsm->nrows(), STORM_GMMADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE);
ASSERT_EQ(gsm->ncols(), STORM_GMMADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE);
ASSERT_EQ(gmm::nnz(*gsm), (STORM_GMMADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE * STORM_GMMADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE + 1) / 2);
row = 0;
col = 0;
everySecondElement = true;
for (int i = 0; i < STORM_GMMADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE * STORM_GMMADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE; ++i) {
if (everySecondElement) {
ASSERT_EQ(values[i], getValue(*gsm, row, col));
}
everySecondElement = !everySecondElement;
++col;
if (col == STORM_GMMADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE) {
++row;
col = 0;
}
}
}

104
test/storage/adapters/StormAdapterTest.cpp

@ -0,0 +1,104 @@
#include "gtest/gtest.h"
#include "gmm/gmm_matrix.h"
#include "src/adapters/StormAdapter.h"
#include "src/exceptions/InvalidArgumentException.h"
#include "boost/integer/integer_mask.hpp"
#define STORM_STORMADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE 5
#define STORM_STORMADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE 5
TEST(StormAdapterTest, SimpleDenseSquareCopy) {
// 5 rows
gmm::csr_matrix<double> gmmSparseMatrix;
/*
* As CSR_Matrix is read-only we have to prepare the data in this row_matrix and then do a copy.
*/
gmm::row_matrix<gmm::wsvector<double>> gmmPreMatrix(STORM_STORMADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE, STORM_STORMADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE);
double values[STORM_STORMADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE * STORM_STORMADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE];
int row = 0;
int col = 0;
for (int i = 0; i < STORM_STORMADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE * STORM_STORMADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE; ++i) {
values[i] = static_cast<double>(i + 1);
gmmPreMatrix(row, col) = values[i];
++col;
if (col == STORM_STORMADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE) {
++row;
col = 0;
}
}
gmm::copy(gmmPreMatrix, gmmSparseMatrix);
auto stormSparseMatrix = storm::adapters::StormAdapter::toStormSparseMatrix(gmmSparseMatrix);
ASSERT_EQ(stormSparseMatrix->getRowCount(), STORM_STORMADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE);
ASSERT_EQ(stormSparseMatrix->getColumnCount(), STORM_STORMADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE);
ASSERT_EQ(stormSparseMatrix->getNonZeroEntryCount(), STORM_STORMADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE * STORM_STORMADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE);
row = 0;
col = 0;
for (int i = 0; i < STORM_STORMADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE * STORM_STORMADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE; ++i) {
ASSERT_EQ(values[i], stormSparseMatrix->getValue(row, col));
++col;
if (col == STORM_STORMADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE) {
++row;
col = 0;
}
}
}
TEST(StormAdapterTest, SimpleSparseSquareCopy) {
// 5 rows
gmm::csr_matrix<double> gmmSparseMatrix;
/*
* As CSR_Matrix is read-only we have to prepare the data in this row_matrix and then do a copy.
*/
gmm::row_matrix<gmm::wsvector<double>> gmmPreMatrix(STORM_STORMADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE, STORM_STORMADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE);
double values[STORM_STORMADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE * STORM_STORMADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE];
int row = 0;
int col = 0;
bool everySecondElement = true;
for (int i = 0; i < STORM_STORMADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE * STORM_STORMADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE; ++i) {
values[i] = static_cast<double>(i + 1);
if (everySecondElement) {
gmmPreMatrix(row, col) = values[i];
}
everySecondElement = !everySecondElement;
++col;
if (col == STORM_STORMADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE) {
++row;
col = 0;
}
}
gmm::copy(gmmPreMatrix, gmmSparseMatrix);
auto stormSparseMatrix = storm::adapters::StormAdapter::toStormSparseMatrix(gmmSparseMatrix);
ASSERT_EQ(stormSparseMatrix->getRowCount(), STORM_STORMADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE);
ASSERT_EQ(stormSparseMatrix->getColumnCount(), STORM_STORMADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE);
ASSERT_EQ(stormSparseMatrix->getNonZeroEntryCount(), (STORM_STORMADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE * STORM_STORMADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE + 1) / 2);
row = 0;
col = 0;
everySecondElement = true;
for (int i = 0; i < STORM_STORMADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE * STORM_STORMADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE; ++i) {
if (everySecondElement) {
ASSERT_EQ(values[i], stormSparseMatrix->getValue(row, col));
}
everySecondElement = !everySecondElement;
++col;
if (col == STORM_STORMADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE) {
++row;
col = 0;
}
}
}
Loading…
Cancel
Save