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

Renamed SquareSparseMatrix to SparseMatrix

tempestpy_adaptions
PBerger 12 years ago
parent
36e2f5f15b
commit
557461a77d
17 changed files with 111 additions and 111 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. 4
      src/adapters/GmmxxAdapter.h
  2. 4
      src/modelChecker/EigenDtmcPrctlModelChecker.h
  3. 6
      src/modelChecker/GmmxxDtmcPrctlModelChecker.h
  4. 14
      src/models/Ctmc.h
  5. 14
      src/models/Dtmc.h
  6. 8
      src/models/GraphTransitions.h
  7. 2
      src/parser/DeterministicSparseTransitionParser.cpp
  8. 6
      src/parser/DeterministicSparseTransitionParser.h
  9. 2
      src/parser/DtmcParser.cpp
  10. 2
      src/parser/NonDeterministicSparseTransitionParser.cpp
  11. 6
      src/parser/NonDeterministicSparseTransitionParser.h
  12. 16
      src/storage/JacobiDecomposition.h
  13. 28
      src/storage/SparseMatrix.h
  14. 2
      src/storm.cpp
  15. 2
      src/utility/IoUtility.cpp
  16. 4
      test/parser/ReadTraFileTest.cpp
  17. 102
      test/storage/SparseMatrixTest.cpp

4
src/adapters/GmmxxAdapter.h
View File

