diff --git a/src/adapters/GmmxxAdapter.h b/src/adapters/GmmxxAdapter.h index 338d07609..3fd990a46 100644 --- a/src/adapters/GmmxxAdapter.h +++ b/src/adapters/GmmxxAdapter.h @@ -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 - static gmm::csr_matrix* toGmmxxSparseMatrix(storm::storage::SquareSparseMatrix const& matrix) { + static gmm::csr_matrix* toGmmxxSparseMatrix(storm::storage::SparseMatrix const& matrix) { uint_fast64_t realNonZeros = matrix.getNonZeroEntryCount(); LOG4CPLUS_DEBUG(logger, "Converting matrix with " << realNonZeros << " non-zeros to gmm++ format."); diff --git a/src/modelChecker/EigenDtmcPrctlModelChecker.h b/src/modelChecker/EigenDtmcPrctlModelChecker.h index 3c387bec5..e6ea58725 100644 --- a/src/modelChecker/EigenDtmcPrctlModelChecker.h +++ b/src/modelChecker/EigenDtmcPrctlModelChecker.h @@ -48,7 +48,7 @@ public: storm::storage::BitVector* rightStates = this->checkStateFormula(formula.getRight()); // Copy the matrix before we make any changes. - storm::storage::SquareSparseMatrix tmpMatrix(*this->getModel().getTransitionProbabilityMatrix()); + storm::storage::SparseMatrix 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 MapType; // Now we can eliminate the rows and columns from the original transition probability matrix. - storm::storage::SquareSparseMatrix* submatrix = this->getModel().getTransitionProbabilityMatrix()->getSubmatrix(maybeStates); + storm::storage::SparseMatrix* 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(); diff --git a/src/modelChecker/GmmxxDtmcPrctlModelChecker.h b/src/modelChecker/GmmxxDtmcPrctlModelChecker.h index 2d4d65d49..c90efc3b0 100644 --- a/src/modelChecker/GmmxxDtmcPrctlModelChecker.h +++ b/src/modelChecker/GmmxxDtmcPrctlModelChecker.h @@ -48,7 +48,7 @@ public: storm::storage::BitVector* rightStates = this->checkStateFormula(formula.getRight()); // Copy the matrix before we make any changes. - storm::storage::SquareSparseMatrix tmpMatrix(*this->getModel().getTransitionProbabilityMatrix()); + storm::storage::SparseMatrix 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* submatrix = this->getModel().getTransitionProbabilityMatrix()->getSubmatrix(maybeStates); + storm::storage::SparseMatrix* 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* submatrix = this->getModel().getTransitionProbabilityMatrix()->getSubmatrix(maybeStates); + storm::storage::SparseMatrix* 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(); diff --git a/src/models/Ctmc.h b/src/models/Ctmc.h index 7f21528f0..413350124 100644 --- a/src/models/Ctmc.h +++ b/src/models/Ctmc.h @@ -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> rateMatrix, + Ctmc(std::shared_ptr> rateMatrix, std::shared_ptr stateLabeling, std::shared_ptr> stateRewards = nullptr, - std::shared_ptr> transitionRewardMatrix = nullptr) + std::shared_ptr> 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> getTransitionRateMatrix() const { + std::shared_ptr> 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> getTransitionRewardMatrix() const { + std::shared_ptr> getTransitionRewardMatrix() const { return this->transitionRewardMatrix; } @@ -164,7 +164,7 @@ public: private: /*! A matrix representing the transition rate function of the CTMC. */ - std::shared_ptr> rateMatrix; + std::shared_ptr> rateMatrix; /*! The labeling of the states of the CTMC. */ std::shared_ptr stateLabeling; @@ -173,7 +173,7 @@ private: std::shared_ptr> stateRewards; /*! The transition-based rewards of the CTMC. */ - std::shared_ptr> transitionRewardMatrix; + std::shared_ptr> transitionRewardMatrix; /*! * A data structure that stores the predecessors for all states. This is diff --git a/src/models/Dtmc.h b/src/models/Dtmc.h index cb75afc28..55abacffe 100644 --- a/src/models/Dtmc.h +++ b/src/models/Dtmc.h @@ -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> probabilityMatrix, + Dtmc(std::shared_ptr> probabilityMatrix, std::shared_ptr stateLabeling, std::shared_ptr> stateRewards = nullptr, - std::shared_ptr> transitionRewardMatrix = nullptr) + std::shared_ptr> 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> getTransitionProbabilityMatrix() const { + std::shared_ptr> 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> getTransitionRewardMatrix() const { + std::shared_ptr> getTransitionRewardMatrix() const { return this->transitionRewardMatrix; } @@ -210,7 +210,7 @@ private: } /*! A matrix representing the transition probability function of the DTMC. */ - std::shared_ptr> probabilityMatrix; + std::shared_ptr> probabilityMatrix; /*! The labeling of the states of the DTMC. */ std::shared_ptr stateLabeling; @@ -219,7 +219,7 @@ private: std::shared_ptr> stateRewards; /*! The transition-based rewards of the DTMC. */ - std::shared_ptr> transitionRewardMatrix; + std::shared_ptr> transitionRewardMatrix; /*! * A data structure that stores the predecessors for all states. This is diff --git a/src/models/GraphTransitions.h b/src/models/GraphTransitions.h index 122f20dfd..576d99f8c 100644 --- a/src/models/GraphTransitions.h +++ b/src/models/GraphTransitions.h @@ -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 #include @@ -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> transitionMatrix, bool forward) + GraphTransitions(std::shared_ptr> 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> transitionMatrix) { + void initializeForward(std::shared_ptr> 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> transitionMatrix) { + void initializeBackward(std::shared_ptr> transitionMatrix) { this->successorList = new uint_fast64_t[numberOfNonZeroTransitions](); this->stateIndications = new uint_fast64_t[numberOfStates + 1](); diff --git a/src/parser/DeterministicSparseTransitionParser.cpp b/src/parser/DeterministicSparseTransitionParser.cpp index 9c2e5c1b4..b72bdcb4a 100644 --- a/src/parser/DeterministicSparseTransitionParser.cpp +++ b/src/parser/DeterministicSparseTransitionParser.cpp @@ -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>(new storm::storage::SquareSparseMatrix(maxnode + 1)); + this->matrix = std::shared_ptr>(new storm::storage::SparseMatrix(maxnode + 1)); if (this->matrix == NULL) { LOG4CPLUS_ERROR(logger, "Could not create matrix of size " << (maxnode+1) << " x " << (maxnode+1) << "."); diff --git a/src/parser/DeterministicSparseTransitionParser.h b/src/parser/DeterministicSparseTransitionParser.h index a5b8560de..1d699d0c8 100644 --- a/src/parser/DeterministicSparseTransitionParser.h +++ b/src/parser/DeterministicSparseTransitionParser.h @@ -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> getMatrix() { + std::shared_ptr> getMatrix() { return this->matrix; } private: - std::shared_ptr> matrix; + std::shared_ptr> matrix; uint_fast64_t firstPass(char* buf, uint_fast64_t &maxnode); diff --git a/src/parser/DtmcParser.cpp b/src/parser/DtmcParser.cpp index 4f4ed2645..1002c021f 100644 --- a/src/parser/DtmcParser.cpp +++ b/src/parser/DtmcParser.cpp @@ -29,7 +29,7 @@ DtmcParser::DtmcParser(std::string const & transitionSystemFile, std::string con uint_fast64_t stateCount = tp.getMatrix()->getRowCount(); std::shared_ptr> stateRewards = nullptr; - std::shared_ptr> transitionRewards = nullptr; + std::shared_ptr> transitionRewards = nullptr; storm::parser::AtomicPropositionLabelingParser lp(stateCount, labelingFile); if (stateRewardFile != "") { diff --git a/src/parser/NonDeterministicSparseTransitionParser.cpp b/src/parser/NonDeterministicSparseTransitionParser.cpp index 822235c11..08045b373 100644 --- a/src/parser/NonDeterministicSparseTransitionParser.cpp +++ b/src/parser/NonDeterministicSparseTransitionParser.cpp @@ -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>(new storm::storage::SquareSparseMatrix(maxnode + 1)); + this->matrix = std::shared_ptr>(new storm::storage::SparseMatrix(maxnode + 1)); if (this->matrix == NULL) { LOG4CPLUS_ERROR(logger, "Could not create matrix of size " << (maxnode+1) << " x " << (maxnode+1) << "."); diff --git a/src/parser/NonDeterministicSparseTransitionParser.h b/src/parser/NonDeterministicSparseTransitionParser.h index bc144b160..bd46b2593 100644 --- a/src/parser/NonDeterministicSparseTransitionParser.h +++ b/src/parser/NonDeterministicSparseTransitionParser.h @@ -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> getMatrix() { + std::shared_ptr> getMatrix() { return this->matrix; } private: - std::shared_ptr> matrix; + std::shared_ptr> matrix; std::unique_ptr> firstPass(char* buf, uint_fast64_t &maxnode, uint_fast64_t &maxchoice); diff --git a/src/storage/JacobiDecomposition.h b/src/storage/JacobiDecomposition.h index d62f36712..f6de68e98 100644 --- a/src/storage/JacobiDecomposition.h +++ b/src/storage/JacobiDecomposition.h @@ -16,7 +16,7 @@ namespace storage { * Forward declaration against Cycle */ template -class SquareSparseMatrix; +class SparseMatrix; /*! @@ -26,7 +26,7 @@ template class JacobiDecomposition { public: - JacobiDecomposition(storm::storage::SquareSparseMatrix * const jacobiLuMatrix, storm::storage::SquareSparseMatrix * const jacobiDInvMatrix) : jacobiLuMatrix(jacobiLuMatrix), jacobiDInvMatrix(jacobiDInvMatrix) { + JacobiDecomposition(storm::storage::SparseMatrix * const jacobiLuMatrix, storm::storage::SparseMatrix * 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& getJacobiLUReference() { + storm::storage::SparseMatrix& 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& getJacobiDInvReference() { + storm::storage::SparseMatrix& 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* getJacobiLU() { + storm::storage::SparseMatrix* 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* getJacobiDInv() { + storm::storage::SparseMatrix* getJacobiDInv() { return this->jacobiDInvMatrix; } @@ -81,12 +81,12 @@ private: /*! * Pointer to the LU Matrix */ - storm::storage::SquareSparseMatrix *jacobiLuMatrix; + storm::storage::SparseMatrix *jacobiLuMatrix; /*! * Pointer to the D^{-1} Matrix */ - storm::storage::SquareSparseMatrix *jacobiDInvMatrix; + storm::storage::SparseMatrix *jacobiDInvMatrix; }; } // namespace storage diff --git a/src/storage/SquareSparseMatrix.h b/src/storage/SparseMatrix.h similarity index 97% rename from src/storage/SquareSparseMatrix.h rename to src/storage/SparseMatrix.h index bcc96243d..6e4ca5066 100644 --- a/src/storage/SquareSparseMatrix.h +++ b/src/storage/SparseMatrix.h @@ -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 #include @@ -37,7 +37,7 @@ namespace storage { * where rows is the first argument to the constructor. */ template -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 &ssm) + SparseMatrix(const SparseMatrix &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* getJacobiDecomposition() const { uint_fast64_t rowCount = this->getRowCount(); - SquareSparseMatrix *resultLU = new SquareSparseMatrix(this); - SquareSparseMatrix *resultDinv = new SquareSparseMatrix(rowCount); + SparseMatrix *resultLU = new SparseMatrix(this); + SparseMatrix *resultDinv = new SparseMatrix(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* getPointwiseProductRowSumVector(storm::storage::SquareSparseMatrix const& otherMatrix) { + std::vector* getPointwiseProductRowSumVector(storm::storage::SparseMatrix const& otherMatrix) { // Prepare result. std::vector* result = new std::vector(rowCount); @@ -1091,4 +1091,4 @@ private: } // namespace storm -#endif // STORM_STORAGE_SQUARESPARSEMATRIX_H_ +#endif // STORM_STORAGE_SPARSEMATRIX_H_ diff --git a/src/storm.cpp b/src/storm.cpp index 0c5951961..cd7fda7e0 100644 --- a/src/storm.cpp +++ b/src/storm.cpp @@ -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" diff --git a/src/utility/IoUtility.cpp b/src/utility/IoUtility.cpp index 4687e719e..d2f78a25a 100644 --- a/src/utility/IoUtility.cpp +++ b/src/utility/IoUtility.cpp @@ -16,7 +16,7 @@ namespace storm { namespace utility { void dtmcToDot(storm::models::Dtmc const &dtmc, std::string filename) { - std::shared_ptr> matrix(dtmc.getTransitionProbabilityMatrix()); + std::shared_ptr> matrix(dtmc.getTransitionProbabilityMatrix()); std::ofstream file; file.open(filename); diff --git a/test/parser/ReadTraFileTest.cpp b/test/parser/ReadTraFileTest.cpp index 752351e33..2bda7561e 100644 --- a/test/parser/ReadTraFileTest.cpp +++ b/test/parser/ReadTraFileTest.cpp @@ -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> result = parser->getMatrix(); + std::shared_ptr> result = parser->getMatrix(); if (result != NULL) { double val = 0; diff --git a/test/storage/SquareSparseMatrixTest.cpp b/test/storage/SparseMatrixTest.cpp similarity index 61% rename from test/storage/SquareSparseMatrixTest.cpp rename to test/storage/SparseMatrixTest.cpp index 289a52fc6..2a29fb736 100644 --- a/test/storage/SquareSparseMatrixTest.cpp +++ b/test/storage/SparseMatrixTest.cpp @@ -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 *ssm = new storm::storage::SquareSparseMatrix(0); - ASSERT_EQ(ssm->getState(), storm::storage::SquareSparseMatrix::MatrixStatus::UnInitialized); +TEST(SparseMatrixTest, ZeroRowsTest) { + storm::storage::SparseMatrix *ssm = new storm::storage::SparseMatrix(0); + ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix::MatrixStatus::UnInitialized); ASSERT_THROW(ssm->initialize(50), storm::exceptions::InvalidArgumentException); - ASSERT_EQ(ssm->getState(), storm::storage::SquareSparseMatrix::MatrixStatus::Error); + ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix::MatrixStatus::Error); delete ssm; } -TEST(SquareSparseMatrixTest, TooManyEntriesTest) { - storm::storage::SquareSparseMatrix *ssm = new storm::storage::SquareSparseMatrix(2); - ASSERT_EQ(ssm->getState(), storm::storage::SquareSparseMatrix::MatrixStatus::UnInitialized); +TEST(SparseMatrixTest, TooManyEntriesTest) { + storm::storage::SparseMatrix *ssm = new storm::storage::SparseMatrix(2); + ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix::MatrixStatus::UnInitialized); ASSERT_THROW(ssm->initialize(10), storm::exceptions::InvalidArgumentException); - ASSERT_EQ(ssm->getState(), storm::storage::SquareSparseMatrix::MatrixStatus::Error); + ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix::MatrixStatus::Error); delete ssm; } -TEST(SquareSparseMatrixTest, addNextValueTest) { - storm::storage::SquareSparseMatrix *ssm = new storm::storage::SquareSparseMatrix(5); - ASSERT_EQ(ssm->getState(), storm::storage::SquareSparseMatrix::MatrixStatus::UnInitialized); +TEST(SparseMatrixTest, addNextValueTest) { + storm::storage::SparseMatrix *ssm = new storm::storage::SparseMatrix(5); + ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix::MatrixStatus::UnInitialized); ASSERT_NO_THROW(ssm->initialize(1)); - ASSERT_EQ(ssm->getState(), storm::storage::SquareSparseMatrix::MatrixStatus::Initialized); + ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix::MatrixStatus::Initialized); ASSERT_THROW(ssm->addNextValue(-1, 1, 1), storm::exceptions::OutOfRangeException); - ASSERT_EQ(ssm->getState(), storm::storage::SquareSparseMatrix::MatrixStatus::Error); + ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix::MatrixStatus::Error); ASSERT_THROW(ssm->addNextValue(1, -1, 1), storm::exceptions::OutOfRangeException); - ASSERT_EQ(ssm->getState(), storm::storage::SquareSparseMatrix::MatrixStatus::Error); + ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix::MatrixStatus::Error); ASSERT_THROW(ssm->addNextValue(6, 1, 1), storm::exceptions::OutOfRangeException); - ASSERT_EQ(ssm->getState(), storm::storage::SquareSparseMatrix::MatrixStatus::Error); + ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix::MatrixStatus::Error); ASSERT_THROW(ssm->addNextValue(1, 6, 1), storm::exceptions::OutOfRangeException); - ASSERT_EQ(ssm->getState(), storm::storage::SquareSparseMatrix::MatrixStatus::Error); + ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix::MatrixStatus::Error); delete ssm; } -TEST(SquareSparseMatrixTest, finalizeTest) { - storm::storage::SquareSparseMatrix *ssm = new storm::storage::SquareSparseMatrix(5); - ASSERT_EQ(ssm->getState(), storm::storage::SquareSparseMatrix::MatrixStatus::UnInitialized); +TEST(SparseMatrixTest, finalizeTest) { + storm::storage::SparseMatrix *ssm = new storm::storage::SparseMatrix(5); + ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix::MatrixStatus::UnInitialized); ASSERT_NO_THROW(ssm->initialize(5)); - ASSERT_EQ(ssm->getState(), storm::storage::SquareSparseMatrix::MatrixStatus::Initialized); + ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix::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::MatrixStatus::Initialized); + ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix::MatrixStatus::Initialized); ASSERT_THROW(ssm->finalize(), storm::exceptions::InvalidStateException); - ASSERT_EQ(ssm->getState(), storm::storage::SquareSparseMatrix::MatrixStatus::Error); + ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix::MatrixStatus::Error); delete ssm; } -TEST(SquareSparseMatrixTest, Test) { +TEST(SparseMatrixTest, Test) { // 25 rows, 50 non zero entries - storm::storage::SquareSparseMatrix *ssm = new storm::storage::SquareSparseMatrix(25); - ASSERT_EQ(ssm->getState(), storm::storage::SquareSparseMatrix::MatrixStatus::UnInitialized); + storm::storage::SparseMatrix *ssm = new storm::storage::SparseMatrix(25); + ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix::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::MatrixStatus::Initialized); + ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix::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::MatrixStatus::Initialized); + ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix::MatrixStatus::Initialized); ASSERT_NO_THROW(ssm->finalize()); - ASSERT_EQ(ssm->getState(), storm::storage::SquareSparseMatrix::MatrixStatus::ReadReady); + ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix::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::MatrixStatus::ReadReady); + ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix::MatrixStatus::ReadReady); delete ssm; } -TEST(SquareSparseMatrixTest, ConversionFromDenseEigen_ColMajor_SparseMatrixTest) { +TEST(SparseMatrixTest, ConversionFromDenseEigen_ColMajor_SparseMatrixTest) { // 10 rows, 100 non zero entries - storm::storage::SquareSparseMatrix *ssm = new storm::storage::SquareSparseMatrix(10); - ASSERT_EQ(ssm->getState(), storm::storage::SquareSparseMatrix::MatrixStatus::UnInitialized); + storm::storage::SparseMatrix *ssm = new storm::storage::SparseMatrix(10); + ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix::MatrixStatus::UnInitialized); Eigen::SparseMatrix 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::MatrixStatus::ReadReady); + ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix::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 *ssm = new storm::storage::SquareSparseMatrix(10); - ASSERT_EQ(ssm->getState(), storm::storage::SquareSparseMatrix::MatrixStatus::UnInitialized); + storm::storage::SparseMatrix *ssm = new storm::storage::SparseMatrix(10); + ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix::MatrixStatus::UnInitialized); Eigen::SparseMatrix 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::MatrixStatus::ReadReady); + ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix::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 *ssm = new storm::storage::SquareSparseMatrix(10); - ASSERT_EQ(ssm->getState(), storm::storage::SquareSparseMatrix::MatrixStatus::UnInitialized); + storm::storage::SparseMatrix *ssm = new storm::storage::SparseMatrix(10); + ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix::MatrixStatus::UnInitialized); Eigen::SparseMatrix esm(10, 10); @@ -227,7 +227,7 @@ TEST(SquareSparseMatrixTest, ConversionFromSparseEigen_ColMajor_SparseMatrixTest ASSERT_NO_THROW(ssm->finalize()); - ASSERT_EQ(ssm->getState(), storm::storage::SquareSparseMatrix::MatrixStatus::ReadReady); + ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix::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 *ssm = new storm::storage::SquareSparseMatrix(10, 10); - ASSERT_EQ(ssm->getState(), storm::storage::SquareSparseMatrix::MatrixStatus::UnInitialized); + storm::storage::SparseMatrix *ssm = new storm::storage::SparseMatrix(10, 10); + ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix::MatrixStatus::UnInitialized); Eigen::SparseMatrix esm(10, 10); @@ -276,7 +276,7 @@ TEST(SquareSparseMatrixTest, ConversionFromSparseEigen_RowMajor_SparseMatrixTest ASSERT_NO_THROW(ssm->finalize()); - ASSERT_EQ(ssm->getState(), storm::storage::SquareSparseMatrix::MatrixStatus::ReadReady); + ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix::MatrixStatus::ReadReady); const std::vector rowP = ssm->getRowIndicationsPointer(); const std::vector 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 *ssm = new storm::storage::SquareSparseMatrix(10); + storm::storage::SparseMatrix *ssm = new storm::storage::SparseMatrix(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::MatrixStatus::Initialized); + ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix::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::MatrixStatus::Initialized); + ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix::MatrixStatus::Initialized); ASSERT_NO_THROW(ssm->finalize()); - ASSERT_EQ(ssm->getState(), storm::storage::SquareSparseMatrix::MatrixStatus::ReadReady); + ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix::MatrixStatus::ReadReady); Eigen::SparseMatrix* esm = ssm->toEigenSparseMatrix();