Browse Source

Merge with master.

main
dehnert 13 years ago
parent
commit
7873dbca74
  1. 4
      CMakeLists.txt
  2. 3361
      cpplint.py
  3. 76
      src/adapters/GmmxxAdapter.h
  4. 29
      src/adapters/IntermediateRepresentationAdapter.h
  5. 12
      src/exceptions/BaseException.h
  6. 2
      src/formula/BoundedEventually.h
  7. 4
      src/modelChecker/EigenDtmcPrctlModelChecker.h
  8. 6
      src/modelChecker/GmmxxDtmcPrctlModelChecker.h
  9. 25
      src/models/AbstractModel.cpp
  10. 64
      src/models/AbstractModel.h
  11. 24
      src/models/Ctmc.h
  12. 49
      src/models/Dtmc.h
  13. 16
      src/models/GraphTransitions.h
  14. 246
      src/models/Mdp.h
  15. 64
      src/parser/AtomicPropositionLabelingParser.cpp
  16. 70
      src/parser/AutoParser.cpp
  17. 61
      src/parser/AutoParser.h
  18. 80
      src/parser/AutoTransitionParser.cpp
  19. 88
      src/parser/AutoTransitionParser.h
  20. 164
      src/parser/DeterministicSparseTransitionParser.cpp
  21. 6
      src/parser/DeterministicSparseTransitionParser.h
  22. 14
      src/parser/DtmcParser.cpp
  23. 10
      src/parser/DtmcParser.h
  24. 53
      src/parser/MdpParser.cpp
  25. 40
      src/parser/MdpParser.h
  26. 302
      src/parser/NonDeterministicSparseTransitionParser.cpp
  27. 16
      src/parser/NonDeterministicSparseTransitionParser.h
  28. 38
      src/parser/Parser.cpp
  29. 5
      src/parser/Parser.h
  30. 29
      src/parser/SparseStateRewardParser.cpp
  31. 16
      src/storage/JacobiDecomposition.h
  32. 488
      src/storage/SparseMatrix.h
  33. 15
      src/storm.cpp
  34. 6
      src/utility/CommandLine.cpp
  35. 118
      src/utility/IoUtility.cpp
  36. 63
      src/utility/Settings.cpp
  37. 26
      src/utility/Settings.h
  38. 183
      src/vector/dense_vector.h
  39. 32
      test/parser/ParseMdpTest.cpp
  40. 8
      test/parser/ReadTraFileTest.cpp
  41. 120
      test/storage/SparseMatrixTest.cpp
  42. 0
      test/storm-tests.cpp

4
CMakeLists.txt

@ -227,4 +227,6 @@ add_custom_target(memcheck valgrind --leak-check=full --show-reachable=yes ${PRO
DEPENDS storm)
add_custom_target(memcheck-tests valgrind --leak-check=full --show-reachable=yes ${PROJECT_BINARY_DIR}/storm-tests
DEPENDS storm-tests)
set (CPPLINT_ARGS --filter=-whitespace/tab,-whitespace/line_length,-legal/copyright,-readability/streams)
add_custom_target(style python cpplint.py ${CPPLINT_ARGS} `find ./src/ -iname "*.h" -or -iname "*.cpp"`)

3361
cpplint.py
File diff suppressed because it is too large
View File

76
src/adapters/GmmxxAdapter.h

@ -5,10 +5,10 @@
* Author: Christian Dehnert
*/
#ifndef GMMXXADAPTER_H_
#define GMMXXADAPTER_H_
#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,74 +26,20 @@ 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) {
uint_fast64_t realNonZeros = matrix.getNonZeroEntryCount() + matrix.getDiagonalNonZeroEntryCount();
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.");
// Prepare the resulting matrix.
gmm::csr_matrix<T>* result = new gmm::csr_matrix<T>(matrix.rowCount, matrix.rowCount);
// Reserve enough elements for the row indications.
result->jc.reserve(matrix.rowCount + 1);
// For the column indications and the actual values, we have to gather
// the values in a temporary array first, as we have to integrate
// the values from the diagonal. For the row indications, we can just count the number of
// inserted diagonal elements and add it to the previous value.
uint_fast64_t* tmpColumnIndicationsArray = new uint_fast64_t[realNonZeros];
T* tmpValueArray = new T[realNonZeros];
T zero(0);
uint_fast64_t currentPosition = 0;
uint_fast64_t insertedDiagonalElements = 0;
for (uint_fast64_t i = 0; i < matrix.rowCount; ++i) {
// Compute correct start index of row.
result->jc[i] = matrix.rowIndications[i] + insertedDiagonalElements;
// If the current row has no non-zero which is not on the diagonal, we have to check the
// diagonal element explicitly.
if (matrix.rowIndications[i + 1] - matrix.rowIndications[i] == 0) {
if (matrix.diagonalStorage[i] != zero) {
tmpColumnIndicationsArray[currentPosition] = i;
tmpValueArray[currentPosition] = matrix.diagonalStorage[i];
++currentPosition; ++insertedDiagonalElements;
}
} else {
// Otherwise, we can just enumerate the non-zeros which are not on the diagonal
// and fit in the diagonal element where appropriate.
bool includedDiagonal = false;
for (uint_fast64_t j = matrix.rowIndications[i]; j < matrix.rowIndications[i + 1]; ++j) {
if (matrix.diagonalStorage[i] != zero && !includedDiagonal && matrix.columnIndications[j] > i) {
includedDiagonal = true;
tmpColumnIndicationsArray[currentPosition] = i;
tmpValueArray[currentPosition] = matrix.diagonalStorage[i];
++currentPosition; ++insertedDiagonalElements;
}
tmpColumnIndicationsArray[currentPosition] = matrix.columnIndications[j];
tmpValueArray[currentPosition] = matrix.valueStorage[j];
++currentPosition;
}
// If the diagonal element is non-zero and was not inserted until now (i.e. all
// off-diagonal elements in the row are before the diagonal element.
if (!includedDiagonal && matrix.diagonalStorage[i] != zero) {
tmpColumnIndicationsArray[currentPosition] = i;
tmpValueArray[currentPosition] = matrix.diagonalStorage[i];
++currentPosition; ++insertedDiagonalElements;
}
}
}
// Fill in sentinel element at the end.
result->jc[matrix.rowCount] = static_cast<unsigned int>(realNonZeros);
// Now, we can copy the temporary array to the GMMXX format.
// Copy Row Indications
std::copy(matrix.rowIndications.begin(), matrix.rowIndications.end(), std::back_inserter(result->jc));
// Copy Columns Indications
result->ir.resize(realNonZeros);
std::copy(tmpColumnIndicationsArray, tmpColumnIndicationsArray + realNonZeros, result->ir.begin());
delete[] tmpColumnIndicationsArray;
std::copy(matrix.columnIndications.begin(), matrix.columnIndications.end(), std::back_inserter(result->ir));
// And do the same thing with the actual values.
result->pr.resize(realNonZeros);
std::copy(tmpValueArray, tmpValueArray + realNonZeros, result->pr.begin());
delete[] tmpValueArray;
std::copy(matrix.valueStorage.begin(), matrix.valueStorage.end(), std::back_inserter(result->pr));
LOG4CPLUS_DEBUG(logger, "Done converting matrix to gmm++ format.");
@ -105,4 +51,4 @@ public:
} //namespace storm
#endif /* GMMXXADAPTER_H_ */
#endif /* STORM_ADAPTERS_GMMXXADAPTER_H_ */

29
src/adapters/IntermediateRepresentationAdapter.h