@ -8,7 +8,7 @@
#ifndef STORM_ADAPTERS_GMMXXADAPTER_H_
#define STORM_ADAPTERS_GMMXXADAPTER_H_
#include "src/storage/SquareSparseMatrix.h"
#include "src/storage/SparseMatrix.h"
#include "log4cplus/logger.h"
#include "log4cplus/loggingmacros.h"
@ -26,7 +26,7 @@ public:
* @return A pointer to a column-major sparse matrix in gmm++ format.
*/
template<class T>
static gmm::csr_matrix<T>* toGmmxxSparseMatrix(storm::storage::SquareSparseMatrix<T> const& matrix) {
static gmm::csr_matrix<T>* toGmmxxSparseMatrix(storm::storage::SparseMatrix<T> const& matrix) {
uint_fast64_t realNonZeros = matrix.getNonZeroEntryCount();
LOG4CPLUS_DEBUG(logger, "Converting matrix with " << realNonZeros << " non-zeros to gmm++ format.");

4
src/modelChecker/EigenDtmcPrctlModelChecker.h
View File

@ -48,7 +48,7 @@ public:
storm::storage::BitVector* rightStates = this->checkStateFormula(formula.getRight());
// Copy the matrix before we make any changes.
storm::storage::SquareSparseMatrix<Type> tmpMatrix(*this->getModel().getTransitionProbabilityMatrix());
storm::storage::SparseMatrix<Type> tmpMatrix(*this->getModel().getTransitionProbabilityMatrix());
// Make all rows absorbing that violate both sub-formulas or satisfy the second sub-formula.
tmpMatrix.makeRowsAbsorbing((~*leftStates | *rightStates) | *rightStates);
@ -148,7 +148,7 @@ public:
typedef Eigen::Map<VectorType> MapType;
// Now we can eliminate the rows and columns from the original transition probability matrix.
storm::storage::SquareSparseMatrix<double>* submatrix = this->getModel().getTransitionProbabilityMatrix()->getSubmatrix(maybeStates);
storm::storage::SparseMatrix<double>* submatrix = this->getModel().getTransitionProbabilityMatrix()->getSubmatrix(maybeStates);
// Converting the matrix to the form needed for the equation system. That is, we go from
// x = A*x + b to (I-A)x = b.
submatrix->convertToEquationSystem();

6
src/modelChecker/GmmxxDtmcPrctlModelChecker.h
View File

@ -48,7 +48,7 @@ public:
storm::storage::BitVector* rightStates = this->checkStateFormula(formula.getRight());
// Copy the matrix before we make any changes.
storm::storage::SquareSparseMatrix<Type> tmpMatrix(*this->getModel().getTransitionProbabilityMatrix());
storm::storage::SparseMatrix<Type> tmpMatrix(*this->getModel().getTransitionProbabilityMatrix());
// Make all rows absorbing that violate both sub-formulas or satisfy the second sub-formula.
tmpMatrix.makeRowsAbsorbing(~(*leftStates | *rightStates) | *rightStates);
@ -130,7 +130,7 @@ public:
// Only try to solve system if there are states for which the probability is unknown.
if (maybeStates.getNumberOfSetBits() > 0) {
// Now we can eliminate the rows and columns from the original transition probability matrix.
storm::storage::SquareSparseMatrix<Type>* submatrix = this->getModel().getTransitionProbabilityMatrix()->getSubmatrix(maybeStates);
storm::storage::SparseMatrix<Type>* submatrix = this->getModel().getTransitionProbabilityMatrix()->getSubmatrix(maybeStates);
// Converting the matrix from the fixpoint notation to the form needed for the equation
// system. That is, we go from x = A*x + b to (I-A)x = b.
submatrix->convertToEquationSystem();
@ -261,7 +261,7 @@ public:
storm::storage::BitVector maybeStates = ~(*targetStates) & ~infinityStates;
if (maybeStates.getNumberOfSetBits() > 0) {
// Now we can eliminate the rows and columns from the original transition probability matrix.
storm::storage::SquareSparseMatrix<Type>* submatrix = this->getModel().getTransitionProbabilityMatrix()->getSubmatrix(maybeStates);
storm::storage::SparseMatrix<Type>* submatrix = this->getModel().getTransitionProbabilityMatrix()->getSubmatrix(maybeStates);
// Converting the matrix from the fixpoint notation to the form needed for the equation
// system. That is, we go from x = A*x + b to (I-A)x = b.
submatrix->convertToEquationSystem();

14
src/models/Ctmc.h
View File

@ -15,7 +15,7 @@
#include "AtomicPropositionsLabeling.h"
#include "GraphTransitions.h"
#include "src/storage/SquareSparseMatrix.h"
#include "src/storage/SparseMatrix.h"
#include "src/exceptions/InvalidArgumentException.h"
namespace storm {
@ -39,10 +39,10 @@ public:
* @param stateLabeling The labeling that assigns a set of atomic
* propositions to each state.
*/
Ctmc(std::shared_ptr<storm::storage::SquareSparseMatrix<T>> rateMatrix,
Ctmc(std::shared_ptr<storm::storage::SparseMatrix<T>> rateMatrix,
std::shared_ptr<storm::models::AtomicPropositionsLabeling> stateLabeling,
std::shared_ptr<std::vector<T>> stateRewards = nullptr,
std::shared_ptr<storm::storage::SquareSparseMatrix<T>> transitionRewardMatrix = nullptr)
std::shared_ptr<storm::storage::SparseMatrix<T>> transitionRewardMatrix = nullptr)
: rateMatrix(rateMatrix), stateLabeling(stateLabeling),
stateRewards(stateRewards), transitionRewardMatrix(transitionRewardMatrix),
backwardTransitions(nullptr) {
@ -104,7 +104,7 @@ public:
* @return A pointer to the matrix representing the transition probability
* function.
*/
std::shared_ptr<storm::storage::SquareSparseMatrix<T>> getTransitionRateMatrix() const {
std::shared_ptr<storm::storage::SparseMatrix<T>> getTransitionRateMatrix() const {
return this->rateMatrix;
}
@ -112,7 +112,7 @@ public:
* Returns a pointer to the matrix representing the transition rewards.
* @return A pointer to the matrix representing the transition rewards.
*/
std::shared_ptr<storm::storage::SquareSparseMatrix<T>> getTransitionRewardMatrix() const {
std::shared_ptr<storm::storage::SparseMatrix<T>> getTransitionRewardMatrix() const {
return this->transitionRewardMatrix;
}
@ -164,7 +164,7 @@ public:
private:
/*! A matrix representing the transition rate function of the CTMC. */
std::shared_ptr<storm::storage::SquareSparseMatrix<T>> rateMatrix;
std::shared_ptr<storm::storage::SparseMatrix<T>> rateMatrix;
/*! The labeling of the states of the CTMC. */
std::shared_ptr<storm::models::AtomicPropositionsLabeling> stateLabeling;
@ -173,7 +173,7 @@ private:
std::shared_ptr<std::vector<T>> stateRewards;
/*! The transition-based rewards of the CTMC. */
std::shared_ptr<storm::storage::SquareSparseMatrix<T>> transitionRewardMatrix;
std::shared_ptr<storm::storage::SparseMatrix<T>> transitionRewardMatrix;
/*!
* A data structure that stores the predecessors for all states. This is

14
src/models/Dtmc.h
View File

@ -15,7 +15,7 @@
#include "AtomicPropositionsLabeling.h"
#include "GraphTransitions.h"
#include "src/storage/SquareSparseMatrix.h"
#include "src/storage/SparseMatrix.h"
#include "src/exceptions/InvalidArgumentException.h"
#include "src/utility/CommandLine.h"
@ -40,10 +40,10 @@ public:
* @param stateLabeling The labeling that assigns a set of atomic
* propositions to each state.
*/
Dtmc(std::shared_ptr<storm::storage::SquareSparseMatrix<T>> probabilityMatrix,
Dtmc(std::shared_ptr<storm::storage::SparseMatrix<T>> probabilityMatrix,
std::shared_ptr<storm::models::AtomicPropositionsLabeling> stateLabeling,
std::shared_ptr<std::vector<T>> stateRewards = nullptr,
std::shared_ptr<storm::storage::SquareSparseMatrix<T>> transitionRewardMatrix = nullptr)
std::shared_ptr<storm::storage::SparseMatrix<T>> transitionRewardMatrix = nullptr)
: probabilityMatrix(probabilityMatrix), stateLabeling(stateLabeling),
stateRewards(stateRewards), transitionRewardMatrix(transitionRewardMatrix),
backwardTransitions(nullptr) {
@ -111,7 +111,7 @@ public:
* @return A pointer to the matrix representing the transition probability
* function.
*/
std::shared_ptr<storm::storage::SquareSparseMatrix<T>> getTransitionProbabilityMatrix() const {
std::shared_ptr<storm::storage::SparseMatrix<T>> getTransitionProbabilityMatrix() const {
return this->probabilityMatrix;
}
@ -119,7 +119,7 @@ public:
* Returns a pointer to the matrix representing the transition rewards.
* @return A pointer to the matrix representing the transition rewards.
*/
std::shared_ptr<storm::storage::SquareSparseMatrix<T>> getTransitionRewardMatrix() const {
std::shared_ptr<storm::storage::SparseMatrix<T>> getTransitionRewardMatrix() const {
return this->transitionRewardMatrix;
}
@ -210,7 +210,7 @@ private:
}
/*! A matrix representing the transition probability function of the DTMC. */
std::shared_ptr<storm::storage::SquareSparseMatrix<T>> probabilityMatrix;
std::shared_ptr<storm::storage::SparseMatrix<T>> probabilityMatrix;
/*! The labeling of the states of the DTMC. */
std::shared_ptr<storm::models::AtomicPropositionsLabeling> stateLabeling;
@ -219,7 +219,7 @@ private:
std::shared_ptr<std::vector<T>> stateRewards;
/*! The transition-based rewards of the DTMC. */
std::shared_ptr<storm::storage::SquareSparseMatrix<T>> transitionRewardMatrix;
std::shared_ptr<storm::storage::SparseMatrix<T>> transitionRewardMatrix;
/*!
* A data structure that stores the predecessors for all states. This is

8
src/models/GraphTransitions.h
View File

@ -8,7 +8,7 @@
#ifndef STORM_MODELS_GRAPHTRANSITIONS_H_
#define STORM_MODELS_GRAPHTRANSITIONS_H_
#include "src/storage/SquareSparseMatrix.h"
#include "src/storage/SparseMatrix.h"
#include <algorithm>
#include <memory>
@ -39,7 +39,7 @@ public:
* @param forward If set to true, this objects will store the graph structure
* of the backwards transition relation.
*/
GraphTransitions(std::shared_ptr<storm::storage::SquareSparseMatrix<T>> transitionMatrix, bool forward)
GraphTransitions(std::shared_ptr<storm::storage::SparseMatrix<T>> transitionMatrix, bool forward)
: successorList(nullptr), stateIndications(nullptr), numberOfStates(transitionMatrix->getRowCount()), numberOfNonZeroTransitions(transitionMatrix->getNonZeroEntryCount()) {
if (forward) {
this->initializeForward(transitionMatrix);
@ -87,7 +87,7 @@ private:
* Initializes this graph transitions object using the forward transition
* relation given by means of a sparse matrix.
*/
void initializeForward(std::shared_ptr<storm::storage::SquareSparseMatrix<T>> transitionMatrix) {
void initializeForward(std::shared_ptr<storm::storage::SparseMatrix<T>> transitionMatrix) {
this->successorList = new uint_fast64_t[numberOfNonZeroTransitions];
this->stateIndications = new uint_fast64_t[numberOfStates + 1];
@ -109,7 +109,7 @@ private:
* relation, whose forward transition relation is given by means of a sparse
* matrix.
*/
void initializeBackward(std::shared_ptr<storm::storage::SquareSparseMatrix<T>> transitionMatrix) {
void initializeBackward(std::shared_ptr<storm::storage::SparseMatrix<T>> transitionMatrix) {
this->successorList = new uint_fast64_t[numberOfNonZeroTransitions]();
this->stateIndications = new uint_fast64_t[numberOfStates + 1]();

2
src/parser/DeterministicSparseTransitionParser.cpp
View File

@ -153,7 +153,7 @@ DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::st
* non-zero elements has to be specified (which is non_zero, computed by make_first_pass)
*/
LOG4CPLUS_INFO(logger, "Attempting to create matrix of size " << (maxnode+1) << " x " << (maxnode+1) << ".");
this->matrix = std::shared_ptr<storm::storage::SquareSparseMatrix<double>>(new storm::storage::SquareSparseMatrix<double>(maxnode + 1));
this->matrix = std::shared_ptr<storm::storage::SparseMatrix<double>>(new storm::storage::SparseMatrix<double>(maxnode + 1));
if (this->matrix == NULL)
{
LOG4CPLUS_ERROR(logger, "Could not create matrix of size " << (maxnode+1) << " x " << (maxnode+1) << ".");

6
src/parser/DeterministicSparseTransitionParser.h
View File

@ -1,7 +1,7 @@
#ifndef STORM_PARSER_TRAPARSER_H_
#define STORM_PARSER_TRAPARSER_H_
#include "src/storage/SquareSparseMatrix.h"
#include "src/storage/SparseMatrix.h"
#include "src/parser/Parser.h"
#include "src/utility/OsDetection.h"
@ -19,12 +19,12 @@ class DeterministicSparseTransitionParser : public Parser {
public:
DeterministicSparseTransitionParser(std::string const &filename);
std::shared_ptr<storm::storage::SquareSparseMatrix<double>> getMatrix() {
std::shared_ptr<storm::storage::SparseMatrix<double>> getMatrix() {
return this->matrix;
}
private:
std::shared_ptr<storm::storage::SquareSparseMatrix<double>> matrix;
std::shared_ptr<storm::storage::SparseMatrix<double>> matrix;
uint_fast64_t firstPass(char* buf, uint_fast64_t &maxnode);

2
src/parser/DtmcParser.cpp
View File

@ -29,7 +29,7 @@ DtmcParser::DtmcParser(std::string const & transitionSystemFile, std::string con
uint_fast64_t stateCount = tp.getMatrix()->getRowCount();
std::shared_ptr<std::vector<double>> stateRewards = nullptr;
std::shared_ptr<storm::storage::SquareSparseMatrix<double>> transitionRewards = nullptr;
std::shared_ptr<storm::storage::SparseMatrix<double>> transitionRewards = nullptr;
storm::parser::AtomicPropositionLabelingParser lp(stateCount, labelingFile);
if (stateRewardFile != "") {

2
src/parser/NonDeterministicSparseTransitionParser.cpp
View File

@ -168,7 +168,7 @@ NonDeterministicSparseTransitionParser::NonDeterministicSparseTransitionParser(s
* non-zero elements has to be specified (which is non_zero, computed by make_first_pass)
*/
LOG4CPLUS_INFO(logger, "Attempting to create matrix of size " << (maxnode+1) << " x " << (maxnode+1) << ".");
this->matrix = std::shared_ptr<storm::storage::SquareSparseMatrix<double>>(new storm::storage::SquareSparseMatrix<double>(maxnode + 1));
this->matrix = std::shared_ptr<storm::storage::SparseMatrix<double>>(new storm::storage::SparseMatrix<double>(maxnode + 1));
if (this->matrix == NULL)
{
LOG4CPLUS_ERROR(logger, "Could not create matrix of size " << (maxnode+1) << " x " << (maxnode+1) << ".");

6
src/parser/NonDeterministicSparseTransitionParser.h
View File

@ -1,7 +1,7 @@
#ifndef STORM_PARSER_NONDETTRAPARSER_H_
#define STORM_PARSER_NONDETTRAPARSER_H_
#include "src/storage/SquareSparseMatrix.h"
#include "src/storage/SparseMatrix.h"
#include "src/parser/Parser.h"
#include "src/utility/OsDetection.h"
@ -20,12 +20,12 @@ class NonDeterministicSparseTransitionParser : public Parser {
public:
NonDeterministicSparseTransitionParser(std::string const &filename);
std::shared_ptr<storm::storage::SquareSparseMatrix<double>> getMatrix() {
std::shared_ptr<storm::storage::SparseMatrix<double>> getMatrix() {
return this->matrix;
}
private:
std::shared_ptr<storm::storage::SquareSparseMatrix<double>> matrix;
std::shared_ptr<storm::storage::SparseMatrix<double>> matrix;
std::unique_ptr<std::vector<uint_fast64_t>> firstPass(char* buf, uint_fast64_t &maxnode, uint_fast64_t &maxchoice);

16
src/storage/JacobiDecomposition.h
View File

@ -16,7 +16,7 @@ namespace storage {
* Forward declaration against Cycle
*/
template <class T>
class SquareSparseMatrix;
class SparseMatrix;
/*!
@ -26,7 +26,7 @@ template <class T>
class JacobiDecomposition {
public:
JacobiDecomposition(storm::storage::SquareSparseMatrix<T> * const jacobiLuMatrix, storm::storage::SquareSparseMatrix<T> * const jacobiDInvMatrix) : jacobiLuMatrix(jacobiLuMatrix), jacobiDInvMatrix(jacobiDInvMatrix) {
JacobiDecomposition(storm::storage::SparseMatrix<T> * const jacobiLuMatrix, storm::storage::SparseMatrix<T> * const jacobiDInvMatrix) : jacobiLuMatrix(jacobiLuMatrix), jacobiDInvMatrix(jacobiDInvMatrix) {
}
~JacobiDecomposition() {
@ -39,7 +39,7 @@ public:
* Ownership stays with this class.
* @return A reference to the Jacobi LU Matrix
*/
storm::storage::SquareSparseMatrix<T>& getJacobiLUReference() {
storm::storage::SparseMatrix<T>& getJacobiLUReference() {
return *(this->jacobiLuMatrix);
}
@ -48,7 +48,7 @@ public:
* Ownership stays with this class.
* @return A reference to the Jacobi D^{-1} Matrix
*/
storm::storage::SquareSparseMatrix<T>& getJacobiDInvReference() {
storm::storage::SparseMatrix<T>& getJacobiDInvReference() {
return *(this->jacobiDInvMatrix);
}
@ -57,7 +57,7 @@ public:
* Ownership stays with this class.
* @return A pointer to the Jacobi LU Matrix
*/
storm::storage::SquareSparseMatrix<T>* getJacobiLU() {
storm::storage::SparseMatrix<T>* getJacobiLU() {
return this->jacobiLuMatrix;
}
@ -66,7 +66,7 @@ public:
* Ownership stays with this class.
* @return A pointer to the Jacobi D^{-1} Matrix
*/
storm::storage::SquareSparseMatrix<T>* getJacobiDInv() {
storm::storage::SparseMatrix<T>* getJacobiDInv() {
return this->jacobiDInvMatrix;
}
@ -81,12 +81,12 @@ private:
/*!
* Pointer to the LU Matrix
*/
storm::storage::SquareSparseMatrix<T> *jacobiLuMatrix;
storm::storage::SparseMatrix<T> *jacobiLuMatrix;
/*!
* Pointer to the D^{-1} Matrix
*/
storm::storage::SquareSparseMatrix<T> *jacobiDInvMatrix;
storm::storage::SparseMatrix<T> *jacobiDInvMatrix;
};
} // namespace storage

28
src/storage/SquareSparseMatrix.h → src/storage/SparseMatrix.h
View File

@ -1,5 +1,5 @@
#ifndef STORM_STORAGE_SQUARESPARSEMATRIX_H_
#define STORM_STORAGE_SQUARESPARSEMATRIX_H_
#ifndef STORM_STORAGE_SPARSEMATRIX_H_
#define STORM_STORAGE_SPARSEMATRIX_H_
#include <exception>
#include <new>
@ -37,7 +37,7 @@ namespace storage {
* where rows is the first argument to the constructor.
*/
template<class T>
class SquareSparseMatrix {
class SparseMatrix {
public:
/*!
* Declare adapter classes as friends to use internal data.
@ -73,7 +73,7 @@ public:
* Constructs a sparse matrix object with the given number of rows.
* @param rows The number of rows of the matrix
*/
SquareSparseMatrix(uint_fast64_t rows, uint_fast64_t cols)
SparseMatrix(uint_fast64_t rows, uint_fast64_t cols)
: rowCount(rows), colCount(cols), nonZeroEntryCount(0),
internalStatus(MatrixStatus::UnInitialized), currentSize(0), lastRow(0) { }
@ -83,7 +83,7 @@ public:
* Constructs a square sparse matrix object with the given number rows
* @param size The number of rows and cols in the matrix
*/ /*
SquareSparseMatrix(uint_fast64_t size) : SquareSparseMatrix(size, size) { }
SparseMatrix(uint_fast64_t size) : SparseMatrix(size, size) { }
*/
//! Constructor
@ -91,7 +91,7 @@ public:
* Constructs a square sparse matrix object with the given number rows
* @param size The number of rows and cols in the matrix
*/
SquareSparseMatrix(uint_fast64_t size) : rowCount(size), colCount(size), nonZeroEntryCount(0),
SparseMatrix(uint_fast64_t size) : rowCount(size), colCount(size), nonZeroEntryCount(0),
internalStatus(MatrixStatus::UnInitialized), currentSize(0), lastRow(0) { }
//! Copy Constructor
@ -99,7 +99,7 @@ public:
* Copy Constructor. Performs a deep copy of the given sparse matrix.
* @param ssm A reference to the matrix to be copied.
*/
SquareSparseMatrix(const SquareSparseMatrix<T> &ssm)
SparseMatrix(const SparseMatrix<T> &ssm)
: rowCount(ssm.rowCount), colCount(ssm.colCount), nonZeroEntryCount(ssm.nonZeroEntryCount),
internalStatus(ssm.internalStatus), currentSize(ssm.currentSize), lastRow(ssm.lastRow) {
LOG4CPLUS_WARN(logger, "Invoking copy constructor.");
@ -128,7 +128,7 @@ public:
/*!
* Destructor. Performs deletion of the reserved storage arrays.
*/
~SquareSparseMatrix() {
~SparseMatrix() {
setState(MatrixStatus::UnInitialized);
valueStorage.resize(0);
columnIndications.resize(0);
@ -728,7 +728,7 @@ public:
* @param constraint A bit vector indicating which rows and columns to drop.
* @return A pointer to a sparse matrix that is a sub-matrix of the current one.
*/
SquareSparseMatrix* getSubmatrix(storm::storage::BitVector& constraint) const {
SparseMatrix* getSubmatrix(storm::storage::BitVector& constraint) const {
LOG4CPLUS_DEBUG(logger, "Creating a sub-matrix with " << constraint.getNumberOfSetBits() << " rows.");
// Check for valid constraint.
@ -749,7 +749,7 @@ public:
}
// Create and initialize resulting matrix.
SquareSparseMatrix* result = new SquareSparseMatrix(constraint.getNumberOfSetBits());
SparseMatrix* result = new SparseMatrix(constraint.getNumberOfSetBits());
result->initialize(subNonZeroEntries);
// Create a temporary array that stores for each index whose bit is set
@ -833,8 +833,8 @@ public:
*/
storm::storage::JacobiDecomposition<T>* getJacobiDecomposition() const {
uint_fast64_t rowCount = this->getRowCount();
SquareSparseMatrix<T> *resultLU = new SquareSparseMatrix<T>(this);
SquareSparseMatrix<T> *resultDinv = new SquareSparseMatrix<T>(rowCount);
SparseMatrix<T> *resultLU = new SparseMatrix<T>(this);
SparseMatrix<T> *resultDinv = new SparseMatrix<T>(rowCount);
// no entries apart from those on the diagonal
resultDinv->initialize(0);
// copy diagonal entries to other matrix
@ -855,7 +855,7 @@ public:
* @return A vector containing the sum of the elements in each row of the matrix resulting from
* pointwise multiplication of the current matrix with the given matrix.
*/
std::vector<T>* getPointwiseProductRowSumVector(storm::storage::SquareSparseMatrix<T> const& otherMatrix) {
std::vector<T>* getPointwiseProductRowSumVector(storm::storage::SparseMatrix<T> const& otherMatrix) {
// Prepare result.
std::vector<T>* result = new std::vector<T>(rowCount);
@ -1091,4 +1091,4 @@ private:
} // namespace storm
#endif // STORM_STORAGE_SQUARESPARSEMATRIX_H_
#endif // STORM_STORAGE_SPARSEMATRIX_H_

2
src/storm.cpp
View File

@ -20,7 +20,7 @@
#include "storm-config.h"
#include "src/models/Dtmc.h"
#include "src/storage/SquareSparseMatrix.h"
#include "src/storage/SparseMatrix.h"
#include "src/models/AtomicPropositionsLabeling.h"
#include "src/modelChecker/EigenDtmcPrctlModelChecker.h"
#include "src/modelChecker/GmmxxDtmcPrctlModelChecker.h"

2
src/utility/IoUtility.cpp
View File

@ -16,7 +16,7 @@ namespace storm {
namespace utility {
void dtmcToDot(storm::models::Dtmc<double> const &dtmc, std::string filename) {
std::shared_ptr<storm::storage::SquareSparseMatrix<double>> matrix(dtmc.getTransitionProbabilityMatrix());
std::shared_ptr<storm::storage::SparseMatrix<double>> matrix(dtmc.getTransitionProbabilityMatrix());
std::ofstream file;
file.open(filename);

4
test/parser/ReadTraFileTest.cpp
View File

@ -7,7 +7,7 @@
#include "gtest/gtest.h"
#include "storm-config.h"
#include "src/storage/SquareSparseMatrix.h"
#include "src/storage/SparseMatrix.h"
#include "src/parser/DeterministicSparseTransitionParser.h"
#include "src/exceptions/FileIoException.h"
#include "src/exceptions/WrongFileFormatException.h"
@ -24,7 +24,7 @@ TEST(ReadTraFileTest, NonExistingFileTest) {
TEST(ReadTraFileTest, ParseFileTest1) {
storm::parser::DeterministicSparseTransitionParser* parser;
ASSERT_NO_THROW(parser = new storm::parser::DeterministicSparseTransitionParser(STORM_CPP_TESTS_BASE_PATH "/parser/tra_files/csl_general_input_01.tra"));
std::shared_ptr<storm::storage::SquareSparseMatrix<double>> result = parser->getMatrix();
std::shared_ptr<storm::storage::SparseMatrix<double>> result = parser->getMatrix();
if (result != NULL) {
double val = 0;

102
test/storage/SquareSparseMatrixTest.cpp → test/storage/SparseMatrixTest.cpp
View File

@ -1,73 +1,73 @@
#include "gtest/gtest.h"
#include "src/storage/SquareSparseMatrix.h"
#include "src/storage/SparseMatrix.h"
#include "src/exceptions/InvalidArgumentException.h"
#include "src/exceptions/OutOfRangeException.h"
TEST(SquareSparseMatrixTest, ZeroRowsTest) {
storm::storage::SquareSparseMatrix<int> *ssm = new storm::storage::SquareSparseMatrix<int>(0);
ASSERT_EQ(ssm->getState(), storm::storage::SquareSparseMatrix<int>::MatrixStatus::UnInitialized);
TEST(SparseMatrixTest, ZeroRowsTest) {
storm::storage::SparseMatrix<int> *ssm = new storm::storage::SparseMatrix<int>(0);
ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix<int>::MatrixStatus::UnInitialized);
ASSERT_THROW(ssm->initialize(50), storm::exceptions::InvalidArgumentException);
ASSERT_EQ(ssm->getState(), storm::storage::SquareSparseMatrix<int>::MatrixStatus::Error);
ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix<int>::MatrixStatus::Error);
delete ssm;
}
TEST(SquareSparseMatrixTest, TooManyEntriesTest) {
storm::storage::SquareSparseMatrix<int> *ssm = new storm::storage::SquareSparseMatrix<int>(2);
ASSERT_EQ(ssm->getState(), storm::storage::SquareSparseMatrix<int>::MatrixStatus::UnInitialized);
TEST(SparseMatrixTest, TooManyEntriesTest) {
storm::storage::SparseMatrix<int> *ssm = new storm::storage::SparseMatrix<int>(2);
ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix<int>::MatrixStatus::UnInitialized);
ASSERT_THROW(ssm->initialize(10), storm::exceptions::InvalidArgumentException);
ASSERT_EQ(ssm->getState(), storm::storage::SquareSparseMatrix<int>::MatrixStatus::Error);
ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix<int>::MatrixStatus::Error);
delete ssm;
}
TEST(SquareSparseMatrixTest, addNextValueTest) {
storm::storage::SquareSparseMatrix<int> *ssm = new storm::storage::SquareSparseMatrix<int>(5);
ASSERT_EQ(ssm->getState(), storm::storage::SquareSparseMatrix<int>::MatrixStatus::UnInitialized);
TEST(SparseMatrixTest, addNextValueTest) {
storm::storage::SparseMatrix<int> *ssm = new storm::storage::SparseMatrix<int>(5);
ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix<int>::MatrixStatus::UnInitialized);
ASSERT_NO_THROW(ssm->initialize(1));
ASSERT_EQ(ssm->getState(), storm::storage::SquareSparseMatrix<int>::MatrixStatus::Initialized);
ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix<int>::MatrixStatus::Initialized);
ASSERT_THROW(ssm->addNextValue(-1, 1, 1), storm::exceptions::OutOfRangeException);
ASSERT_EQ(ssm->getState(), storm::storage::SquareSparseMatrix<int>::MatrixStatus::Error);
ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix<int>::MatrixStatus::Error);
ASSERT_THROW(ssm->addNextValue(1, -1, 1), storm::exceptions::OutOfRangeException);
ASSERT_EQ(ssm->getState(), storm::storage::SquareSparseMatrix<int>::MatrixStatus::Error);
ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix<int>::MatrixStatus::Error);
ASSERT_THROW(ssm->addNextValue(6, 1, 1), storm::exceptions::OutOfRangeException);
ASSERT_EQ(ssm->getState(), storm::storage::SquareSparseMatrix<int>::MatrixStatus::Error);
ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix<int>::MatrixStatus::Error);
ASSERT_THROW(ssm->addNextValue(1, 6, 1), storm::exceptions::OutOfRangeException);
ASSERT_EQ(ssm->getState(), storm::storage::SquareSparseMatrix<int>::MatrixStatus::Error);
ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix<int>::MatrixStatus::Error);
delete ssm;
}
TEST(SquareSparseMatrixTest, finalizeTest) {
storm::storage::SquareSparseMatrix<int> *ssm = new storm::storage::SquareSparseMatrix<int>(5);
ASSERT_EQ(ssm->getState(), storm::storage::SquareSparseMatrix<int>::MatrixStatus::UnInitialized);
TEST(SparseMatrixTest, finalizeTest) {
storm::storage::SparseMatrix<int> *ssm = new storm::storage::SparseMatrix<int>(5);
ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix<int>::MatrixStatus::UnInitialized);
ASSERT_NO_THROW(ssm->initialize(5));
ASSERT_EQ(ssm->getState(), storm::storage::SquareSparseMatrix<int>::MatrixStatus::Initialized);
ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix<int>::MatrixStatus::Initialized);
ASSERT_NO_THROW(ssm->addNextValue(1, 2, 1));
ASSERT_NO_THROW(ssm->addNextValue(1, 3, 1));
ASSERT_NO_THROW(ssm->addNextValue(1, 4, 1));
ASSERT_NO_THROW(ssm->addNextValue(1, 5, 1));
ASSERT_EQ(ssm->getState(), storm::storage::SquareSparseMatrix<int>::MatrixStatus::Initialized);
ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix<int>::MatrixStatus::Initialized);
ASSERT_THROW(ssm->finalize(), storm::exceptions::InvalidStateException);
ASSERT_EQ(ssm->getState(), storm::storage::SquareSparseMatrix<int>::MatrixStatus::Error);
ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix<int>::MatrixStatus::Error);
delete ssm;
}
TEST(SquareSparseMatrixTest, Test) {
TEST(SparseMatrixTest, Test) {
// 25 rows, 50 non zero entries
storm::storage::SquareSparseMatrix<int> *ssm = new storm::storage::SquareSparseMatrix<int>(25);
ASSERT_EQ(ssm->getState(), storm::storage::SquareSparseMatrix<int>::MatrixStatus::UnInitialized);
storm::storage::SparseMatrix<int> *ssm = new storm::storage::SparseMatrix<int>(25);
ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix<int>::MatrixStatus::UnInitialized);
int values[50] = {
0, 1, 2, 3, 4, 5, 6, 7, 8, 9,
@ -96,15 +96,15 @@ TEST(SquareSparseMatrixTest, Test) {
};
ASSERT_NO_THROW(ssm->initialize(50));
ASSERT_EQ(ssm->getState(), storm::storage::SquareSparseMatrix<int>::MatrixStatus::Initialized);
ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix<int>::MatrixStatus::Initialized);
for (int i = 0; i < 50; ++i) {
ASSERT_NO_THROW(ssm->addNextValue(position_row[i], position_col[i], values[i]));
}
ASSERT_EQ(ssm->getState(), storm::storage::SquareSparseMatrix<int>::MatrixStatus::Initialized);
ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix<int>::MatrixStatus::Initialized);
ASSERT_NO_THROW(ssm->finalize());
ASSERT_EQ(ssm->getState(), storm::storage::SquareSparseMatrix<int>::MatrixStatus::ReadReady);
ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix<int>::MatrixStatus::ReadReady);
int target;
for (int i = 0; i < 50; ++i) {
@ -121,15 +121,15 @@ TEST(SquareSparseMatrixTest, Test) {
ASSERT_EQ(0, target);
}
}
ASSERT_EQ(ssm->getState(), storm::storage::SquareSparseMatrix<int>::MatrixStatus::ReadReady);
ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix<int>::MatrixStatus::ReadReady);
delete ssm;
}
TEST(SquareSparseMatrixTest, ConversionFromDenseEigen_ColMajor_SparseMatrixTest) {
TEST(SparseMatrixTest, ConversionFromDenseEigen_ColMajor_SparseMatrixTest) {
// 10 rows, 100 non zero entries
storm::storage::SquareSparseMatrix<int> *ssm = new storm::storage::SquareSparseMatrix<int>(10);
ASSERT_EQ(ssm->getState(), storm::storage::SquareSparseMatrix<int>::MatrixStatus::UnInitialized);
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);
for (int row = 0; row < 10; ++row) {
@ -145,7 +145,7 @@ TEST(SquareSparseMatrixTest, ConversionFromDenseEigen_ColMajor_SparseMatrixTest)
ASSERT_NO_THROW(ssm->finalize());
ASSERT_EQ(ssm->getState(), storm::storage::SquareSparseMatrix<int>::MatrixStatus::ReadReady);
ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix<int>::MatrixStatus::ReadReady);
int target = -1;
for (int row = 0; row < 10; ++row) {
@ -158,10 +158,10 @@ TEST(SquareSparseMatrixTest, ConversionFromDenseEigen_ColMajor_SparseMatrixTest)
delete ssm;
}
TEST(SquareSparseMatrixTest, ConversionFromDenseEigen_RowMajor_SparseMatrixTest) {
TEST(SparseMatrixTest, ConversionFromDenseEigen_RowMajor_SparseMatrixTest) {
// 10 rows, 100 non zero entries
storm::storage::SquareSparseMatrix<int> *ssm = new storm::storage::SquareSparseMatrix<int>(10);
ASSERT_EQ(ssm->getState(), storm::storage::SquareSparseMatrix<int>::MatrixStatus::UnInitialized);
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);
for (int row = 0; row < 10; ++row) {
@ -177,7 +177,7 @@ TEST(SquareSparseMatrixTest, ConversionFromDenseEigen_RowMajor_SparseMatrixTest)
ASSERT_NO_THROW(ssm->finalize());
ASSERT_EQ(ssm->getState(), storm::storage::SquareSparseMatrix<int>::MatrixStatus::ReadReady);
ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix<int>::MatrixStatus::ReadReady);
int target = -1;
for (int row = 0; row < 10; ++row) {
@ -190,10 +190,10 @@ TEST(SquareSparseMatrixTest, ConversionFromDenseEigen_RowMajor_SparseMatrixTest)
delete ssm;
}
TEST(SquareSparseMatrixTest, ConversionFromSparseEigen_ColMajor_SparseMatrixTest) {
TEST(SparseMatrixTest, ConversionFromSparseEigen_ColMajor_SparseMatrixTest) {
// 10 rows, 15 non zero entries
storm::storage::SquareSparseMatrix<int> *ssm = new storm::storage::SquareSparseMatrix<int>(10);
ASSERT_EQ(ssm->getState(), storm::storage::SquareSparseMatrix<int>::MatrixStatus::UnInitialized);
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);
@ -227,7 +227,7 @@ TEST(SquareSparseMatrixTest, ConversionFromSparseEigen_ColMajor_SparseMatrixTest
ASSERT_NO_THROW(ssm->finalize());
ASSERT_EQ(ssm->getState(), storm::storage::SquareSparseMatrix<int>::MatrixStatus::ReadReady);
ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix<int>::MatrixStatus::ReadReady);
int target = -1;
@ -239,10 +239,10 @@ TEST(SquareSparseMatrixTest, ConversionFromSparseEigen_ColMajor_SparseMatrixTest
delete ssm;
}
TEST(SquareSparseMatrixTest, ConversionFromSparseEigen_RowMajor_SparseMatrixTest) {
TEST(SparseMatrixTest, ConversionFromSparseEigen_RowMajor_SparseMatrixTest) {
// 10 rows, 15 non zero entries
storm::storage::SquareSparseMatrix<int> *ssm = new storm::storage::SquareSparseMatrix<int>(10, 10);
ASSERT_EQ(ssm->getState(), storm::storage::SquareSparseMatrix<int>::MatrixStatus::UnInitialized);
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);
@ -276,7 +276,7 @@ TEST(SquareSparseMatrixTest, ConversionFromSparseEigen_RowMajor_SparseMatrixTest
ASSERT_NO_THROW(ssm->finalize());
ASSERT_EQ(ssm->getState(), storm::storage::SquareSparseMatrix<int>::MatrixStatus::ReadReady);
ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix<int>::MatrixStatus::ReadReady);
const std::vector<uint_fast64_t> rowP = ssm->getRowIndicationsPointer();
const std::vector<uint_fast64_t> colP = ssm->getColumnIndicationsPointer();
@ -292,26 +292,26 @@ TEST(SquareSparseMatrixTest, ConversionFromSparseEigen_RowMajor_SparseMatrixTest
delete ssm;
}
TEST(SquareSparseMatrixTest, ConversionToSparseEigen_RowMajor_SparseMatrixTest) {
TEST(SparseMatrixTest, ConversionToSparseEigen_RowMajor_SparseMatrixTest) {
int values[100];
storm::storage::SquareSparseMatrix<int> *ssm = new storm::storage::SquareSparseMatrix<int>(10);
storm::storage::SparseMatrix<int> *ssm = new storm::storage::SparseMatrix<int>(10);
for (uint_fast32_t i = 0; i < 100; ++i) {
values[i] = i;
}
ASSERT_NO_THROW(ssm->initialize(100));
ASSERT_EQ(ssm->getState(), storm::storage::SquareSparseMatrix<int>::MatrixStatus::Initialized);
ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix<int>::MatrixStatus::Initialized);
for (uint_fast32_t row = 0; row < 10; ++row) {
for (uint_fast32_t col = 0; col < 10; ++col) {
ASSERT_NO_THROW(ssm->addNextValue(row, col, values[row * 10 + col]));
}
}
ASSERT_EQ(ssm->getState(), storm::storage::SquareSparseMatrix<int>::MatrixStatus::Initialized);
ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix<int>::MatrixStatus::Initialized);
ASSERT_NO_THROW(ssm->finalize());
ASSERT_EQ(ssm->getState(), storm::storage::SquareSparseMatrix<int>::MatrixStatus::ReadReady);
ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix<int>::MatrixStatus::ReadReady);
Eigen::SparseMatrix<int, Eigen::RowMajor, int_fast32_t>* esm = ssm->toEigenSparseMatrix();
Write Preview
Loading…
Cancel
Save