@ -165,7 +165,8 @@ public:
storm::storage::SquareSparseMatrix<T>* resultMatrix = new storm::storage::SquareSparseMatrix<T>(allStates.size());
resultMatrix->initialize(totalNumberOfTransitions);
for (StateType* state : allStates) {
uint_fast64_t currentIndex = 0;
for (StateType* currentState : allStates) {
// Iterate over all modules.
for (uint_fast64_t i = 0; i < program.getNumberOfModules(); ++i) {
storm::ir::Module const& module = program.getModule(i);
@ -176,7 +177,7 @@ public:
// Check if this command is enabled in the current state.
if (command.getGuard()->getValueAsBool(*currentState)) {
std::unordered_map<StateType*, double, StateHash, StateCompare> stateToProbabilityMap;
std::map<uint_fast64_t, double> stateIndexToProbabilityMap;
for (uint_fast64_t k = 0; k < command.getNumberOfUpdates(); ++k) {
storm::ir::Update const& update = command.getUpdate(k);
@ -191,15 +192,29 @@ public:
setValue(newState, integerVariableToIndexMap[assignedVariable.first], assignedVariable.second.getExpression()->getValueAsInt(*currentState));
}
auto probIt = stateToProbabilityMap.find(newState);
if (probIt != stateToProbabilityMap.end()) {
stateToProbabilityMap[newState] += update.getLikelihoodExpression()->getValueAsDouble(*currentState);
uint_fast64_t targetIndex = (*stateToIndexMap.find(newState)).second;
delete newState;
auto probIt = stateIndexToProbabilityMap.find(targetIndex);
if (probIt != stateIndexToProbabilityMap.end()) {
stateIndexToProbabilityMap[targetIndex] += update.getLikelihoodExpression()->getValueAsDouble(*currentState);
} else {
++totalNumberOfTransitions;
stateToProbabilityMap[newState] = update.getLikelihoodExpression()->getValueAsDouble(*currentState);
stateIndexToProbabilityMap[targetIndex] = update.getLikelihoodExpression()->getValueAsDouble(*currentState);
}
}
// Now insert the actual values into the matrix.
//for (auto targetIndex : stateIndexToProbabilityMap) {
// resultMatrix->addNextValue(currentIndex, targetIndex.first, targetIndex.second);
//}
}
}
}
++currentIndex;
}
resultMatrix->finalize();
// Now free all the elements we allocated.
for (auto element : allStates) {
delete element;

12
src/exceptions/BaseException.h

@ -8,13 +8,11 @@ namespace storm {
namespace exceptions {
template<typename E>
class BaseException : public std::exception
{
class BaseException : public std::exception {
public:
BaseException() : exception() {}
BaseException(const BaseException& cp)
: exception(cp), stream(cp.stream.str())
{
: exception(cp), stream(cp.stream.str()) {
}
BaseException(const char* cstr) {
@ -24,14 +22,12 @@ class BaseException : public std::exception
~BaseException() throw() { }
template<class T>
E& operator<<(const T& var)
{
E& operator<<(const T& var) {
this->stream << var;
return * dynamic_cast<E*>(this);
}
virtual const char* what() const throw()
{
virtual const char* what() const throw() {
return this->stream.str().c_str();
}

2
src/formula/BoundedEventually.h

@ -120,7 +120,7 @@ public:
BoundedEventually<T>* result = new BoundedEventually<T>();
result->setBound(bound);
if (child != nullptr) {
result->setRight(child->clone());
result->setChild(child->clone());
}
return result;
}

4
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<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

@ -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();

25
src/models/AbstractModel.cpp

@ -0,0 +1,25 @@
#include "src/models/AbstractModel.h"
#include <iostream>
/*!
* This method will output the name of the model type or "Unknown".
* If something went terribly wrong, i.e. if type does not contain any value
* that is valid for a ModelType or some value of the enum was not
* implemented here, it will output "Invalid ModelType".
*
* @param os Output stream.
* @param type Model type.
* @return Output stream os.
*/
std::ostream& storm::models::operator<<(std::ostream& os, storm::models::ModelType const type) {
switch (type) {
case storm::models::Unknown: os << "Unknown"; break;
case storm::models::DTMC: os << "DTMC"; break;
case storm::models::CTMC: os << "CTMC"; break;
case storm::models::MDP: os << "MDP"; break;
case storm::models::CTMDP: os << "CTMDP"; break;
default: os << "Invalid ModelType"; break;
}
return os;
}

64
src/models/AbstractModel.h

@ -0,0 +1,64 @@
#ifndef STORM_MODELS_ABSTRACTMODEL_H_
#define STORM_MODELS_ABSTRACTMODEL_H_
#include <memory>
namespace storm {
namespace models {
/*!
* @brief Enumeration of all supported types of models.
*/
enum ModelType {
Unknown, DTMC, CTMC, MDP, CTMDP
};
/*!
* @brief Stream output operator for ModelType.
*/
std::ostream& operator<<(std::ostream& os, ModelType const type);
/*!
* @brief Base class for all model classes.
*
* This is base class defines a common interface for all models to identify
* their type and obtain the special model.
*/
class AbstractModel {
public:
/*!
* @brief Casts the model to the model type that was actually
* created.
*
* As all methods that work on generic models will use this
* AbstractModel class, this method provides a convenient way to
* cast an AbstractModel object to an object of a concrete model
* type, which can be obtained via getType(). The mapping from an
* element of the ModelType enum to the actual class must be done
* by the caller.
*
* This methods uses std::dynamic_pointer_cast internally.
*
* @return Shared pointer of new type to this object.
*/
template <typename Model>
std::shared_ptr<Model> as() {
return std::dynamic_pointer_cast<Model>(std::shared_ptr<AbstractModel>(this));
}
/*!
* @brief Return the actual type of the model.
*
* Each model must implement this method.
*
* @return Type of the model.
*/
virtual ModelType getType() = 0;
};
} // namespace models
} // namespace storm
#endif /* STORM_MODELS_ABSTRACTMODEL_H_ */

24
src/models/Ctmc.h

@ -15,9 +15,11 @@
#include "AtomicPropositionsLabeling.h"
#include "GraphTransitions.h"
#include "src/storage/SquareSparseMatrix.h"
#include "src/storage/SparseMatrix.h"
#include "src/exceptions/InvalidArgumentException.h"
#include "src/models/AbstractModel.h"
namespace storm {
namespace models {
@ -27,7 +29,7 @@ namespace models {
* labeled with atomic propositions.
*/
template <class T>
class Ctmc {
class Ctmc : public storm::models::AbstractModel {
public:
//! Constructor
@ -39,10 +41,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) {
@ -56,7 +58,7 @@ public:
Ctmc(const Ctmc<T> &ctmc) : rateMatrix(ctmc.rateMatrix),
stateLabeling(ctmc.stateLabeling), stateRewards(ctmc.stateRewards),
transitionRewardMatrix(ctmc.transitionRewardMatrix) {
if (ctmc.backardTransitions != nullptr) {
if (ctmc.backwardTransitions != nullptr) {
this->backwardTransitions = new storm::models::GraphTransitions<T>(*ctmc.backwardTransitions);
}
}
@ -104,7 +106,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 +114,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;
}
@ -161,10 +163,14 @@ public:
<< std::endl;
}
storm::models::ModelType getType() {
return CTMC;
}
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 +179,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

49
src/models/Dtmc.h

@ -15,9 +15,11 @@
#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"
#include "src/utility/Settings.h"
#include "src/models/AbstractModel.h"
namespace storm {
@ -28,7 +30,7 @@ namespace models {
* labeled with atomic propositions.
*/
template <class T>
class Dtmc {
class Dtmc : public storm::models::AbstractModel {
public:
//! Constructor
@ -40,15 +42,16 @@ 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) {
if (!this->checkValidityProbabilityMatrix()) {
std::cerr << "Probability matrix is invalid" << std::endl;
if (!this->checkValidityOfProbabilityMatrix()) {
LOG4CPLUS_ERROR(logger, "Probability matrix is invalid.");
throw storm::exceptions::InvalidArgumentException() << "Probability matrix is invalid.";
}
}
@ -60,11 +63,12 @@ public:
Dtmc(const Dtmc<T> &dtmc) : probabilityMatrix(dtmc.probabilityMatrix),
stateLabeling(dtmc.stateLabeling), stateRewards(dtmc.stateRewards),
transitionRewardMatrix(dtmc.transitionRewardMatrix) {
if (dtmc.backardTransitions != nullptr) {
if (dtmc.backwardTransitions != nullptr) {
this->backwardTransitions = new storm::models::GraphTransitions<T>(*dtmc.backwardTransitions);
}
if (!this->checkValidityProbabilityMatrix()) {
std::cerr << "Probability matrix is invalid" << std::endl;
if (!this->checkValidityOfProbabilityMatrix()) {
LOG4CPLUS_ERROR(logger, "Probability matrix is invalid.");
throw storm::exceptions::InvalidArgumentException() << "Probability matrix is invalid.";
}
}
@ -111,7 +115,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 +123,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;
}
@ -192,6 +196,10 @@ public:
out << std::endl;
storm::utility::printSeparationLine(out);
}
storm::models::ModelType getType() {
return DTMC;
}
private:
@ -200,17 +208,26 @@ private:
*
* Checks probability matrix if all rows sum up to one.
*/
bool checkValidityProbabilityMatrix() {
bool checkValidityOfProbabilityMatrix() {
// Get the settings object to customize linear solving.
storm::settings::Settings* s = storm::settings::instance();
double precision = s->get<double>("precision");
if (this->probabilityMatrix->getRowCount() != this->probabilityMatrix->getColumnCount()) {
// not square
return false;
}
for (uint_fast64_t row = 0; row < this->probabilityMatrix->getRowCount(); row++) {
T sum = this->probabilityMatrix->getRowSum(row);
if (sum == 0) continue;
if (std::abs(sum - 1) > 1e-10) return false;
if (sum == 0) return false;
if (std::abs(sum - 1) > precision) return false;
}
return true;
}
/*! 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 +236,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

16
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 <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,18 +87,18 @@ 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];
// First, we copy the index list from the sparse matrix as this will
// stay the same.
std::copy(transitionMatrix->getRowIndicationsPointer(), transitionMatrix->getRowIndicationsPointer() + numberOfStates + 1, this->stateIndications);
std::copy(transitionMatrix->getRowIndicationsPointer().begin(), transitionMatrix->getRowIndicationsPointer().end(), this->stateIndications);
// Now we can iterate over all rows of the transition matrix and record
// the target state.
for (uint_fast64_t i = 0, currentNonZeroElement = 0; i < numberOfStates; i++) {
for (auto rowIt = transitionMatrix->beginConstColumnNoDiagIterator(i); rowIt != transitionMatrix->endConstColumnNoDiagIterator(i); ++rowIt) {
for (auto rowIt = transitionMatrix->beginConstColumnIterator(i); rowIt != transitionMatrix->endConstColumnIterator(i); ++rowIt) {
this->stateIndications[currentNonZeroElement++] = *rowIt;
}
}
@ -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]();
@ -117,7 +117,7 @@ private:
// NOTE: We disregard the diagonal here, as we only consider "true"
// predecessors.
for (uint_fast64_t i = 0; i < numberOfStates; i++) {
for (auto rowIt = transitionMatrix->beginConstColumnNoDiagIterator(i); rowIt != transitionMatrix->endConstColumnNoDiagIterator(i); ++rowIt) {
for (auto rowIt = transitionMatrix->beginConstColumnIterator(i); rowIt != transitionMatrix->endConstColumnIterator(i); ++rowIt) {
this->stateIndications[*rowIt + 1]++;
}
}
@ -140,7 +140,7 @@ private:
// Now we are ready to actually fill in the list of predecessors for
// every state. Again, we start by considering all but the last row.
for (uint_fast64_t i = 0; i < numberOfStates; i++) {
for (auto rowIt = transitionMatrix->beginConstColumnNoDiagIterator(i); rowIt != transitionMatrix->endConstColumnNoDiagIterator(i); ++rowIt) {
for (auto rowIt = transitionMatrix->beginConstColumnIterator(i); rowIt != transitionMatrix->endConstColumnIterator(i); ++rowIt) {
this->successorList[nextIndicesList[*rowIt]++] = i;
}
}

246
src/models/Mdp.h

@ -0,0 +1,246 @@
/*
* Mdp.h
*
* Created on: 14.01.2013
* Author: Philipp Berger
*/
#ifndef STORM_MODELS_MDP_H_
#define STORM_MODELS_MDP_H_
#include <ostream>
#include <iostream>
#include <memory>
#include <cstdlib>
#include "AtomicPropositionsLabeling.h"
#include "GraphTransitions.h"
#include "src/storage/SparseMatrix.h"
#include "src/exceptions/InvalidArgumentException.h"
#include "src/utility/CommandLine.h"
#include "src/utility/Settings.h"
#include "src/models/AbstractModel.h"
namespace storm {
namespace models {
/*!
* This class represents a Markov Decision Process (MDP) whose states are
* labeled with atomic propositions.
*/
template <class T>
class Mdp : public storm::models::AbstractModel {
public:
//! Constructor
/*!
* Constructs a MDP object from the given transition probability matrix and
* the given labeling of the states.
* @param probabilityMatrix The transition probability relation of the
* MDP given by a matrix.
* @param stateLabeling The labeling that assigns a set of atomic
* propositions to each state.
*/
Mdp(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::SparseMatrix<T>> transitionRewardMatrix = nullptr)
: probabilityMatrix(probabilityMatrix), stateLabeling(stateLabeling),
stateRewards(stateRewards), transitionRewardMatrix(transitionRewardMatrix),
backwardTransitions(nullptr) {
if (!this->checkValidityOfProbabilityMatrix()) {
LOG4CPLUS_ERROR(logger, "Probability matrix is invalid.");
throw storm::exceptions::InvalidArgumentException() << "Probability matrix is invalid.";
}
}
//! Copy Constructor
/*!
* Copy Constructor. Performs a deep copy of the given MDP.
* @param mdp A reference to the MDP that is to be copied.
*/
Mdp(const Mdp<T> &mdp) : probabilityMatrix(mdp.probabilityMatrix),
stateLabeling(mdp.stateLabeling), stateRewards(mdp.stateRewards),
transitionRewardMatrix(mdp.transitionRewardMatrix) {
if (mdp.backwardTransitions != nullptr) {
this->backwardTransitions = new storm::models::GraphTransitions<T>(*mdp.backwardTransitions);
}
if (!this->checkValidityOfProbabilityMatrix()) {
LOG4CPLUS_ERROR(logger, "Probability matrix is invalid.");
throw storm::exceptions::InvalidArgumentException() << "Probability matrix is invalid.";
}
}
//! Destructor
/*!
* Destructor. Frees the matrix and labeling associated with this MDP.
*/
~Mdp() {
if (this->backwardTransitions != nullptr) {
delete this->backwardTransitions;
}
}
/*!
* Returns the state space size of the MDP.
* @return The size of the state space of the MDP.
*/
uint_fast64_t getNumberOfStates() const {
return this->probabilityMatrix->getColumnCount();
}
/*!
* Returns the number of (non-zero) transitions of the MDP.
* @return The number of (non-zero) transitions of the MDP.
*/
uint_fast64_t getNumberOfTransitions() const {
return this->probabilityMatrix->getNonZeroEntryCount();
}
/*!
* Returns a bit vector in which exactly those bits are set to true that
* correspond to a state labeled with the given atomic proposition.
* @param ap The atomic proposition for which to get the bit vector.
* @return A bit vector in which exactly those bits are set to true that
* correspond to a state labeled with the given atomic proposition.
*/
storm::storage::BitVector* getLabeledStates(std::string ap) const {
return this->stateLabeling->getAtomicProposition(ap);
}
/*!
* Returns a pointer to the matrix representing the transition probability
* function.
* @return A pointer to the matrix representing the transition probability
* function.
*/
std::shared_ptr<storm::storage::SparseMatrix<T>> getTransitionProbabilityMatrix() const {
return this->probabilityMatrix;
}
/*!
* 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::SparseMatrix<T>> getTransitionRewardMatrix() const {
return this->transitionRewardMatrix;
}
/*!
* Returns a pointer to the vector representing the state rewards.
* @return A pointer to the vector representing the state rewards.
*/
std::shared_ptr<std::vector<T>> getStateRewards() const {
return this->stateRewards;
}
/*!
*
*/
std::set<std::string> const getPropositionsForState(uint_fast64_t const &state) const {
return stateLabeling->getPropositionsForState(state);
}
/*!
* Retrieves a reference to the backwards transition relation.
* @return A reference to the backwards transition relation.
*/
storm::models::GraphTransitions<T>& getBackwardTransitions() {
if (this->backwardTransitions == nullptr) {
this->backwardTransitions = new storm::models::GraphTransitions<T>(this->probabilityMatrix, false);
}
return *this->backwardTransitions;
}
/*!
* Retrieves whether this MDP has a state reward model.
* @return True if this MDP has a state reward model.
*/
bool hasStateRewards() {
return this->stateRewards != nullptr;
}
/*!
* Retrieves whether this MDP has a transition reward model.
* @return True if this MDP has a transition reward model.
*/
bool hasTransitionRewards() {
return this->transitionRewardMatrix != nullptr;
}
/*!
* Retrieves whether the given atomic proposition is a valid atomic proposition in this model.
* @param atomicProposition The atomic proposition to be checked for validity.
* @return True if the given atomic proposition is valid in this model.
*/
bool hasAtomicProposition(std::string const& atomicProposition) {
return this->stateLabeling->containsAtomicProposition(atomicProposition);
}
/*!
* Prints information about the model to the specified stream.
* @param out The stream the information is to be printed to.
*/
void printModelInformationToStream(std::ostream& out) const {
storm::utility::printSeparationLine(out);
out << std::endl;
out << "Model type: \t\tMDP" << std::endl;
out << "States: \t\t" << this->getNumberOfStates() << std::endl;
out << "Transitions: \t\t" << this->getNumberOfTransitions() << std::endl;
this->stateLabeling->printAtomicPropositionsInformationToStream(out);
out << "Size in memory: \t"
<< (this->probabilityMatrix->getSizeInMemory() +
this->stateLabeling->getSizeInMemory() +
sizeof(*this))/1024 << " kbytes" << std::endl;
out << std::endl;
storm::utility::printSeparationLine(out);
}
storm::models::ModelType getType() {
return MDP;
}
private:
/*!
* @brief Perform some sanity checks.
*
* Checks probability matrix if all rows sum up to one.
*/
bool checkValidityOfProbabilityMatrix() {
// Get the settings object to customize linear solving.
storm::settings::Settings* s = storm::settings::instance();
double precision = s->get<double>("precision");
for (uint_fast64_t row = 0; row < this->probabilityMatrix->getRowCount(); row++) {
T sum = this->probabilityMatrix->getRowSum(row);
if (sum == 0) continue;
if (std::abs(sum - 1) > precision) return false;
}
return true;
}
/*! A matrix representing the transition probability function of the MDP. */
std::shared_ptr<storm::storage::SparseMatrix<T>> probabilityMatrix;
/*! The labeling of the states of the MDP. */
std::shared_ptr<storm::models::AtomicPropositionsLabeling> stateLabeling;
/*! The state-based rewards of the MDP. */
std::shared_ptr<std::vector<T>> stateRewards;
/*! The transition-based rewards of the MDP. */
std::shared_ptr<storm::storage::SparseMatrix<T>> transitionRewardMatrix;
/*!
* A data structure that stores the predecessors for all states. This is
* needed for backwards directed searches.
*/
storm::models::GraphTransitions<T>* backwardTransitions;
};
} // namespace models
} // namespace storm
#endif /* STORM_MODELS_MDP_H_ */

64
src/parser/AtomicPropositionLabelingParser.cpp

@ -7,20 +7,22 @@
#include "src/parser/AtomicPropositionLabelingParser.h"
#include "src/exceptions/WrongFileFormatException.h"
#include "src/exceptions/FileIoException.h"
#include <errno.h>
#include <time.h>
#include <sys/stat.h>
#include <fcntl.h>
#include <locale.h>
#include "src/utility/OsDetection.h"
#include <cstdlib>
#include <cstdio>
#include <cstring>
#include <string>
#include <clocale>
#include <iostream>
#include <errno.h>
#include <time.h>
#include <sys/stat.h>
#include <fcntl.h>
#include <locale.h>
#include "src/exceptions/WrongFileFormatException.h"
#include "src/exceptions/FileIoException.h"
#include "src/utility/OsDetection.h"
#include "log4cplus/logger.h"
#include "log4cplus/loggingmacros.h"
@ -39,17 +41,16 @@ namespace parser {
* @return The pointer to the created labeling object.
*/
AtomicPropositionLabelingParser::AtomicPropositionLabelingParser(uint_fast64_t node_count,
std::string const & filename)
: labeling(nullptr)
{
std::string const & filename)
: labeling(nullptr) {
/*
* open file
* Open file.
*/
MappedFile file(filename.c_str());
char* buf = file.data;
/*
* first run: obtain number of propositions
* First run: obtain number of propositions.
*/
char separator[] = " \r\n\t";
bool foundDecl = false, foundEnd = false;
@ -57,11 +58,11 @@ AtomicPropositionLabelingParser::AtomicPropositionLabelingParser(uint_fast64_t n
{
size_t cnt = 0;
/*
* iterate over tokens until we hit #END or end of file
* Iterate over tokens until we hit #END or end of file.
*/
while(buf[0] != '\0') {
buf += cnt;
cnt = strcspn(buf, separator); // position of next separator
cnt = strcspn(buf, separator); // position of next separator
if (cnt > 0) {
/*
* next token is #DECLARATION: just skip it
@ -71,31 +72,32 @@ AtomicPropositionLabelingParser::AtomicPropositionLabelingParser(uint_fast64_t n
if (strncmp(buf, "#DECLARATION", cnt) == 0) {
foundDecl = true;
continue;
}
else if (strncmp(buf, "#END", cnt) == 0) {
} else if (strncmp(buf, "#END", cnt) == 0) {
foundEnd = true;
break;
}
proposition_count++;
} else buf++; // next char is separator, one step forward
} else {
buf++; // next char is separator, one step forward
}
}
/*
* If #DECLARATION or #END were not found, the file format is wrong
*/
if (! (foundDecl && foundEnd)) {
if (!(foundDecl && foundEnd)) {
LOG4CPLUS_ERROR(logger, "Wrong file format in (" << filename << "). File header is corrupted.");
if (! foundDecl) LOG4CPLUS_ERROR(logger, "\tDid not find #DECLARATION token.");
if (! foundEnd) LOG4CPLUS_ERROR(logger, "\tDid not find #END token.");
if (!foundDecl) LOG4CPLUS_ERROR(logger, "\tDid not find #DECLARATION token.");
if (!foundEnd) LOG4CPLUS_ERROR(logger, "\tDid not find #END token.");
throw storm::exceptions::WrongFileFormatException();
}
}
/*
* create labeling object with given node and proposition count
*/
this->labeling = std::shared_ptr<storm::models::AtomicPropositionsLabeling>(new storm::models::AtomicPropositionsLabeling(node_count, proposition_count));
/*
* second run: add propositions and node labels to labeling
*
@ -107,11 +109,11 @@ AtomicPropositionLabelingParser::AtomicPropositionLabelingParser(uint_fast64_t n
* load propositions
* As we already checked the file format, we can be a bit sloppy here...
*/
char proposition[128]; // buffer for proposition names
char proposition[128]; // buffer for proposition names
size_t cnt = 0;
do {
buf += cnt;
cnt = strcspn(buf, separator); // position of next separator
cnt = strcspn(buf, separator); // position of next separator
if (cnt >= sizeof(proposition)) {
/*
* if token is longer than our buffer, the following strncpy code might get risky...
@ -129,7 +131,9 @@ AtomicPropositionLabelingParser::AtomicPropositionLabelingParser(uint_fast64_t n
strncpy(proposition, buf, cnt);
proposition[cnt] = '\0';
this->labeling->addAtomicProposition(proposition);
} else cnt = 1; // next char is separator, one step forward
} else {
cnt = 1; // next char is separator, one step forward
}
} while (cnt > 0);
/*
* Right here, the buf pointer is still pointing to our last token,
@ -137,7 +141,7 @@ AtomicPropositionLabelingParser::AtomicPropositionLabelingParser(uint_fast64_t n
*/
buf += 4;
}
{
/*
* now parse node label assignments
@ -178,5 +182,5 @@ AtomicPropositionLabelingParser::AtomicPropositionLabelingParser(uint_fast64_t n
}
}
} //namespace parser
} //namespace storm
} // namespace parser
} // namespace storm

70
src/parser/AutoParser.cpp

@ -0,0 +1,70 @@
#include "src/parser/AutoParser.h"
#include <string>
#include <cctype>
#include "src/exceptions/WrongFileFormatException.h"
#include "src/models/AbstractModel.h"
#include "src/parser/DtmcParser.h"
#include "src/parser/MdpParser.h"
namespace storm {
namespace parser {
AutoParser::AutoParser(std::string const & transitionSystemFile, std::string const & labelingFile,
std::string const & stateRewardFile, std::string const & transitionRewardFile)
: model(nullptr) {
storm::models::ModelType type = this->analyzeHint(transitionSystemFile);
if (type == storm::models::Unknown) {
LOG4CPLUS_ERROR(logger, "Could not determine file type of " << transitionSystemFile << ".");
LOG4CPLUS_ERROR(logger, "The first line of the file should contain a format hint. Please fix your file and try again.");
throw storm::exceptions::WrongFileFormatException() << "Could not determine type of file " << transitionSystemFile;
} else {
LOG4CPLUS_INFO(logger, "Model type seems to be " << type);
}
// Do actual parsing
switch (type) {
case storm::models::DTMC: {
DtmcParser* parser = new DtmcParser(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile);
this->model = parser->getDtmc();
break;
}
case storm::models::CTMC:
break;
case storm::models::MDP: {
MdpParser* parser = new MdpParser(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile);
this->model = parser->getMdp();
break;
}
case storm::models::CTMDP:
break;
default: ; // Unknown
}
if (!this->model) std::cout << "model is still null" << std::endl;
}
storm::models::ModelType AutoParser::analyzeHint(const std::string& filename) {
storm::models::ModelType hintType = storm::models::Unknown;
// Open file
MappedFile file(filename.c_str());
char* buf = file.data;
// parse hint
char hint[128];
sscanf(buf, "%s\n", hint);
for (char* c = hint; *c != '\0'; c++) *c = toupper(*c);
// check hint
if (strncmp(hint, "DTMC", sizeof(hint)) == 0) hintType = storm::models::DTMC;
else if (strncmp(hint, "CTMC", sizeof(hint)) == 0) hintType = storm::models::CTMC;
else if (strncmp(hint, "MDP", sizeof(hint)) == 0) hintType = storm::models::MDP;
else if (strncmp(hint, "CTMDP", sizeof(hint)) == 0) hintType = storm::models::CTMDP;
return hintType;
}
} // namespace parser
} // namespace storm

61
src/parser/AutoParser.h

@ -0,0 +1,61 @@
#ifndef STORM_PARSER_AUTOPARSER_H_
#define STORM_PARSER_AUTOPARSER_H_
#include "src/parser/Parser.h"
#include "src/models/AbstractModel.h"
#include <memory>
#include <iostream>
#include <utility>
namespace storm {
namespace parser {
/*!
* @brief Checks the given files and parses the model within these files.
*
* This parser analyzes the format hitn in the first line of the transition
* file. If this is a valid format, it will use the parser for this format,
* otherwise it will throw an exception.
*
* When the files are parsed successfully, the parsed ModelType and Model
* can be obtained via getType() and getModel<ModelClass>().
*/
class AutoParser : Parser {
public:
AutoParser(std::string const & transitionSystemFile, std::string const & labelingFile,
std::string const & stateRewardFile = "", std::string const & transitionRewardFile = "");
/*!
* @brief Returns the type of model that was parsed.
*/
storm::models::ModelType getType() {
if (this->model) return this->model->getType();
else return storm::models::Unknown;
}
/*!
* @brief Returns the model with the given type.
*/
template <typename Model>
std::shared_ptr<Model> getModel() {
return this->model->as<Model>();
}
private:
/*!
* @brief Open file and read file format hint.
*/
storm::models::ModelType analyzeHint(const std::string& filename);
/*!
* @brief Pointer to a parser that has parsed the given transition system.
*/
std::shared_ptr<storm::models::AbstractModel> model;
};
} // namespace parser
} // namespace storm
#endif /* STORM_PARSER_AUTOPARSER_H_ */

80
src/parser/AutoTransitionParser.cpp

@ -1,80 +0,0 @@
#include "src/parser/AutoTransitionParser.h"
#include "src/exceptions/WrongFileFormatException.h"
#include "DeterministicSparseTransitionParser.h"
#include "NonDeterministicSparseTransitionParser.h"
namespace storm {
namespace parser {
AutoTransitionParser::AutoTransitionParser(const std::string& filename)
: type(Unknown) {
TransitionType name = this->analyzeFilename(filename);
std::pair<TransitionType,TransitionType> content = this->analyzeContent(filename);
TransitionType hint = content.first, transitions = content.second;
if (hint == Unknown) {
if (name == transitions) this->type = name;
else {
LOG4CPLUS_ERROR(logger, "Could not determine file type of " << filename << ". Filename suggests " << name << " but transitions look like " << transitions);
LOG4CPLUS_ERROR(logger, "Please fix your file and try again.");
throw storm::exceptions::WrongFileFormatException() << "Could not determine type of file " << filename;
}
} else {
if ((hint == name) && (name == transitions)) this->type = name;
else if (hint == name) {
LOG4CPLUS_WARN(logger, "Transition format in file " << filename << " of type " << name << " look like " << transitions << " transitions.");
LOG4CPLUS_WARN(logger, "We will use the parser for " << name << " and hope for the best!");
this->type = name;
}
else if (hint == transitions) {
LOG4CPLUS_WARN(logger, "File extension of " << filename << " suggests type " << name << " but the content seems to be " << hint);
LOG4CPLUS_WARN(logger, "We will use the parser for " << hint << " and hope for the best!");
this->type = hint;
}
else if (name == transitions) {
LOG4CPLUS_WARN(logger, "File " << filename << " contains a hint that it is " << hint << " but filename and transition pattern suggests " << name);
LOG4CPLUS_WARN(logger, "We will use the parser for " << name << " and hope for the best!");
this->type = name;
}
else {
LOG4CPLUS_WARN(logger, "File " << filename << " contains a hint that it is " << hint << " but filename suggests " << name << " and transition pattern suggests " << transitions);
LOG4CPLUS_WARN(logger, "We will stick to the hint, use the parser for " << hint << " and hope for the best!");
this->type = hint;
}
}
// Do actual parsing
switch (this->type) {
case DTMC:
this->parser = new DeterministicSparseTransitionParser(filename);
break;
case NDTMC:
this->parser = new NonDeterministicSparseTransitionParser(filename);
break;
default: ; // Unknown
}
}
TransitionType AutoTransitionParser::analyzeFilename(const std::string& filename) {
TransitionType type = Unknown;
return type;
}
std::pair<TransitionType,TransitionType> AutoTransitionParser::analyzeContent(const std::string& filename) {
TransitionType hintType = Unknown, transType = Unknown;
// Open file
MappedFile file(filename.c_str());
//char* buf = file.data;
return std::pair<TransitionType,TransitionType>(hintType, transType);
}
} //namespace parser
} //namespace storm

88
src/parser/AutoTransitionParser.h

@ -1,88 +0,0 @@
#ifndef STORM_PARSER_AUTOPARSER_H_
#define STORM_PARSER_AUTOPARSER_H_
#include "src/models/AtomicPropositionsLabeling.h"
#include "boost/integer/integer_mask.hpp"
#include "src/parser/Parser.h"
#include <memory>
#include <iostream>
#include <utility>
namespace storm {
namespace parser {
/*!
* @brief Enumeration of all supported types of transition systems.
*/
enum TransitionType {
Unknown, DTMC, NDTMC
};
std::ostream& operator<<(std::ostream& os, const TransitionType type)
{
switch (type) {
case Unknown: os << "Unknown"; break;
case DTMC: os << "DTMC"; break;
case NDTMC: os << "NDTMC"; break;
default: os << "Invalid TransitionType";
}
return os;
}
/*!
* @brief Checks the given file and tries to call the correct parser.
*
* This parser analyzes the filename, an optional format hint (in the first
* line of the file) and the transitions within the file.
*
* If all three (or two, if the hint is not given) are consistent, it will
* call the appropriate parser.
* If two guesses are the same but the third one contradicts, it will issue
* a warning to the user and call the (hopefully) appropriate parser.
* If all guesses differ, but a format hint is given, it will issue a
* warning to the user and use the format hint to determine the correct
* parser.
* Otherwise, it will issue an error.
*/
class AutoTransitionParser : Parser {
public:
AutoTransitionParser(const std::string& filename);
/*!
* @brief Returns the type of transition system that was detected.
*/
TransitionType getTransitionType() {
return this->type;
}
// TODO: is this actually safe with shared_ptr?
template <typename T>
T* getParser() {
return dynamic_cast<T*>( this->parser );
}
~AutoTransitionParser() {
delete this->parser;
}
private:
TransitionType analyzeFilename(const std::string& filename);
std::pair<TransitionType,TransitionType> analyzeContent(const std::string& filename);
/*!
* @brief Type of the transition system.
*/
TransitionType type;
/*!
* @brief Pointer to a parser that has parsed the given transition system.
*/
Parser* parser;
};
} // namespace parser
} // namespace storm
#endif /* STORM_PARSER_AUTOPARSER_H_ */

164
src/parser/DeterministicSparseTransitionParser.cpp

@ -6,91 +6,101 @@
*/
#include "src/parser/DeterministicSparseTransitionParser.h"
#include "src/exceptions/FileIoException.h"
#include "src/exceptions/WrongFileFormatException.h"
#include "boost/integer/integer_mask.hpp"
#include <cstdlib>
#include <cstdio>
#include <cstring>
#include <clocale>
#include <iostream>
#include <errno.h>
#include <time.h>
#include <sys/stat.h>
#include <fcntl.h>
#include <locale.h>
#include <cstdlib>
#include <cstdio>
#include <cstring>
#include <clocale>
#include <iostream>
#include <string>
#include "src/exceptions/FileIoException.h"
#include "src/exceptions/WrongFileFormatException.h"
#include "boost/integer/integer_mask.hpp"
#include "src/utility/Settings.h"
#include "log4cplus/logger.h"
#include "log4cplus/loggingmacros.h"
extern log4cplus::Logger logger;
namespace storm {
namespace parser{
namespace parser {
/*!
* @brief Perform first pass through the file and obtain number of
* non-zero cells and maximum node id.
*
* This method does the first pass through the .tra file and computes
* the number of non-zero elements that are not diagonal elements,
* which correspondents to the number of transitions that are not
* self-loops.
* (Diagonal elements are treated in a special way).
* the number of non-zero elements.
* It also calculates the maximum node id and stores it in maxnode.
*
* @return The number of non-zero elements that are not on the diagonal
* @return The number of non-zero elements
* @param buf Data to scan. Is expected to be some char array.
* @param maxnode Is set to highest id of all nodes.
*/
uint_fast64_t DeterministicSparseTransitionParser::firstPass(char* buf, uint_fast64_t &maxnode) {
uint_fast64_t DeterministicSparseTransitionParser::firstPass(char* buf, uint_fast64_t& maxnode) {
uint_fast64_t non_zero = 0;
/*
* check file header and extract number of transitions
* Check file header and extract number of transitions.
*/
buf = strchr(buf, '\n') + 1; // skip format hint
if (strncmp(buf, "STATES ", 7) != 0) {
LOG4CPLUS_ERROR(logger, "Expected \"STATES\" but got \"" << std::string(buf, 0, 16) << "\".");
return 0;
}
buf += 7; // skip "STATES "
buf += 7; // skip "STATES "
if (strtol(buf, &buf, 10) == 0) return 0;
buf = trimWhitespaces(buf);
if (strncmp(buf, "TRANSITIONS ", 12) != 0) {
LOG4CPLUS_ERROR(logger, "Expected \"TRANSITIONS\" but got \"" << std::string(buf, 0, 16) << "\".");
return 0;
}
buf += 12; // skip "TRANSITIONS "
buf += 12; // skip "TRANSITIONS "
if ((non_zero = strtol(buf, &buf, 10)) == 0) return 0;
/*
* check all transitions for non-zero diagonal entrys
* Check all transitions for non-zero diagonal entrys.
*/
uint_fast64_t row, col;
uint_fast64_t row, lastrow = 0, col;
double val;
maxnode = 0;
char* tmp;
while (buf[0] != '\0') {
/*
* read row and column
* Read row and column.
*/
row = checked_strtol(buf, &buf);
col = checked_strtol(buf, &buf);
/*
* check if one is larger than the current maximum id
* Check if one is larger than the current maximum id.
*/
if (row > maxnode) maxnode = row;
if (col > maxnode) maxnode = col;
/*
* read value. if value is 0.0, either strtod could not read a number or we encountered a probability of zero.
* if row == col, we have a diagonal element which is treated separately and this non_zero must be decreased.
* Check if a node was skipped, i.e. if a node has no outgoing
* transitions. If so, increase non_zero, as the second pass will
* either throw an exception (in this case, it doesn't matter
* anyway) or add a self-loop (in this case, we'll need the
* additional transition).
*/
if (lastrow < row-1) non_zero += row - lastrow - 1;
lastrow = row;
/*
* Read probability of this transition.
* Check, if the value is a probability, i.e. if it is between 0 and 1.
*/
val = strtod(buf, &tmp);
if (val == 0.0) {
LOG4CPLUS_ERROR(logger, "Expected a positive probability but got \"" << std::string(buf, 0, 16) << "\".");
val = checked_strtod(buf, &buf);
if ((val < 0.0) || (val > 1.0)) {
LOG4CPLUS_ERROR(logger, "Expected a positive probability but got \"" << val << "\".");
return 0;
}
if (row == col) non_zero--;
buf = trimWhitespaces(tmp);
buf = trimWhitespaces(buf);
}
return non_zero;
@ -107,86 +117,102 @@ uint_fast64_t DeterministicSparseTransitionParser::firstPass(char* buf, uint_fas
*/
DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::string const &filename)
: matrix(nullptr)
{
: matrix(nullptr) {
/*
* enforce locale where decimal point is '.'
*/
setlocale( LC_NUMERIC, "C" );
* Enforce locale where decimal point is '.'.
*/
setlocale(LC_NUMERIC, "C");
/*
* open file
* Open file.
*/
MappedFile file(filename.c_str());
char* buf = file.data;
/*
* perform first pass, i.e. count entries that are not zero and not on the diagonal
* Perform first pass, i.e. count entries that are not zero.
*/
uint_fast64_t maxnode;
uint_fast64_t non_zero = this->firstPass(file.data, maxnode);
/*
* if first pass returned zero, the file format was wrong
* If first pass returned zero, the file format was wrong.
*/
if (non_zero == 0)
{
if (non_zero == 0) {
LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": erroneous file format.");
throw storm::exceptions::WrongFileFormatException();
}
/*
* perform second pass
* Perform second pass-
*
* from here on, we already know that the file header is correct
* From here on, we already know that the file header is correct.
*/
/*
* read file header, extract number of states
* Read file header, extract number of states.
*/
buf += 7; // skip "STATES "
buf = strchr(buf, '\n') + 1; // skip format hint
buf += 7; // skip "STATES "
checked_strtol(buf, &buf);
buf = trimWhitespaces(buf);
buf += 12; // skip "TRANSITIONS "
buf += 12; // skip "TRANSITIONS "
checked_strtol(buf, &buf);
/*
* Creating matrix
* Memory for diagonal elements is automatically allocated, hence only the number of non-diagonal
* non-zero elements has to be specified (which is non_zero, computed by make_first_pass)
* Creating matrix here.
* The number of non-zero elements is computed by firstPass().
*/
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));
if (this->matrix == NULL)
{
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) << ".");
throw std::bad_alloc();
}
this->matrix->initialize(non_zero);
uint_fast64_t row, col;
uint_fast64_t row, lastrow = 0, col;
double val;
bool fixDeadlocks = storm::settings::instance()->isSet("fix-deadlocks");
bool hadDeadlocks = false;
/*
* read all transitions from file
* Read all transitions from file. Note that we assume, that the
* transitions are listed in canonical order, otherwise this will not
* work, i.e. the values in the matrix will be at wrong places.
*/
while (buf[0] != '\0')
{
while (buf[0] != '\0') {
/*
* read row, col and value.
* Read row, col and value.
*/
row = checked_strtol(buf, &buf);
col = checked_strtol(buf, &buf);
val = strtod(buf, &buf);
this->matrix->addNextValue(row,col,val);
val = checked_strtod(buf, &buf);
/*
* Check if we skipped a node, i.e. if a node does not have any
* outgoing transitions.
*/
for (uint_fast64_t node = lastrow + 1; node < row; node++) {
hadDeadlocks = true;
if (fixDeadlocks) {
this->matrix->addNextValue(node, node, 1);
LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": node " << node << " has no outgoing transitions. A self-loop was inserted.");
} else {
LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": node " << node << " has no outgoing transitions.");
}
}
lastrow = row;
this->matrix->addNextValue(row, col, val);
buf = trimWhitespaces(buf);
}
if (!fixDeadlocks && hadDeadlocks) throw storm::exceptions::WrongFileFormatException() << "Some of the nodes had deadlocks. You can use --fix-deadlocks to insert self-loops on the fly.";
/*
* clean up
* Finalize Matrix.
*/
this->matrix->finalize();
}
} //namespace parser
} //namespace storm
} // namespace parser
} // namespace storm

6
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<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);

14
src/parser/DtmcParser.cpp

@ -5,10 +5,14 @@
* Author: thomas
*/
#include "DtmcParser.h"
#include "DeterministicSparseTransitionParser.h"
#include "AtomicPropositionLabelingParser.h"
#include "SparseStateRewardParser.h"
#include "src/parser/DtmcParser.h"
#include <string>
#include <vector>
#include "src/parser/DeterministicSparseTransitionParser.h"
#include "src/parser/AtomicPropositionLabelingParser.h"
#include "src/parser/SparseStateRewardParser.h"
namespace storm {
namespace parser {
@ -29,7 +33,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 != "") {

10
src/parser/DtmcParser.h

@ -5,11 +5,11 @@
* Author: thomas
*/
#ifndef DTMCPARSER_H_
#define DTMCPARSER_H_
#ifndef STORM_PARSER_DTMCPARSER_H_
#define STORM_PARSER_DTMCPARSER_H_
#include "Parser.h"
#include "models/Dtmc.h"
#include "src/parser/Parser.h"
#include "src/models/Dtmc.h"
namespace storm {
namespace parser {
@ -37,4 +37,4 @@ private:
} /* namespace parser */
} /* namespace storm */
#endif /* DTMCPARSER_H_ */
#endif /* STORM_PARSER_DTMCPARSER_H_ */

53
src/parser/MdpParser.cpp

@ -0,0 +1,53 @@
/*
* MdpParser.cpp
*
* Created on: 14.01.2013
* Author: Philipp Berger
*/
#include "src/parser/MdpParser.h"
#include <string>
#include <vector>
#include "src/parser/NonDeterministicSparseTransitionParser.h"
#include "src/parser/AtomicPropositionLabelingParser.h"
#include "src/parser/SparseStateRewardParser.h"
namespace storm {
namespace parser {
/*!
* Parses a transition file and a labeling file and produces a MDP out of them; a pointer to the mdp
* is saved in the field "mdp"
* Note that the labeling file may have at most as many nodes as the transition file!
*
* @param transitionSystemFile String containing the location of the transition file (....tra)
* @param labelingFile String containing the location of the labeling file (....lab)
* @param stateRewardFile String containing the location of the state reward file (...srew)
* @param transitionRewardFile String containing the location of the transition reward file (...trew)
*/
MdpParser::MdpParser(std::string const & transitionSystemFile, std::string const & labelingFile,
std::string const & stateRewardFile, std::string const & transitionRewardFile) {
storm::parser::NonDeterministicSparseTransitionParser tp(transitionSystemFile);
uint_fast64_t stateCount = tp.getMatrix()->getRowCount();
std::shared_ptr<std::vector<double>> stateRewards = nullptr;
std::shared_ptr<storm::storage::SparseMatrix<double>> transitionRewards = nullptr;
storm::parser::AtomicPropositionLabelingParser lp(stateCount, labelingFile);
if (stateRewardFile != "") {
storm::parser::SparseStateRewardParser srp(stateCount, stateRewardFile);
stateRewards = srp.getStateRewards();
}
if (transitionRewardFile != "") {
storm::parser::NonDeterministicSparseTransitionParser trp(transitionRewardFile);
transitionRewards = trp.getMatrix();
}
mdp = std::shared_ptr<storm::models::Mdp<double>>(new storm::models::Mdp<double>(tp.getMatrix(), lp.getLabeling(), stateRewards, transitionRewards));
}
} /* namespace parser */
} /* namespace storm */

40
src/parser/MdpParser.h

@ -0,0 +1,40 @@
/*
* MdpParser.h
*
* Created on: 14.01.2013
* Author: thomas
*/
#ifndef STORM_PARSER_MDPPARSER_H_
#define STORM_PARSER_MDPPARSER_H_
#include "src/parser/Parser.h"
#include "src/models/Mdp.h"
namespace storm {
namespace parser {
/*!
* @brief Load label and transition file and return initialized mdp object
*
* @Note This class creates a new Mdp object that can
* be accessed via getMdp(). However, it will not delete this object!
*
* @Note The labeling representation in the file may use at most as much nodes as are specified in the mdp.
*/
class MdpParser: public storm::parser::Parser {
public:
MdpParser(std::string const & transitionSystemFile, std::string const & labelingFile,
std::string const & stateRewardFile = "", std::string const & transitionRewardFile = "");
std::shared_ptr<storm::models::Mdp<double>> getMdp() {
return this->mdp;
}
private:
std::shared_ptr<storm::models::Mdp<double>> mdp;
};
} /* namespace parser */
} /* namespace storm */
#endif /* STORM_PARSER_MDPPARSER_H_ */

302
src/parser/NonDeterministicSparseTransitionParser.cpp

@ -6,106 +6,141 @@
*/
#include "src/parser/NonDeterministicSparseTransitionParser.h"
#include "src/exceptions/FileIoException.h"
#include "src/exceptions/WrongFileFormatException.h"
#include "boost/integer/integer_mask.hpp"
#include <cstdlib>
#include <cstdio>
#include <cstring>
#include <clocale>
#include <iostream>
#include <errno.h>
#include <time.h>
#include <sys/stat.h>
#include <fcntl.h>
#include <locale.h>
#include <cstdlib>
#include <cstdio>
#include <cstring>
#include <clocale>
#include <iostream>
#include <utility>
#include <string>
#include "src/utility/Settings.h"
#include "src/exceptions/FileIoException.h"
#include "src/exceptions/WrongFileFormatException.h"
#include "boost/integer/integer_mask.hpp"
#include "log4cplus/logger.h"
#include "log4cplus/loggingmacros.h"
extern log4cplus::Logger logger;
namespace storm {
namespace parser{
namespace parser {
/*!
* @brief Perform first pass through the file and obtain number of
* non-zero cells and maximum node id.
* @brief Perform first pass through the file and obtain overall number of
* choices, number of non-zero cells and maximum node id.
*
* This method does the first pass through the .tra file and computes
* the number of non-zero elements that are not diagonal elements,
* which correspondents to the number of transitions that are not
* self-loops.
* (Diagonal elements are treated in a special way).
* It also calculates the maximum node id and stores it in maxnode.
* It also stores the maximum number of nondeterministic choices for a
* single single node in maxchoices.
* This method does the first pass through the transition file.
*
* It computes the overall number of nondeterministic choices, i.e. the
* number of rows in the matrix that should be created.
* It also calculates the overall number of non-zero cells, i.e. the number
* of elements the matrix has to hold, and the maximum node id, i.e. the
* number of columns of the matrix.
*
* @return The number of non-zero elements that are not on the diagonal
* @param buf Data to scan. Is expected to be some char array.
* @param choices Overall number of choices.
* @param maxnode Is set to highest id of all nodes.
* @return The number of non-zero elements.
*/
std::unique_ptr<std::vector<uint_fast64_t>> NonDeterministicSparseTransitionParser::firstPass(char* buf, uint_fast64_t &maxnode, uint_fast64_t &maxchoice) {
std::unique_ptr<std::vector<uint_fast64_t>> non_zero = std::unique_ptr<std::vector<uint_fast64_t>>(new std::vector<uint_fast64_t>());
uint_fast64_t NonDeterministicSparseTransitionParser::firstPass(char* buf, uint_fast64_t& choices, uint_fast64_t& maxnode) {
/*
* check file header and extract number of transitions
* Check file header and extract number of transitions.
*/
buf = strchr(buf, '\n') + 1; // skip format hint
if (strncmp(buf, "STATES ", 7) != 0) {
LOG4CPLUS_ERROR(logger, "Expected \"STATES\" but got \"" << std::string(buf, 0, 16) << "\".");
return nullptr;
return 0;
}
buf += 7; // skip "STATES "
buf += 7; // skip "STATES "
if (strtol(buf, &buf, 10) == 0) return 0;
buf = trimWhitespaces(buf);
if (strncmp(buf, "TRANSITIONS ", 12) != 0) {
LOG4CPLUS_ERROR(logger, "Expected \"TRANSITIONS\" but got \"" << std::string(buf, 0, 16) << "\".");
return 0;
}
buf += 12; // skip "TRANSITIONS "
strtol(buf, &buf, 10);
buf += 12; // skip "TRANSITIONS "
/*
* check all transitions for non-zero diagonal entrys
* 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
* vlaue is wrong.
*/
uint_fast64_t row, col, ndchoice;
uint_fast64_t parsed_nonzero = strtol(buf, &buf, 10);
/*
* Read all transitions.
*/
uint_fast64_t source, target;
uint_fast64_t lastsource = 0;
uint_fast64_t nonzero = 0;
double val;
choices = 0;
maxnode = 0;
maxchoice = 0;
char* tmp;
while (buf[0] != '\0') {
/*
* read row and column
*/
row = checked_strtol(buf, &buf);
ndchoice = checked_strtol(buf, &buf);
col = checked_strtol(buf, &buf);
/*
* check if one is larger than the current maximum id
*/
if (row > maxnode) maxnode = row;
if (col > maxnode) maxnode = col;
/*
* check if nondeterministic choice is larger than current maximum
* Read source node.
* Check if current source node is larger than current maximum node id.
* Increase number of choices.
* Check if we have skipped any source node, i.e. if any node has no
* outgoing transitions. If so, increase nonzero (and
* parsed_nonzero).
*/
if (ndchoice > maxchoice)
{
maxchoice = ndchoice;
while (non_zero->size() < maxchoice) non_zero->push_back(0);
source = checked_strtol(buf, &buf);
if (source > maxnode) maxnode = source;
choices++;
if (source > lastsource + 1) {
nonzero += source - lastsource - 1;
parsed_nonzero += source - lastsource - 1;
}
lastsource = source;
buf = trimWhitespaces(buf); // Skip to name of choice
buf += strcspn(buf, " \t\n\r"); // Skip name of choice.
/*
* read value. if value is 0.0, either strtod could not read a number or we encountered a probability of zero.
* if row == col, we have a diagonal element which is treated separately and this non_zero must be decreased.
* Read all targets for this choice.
*/
val = strtod(buf, &tmp);
if (val == 0.0) {
LOG4CPLUS_ERROR(logger, "Expected a positive probability but got \"" << std::string(buf, 0, 16) << "\".");
return 0;
buf = trimWhitespaces(buf);
while (buf[0] == '*') {
buf++;
/*
* Read target node and transition value.
* Check if current target node is larger than current maximum node id.
* Check if the transition value is a valid probability.
*/
target = checked_strtol(buf, &buf);
if (target > maxnode) maxnode = target;
val = checked_strtod(buf, &buf);
if ((val < 0.0) || (val > 1.0)) {
LOG4CPLUS_ERROR(logger, "Expected a positive probability but got \"" << std::string(buf, 0, 16) << "\".");
return 0;
}
/*
* Increase number of non-zero values.
*/
nonzero++;
/*
* Proceed to beginning of next line.
*/
buf = trimWhitespaces(buf);
}
if (row != col) (*non_zero)[ndchoice-1]++;
buf = trimWhitespaces(tmp);
}
return non_zero;
/*
* 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;
}
@ -119,89 +154,144 @@ std::unique_ptr<std::vector<uint_fast64_t>> NonDeterministicSparseTransitionPars
*/
NonDeterministicSparseTransitionParser::NonDeterministicSparseTransitionParser(std::string const &filename)
: matrix(nullptr)
{
: matrix(nullptr) {
/*
* enforce locale where decimal point is '.'
*/
setlocale( LC_NUMERIC, "C" );
* Enforce locale where decimal point is '.'.
*/
setlocale(LC_NUMERIC, "C");
/*
* open file
* Open file.
*/
MappedFile file(filename.c_str());
char* buf = file.data;
/*
* perform first pass, i.e. count entries that are not zero and not on the diagonal
* Perform first pass, i.e. obtain number of columns, rows and non-zero elements.
*/
uint_fast64_t maxnode, maxchoices;
std::unique_ptr<std::vector<uint_fast64_t>> non_zero = this->firstPass(file.data, maxnode, maxchoices);
uint_fast64_t maxnode, choices;
uint_fast64_t nonzero = this->firstPass(file.data, choices, maxnode);
/*
* if first pass returned zero, the file format was wrong
* If first pass returned zero, the file format was wrong.
*/
if (non_zero == nullptr)
{
if (nonzero == 0) {
LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": erroneous file format.");
throw storm::exceptions::WrongFileFormatException();
}
/*
* perform second pass
* Perform second pass.
*
* from here on, we already know that the file header is correct
* From here on, we already know that the file header is correct.
*/
/*
* read file header, extract number of states
* Read file header, ignore values within.
*/
buf += 7; // skip "STATES "
buf = strchr(buf, '\n') + 1; // skip format hint
buf += 7; // skip "STATES "
checked_strtol(buf, &buf);
buf = trimWhitespaces(buf);
buf += 12; // skip "TRANSITIONS "
buf += 12; // skip "TRANSITIONS "
checked_strtol(buf, &buf);
/*
* Creating matrix
* Memory for diagonal elements is automatically allocated, hence only the number of non-diagonal
* non-zero elements has to be specified (which is non_zero, computed by make_first_pass)
* Create and initialize matrix.
* The matrix should have as many columns as we have nodes and as many rows as we have choices.
* Those two values, as well as the number of nonzero elements, was been calculated in the first run.
*/
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));
if (this->matrix == NULL)
{
LOG4CPLUS_ERROR(logger, "Could not create matrix of size " << (maxnode+1) << " x " << (maxnode+1) << ".");
LOG4CPLUS_INFO(logger, "Attempting to create matrix of size " << choices << " x " << (maxnode+1) << " with " << nonzero << " entries.");
this->matrix = std::shared_ptr<storm::storage::SparseMatrix<double>>(new storm::storage::SparseMatrix<double>(choices, maxnode + 1));
if (this->matrix == nullptr) {
LOG4CPLUS_ERROR(logger, "Could not create matrix of size " << choices << " x " << (maxnode+1) << ".");
throw std::bad_alloc();
}
// TODO: put stuff in matrix / matrices.
//this->matrix->initialize(*non_zero);
this->matrix->initialize(nonzero);
uint_fast64_t row, col, ndchoice;
/*
* Create row mapping.
*/
this->rowMapping = std::shared_ptr<RowMapping>(new RowMapping());
/*
* Parse file content.
*/
uint_fast64_t source, target, lastsource = 0;
uint_fast64_t curRow = 0;
std::string choice;
double val;
bool fixDeadlocks = storm::settings::instance()->isSet("fix-deadlocks");
bool hadDeadlocks = false;
/*
* read all transitions from file
* Read all transitions from file.
*/
while (buf[0] != '\0')
{
while (buf[0] != '\0') {
/*
* read row, col and value.
* Read source node and choice name.
*/
source = checked_strtol(buf, &buf);
buf = trimWhitespaces(buf); // Skip to name of choice
choice = std::string(buf, strcspn(buf, " \t\n\r"));
/*
* Check if we have skipped any source node, i.e. if any node has no
* outgoing transitions. If so, insert a self-loop.
* Also add self-loops to rowMapping.
*/
for (uint_fast64_t node = lastsource + 1; node < source; node++) {
hadDeadlocks = true;
if (fixDeadlocks) {
this->rowMapping->insert(RowMapping::value_type(curRow, std::pair<uint_fast64_t, std::string>(node, "")));
this->matrix->addNextValue(curRow, node, 1);
curRow++;
LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": node " << node << " has no outgoing transitions. A self-loop was inserted.");
} else {
LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": node " << node << " has no outgoing transitions.");
}
}
lastsource = source;
/*
* Add this source-choice pair to rowMapping.
*/
this->rowMapping->insert(RowMapping::value_type(curRow, std::pair<uint_fast64_t, std::string>(source, choice)));
/*
* Skip name of choice.
*/
buf += strcspn(buf, " \t\n\r");
/*
* Read all targets for this choice.
*/
row = checked_strtol(buf, &buf);
ndchoice = checked_strtol(buf, &buf);
col = checked_strtol(buf, &buf);
val = strtod(buf, &buf);
//this->matrix->addNextValue(row,col,val);
buf = trimWhitespaces(buf);
while (buf[0] == '*') {
buf++;
/*
* Read target node and transition value.
* Put it into the matrix.
*/
target = checked_strtol(buf, &buf);
val = checked_strtod(buf, &buf);
this->matrix->addNextValue(curRow, target, val);
/*
* Proceed to beginning of next line in file and next row in matrix.
*/
buf = trimWhitespaces(buf);
}
curRow++;
}
if (!fixDeadlocks && hadDeadlocks) throw storm::exceptions::WrongFileFormatException() << "Some of the nodes had deadlocks. You can use --fix-deadlocks to insert self-loops on the fly.";
/*
* clean up
* Finalize matrix.
*/
//this->matrix->finalize();
this->matrix->finalize();
}
} //namespace parser
} //namespace storm
} // namespace parser
} // namespace storm

16
src/parser/NonDeterministicSparseTransitionParser.h

@ -1,11 +1,13 @@
#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"
#include <boost/bimap.hpp>
#include <utility>
#include <memory>
#include <vector>
@ -20,14 +22,20 @@ class NonDeterministicSparseTransitionParser : public Parser {
public:
NonDeterministicSparseTransitionParser(std::string const &filename);
std::shared_ptr<storm::storage::SquareSparseMatrix<double>> getMatrix() {
inline std::shared_ptr<storm::storage::SparseMatrix<double>> getMatrix() const {
return this->matrix;
}
typedef boost::bimap<uint_fast64_t, std::pair<uint_fast64_t,std::string>> RowMapping;
inline std::shared_ptr<RowMapping> getRowMapping() const {
return this->rowMapping;
}
private:
std::shared_ptr<storm::storage::SquareSparseMatrix<double>> matrix;
std::shared_ptr<storm::storage::SparseMatrix<double>> matrix;
std::shared_ptr<RowMapping> rowMapping;
std::unique_ptr<std::vector<uint_fast64_t>> firstPass(char* buf, uint_fast64_t &maxnode, uint_fast64_t &maxchoice);
uint_fast64_t firstPass(char* buf, uint_fast64_t& choices, uint_fast64_t& maxnode);
};

38
src/parser/Parser.cpp

@ -2,6 +2,7 @@
#include <iostream>
#include <cstring>
#include <string>
#include "src/exceptions/FileIoException.h"
#include "src/exceptions/WrongFileFormatException.h"
@ -28,6 +29,24 @@ uint_fast64_t storm::parser::Parser::checked_strtol(const char* str, char** end)
return res;
}
/*!
* Calls strtod() internally and checks if the new pointer is different
* from the original one, i.e. if str != *end. If they are the same, a
* storm::exceptions::WrongFileFormatException will be thrown.
* @param str String to parse
* @param end New pointer will be written there
* @return Result of strtod()
*/
double storm::parser::Parser::checked_strtod(const char* str, char** end) {
double res = strtod(str, end);
if (str == *end) {
LOG4CPLUS_ERROR(logger, "Error while parsing floating point. Next input token is not a number.");
LOG4CPLUS_ERROR(logger, "\tUpcoming input is: \"" << std::string(str, 0, 16) << "\"");
throw storm::exceptions::WrongFileFormatException("Error while parsing floating point. Next input token is not a number.");
}
return res;
}
/*!
* Skips spaces, tabs, newlines and carriage returns. Returns pointer
* to first char that is not a whitespace.
@ -35,13 +54,10 @@ uint_fast64_t storm::parser::Parser::checked_strtol(const char* str, char** end)
* @return pointer to first non-whitespace character
*/
char* storm::parser::Parser::trimWhitespaces(char* buf) {
/*TODO: Maybe use memcpy to copy all the stuff from the first non-whitespace char
* to the position of the buffer, so we don't have to keep track of 2 pointers.
*/
while ((*buf == ' ') || (*buf == '\t') || (*buf == '\n') || (*buf == '\r')) buf++;
return buf;
}
/*!
* Will stat the given file, open it and map it to memory.
* If anything of this fails, an appropriate exception is raised
@ -68,9 +84,9 @@ storm::parser::MappedFile::MappedFile(const char* filename) {
LOG4CPLUS_ERROR(logger, "Error in open(" << filename << ").");
throw exceptions::FileIoException("storm::parser::MappedFile Error in open()");
}
this->data = (char*) mmap(NULL, this->st.st_size, PROT_READ, MAP_PRIVATE, this->file, 0);
if (this->data == (char*)-1) {
this->data = reinterpret_cast<char*>(mmap(NULL, this->st.st_size, PROT_READ, MAP_PRIVATE, this->file, 0));
if (this->data == reinterpret_cast<char*>(-1)) {
close(this->file);
LOG4CPLUS_ERROR(logger, "Error in mmap(" << filename << ").");
throw exceptions::FileIoException("storm::parser::MappedFile Error in mmap()");
@ -85,20 +101,20 @@ storm::parser::MappedFile::MappedFile(const char* filename) {
LOG4CPLUS_ERROR(logger, "Error in _stat(" << filename << ").");
throw exceptions::FileIoException("storm::parser::MappedFile Error in stat()");
}
this->file = CreateFileA(filename, GENERIC_READ, 0, NULL, OPEN_ALWAYS, FILE_ATTRIBUTE_NORMAL, NULL);
if (this->file == INVALID_HANDLE_VALUE) {
LOG4CPLUS_ERROR(logger, "Error in CreateFileA(" << filename << ").");
throw exceptions::FileIoException("storm::parser::MappedFile Error in CreateFileA()");
}
this->mapping = CreateFileMappingA(this->file, NULL, PAGE_READONLY, (DWORD)(st.st_size >> 32), (DWORD)st.st_size, NULL);
if (this->mapping == NULL) {
CloseHandle(this->file);
LOG4CPLUS_ERROR(logger, "Error in CreateFileMappingA(" << filename << ").");
throw exceptions::FileIoException("storm::parser::MappedFile Error in CreateFileMappingA()");
}
this->data = static_cast<char*>(MapViewOfFile(this->mapping, FILE_MAP_READ, 0, 0, this->st.st_size));
if (this->data == NULL) {
CloseHandle(this->mapping);
@ -109,7 +125,7 @@ storm::parser::MappedFile::MappedFile(const char* filename) {
this->dataend = this->data + this->st.st_size;
#endif
}
/*!
* Will unmap the data and close the file.
*/

5
src/parser/Parser.h

@ -102,6 +102,11 @@ namespace parser {
* @brief Parses integer and checks, if something has been parsed.
*/
uint_fast64_t checked_strtol(const char* str, char** end);
/*!
* @brief Parses floating point and checks, if something has been parsed.
*/
double checked_strtod(const char* str, char** end);
/*!
* @brief Skips common whitespaces in a string.

29
src/parser/SparseStateRewardParser.cpp

@ -6,21 +6,23 @@
*/
#include "src/parser/SparseStateRewardParser.h"
#include "src/exceptions/WrongFileFormatException.h"
#include "src/exceptions/FileIoException.h"
#include "src/utility/OsDetection.h"
#include <cstdlib>
#include <cstdio>
#include <cstring>
#include <clocale>
#include <iostream>
#include <errno.h>
#include <time.h>
#include <sys/stat.h>
#include <fcntl.h>
#include <locale.h>
#include <iostream>
#include <cstdlib>
#include <cstdio>
#include <cstring>
#include <string>
#include <vector>
#include <clocale>
#include "src/exceptions/WrongFileFormatException.h"
#include "src/exceptions/FileIoException.h"
#include "src/utility/OsDetection.h"
#include "log4cplus/logger.h"
#include "log4cplus/loggingmacros.h"
extern log4cplus::Logger logger;
@ -44,7 +46,7 @@ SparseStateRewardParser::SparseStateRewardParser(uint_fast64_t stateCount, std::
// Create state reward vector with given state count.
this->stateRewards = std::shared_ptr<std::vector<double>>(new std::vector<double>(stateCount));
{
// Now parse state reward assignments.
uint_fast64_t state;
@ -54,9 +56,9 @@ SparseStateRewardParser::SparseStateRewardParser(uint_fast64_t stateCount, std::
while (buf[0] != '\0') {
// Parse state number and reward value.
state = checked_strtol(buf, &buf);
reward = strtod(buf, &buf);
reward = checked_strtod(buf, &buf);
if (reward < 0.0) {
LOG4CPLUS_ERROR(logger, "Expected positive probability but got \"" << std::string(buf, 0, 16) << "\".");
LOG4CPLUS_ERROR(logger, "Expected positive reward value but got \"" << reward << "\".");
throw storm::exceptions::WrongFileFormatException() << "State reward file specifies illegal reward value.";
}
@ -67,6 +69,5 @@ SparseStateRewardParser::SparseStateRewardParser(uint_fast64_t stateCount, std::
}
}
} //namespace parser
} //namespace storm
} // namespace parser
} // namespace storm

16
src/storage/JacobiDecomposition.h

@ -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

488
src/storage/SquareSparseMatrix.h → src/storage/SparseMatrix.h

@ -1,10 +1,11 @@
#ifndef STORM_STORAGE_SQUARESPARSEMATRIX_H_
#define STORM_STORAGE_SQUARESPARSEMATRIX_H_
#ifndef STORM_STORAGE_SPARSEMATRIX_H_
#define STORM_STORAGE_SPARSEMATRIX_H_
#include <exception>
#include <new>
#include <algorithm>
#include <iostream>
#include <iterator>
#include "boost/integer/integer_mask.hpp"
#include "src/exceptions/InvalidStateException.h"
@ -31,13 +32,12 @@ namespace storm {
namespace storage {
/*!
* A sparse matrix class with a constant number of non-zero entries on the non-diagonal fields
* and a separate dense storage for the diagonal elements.
* A sparse matrix class with a constant number of non-zero entries.
* NOTE: Addressing *is* zero-based, so the valid range for getValue and addNextValue is 0..(rows - 1)
* 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,9 +73,25 @@ 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)
: rowCount(rows), nonZeroEntryCount(0), valueStorage(nullptr),
diagonalStorage(nullptr),columnIndications(nullptr), rowIndications(nullptr),
SparseMatrix(uint_fast64_t rows, uint_fast64_t cols)
: rowCount(rows), colCount(cols), nonZeroEntryCount(0),
internalStatus(MatrixStatus::UnInitialized), currentSize(0), lastRow(0) { }
/* Sadly, Delegate Constructors are not yet available with MSVC2012 */
//! Constructor
/*!
* Constructs a square sparse matrix object with the given number rows
* @param size The number of rows and cols in the matrix
*/ /*
SparseMatrix(uint_fast64_t size) : SparseMatrix(size, size) { }
*/
//! Constructor
/*!
* Constructs a square sparse matrix object with the given number rows
* @param size The number of rows and cols in the matrix
*/
SparseMatrix(uint_fast64_t size) : rowCount(size), colCount(size), nonZeroEntryCount(0),
internalStatus(MatrixStatus::UnInitialized), currentSize(0), lastRow(0) { }
//! Copy Constructor
@ -83,8 +99,8 @@ 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)
: rowCount(ssm.rowCount), nonZeroEntryCount(ssm.nonZeroEntryCount),
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.");
// Check whether copying the matrix is safe.
@ -98,24 +114,12 @@ public:
LOG4CPLUS_ERROR(logger, "Unable to allocate internal storage.");
throw std::bad_alloc();
} else {
// Now that all storages have been prepared, copy over all
// elements. Start by copying the elements of type value and
// copy them seperately in order to invoke copy their copy
// constructor. This may not be necessary, but it is safer to
// do so in any case.
for (uint_fast64_t i = 0; i < nonZeroEntryCount; ++i) {
// use T() to force use of the copy constructor for complex T types
valueStorage[i] = T(ssm.valueStorage[i]);
}
for (uint_fast64_t i = 0; i < rowCount; ++i) {
// use T() to force use of the copy constructor for complex T types
diagonalStorage[i] = T(ssm.diagonalStorage[i]);
}
std::copy(ssm.valueStorage.begin(), ssm.valueStorage.end(), std::back_inserter(valueStorage));
// The elements that are not of the value type but rather the
// index type may be copied directly.
std::copy(ssm.columnIndications, ssm.columnIndications + nonZeroEntryCount, columnIndications);
std::copy(ssm.rowIndications, ssm.rowIndications + rowCount + 1, rowIndications);
std::copy(ssm.columnIndications.begin(), ssm.columnIndications.end(), std::back_inserter(columnIndications));
std::copy(ssm.rowIndications.begin(), ssm.rowIndications.end(), std::back_inserter(rowIndications));
}
}
}
@ -124,20 +128,11 @@ public:
/*!
* Destructor. Performs deletion of the reserved storage arrays.
*/
~SquareSparseMatrix() {
~SparseMatrix() {
setState(MatrixStatus::UnInitialized);
if (valueStorage != nullptr) {
delete[] valueStorage;
}
if (columnIndications != nullptr) {
delete[] columnIndications;
}
if (rowIndications != nullptr) {
delete[] rowIndications;
}
if (diagonalStorage != nullptr) {
delete[] diagonalStorage;
}
valueStorage.resize(0);
columnIndications.resize(0);
rowIndications.resize(0);
}
/*!
@ -155,11 +150,11 @@ public:
triggerErrorState();
LOG4CPLUS_ERROR(logger, "Trying to initialize matrix that is not uninitialized.");
throw storm::exceptions::InvalidStateException("Trying to initialize matrix that is not uninitialized.");
} else if (rowCount == 0) {
} else if ((rowCount == 0) || (colCount == 0)) {
triggerErrorState();
LOG4CPLUS_ERROR(logger, "Trying to create initialize a matrix with 0 rows.");
throw storm::exceptions::InvalidArgumentException("Trying to create initialize a matrix with 0 rows.");
} else if (((rowCount * rowCount) - rowCount) < nonZeroEntries) {
LOG4CPLUS_ERROR(logger, "Trying to create initialize a matrix with 0 rows or 0 columns.");
throw storm::exceptions::InvalidArgumentException("Trying to create initialize a matrix with 0 rows or 0 columns.");
} else if ((rowCount * colCount) < nonZeroEntries) {
triggerErrorState();
LOG4CPLUS_ERROR(logger, "Trying to initialize a matrix with more non-zero entries than there can be.");
throw storm::exceptions::InvalidArgumentException("Trying to initialize a matrix with more non-zero entries than there can be.");
@ -196,37 +191,72 @@ public:
throw storm::exceptions::InvalidArgumentException("Trying to initialize from an Eigen matrix that is not in compressed form.");
}
// Compute the actual (i.e. non-diagonal) number of non-zero entries.
nonZeroEntryCount = getEigenSparseMatrixCorrectNonZeroEntryCount(eigenSparseMatrix);
if (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 (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 _Index entryCount = eigenSparseMatrix.nonZeros();
nonZeroEntryCount = entryCount;
lastRow = 0;
// Try to prepare the internal storage and throw an error in case of
// failure.
if (!prepareInternalStorage()) {
triggerErrorState();
LOG4CPLUS_ERROR(logger, "Unable to allocate internal storage.");
throw std::bad_alloc();
} else {
// 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.
const _Index rowCount = eigenSparseMatrix.outerSize();
for (_Index row = 0; row < rowCount; ++row) {
for (_Index col = outerPtr[row]; col < outerPtr[row + 1]; ++col) {
addNextValue(row, indexPtr[col], valuePtr[col]);
}
// 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 ((eigenSparseMatrix.innerSize() > nonZeroEntryCount) || (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;
for (uint_fast64_t i = 0; i < entryCount; ++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 {
const _Index entryCount = eigenSparseMatrix.nonZeros();
// Because of the ColMajor format outerSize evaluates to the
// number of columns.
const _Index colCount = eigenSparseMatrix.outerSize();
@ -250,8 +280,7 @@ public:
// 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]]);
addNextValue(currentRow, currentColumn, valuePtr[positions[currentColumn]]);
// Remember that we found one more non-zero element.
++i;
// Mark this position as "used".
@ -268,8 +297,8 @@ public:
}
delete[] positions;
}
setState(MatrixStatus::Initialized);
}
setState(MatrixStatus::Initialized);
}
/*!
@ -283,30 +312,27 @@ public:
void addNextValue(const uint_fast64_t row, const uint_fast64_t col, const T& value) {
// Check whether the given row and column positions are valid and throw
// error otherwise.
if ((row > rowCount) || (col > rowCount)) {
if ((row > rowCount) || (col > colCount)) {
triggerErrorState();
LOG4CPLUS_ERROR(logger, "Trying to add a value at illegal position (" << row << ", " << col << ").");
throw storm::exceptions::OutOfRangeException("Trying to add a value at illegal position.");
}
if (row == col) { // Set a diagonal element.
diagonalStorage[row] = value;
} else { // Set a non-diagonal element.
// If we switched to another row, we have to adjust the missing
// entries in the row_indications array.
if (row != lastRow) {
for (uint_fast64_t i = lastRow + 1; i <= row; ++i) {
rowIndications[i] = currentSize;
}
lastRow = row;
// If we switched to another row, we have to adjust the missing
// entries in the row_indications array.
if (row != lastRow) {
for (uint_fast64_t i = lastRow + 1; i <= row; ++i) {
rowIndications[i] = currentSize;
}
lastRow = row;
}
// Finally, set the element and increase the current size.
valueStorage[currentSize] = value;
columnIndications[currentSize] = col;
// Finally, set the element and increase the current size.
valueStorage[currentSize] = value;
columnIndications[currentSize] = col;
++currentSize;
}
++currentSize;
}
/*
@ -355,18 +381,12 @@ public:
*/
inline bool getValue(uint_fast64_t row, uint_fast64_t col, T* const target) const {
// Check for illegal access indices.
if ((row > rowCount) || (col > rowCount)) {
if ((row > rowCount) || (col > colCount)) {
LOG4CPLUS_ERROR(logger, "Trying to read a value from illegal position (" << row << ", " << col << ").");
throw storm::exceptions::OutOfRangeException("Trying to read a value from illegal position.");
return false;
}
// Read elements on the diagonal directly.
if (row == col) {
*target = diagonalStorage[row];
return true;
}
// In case the element is not on the diagonal, we have to iterate
// over the accessed row to find the element.
uint_fast64_t rowStart = rowIndications[row];
@ -405,17 +425,12 @@ public:
*/
inline T& getValue(uint_fast64_t row, uint_fast64_t col) {
// Check for illegal access indices.
if ((row > rowCount) || (col > rowCount)) {
if ((row > rowCount) || (col > colCount)) {
LOG4CPLUS_ERROR(logger, "Trying to read a value from illegal position (" << row << ", " << col << ").");
throw storm::exceptions::OutOfRangeException("Trying to read a value from illegal position.");
}
// Read elements on the diagonal directly.
if (row == col) {
return diagonalStorage[row];
}
// In case the element is not on the diagonal, we have to iterate
// we have to iterate
// over the accessed row to find the element.
uint_fast64_t rowStart = rowIndications[row];
uint_fast64_t rowEnd = rowIndications[row + 1];
@ -445,20 +460,18 @@ public:
}
/*!
* Returns a pointer to the value storage of the matrix. This storage does
* *not* include elements on the diagonal.
* @return A pointer to the value storage of the matrix.
* Returns the number of columns of the matrix.
*/
T* getStoragePointer() const {
return valueStorage;
uint_fast64_t getColumnCount() const {
return colCount;
}
/*!
* Returns a pointer to the storage of elements on the diagonal.
* @return A pointer to the storage of elements on the diagonal.
* Returns a pointer to the value storage of the matrix.
* @return A pointer to the value storage of the matrix.
*/
T* getDiagonalStoragePointer() const {
return diagonalStorage;
std::vector<T> const & getStoragePointer() const {
return valueStorage;
}
/*!
@ -467,17 +480,17 @@ public:
* @return A pointer to the array that stores the start indices of non-zero
* entries in the value storage for each row.
*/
uint_fast64_t* getRowIndicationsPointer() const {
std::vector<uint_fast64_t> const & getRowIndicationsPointer() const {
return rowIndications;
}
/*!
* Returns a pointer to an array that stores the column of each non-zero
* element that is not on the diagonal.
* element.
* @return A pointer to an array that stores the column of each non-zero
* element that is not on the diagonal.
* element.
*/
uint_fast64_t* getColumnIndicationsPointer() const {
std::vector<uint_fast64_t> const & getColumnIndicationsPointer() const {
return columnIndications;
}
@ -548,10 +561,6 @@ public:
#define STORM_USE_TRIPLETCONVERT
# ifdef STORM_USE_TRIPLETCONVERT
// FIXME: Wouldn't it be more efficient to add the elements in
// order including the diagonal elements? Otherwise, Eigen has to
// perform some sorting.
// Prepare the triplet storage.
typedef Eigen::Triplet<T> IntTriplet;
std::vector<IntTriplet> tripletList;
@ -572,12 +581,6 @@ public:
}
}
// Then add the elements on the diagonal.
for (uint_fast64_t i = 0; i < rowCount; ++i) {
if (diagonalStorage[i] == 0) zeroCount++;
tripletList.push_back(IntTriplet(static_cast<int_fast32_t>(i), static_cast<int_fast32_t>(i), diagonalStorage[i]));
}
// Let Eigen create a matrix from the given list of triplets.
mat->setFromTriplets(tripletList.begin(), tripletList.end());
@ -596,10 +599,6 @@ public:
rowStart = rowIndications[row];
rowEnd = rowIndications[row + 1];
// Insert the element on the diagonal.
mat->insert(row, row) = diagonalStorage[row];
count++;
// Insert the elements that are not on the diagonal
while (rowStart < rowEnd) {
mat->insert(row, columnIndications[rowStart]) = valueStorage[rowStart];
@ -628,19 +627,6 @@ public:
return nonZeroEntryCount;
}
/*!
* Returns the number of non-zero entries on the diagonal.
* @return The number of non-zero entries on the diagonal.
*/
uint_fast64_t getDiagonalNonZeroEntryCount() const {
uint_fast64_t result = 0;
T zero(0);
for (uint_fast64_t i = 0; i < rowCount; ++i) {
if (diagonalStorage[i] != zero) ++result;
}
return result;
}
/*!
* This function makes the rows given by the bit vector absorbing.
* @param rows A bit vector indicating which rows to make absorbing.
@ -658,7 +644,7 @@ public:
/*!
* This function makes the given row absorbing. This means that all
* entries in will be set to 0 and the value 1 will be written
* to the element on the diagonal.
* to the element on the (pseudo-) diagonal.
* @param row The row to be made absorbing.
* @returns True iff the operation was successful.
*/
@ -675,13 +661,31 @@ public:
uint_fast64_t rowStart = rowIndications[row];
uint_fast64_t rowEnd = rowIndications[row + 1];
if (rowStart >= rowEnd) {
LOG4CPLUS_ERROR(logger, "The row " << row << " can not be made absorbing, no state in row, would have to recreate matrix!");
throw storm::exceptions::InvalidStateException("A row can not be made absorbing, no state in row, would have to recreate matrix!");
}
uint_fast64_t pseudoDiagonal = row % colCount;
bool foundDiagonal = false;
while (rowStart < rowEnd) {
valueStorage[rowStart] = storm::utility::constGetZero<T>();
if (!foundDiagonal && columnIndications[rowStart] >= pseudoDiagonal) {
foundDiagonal = true;
// insert/replace the diagonal entry
columnIndications[rowStart] = pseudoDiagonal;
valueStorage[rowStart] = storm::utility::constGetOne<T>();
} else {
valueStorage[rowStart] = storm::utility::constGetZero<T>();
}
++rowStart;
}
// Set the element on the diagonal to one.
diagonalStorage[row] = storm::utility::constGetOne<T>();
if (!foundDiagonal) {
--rowStart;
columnIndications[rowStart] = pseudoDiagonal;
valueStorage[rowStart] = storm::utility::constGetOne<T>();
}
return true;
}
@ -724,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.
@ -745,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
@ -763,8 +767,6 @@ public:
// Copy over selected entries.
uint_fast64_t rowCount = 0;
for (auto rowIndex : constraint) {
result->addNextValue(rowCount, rowCount, diagonalStorage[rowIndex]);
for (uint_fast64_t i = rowIndications[rowIndex]; i < rowIndications[rowIndex + 1]; ++i) {
if (constraint.get(columnIndications[i])) {
result->addNextValue(rowCount, bitsSetBeforeIndex[columnIndications[i]], valueStorage[i]);
@ -793,9 +795,20 @@ public:
* value.
*/
void invertDiagonal() {
if (this->getRowCount() != this->getColumnCount()) {
throw storm::exceptions::InvalidArgumentException() << "SparseMatrix::invertDiagonal requires the Matrix to be square!";
}
T one(1);
for (uint_fast64_t i = 0; i < rowCount; ++i) {
diagonalStorage[i] = one - diagonalStorage[i];
for (uint_fast64_t row = 0; row < rowCount; ++row) {
uint_fast64_t rowStart = rowIndications[row];
uint_fast64_t rowEnd = rowIndications[row + 1];
while (rowStart < rowEnd) {
if (columnIndications[rowStart] == row) {
valueStorage[rowStart] = one - valueStorage[rowStart];
break;
}
++rowStart;
}
}
}
@ -803,8 +816,18 @@ public:
* Negates all non-zero elements that are not on the diagonal.
*/
void negateAllNonDiagonalElements() {
for (uint_fast64_t i = 0; i < nonZeroEntryCount; ++i) {
valueStorage[i] = - valueStorage[i];
if (this->getRowCount() != this->getColumnCount()) {
throw storm::exceptions::InvalidArgumentException() << "SparseMatrix::invertDiagonal requires the Matrix to be square!";
}
for (uint_fast64_t row = 0; row < rowCount; ++row) {
uint_fast64_t rowStart = rowIndications[row];
uint_fast64_t rowEnd = rowIndications[row + 1];
while (rowStart < rowEnd) {
if (columnIndications[rowStart] != row) {
valueStorage[rowStart] = - valueStorage[rowStart];
}
++rowStart;
}
}
}
@ -814,8 +837,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
@ -836,7 +859,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);
@ -844,7 +867,6 @@ public:
// in case the given matrix does not have a non-zero element at this column position, or
// multiply the two entries and add the result to the corresponding position in the vector.
for (uint_fast64_t row = 0; row < rowCount && row < otherMatrix.rowCount; ++row) {
(*result)[row] += diagonalStorage[row] * otherMatrix.diagonalStorage[row];
for (uint_fast64_t element = rowIndications[row], nextOtherElement = otherMatrix.rowIndications[row]; element < rowIndications[row + 1] && nextOtherElement < otherMatrix.rowIndications[row + 1]; ++element) {
if (columnIndications[element] < otherMatrix.columnIndications[nextOtherElement]) {
continue;
@ -868,25 +890,23 @@ public:
uint_fast64_t getSizeInMemory() const {
uint_fast64_t size = sizeof(*this);
// Add value_storage size.
size += sizeof(T) * nonZeroEntryCount;
// Add diagonal_storage size.
size += sizeof(T) * (rowCount + 1);
size += sizeof(T) * valueStorage.capacity();
// Add column_indications size.
size += sizeof(uint_fast64_t) * nonZeroEntryCount;
size += sizeof(uint_fast64_t) * columnIndications.capacity();
// Add row_indications size.
size += sizeof(uint_fast64_t) * (rowCount + 1);
size += sizeof(uint_fast64_t) * rowIndications.capacity();
return size;
}
/*!
* Returns an iterator to the columns of the non-zero entries of the given
* row that are not on the diagonal.
* row.
* @param row The row whose columns the iterator will return.
* @return An iterator to the columns of the non-zero entries of the given
* row that are not on the diagonal.
* row.
*/
constIndexIterator beginConstColumnNoDiagIterator(uint_fast64_t row) const {
return this->columnIndications + this->rowIndications[row];
constIndexIterator beginConstColumnIterator(uint_fast64_t row) const {
return &(this->columnIndications[0]) + this->rowIndications[row];
}
/*!
@ -894,18 +914,18 @@ public:
* @param row The row for which the iterator should point to the past-the-end
* element.
*/
constIndexIterator endConstColumnNoDiagIterator(uint_fast64_t row) const {
return this->columnIndications + this->rowIndications[row + 1];
constIndexIterator endConstColumnIterator(uint_fast64_t row) const {
return &(this->columnIndications[0]) + this->rowIndications[row + 1];
}
/*!
* Returns an iterator over the elements of the given row. The iterator
* will include neither the diagonal element nor zero entries.
* will include no zero entries.
* @param row The row whose elements the iterator will return.
* @return An iterator over the elements of the given row.
*/
constIterator beginConstNoDiagIterator(uint_fast64_t row) const {
return this->valueStorage + this->rowIndications[row];
constIterator beginConstIterator(uint_fast64_t row) const {
return &(this->valueStorage[0]) + this->rowIndications[row];
}
/*!
* Returns an iterator pointing to the first element after the given
@ -914,32 +934,28 @@ public:
* past-the-end element.
* @return An iterator to the element after the given row.
*/
constIterator endConstNoDiagIterator(uint_fast64_t row) const {
return this->valueStorage + this->rowIndications[row + 1];
constIterator endConstIterator(uint_fast64_t row) const {
return &(this->valueStorage[0]) + this->rowIndications[row + 1];
}
/*!
* @brief Calculate sum of all entries in given row.
*
* Adds up all values in the given row (including the diagonal value)
* Adds up all values in the given row
* and returns the sum.
* @param row The row that should be added up.
* @return Sum of the row.
*/
T getRowSum(uint_fast64_t row) const {
T sum = this->diagonalStorage[row];
for (auto it = this->beginConstNoDiagIterator(row); it != this->endConstNoDiagIterator(row); it++) {
T sum = storm::utility::constGetZero<T>();
for (auto it = this->beginConstIterator(row); it != this->endConstIterator(row); it++) {
sum += *it;
}
return sum;
}
void print() const {
std::cout << "diag: --------------------------------" << std::endl;
for (uint_fast64_t i = 0; i < rowCount; ++i) {
std::cout << "(" << i << "," << i << ") = " << diagonalStorage[i] << std::endl;
}
std::cout << "non diag: ----------------------------" << std::endl;
std::cout << "entries: ----------------------------" << std::endl;
for (uint_fast64_t i = 0; i < rowCount; ++i) {
for (uint_fast64_t j = rowIndications[i]; j < rowIndications[i + 1]; ++j) {
std::cout << "(" << i << "," << columnIndications[j] << ") = " << valueStorage[j] << std::endl;
@ -955,31 +971,31 @@ private:
uint_fast64_t rowCount;
/*!
* The number of non-zero elements that are not on the diagonal.
* The number of columns of the matrix.
*/
uint_fast64_t nonZeroEntryCount;
uint_fast64_t colCount;
/*!
* Stores all non-zero values that are not on the diagonal.
* The number of non-zero elements.
*/
T* valueStorage;
uint_fast64_t nonZeroEntryCount;
/*!
* Stores all elements on the diagonal, even the ones that are zero.
* Stores all non-zero values.
*/
T* diagonalStorage;
std::vector<T> valueStorage;
/*!
* Stores the column for each non-zero element that is not on the diagonal.
* Stores the column for each non-zero element.
*/
uint_fast64_t* columnIndications;
std::vector<uint_fast64_t> columnIndications;
/*!
* Array containing the boundaries (indices) in the value_storage array
* Vector containing the boundaries (indices) in the value_storage array
* for each row. All elements of value_storage with indices between the
* i-th and the (i+1)-st element of this array belong to row i.
*/
uint_fast64_t* rowIndications;
std::vector<uint_fast64_t> rowIndications;
/*!
* The internal status of the matrix.
@ -1017,24 +1033,37 @@ private:
/*!
* Prepares the internal CSR storage. For this, it requires
* non_zero_entry_count and row_count to be set correctly.
* @param alsoPerformAllocation If set to true, all entries are pre-allocated. This is the default.
* @return True on success, false otherwise (allocation failed).
*/
bool prepareInternalStorage() {
// Set up the arrays for the elements that are not on the diagonal.
valueStorage = new (std::nothrow) T[nonZeroEntryCount]();
columnIndications = new (std::nothrow) uint_fast64_t[nonZeroEntryCount]();
// Set up the row_indications array and reserve one element more than
// there are rows in order to put a sentinel element at the end,
// which eases iteration process.
rowIndications = new (std::nothrow) uint_fast64_t[rowCount + 1]();
// Set up the array for the elements on the diagonal.
diagonalStorage = new (std::nothrow) T[rowCount]();
bool prepareInternalStorage(const bool alsoPerformAllocation) {
if (alsoPerformAllocation) {
// Set up the arrays for the elements that are not on the diagonal.
valueStorage.resize(nonZeroEntryCount, storm::utility::constGetZero<T>());
columnIndications.resize(nonZeroEntryCount, 0);
// Set up the row_indications vector and reserve one element more than
// there are rows in order to put a sentinel element at the end,
// which eases iteration process.
rowIndications.resize(rowCount + 1, 0);
// Return whether all the allocations could be made without error.
return ((valueStorage.capacity() >= nonZeroEntryCount) && (columnIndications.capacity() >= nonZeroEntryCount)
&& (rowIndications.capacity() >= (rowCount + 1)));
} else {
valueStorage.reserve(nonZeroEntryCount);
columnIndications.reserve(nonZeroEntryCount);
rowIndications.reserve(rowCount + 1);
return true;
}
}
// Return whether all the allocations could be made without error.
return ((valueStorage != NULL) && (columnIndications != NULL)
&& (rowIndications != NULL) && (diagonalStorage != NULL));
/*!
* Shorthand for prepareInternalStorage(true)
* @see prepareInternalStorage(const bool)
*/
bool prepareInternalStorage() {
return this->prepareInternalStorage(true);
}
/*!
@ -1060,57 +1089,10 @@ private:
return false;
}
/*!
* Helper function to determine the number of non-zero elements that are
* not on the diagonal of the given Eigen matrix.
* @param eigen_sparse_matrix The Eigen matrix to analyze.
* @return The number of non-zero elements that are not on the diagonal of
* the given Eigen matrix.
*/
template<typename _Scalar, int _Options, typename _Index>
_Index getEigenSparseMatrixCorrectNonZeroEntryCount(const Eigen::SparseMatrix<_Scalar, _Options, _Index>& eigen_sparse_matrix) const {
const _Index* indexPtr = eigen_sparse_matrix.innerIndexPtr();
const _Index* outerPtr = eigen_sparse_matrix.outerIndexPtr();
const _Index entryCount = eigen_sparse_matrix.nonZeros();
const _Index outerCount = eigen_sparse_matrix.outerSize();
uint_fast64_t diagNonZeros = 0;
// For RowMajor, row is the current row and col the column and for
// ColMajor, row is the current column and col the row, but this is
// not important as we are only looking for elements on the diagonal.
_Index innerStart = 0;
_Index innerEnd = 0;
_Index innerMid = 0;
for (_Index row = 0; row < outerCount; ++row) {
innerStart = outerPtr[row];
innerEnd = outerPtr[row + 1] - 1;
// Now use binary search (but defer equality detection).
while (innerStart < innerEnd) {
innerMid = innerStart + ((innerEnd - innerStart) / 2);
if (indexPtr[innerMid] < row) {
innerStart = innerMid + 1;
} else {
innerEnd = innerMid;
}
}
// Check whether we have found an element on the diagonal.
if ((innerStart == innerEnd) && (indexPtr[innerStart] == row)) {
++diagNonZeros;
}
}
return static_cast<_Index>(entryCount - diagNonZeros);
}
};
} // namespace storage
} // namespace storm
#endif // STORM_STORAGE_SQUARESPARSEMATRIX_H_
#endif // STORM_STORAGE_SPARSEMATRIX_H_

15
src/storm.cpp

@ -20,12 +20,12 @@
#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"
#include "src/parser/DtmcParser.h"
// #include "src/parser/PrctlParser.h"
#include "src/parser/AutoParser.h"
#include "src/parser/PrctlParser.h"
#include "src/solver/GraphAnalyzer.h"
#include "src/utility/Settings.h"
#include "src/formula/Formulas.h"
@ -219,10 +219,13 @@ void testCheckingSynchronousLeader(storm::models::Dtmc<double>& dtmc, uint_fast6
*/
void testChecking() {
storm::settings::Settings* s = storm::settings::instance();
storm::parser::DtmcParser dtmcParser(s->getString("trafile"), s->getString("labfile"), s->getString("staterew"), s->getString("transrew"));
std::shared_ptr<storm::models::Dtmc<double>> dtmc = dtmcParser.getDtmc();
storm::parser::AutoParser parser(s->getString("trafile"), s->getString("labfile"), s->getString("staterew"), s->getString("transrew"));
dtmc->printModelInformationToStream(std::cout);
if (parser.getType() == storm::models::DTMC) {
std::shared_ptr<storm::models::Dtmc<double>> dtmc = parser.getModel<storm::models::Dtmc<double>>();
dtmc->printModelInformationToStream(std::cout);
}
else std::cout << "Input is not DTMC" << std::endl;
// testCheckingDie(*dtmc);
// testCheckingCrowds(*dtmc);

6
src/utility/CommandLine.cpp

@ -8,13 +8,11 @@
#include <ostream>
namespace storm {
namespace utility {
void printSeparationLine(std::ostream& out) {
out << "------------------------------------------------------" << std::endl;
}
} // namespace utility
} // namespace storm
} // namespace utility
} // namespace storm

118
src/utility/IoUtility.cpp

@ -1,75 +1,71 @@
/*
* IoUtility.cpp
*
* Created on: 17.10.2012
* Author: Thomas Heinemann
*/
* IoUtility.cpp
*
* Created on: 17.10.2012
* Author: Thomas Heinemann
*/
#include "src/utility/IoUtility.h"
#include "src/parser/DeterministicSparseTransitionParser.h"
#include "src/parser/AtomicPropositionLabelingParser.h"
#include <fstream>
#include "src/parser/DeterministicSparseTransitionParser.h"
#include "src/parser/AtomicPropositionLabelingParser.h"
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());
double* diagonal_storage = matrix->getDiagonalStoragePointer();
std::ofstream file;
file.open(filename);
file << "digraph dtmc {\n";
//Specify the nodes and their labels
for (uint_fast64_t i = 1; i < dtmc.getNumberOfStates(); i++) {
file << "\t" << i << "[label=\"" << i << "\\n{";
char komma=' ';
std::set<std::string> propositions = dtmc.getPropositionsForState(i);
for(auto it = propositions.begin();
it != propositions.end();
it++) {
file << komma << *it;
komma=',';
}
file << " }\"];\n";
}
for (uint_fast64_t row = 0; row < dtmc.getNumberOfStates(); row++ ) {
//write diagonal entry/self loop first
if (diagonal_storage[row] != 0) {
file << "\t" << row << " -> " << row << " [label=" << diagonal_storage[row] <<"]\n";
}
//Then, iterate through the row and write each non-diagonal value into the file
for ( auto it = matrix->beginConstColumnNoDiagIterator(row);
it != matrix->endConstColumnNoDiagIterator(row);
it++) {
double value = 0;
matrix->getValue(row,*it,&value);
file << "\t" << row << " -> " << *it << " [label=" << value << "]\n";
}
}
file << "}\n";
file.close();
}
namespace utility {
//TODO: Should this stay here or be integrated in the new parser structure?
/*storm::models::Dtmc<double>* parseDTMC(std::string const &tra_file, std::string const &lab_file) {
storm::parser::DeterministicSparseTransitionParser tp(tra_file);
uint_fast64_t node_count = tp.getMatrix()->getRowCount();
void dtmcToDot(storm::models::Dtmc<double> const &dtmc, std::string filename) {
std::shared_ptr<storm::storage::SparseMatrix<double>> matrix(dtmc.getTransitionProbabilityMatrix());
std::ofstream file;
file.open(filename);
storm::parser::AtomicPropositionLabelingParser lp(node_count, lab_file);
file << "digraph dtmc {\n";
storm::models::Dtmc<double>* result = new storm::models::Dtmc<double>(tp.getMatrix(), lp.getLabeling());
return result;
}*/
//Specify the nodes and their labels
for (uint_fast64_t i = 1; i < dtmc.getNumberOfStates(); i++) {
file << "\t" << i << "[label=\"" << i << "\\n{";
char komma=' ';
std::set<std::string> propositions = dtmc.getPropositionsForState(i);
for(auto it = propositions.begin();
it != propositions.end();
it++) {
file << komma << *it;
komma=',';
}
}
file << " }\"];\n";
}
for (uint_fast64_t row = 0; row < dtmc.getNumberOfStates(); row++ ) {
//Then, iterate through the row and write each non-diagonal value into the file
for ( auto it = matrix->beginConstColumnIterator(row);
it != matrix->endConstColumnIterator(row);
it++) {
double value = 0;
matrix->getValue(row,*it,&value);
file << "\t" << row << " -> " << *it << " [label=" << value << "]\n";
}
}
file << "}\n";
file.close();
}
//TODO: Should this stay here or be integrated in the new parser structure?
/*storm::models::Dtmc<double>* parseDTMC(std::string const &tra_file, std::string const &lab_file) {
storm::parser::DeterministicSparseTransitionParser tp(tra_file);
uint_fast64_t node_count = tp.getMatrix()->getRowCount();
storm::parser::AtomicPropositionLabelingParser lp(node_count, lab_file);
storm::models::Dtmc<double>* result = new storm::models::Dtmc<double>(tp.getMatrix(), lp.getLabeling());
return result;
}*/
}
}

63
src/utility/Settings.cpp

@ -7,13 +7,17 @@
#include "src/utility/Settings.h"
#include "src/exceptions/BaseException.h"
#include <boost/algorithm/string/join.hpp>
#include <utility>
#include <map>
#include <string>
#include <list>
#include "src/exceptions/BaseException.h"
#include "log4cplus/logger.h"
#include "log4cplus/loggingmacros.h"
extern log4cplus::Logger logger;
#include <boost/algorithm/string/join.hpp>
namespace storm {
namespace settings {
@ -21,7 +25,7 @@ namespace settings {
namespace bpo = boost::program_options;
/*
* static initializers
* Static initializers.
*/
std::unique_ptr<bpo::options_description> storm::settings::Settings::desc = nullptr;
std::string storm::settings::Settings::binaryName = "";
@ -42,37 +46,37 @@ std::map< std::pair<std::string, std::string>, std::shared_ptr<bpo::options_desc
* @param argv should be argv passed to main function
* @param filename either nullptr or name of config file
*/
Settings::Settings(const int argc, const char* argv[], const char* filename) {
Settings::Settings(int const argc, char const * const argv[], char const * const filename) {
Settings::binaryName = std::string(argv[0]);
try {
// Initially fill description objects
// Initially fill description objects.
this->initDescriptions();
// Take care of positional arguments
// Take care of positional arguments.
Settings::positional.add("trafile", 1);
Settings::positional.add("labfile", 1);
// Check module triggers, add corresponding options
// Check module triggers, add corresponding options.
std::map< std::string, std::list< std::string > > options;
for (auto it : Settings::modules) {
options[it.first.first].push_back(it.first.second);
}
for (auto it : options) {
std::stringstream str;
str << "select " << it.first << " module (" << boost::algorithm::join(it.second, ", ") << ")";
Settings::desc->add_options()
(it.first.c_str(), bpo::value<std::string>()->default_value(it.second.front()), str.str().c_str())
;
}
// Perform first parse run
// Perform first parse run.
this->firstRun(argc, argv, filename);
// Buffer for items to be deleted
// Buffer for items to be deleted.
std::list< std::pair< std::string, std::string > > deleteQueue;
// Check module triggers
// Check module triggers.
for (auto it : Settings::modules) {
std::pair< std::string, std::string > trigger = it.first;
if (this->vm.count(trigger.first)) {
@ -83,17 +87,16 @@ Settings::Settings(const int argc, const char* argv[], const char* filename) {
}
}
for (auto it : deleteQueue) Settings::modules.erase(it);
// Stop if help is set
// Stop if help is set.
if (this->vm.count("help") > 0) {
return;
}
// Perform second run
// Perform second run.
this->secondRun(argc, argv, filename);
// Finalize parsed options, check for specified requirements
// Finalize parsed options, check for specified requirements.
bpo::notify(this->vm);
LOG4CPLUS_DEBUG(logger, "Finished loading config.");
}
@ -117,7 +120,6 @@ Settings::Settings(const int argc, const char* argv[], const char* filename) {
/*!
* Initially fill options_description objects.
* First puts some generic options, then calls all register Callbacks.
*/
void Settings::initDescriptions() {
LOG4CPLUS_DEBUG(logger, "Initializing descriptions.");
@ -132,6 +134,7 @@ void Settings::initDescriptions() {
("labfile", bpo::value<std::string>()->required(), "name of the .lab file")
("transrew", bpo::value<std::string>()->default_value(""), "name of transition reward file")
("staterew", bpo::value<std::string>()->default_value(""), "name of state reward file")
("fix-deadlocks", "insert self-loops for states without outgoing transitions")
;
}
@ -140,13 +143,13 @@ void Settings::initDescriptions() {
* given), but allow for unregistered options, do not check requirements
* from options_description objects, do not check positional arguments.
*/
void Settings::firstRun(const int argc, const char* argv[], const char* filename) {
void Settings::firstRun(int const argc, char const * const argv[], char const * const filename) {
LOG4CPLUS_DEBUG(logger, "Performing first run.");
// parse command line
// Parse command line.
bpo::store(bpo::command_line_parser(argc, argv).options(*(Settings::desc)).allow_unregistered().run(), this->vm);
/*
* load config file if specified
* Load config file if specified.
*/
if (this->vm.count("configfile")) {
bpo::store(bpo::parse_config_file<char>(this->vm["configfile"].as<std::string>().c_str(), *(Settings::desc)), this->vm, true);
@ -160,12 +163,12 @@ void Settings::firstRun(const int argc, const char* argv[], const char* filename
* given) and check for unregistered options, requirements from
* options_description objects and positional arguments.
*/
void Settings::secondRun(const int argc, const char* argv[], const char* filename) {
void Settings::secondRun(int const argc, char const * const argv[], char const * const filename) {
LOG4CPLUS_DEBUG(logger, "Performing second run.");
// Parse command line
// Parse command line.
bpo::store(bpo::command_line_parser(argc, argv).options(*(Settings::desc)).positional(this->positional).run(), this->vm);
/*
* load config file if specified
* Load config file if specified.
*/
if (this->vm.count("configfile")) {
bpo::store(bpo::parse_config_file<char>(this->vm["configfile"].as<std::string>().c_str(), *(Settings::desc)), this->vm, true);
@ -191,5 +194,5 @@ std::ostream& help(std::ostream& os) {
return os;
}
} // namespace settings
} // namespace storm
} // namespace settings
} // namespace storm

26
src/utility/Settings.h

@ -51,7 +51,7 @@ namespace settings {
* @brief Get value of a generic option.
*/
template <typename T>
const T& get(const std::string &name) const {
inline const T& get( std::string const & name) const {
if (this->vm.count(name) == 0) throw storm::exceptions::InvalidSettingsException() << "Could not read option " << name << ".";
return this->vm[name].as<T>();
}
@ -59,14 +59,14 @@ namespace settings {
/*!
* @brief Get value of string option
*/
const std::string& getString(const std::string &name) const {
inline const std::string& getString(std::string const & name) const {
return this->get<std::string>(name);
}
/*!
* @brief Check if an option is set
*/
const bool isSet(const std::string &name) const {
inline const bool isSet(std::string const & name) const {
return this->vm.count(name) > 0;
}
@ -107,28 +107,28 @@ namespace settings {
*/
template <typename T>
static void registerModule() {
// get trigger
// Get trigger values.
std::pair< std::string, std::string > trigger = T::getOptionTrigger();
// build description name
// Build description name.
std::stringstream str;
str << "Options for " << T::getModuleName() << " (" << trigger.first << " = " << trigger.second << ")";
std::shared_ptr<bpo::options_description> desc = std::shared_ptr<bpo::options_description>(new bpo::options_description(str.str()));
// but options
// Put options into description.
T::putOptions(desc.get());
// store
// Store module.
Settings::modules[ trigger ] = desc;
}
friend std::ostream& help(std::ostream& os);
friend std::ostream& helpConfigfile(std::ostream& os);
friend Settings* instance();
friend Settings* newInstance(const int argc, const char* argv[], const char* filename);
friend Settings* newInstance(int const argc, char const * const argv[], char const * const filename);
private:
/*!
* @brief Constructor.
*/
Settings(const int argc, const char* argv[], const char* filename);
Settings(int const argc, char const * const argv[], char const * const filename);
/*!
* @brief Initialize options_description object.
@ -138,12 +138,12 @@ namespace settings {
/*!
* @brief Perform first parser run
*/
void firstRun(const int argc, const char* argv[], const char* filename);
void firstRun(int const argc, char const * const argv[], char const * const filename);
/*!
* @brief Perform second parser run.
*/
void secondRun(const int argc, const char* argv[], const char* filename);
void secondRun(int const argc, char const * const argv[], char const * const filename);
/*!
* @brief Option description for positional arguments on command line.
@ -197,10 +197,10 @@ namespace settings {
*
* @param argc should be argc passed to main function
* @param argv should be argv passed to main function
* @param filename either NULL or name of config file
* @param filename either NULL or name of config file
* @return The new instance of Settings.
*/
inline Settings* newInstance(const int argc, const char* argv[], const char* filename) {
inline Settings* newInstance(int const argc, char const * const argv[], char const * const filename) {
if (Settings::inst != nullptr) delete Settings::inst;
Settings::inst = new Settings(argc, argv, filename);
return Settings::inst;

183
src/vector/dense_vector.h

@ -0,0 +1,183 @@
#ifndef MRMC_VECTOR_BITVECTOR_H_
#define MRMC_VECTOR_BITVECTOR_H_
#include <exception>
#include <new>
#include <cmath>
#include "boost/integer/integer_mask.hpp"
#include <pantheios/pantheios.hpp>
#include <pantheios/inserters/integer.hpp>
#include "src/exceptions/invalid_state.h"
#include "src/exceptions/invalid_argument.h"
#include "src/exceptions/out_of_range.h"
namespace mrmc {
namespace vector {
//! A Vector
/*!
A bit vector for boolean fields or quick selection schemas on Matrix entries.
Does NOT perform index bound checks!
*/
template <class T>
class DenseVector {
public:
//! Constructor
/*!
\param initial_length The initial size of the boolean Array. Can be changed later on via BitVector::resize()
*/
BitVector(uint_fast64_t initial_length) {
bucket_count = initial_length / 64;
if (initial_length % 64 != 0) {
++bucket_count;
}
bucket_array = new uint_fast64_t[bucket_count]();
// init all 0
for (uint_fast64_t i = 0; i < bucket_count; ++i) {
bucket_array[i] = 0;
}
}
//! Copy Constructor
/*!
Copy Constructor. Creates an exact copy of the source bit vector bv. Modification of either bit vector does not affect the other.
@param bv A reference to the bit vector that should be copied from
*/
BitVector(const BitVector &bv) : bucket_count(bv.bucket_count)
{
pantheios::log_DEBUG("BitVector::CopyCTor: Using Copy() Ctor.");
bucket_array = new uint_fast64_t[bucket_count]();
memcpy(bucket_array, bv.bucket_array, sizeof(uint_fast64_t) * bucket_count);
}
~BitVector() {
if (bucket_array != NULL) {
delete[] bucket_array;
}
}
void resize(uint_fast64_t new_length) {
uint_fast64_t* tempArray = new uint_fast64_t[new_length]();
// 64 bit/entries per uint_fast64_t
uint_fast64_t copySize = (new_length <= (bucket_count * 64)) ? (new_length/64) : (bucket_count);
memcpy(tempArray, bucket_array, sizeof(uint_fast64_t) * copySize);
bucket_count = new_length / 64;
if (new_length % 64 != 0) {
++bucket_count;
}
delete[] bucket_array;
bucket_array = tempArray;
}
void set(const uint_fast64_t index, const bool value) {
uint_fast64_t bucket = index / 64;
// Taking the step with mask is crucial as we NEED a 64bit shift, not a 32bit one.
// MSVC: C4334, use 1i64 or cast to __int64.
// result of 32-bit shift implicitly converted to 64 bits (was 64-bit shift intended?)
uint_fast64_t mask = 1;
mask = mask << (index % 64);
if (value) {
bucket_array[bucket] |= mask;
} else {
bucket_array[bucket] &= ~mask;
}
}
bool get(const uint_fast64_t index) {
uint_fast64_t bucket = index / 64;
// Taking the step with mask is crucial as we NEED a 64bit shift, not a 32bit one.
// MSVC: C4334, use 1i64 or cast to __int64.
// result of 32-bit shift implicitly converted to 64 bits (was 64-bit shift intended?)
uint_fast64_t mask = 1;
mask = mask << (index % 64);
return ((bucket_array[bucket] & mask) == mask);
}
// Operators
BitVector operator &(BitVector const &bv) {
uint_fast64_t minSize = (bv.bucket_count < this->bucket_count) ? bv.bucket_count : this->bucket_count;
BitVector result(minSize * 64);
for (uint_fast64_t i = 0; i < minSize; ++i) {
result.bucket_array[i] = this->bucket_array[i] & bv.bucket_array[i];
}
return result;
}
BitVector operator |(BitVector const &bv) {
uint_fast64_t minSize = (bv.bucket_count < this->bucket_count) ? bv.bucket_count : this->bucket_count;
BitVector result(minSize * 64);
for (uint_fast64_t i = 0; i < minSize; ++i) {
result.bucket_array[i] = this->bucket_array[i] | bv.bucket_array[i];
}
return result;
}
BitVector operator ^(BitVector const &bv) {
uint_fast64_t minSize = (bv.bucket_count < this->bucket_count) ? bv.bucket_count : this->bucket_count;
BitVector result(minSize * 64);
for (uint_fast64_t i = 0; i < minSize; ++i) {
result.bucket_array[i] = this->bucket_array[i] ^ bv.bucket_array[i];
}
return result;
}
BitVector operator ~() {
BitVector result(this->bucket_count * 64);
for (uint_fast64_t i = 0; i < this->bucket_count; ++i) {
result.bucket_array[i] = ~this->bucket_array[i];
}
return result;
}
/*!
* Returns the number of bits that are set (to one) in this bit vector.
* @return The number of bits that are set (to one) in this bit vector.
*/
uint_fast64_t getNumberOfSetBits() {
uint_fast64_t set_bits = 0;
for (uint_fast64_t i = 0; i < bucket_count; i++) {
#ifdef __GNUG__ // check if we are using g++ and use built-in function if available
set_bits += __builtin_popcount (this->bucket_array[i]);
#else
uint_fast32_t cnt;
uint_fast64_t bitset = this->bucket_array[i];
for (cnt = 0; bitset; cnt++) {
bitset &= bitset - 1;
}
set_bits += cnt;
#endif
}
return set_bits;
}
/*!
* Returns the size of the bit vector in memory measured in bytes.
* @return The size of the bit vector in memory measured in bytes.
*/
uint_fast64_t getSizeInMemory() {
return sizeof(*this) + sizeof(uint_fast64_t) * bucket_count;
}
private:
uint_fast64_t bucket_count;
/*! Array containing the boolean bits for each node, 64bits/64nodes per element */
uint_fast64_t* bucket_array;
};
} // namespace vector
} // namespace mrmc
#endif // MRMC_SPARSE_STATIC_SPARSE_MATRIX_H_

32
test/parser/ParseMdpTest.cpp

@ -0,0 +1,32 @@
/*
* ParseMdpTest.cpp
*
* Created on: 14.01.2013
* Author: Thomas Heinemann
*/
#include "gtest/gtest.h"
#include "storm-config.h"
#include "src/parser/MdpParser.h"
#include "src/utility/IoUtility.h"
TEST(ParseMdpTest, parseAndOutput) {
storm::parser::MdpParser* mdpParser;
ASSERT_NO_THROW(mdpParser = new storm::parser::MdpParser(
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"));
std::shared_ptr<storm::models::Mdp<double>> mdp = mdpParser->getMdp();
std::shared_ptr<storm::storage::SparseMatrix<double>> matrix = mdp->getTransitionProbabilityMatrix();
ASSERT_EQ(mdp->getNumberOfStates(), 3);
ASSERT_EQ(mdp->getNumberOfTransitions(), 11);
ASSERT_EQ(matrix->getRowCount(), 2 * 3);
ASSERT_EQ(matrix->getColumnCount(), 3);
delete mdpParser;
}

8
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<storm::storage::SquareSparseMatrix<double>> result = parser->getMatrix();
std::shared_ptr<storm::storage::SparseMatrix<double>> result = parser->getMatrix();
if (result != NULL) {
double val = 0;
@ -53,13 +53,13 @@ TEST(ReadTraFileTest, ParseFileTest1) {
ASSERT_TRUE(result->getValue(3,2,&val));
ASSERT_EQ(val,0.0806451612903225806451612903225812);
ASSERT_TRUE(result->getValue(3,3,&val));
ASSERT_FALSE(result->getValue(3,3,&val));
ASSERT_EQ(val,0);
ASSERT_TRUE(result->getValue(3,4,&val));
ASSERT_EQ(val,0.080645161290322580645161290322581);
ASSERT_TRUE(result->getValue(4,4,&val));
ASSERT_FALSE(result->getValue(4,4,&val));
ASSERT_EQ(val,0);
delete parser;

120
test/storage/SquareSparseMatrixTest.cpp → 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<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) {
@ -116,24 +116,20 @@ TEST(SquareSparseMatrixTest, Test) {
for (int row = 15; row < 24; ++row) {
for (int col = 1; col <= 25; ++col) {
target = 1;
if (row != col) {
ASSERT_FALSE(ssm->getValue(row, col, &target));
} else {
ASSERT_TRUE(ssm->getValue(row, col, &target));
}
ASSERT_FALSE(ssm->getValue(row, col, &target));
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) {
@ -149,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) {
@ -162,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) {
@ -181,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) {
@ -194,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);
@ -231,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;
@ -243,17 +239,17 @@ 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);
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);
typedef Eigen::Triplet<int> IntTriplet;
std::vector<IntTriplet> tripletList;
tripletList.reserve(15);
tripletList.push_back(IntTriplet(1, 0, 0));
tripletList.push_back(IntTriplet(1, 0, 15));
tripletList.push_back(IntTriplet(1, 1, 1));
tripletList.push_back(IntTriplet(1, 2, 2));
tripletList.push_back(IntTriplet(1, 3, 3));
@ -280,38 +276,42 @@ 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();
const std::vector<int> valP = ssm->getStoragePointer();
int target = -1;
for (auto &coeff: tripletList) {
ASSERT_TRUE(ssm->getValue(coeff.row(), coeff.col(), &target));
bool retVal = ssm->getValue(coeff.row(), coeff.col(), &target);
ASSERT_TRUE(retVal);
ASSERT_EQ(target, coeff.value());
}
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 - 10));
ASSERT_EQ(ssm->getState(), storm::storage::SquareSparseMatrix<int>::MatrixStatus::Initialized);
ASSERT_NO_THROW(ssm->initialize(100));
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();

0
test/mrmc-tests.cpp → test/storm-tests.cpp

Loading…
Cancel
Save