Browse Source

Finished reworking the sparse matrix implementation. Adapted all other classes to the (partially) new API of the matrix.

Former-commit-id: 2c3b5a5bc3
main
dehnert 12 years ago
parent
commit
a26f63be30
  1. 66
      src/adapters/EigenAdapter.h
  2. 31
      src/adapters/ExplicitModelAdapter.h
  3. 10
      src/adapters/GmmxxAdapter.h
  4. 25
      src/adapters/StormAdapter.h
  5. 75
      src/counterexamples/MILPMinimalLabelSetGenerator.h
  6. 12
      src/counterexamples/PathBasedSubsystemGenerator.h
  7. 94
      src/counterexamples/SMTMinimalCommandSetGenerator.h
  8. 11
      src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h
  9. 7
      src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h
  10. 2
      src/modelchecker/prctl/SparseMdpPrctlModelChecker.h
  11. 19
      src/models/AbstractDeterministicModel.h
  12. 24
      src/models/AbstractModel.h
  13. 37
      src/models/AbstractNondeterministicModel.h
  14. 48
      src/models/Dtmc.h
  15. 42
      src/models/MarkovAutomaton.h
  16. 10
      src/models/Mdp.h
  17. 7
      src/parser/DeterministicSparseTransitionParser.cpp
  18. 3
      src/parser/MarkovAutomatonSparseTransitionParser.h
  19. 8
      src/parser/NondeterministicSparseTransitionParser.cpp
  20. 11
      src/solver/AbstractNondeterministicLinearEquationSolver.h
  21. 14
      src/storage/MaximalEndComponentDecomposition.cpp
  22. 332
      src/storage/SparseMatrix.cpp
  23. 20
      src/storage/SparseMatrix.h
  24. 4
      src/storage/StronglyConnectedComponentDecomposition.cpp
  25. 16
      src/utility/counterexamples.h
  26. 105
      src/utility/graph.h
  27. 6
      src/utility/matrix.h
  28. 17
      src/utility/vector.h
  29. 79
      test/functional/eigen/EigenSparseMatrixTest.cpp
  30. 1
      test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp
  31. 77
      test/functional/parser/ReadTraFileTest.cpp
  32. 386
      test/functional/storage/SparseMatrixTest.cpp
  33. 100
      test/functional/storage/adapters/EigenAdapterTest.cpp
  34. 111
      test/functional/storage/adapters/GmmAdapterTest.cpp
  35. 104
      test/functional/storage/adapters/StormAdapterTest.cpp
  36. BIN
      util/checklist/storage.ods

66
src/adapters/EigenAdapter.h

@ -1,66 +0,0 @@
/*
* EigenAdapter.h
*
* Created on: 21.01.2013
* Author: Philipp Berger
*/
#ifndef STORM_ADAPTERS_EIGENADAPTER_H_
#define STORM_ADAPTERS_EIGENADAPTER_H_
#include "src/storage/SparseMatrix.h"
#include "Eigen/Sparse"
#include "log4cplus/logger.h"
#include "log4cplus/loggingmacros.h"
#include "src/utility/OsDetection.h"
extern log4cplus::Logger logger;
namespace storm {
namespace adapters {
class EigenAdapter {
public:
/*!
* Converts a sparse matrix into the sparse matrix in the eigen format.
* @return A pointer to a row-major sparse matrix in eigen format.
*/
template<class T>
static Eigen::SparseMatrix<T, Eigen::RowMajor, int_fast32_t>* toEigenSparseMatrix(storm::storage::SparseMatrix<T> const& matrix) {
uint_fast64_t realNonZeros = matrix.getNonZeroEntryCount();
LOG4CPLUS_DEBUG(logger, "Converting matrix with " << realNonZeros << " non-zeros to Eigen format.");
// Prepare the resulting matrix.
Eigen::SparseMatrix<T, Eigen::RowMajor, int_fast32_t>* result = new Eigen::SparseMatrix<T, Eigen::RowMajor, int_fast32_t>(static_cast<int>(matrix.rowCount), static_cast<int>(matrix.colCount));
result->resizeNonZeros(static_cast<int>(realNonZeros));
//result->reserve(realNonZeros);
#ifdef WINDOWS
# pragma warning(push)
# pragma warning(disable: 4244) // possible loss of data
#endif
// Copy Row Indications
std::copy(matrix.rowIndications.begin(), matrix.rowIndications.end(), (result->outerIndexPtr()));
// Copy Columns Indications
std::copy(matrix.columnIndications.begin(), matrix.columnIndications.end(), (result->innerIndexPtr()));
// And do the same thing with the actual values.
std::copy(matrix.valueStorage.begin(), matrix.valueStorage.end(), (result->valuePtr()));
#ifdef WINDOWS
# pragma warning(pop)
#endif
LOG4CPLUS_DEBUG(logger, "Done converting matrix to Eigen format.");
return result;
}
};
} //namespace adapters
} //namespace storm
#endif /* STORM_ADAPTERS_EIGENADAPTER_H_ */

31
src/adapters/ExplicitModelAdapter.h

@ -480,10 +480,7 @@ namespace storm {
// requested and issue an error otherwise. // requested and issue an error otherwise.
if (totalNumberOfChoices == 0) { if (totalNumberOfChoices == 0) {
if (storm::settings::Settings::getInstance()->isSet("fixDeadlocks")) { if (storm::settings::Settings::getInstance()->isSet("fixDeadlocks")) {
transitionMatrix.insertNextValue(currentRow, currentState, storm::utility::constantOne<ValueType>(), true);
if (transitionRewards.size() > 0) {
transitionRewardMatrix.insertEmptyRow(true);
}
transitionMatrix.addNextValue(currentRow, currentState, storm::utility::constantOne<ValueType>());
++currentRow; ++currentRow;
} else { } else {
LOG4CPLUS_ERROR(logger, "Error while creating sparse matrix from probabilistic program: found deadlock state. For fixing these, please provide the appropriate option."); LOG4CPLUS_ERROR(logger, "Error while creating sparse matrix from probabilistic program: found deadlock state. For fixing these, please provide the appropriate option.");
@ -531,16 +528,14 @@ namespace storm {
choiceLabels.push_back(globalChoice.getChoiceLabels()); choiceLabels.push_back(globalChoice.getChoiceLabels());
for (auto const& stateProbabilityPair : globalChoice) { for (auto const& stateProbabilityPair : globalChoice) {
transitionMatrix.insertNextValue(currentRow, stateProbabilityPair.first, stateProbabilityPair.second, true);
transitionMatrix.addNextValue(currentRow, stateProbabilityPair.first, stateProbabilityPair.second);
} }
// Add all transition rewards to the matrix and add dummy entry if there is none. // Add all transition rewards to the matrix and add dummy entry if there is none.
if (stateToRewardMap.size() > 0) { if (stateToRewardMap.size() > 0) {
for (auto const& stateRewardPair : stateToRewardMap) { for (auto const& stateRewardPair : stateToRewardMap) {
transitionRewardMatrix.insertNextValue(currentRow, stateRewardPair.first, stateRewardPair.second, true);
transitionRewardMatrix.addNextValue(currentRow, stateRewardPair.first, stateRewardPair.second);
} }
} else if (transitionRewards.size() > 0) {
transitionRewardMatrix.insertEmptyRow(true);
} }
++currentRow; ++currentRow;
@ -554,7 +549,7 @@ namespace storm {
choiceLabels.emplace_back(std::move(choice.getChoiceLabels())); choiceLabels.emplace_back(std::move(choice.getChoiceLabels()));
for (auto const& stateProbabilityPair : choice) { for (auto const& stateProbabilityPair : choice) {
transitionMatrix.insertNextValue(currentRow, stateProbabilityPair.first, stateProbabilityPair.second, true);
transitionMatrix.addNextValue(currentRow, stateProbabilityPair.first, stateProbabilityPair.second);
// Now add all rewards that match this choice. // Now add all rewards that match this choice.
for (auto const& transitionReward : transitionRewards) { for (auto const& transitionReward : transitionRewards) {
@ -568,10 +563,8 @@ namespace storm {
// Add all transition rewards to the matrix and add dummy entry if there is none. // Add all transition rewards to the matrix and add dummy entry if there is none.
if (stateToRewardMap.size() > 0) { if (stateToRewardMap.size() > 0) {
for (auto const& stateRewardPair : stateToRewardMap) { for (auto const& stateRewardPair : stateToRewardMap) {
transitionRewardMatrix.insertNextValue(currentRow, stateRewardPair.first, stateRewardPair.second, true);
transitionRewardMatrix.addNextValue(currentRow, stateRewardPair.first, stateRewardPair.second);
} }
} else if (transitionRewards.size() > 0) {
transitionRewardMatrix.insertEmptyRow(true);
} }
++currentRow; ++currentRow;
@ -583,7 +576,7 @@ namespace storm {
choiceLabels.emplace_back(std::move(choice.getChoiceLabels())); choiceLabels.emplace_back(std::move(choice.getChoiceLabels()));
for (auto const& stateProbabilityPair : choice) { for (auto const& stateProbabilityPair : choice) {
transitionMatrix.insertNextValue(currentRow, stateProbabilityPair.first, stateProbabilityPair.second, true);
transitionMatrix.addNextValue(currentRow, stateProbabilityPair.first, stateProbabilityPair.second);
// Now add all rewards that match this choice. // Now add all rewards that match this choice.
for (auto const& transitionReward : transitionRewards) { for (auto const& transitionReward : transitionRewards) {
@ -597,10 +590,8 @@ namespace storm {
// Add all transition rewards to the matrix and add dummy entry if there is none. // Add all transition rewards to the matrix and add dummy entry if there is none.
if (stateToRewardMap.size() > 0) { if (stateToRewardMap.size() > 0) {
for (auto const& stateRewardPair : stateToRewardMap) { for (auto const& stateRewardPair : stateToRewardMap) {
transitionRewardMatrix.insertNextValue(currentRow, stateRewardPair.first, stateRewardPair.second, true);
transitionRewardMatrix.addNextValue(currentRow, stateRewardPair.first, stateRewardPair.second);
} }
} else if (transitionRewards.size() > 0) {
transitionRewardMatrix.insertEmptyRow(true);
} }
++currentRow; ++currentRow;
@ -629,10 +620,6 @@ namespace storm {
VariableInformation variableInformation = createVariableInformation(program); VariableInformation variableInformation = createVariableInformation(program);
// Initialize the matrices.
modelComponents.transitionMatrix.initialize();
modelComponents.transitionRewardMatrix.initialize();
// Create the structure for storing the reachable state space. // Create the structure for storing the reachable state space.
StateInformation stateInformation; StateInformation stateInformation;
@ -649,8 +636,8 @@ namespace storm {
modelComponents.choiceLabeling = std::move(nondeterministicChoiceIndicesAndChoiceLabelsPair.second); modelComponents.choiceLabeling = std::move(nondeterministicChoiceIndicesAndChoiceLabelsPair.second);
// Finalize the resulting matrices. // Finalize the resulting matrices.
modelComponents.transitionMatrix.finalize(true);
modelComponents.transitionRewardMatrix.finalize(true);
modelComponents.transitionMatrix.finalize();
modelComponents.transitionRewardMatrix.finalize();
// Now build the state labeling. // Now build the state labeling.
modelComponents.stateLabeling = buildStateLabeling(program, variableInformation, stateInformation); modelComponents.stateLabeling = buildStateLabeling(program, variableInformation, stateInformation);

10
src/adapters/GmmxxAdapter.h

@ -32,11 +32,11 @@ public:
*/ */
template<class T> template<class T>
static gmm::csr_matrix<T>* toGmmxxSparseMatrix(storm::storage::SparseMatrix<T> const& matrix) { static gmm::csr_matrix<T>* toGmmxxSparseMatrix(storm::storage::SparseMatrix<T> const& matrix) {
uint_fast64_t realNonZeros = matrix.getNonZeroEntryCount();
uint_fast64_t realNonZeros = matrix.getEntryCount();
LOG4CPLUS_DEBUG(logger, "Converting matrix with " << realNonZeros << " non-zeros to gmm++ format."); LOG4CPLUS_DEBUG(logger, "Converting matrix with " << realNonZeros << " non-zeros to gmm++ format.");
// Prepare the resulting matrix. // Prepare the resulting matrix.
gmm::csr_matrix<T>* result = new gmm::csr_matrix<T>(matrix.rowCount, matrix.colCount);
gmm::csr_matrix<T>* result = new gmm::csr_matrix<T>(matrix.rowCount, matrix.columnCount);
// Copy Row Indications // Copy Row Indications
std::copy(matrix.rowIndications.begin(), matrix.rowIndications.end(), result->jc.begin()); std::copy(matrix.rowIndications.begin(), matrix.rowIndications.end(), result->jc.begin());
@ -57,12 +57,12 @@ public:
* @return A pointer to a row-major sparse matrix in gmm++ format. * @return A pointer to a row-major sparse matrix in gmm++ format.
*/ */
template<class T> template<class T>
static gmm::csr_matrix<T>* toGmmxxSparseMatrix(storm::storage::SparseMatrix<T> && matrix) {
uint_fast64_t realNonZeros = matrix.getNonZeroEntryCount();
static gmm::csr_matrix<T>* toGmmxxSparseMatrix(storm::storage::SparseMatrix<T>&& matrix) {
uint_fast64_t realNonZeros = matrix.getEntryCount();
LOG4CPLUS_DEBUG(logger, "Converting matrix with " << realNonZeros << " non-zeros to gmm++ format."); LOG4CPLUS_DEBUG(logger, "Converting matrix with " << realNonZeros << " non-zeros to gmm++ format.");
// Prepare the resulting matrix. // Prepare the resulting matrix.
gmm::csr_matrix<T>* result = new gmm::csr_matrix<T>(matrix.rowCount, matrix.colCount);
gmm::csr_matrix<T>* result = new gmm::csr_matrix<T>(matrix.rowCount, matrix.columnCount);
typedef unsigned long long IND_TYPE; typedef unsigned long long IND_TYPE;
typedef std::vector<IND_TYPE> vectorType_ull_t; typedef std::vector<IND_TYPE> vectorType_ull_t;

25
src/adapters/StormAdapter.h

@ -33,30 +33,7 @@ public:
LOG4CPLUS_DEBUG(logger, "Converting matrix with " << realNonZeros << " non-zeros from gmm++ format into Storm."); LOG4CPLUS_DEBUG(logger, "Converting matrix with " << realNonZeros << " non-zeros from gmm++ format into Storm.");
// Prepare the resulting matrix. // Prepare the resulting matrix.
storm::storage::SparseMatrix<T>* result = new storm::storage::SparseMatrix<T>(matrix.nrows(), matrix.ncols());
// Set internal NonZero Counter
result->nonZeroEntryCount = realNonZeros;
result->setState(result->Initialized);
if (!result->prepareInternalStorage(false)) {
LOG4CPLUS_ERROR(logger, "Unable to allocate internal storage while converting GMM++ Matrix to Storm.");
delete result;
return nullptr;
} else {
// Copy Row Indications
std::copy(matrix.jc.begin(), matrix.jc.end(), std::back_inserter(result->rowIndications));
// Copy Columns Indications
std::copy(matrix.ir.begin(), matrix.ir.end(), std::back_inserter(result->columnIndications));
// And do the same thing with the actual values.
std::copy(matrix.pr.begin(), matrix.pr.end(), std::back_inserter(result->valueStorage));
result->currentSize = realNonZeros;
result->lastRow = matrix.nrows() - 1;
}
result->finalize();
storm::storage::SparseMatrix<T>* result = new storm::storage::SparseMatrix<T>(matrix.ncols(), matrix.jc, matrix.ir, matrix.pr);
LOG4CPLUS_DEBUG(logger, "Done converting matrix to storm format."); LOG4CPLUS_DEBUG(logger, "Done converting matrix to storm format.");

75
src/counterexamples/MILPMinimalLabelSetGenerator.h

@ -129,9 +129,9 @@ namespace storm {
for (uint_fast64_t row = nondeterministicChoiceIndices[state]; row < nondeterministicChoiceIndices[state + 1]; ++row) { for (uint_fast64_t row = nondeterministicChoiceIndices[state]; row < nondeterministicChoiceIndices[state + 1]; ++row) {
bool currentChoiceRelevant = false; bool currentChoiceRelevant = false;
bool allSuccessorsProblematic = true; bool allSuccessorsProblematic = true;
for (typename storm::storage::SparseMatrix<T>::ConstIndexIterator successorIt = transitionMatrix.constColumnIteratorBegin(row); successorIt != transitionMatrix.constColumnIteratorEnd(row); ++successorIt) {
for (auto const& successorEntry : transitionMatrix.getRow(row)) {
// If there is a relevant successor, we need to add the labels of the current choice. // If there is a relevant successor, we need to add the labels of the current choice.
if (stateInformation.relevantStates.get(*successorIt) || psiStates.get(*successorIt)) {
if (stateInformation.relevantStates.get(successorEntry.column()) || psiStates.get(successorEntry.column())) {
for (auto const& label : choiceLabeling[row]) { for (auto const& label : choiceLabeling[row]) {
result.allRelevantLabels.insert(label); result.allRelevantLabels.insert(label);
} }
@ -140,7 +140,7 @@ namespace storm {
result.relevantChoicesForRelevantStates[state].push_back(row); result.relevantChoicesForRelevantStates[state].push_back(row);
} }
} }
if (!stateInformation.problematicStates.get(*successorIt)) {
if (!stateInformation.problematicStates.get(successorEntry.column())) {
allSuccessorsProblematic = false; allSuccessorsProblematic = false;
} }
} }
@ -303,12 +303,12 @@ namespace storm {
std::list<uint_fast64_t> const& relevantChoicesForState = choiceInformation.relevantChoicesForRelevantStates.at(state); std::list<uint_fast64_t> const& relevantChoicesForState = choiceInformation.relevantChoicesForRelevantStates.at(state);
for (uint_fast64_t row : relevantChoicesForState) { for (uint_fast64_t row : relevantChoicesForState) {
for (typename storm::storage::SparseMatrix<T>::ConstIndexIterator successorIt = labeledMdp.getTransitionMatrix().constColumnIteratorBegin(row); successorIt != labeledMdp.getTransitionMatrix().constColumnIteratorEnd(row); ++successorIt) {
if (stateInformation.relevantStates.get(*successorIt)) {
if (resultingMap.find(*successorIt) == resultingMap.end()) {
for (auto const& successorEntry : labeledMdp.getTransitionMatrix().getRow(row)) {
if (stateInformation.relevantStates.get(successorEntry.column())) {
if (resultingMap.find(successorEntry.column()) == resultingMap.end()) {
variableNameBuffer.str(""); variableNameBuffer.str("");
variableNameBuffer.clear(); variableNameBuffer.clear();
variableNameBuffer << "r" << *successorIt;
variableNameBuffer << "r" << successorEntry.column();
resultingMap[state] = solver.createContinuousVariable(variableNameBuffer.str(), storm::solver::LpSolver::BOUNDED, 0, 1, 0); resultingMap[state] = solver.createContinuousVariable(variableNameBuffer.str(), storm::solver::LpSolver::BOUNDED, 0, 1, 0);
++numberOfVariablesCreated; ++numberOfVariablesCreated;
} }
@ -337,12 +337,12 @@ namespace storm {
for (auto state : stateInformation.problematicStates) { for (auto state : stateInformation.problematicStates) {
std::list<uint_fast64_t> const& relevantChoicesForState = choiceInformation.relevantChoicesForRelevantStates.at(state); std::list<uint_fast64_t> const& relevantChoicesForState = choiceInformation.relevantChoicesForRelevantStates.at(state);
for (uint_fast64_t row : relevantChoicesForState) { for (uint_fast64_t row : relevantChoicesForState) {
for (typename storm::storage::SparseMatrix<T>::ConstIndexIterator successorIt = labeledMdp.getTransitionMatrix().constColumnIteratorBegin(row); successorIt != labeledMdp.getTransitionMatrix().constColumnIteratorEnd(row); ++successorIt) {
if (stateInformation.relevantStates.get(*successorIt)) {
for (auto const& successorEntry : labeledMdp.getTransitionMatrix().getRow(row)) {
if (stateInformation.relevantStates.get(successorEntry.column())) {
variableNameBuffer.str(""); variableNameBuffer.str("");
variableNameBuffer.clear(); variableNameBuffer.clear();
variableNameBuffer << "t" << state << "to" << *successorIt;
resultingMap[std::make_pair(state, *successorIt)] = solver.createBinaryVariable(variableNameBuffer.str(), 0);
variableNameBuffer << "t" << state << "to" << successorEntry.column();
resultingMap[std::make_pair(state, successorEntry.column())] = solver.createBinaryVariable(variableNameBuffer.str(), 0);
++numberOfVariablesCreated; ++numberOfVariablesCreated;
} }
} }
@ -550,13 +550,12 @@ namespace storm {
coefficients.push_back(1.0); coefficients.push_back(1.0);
double rightHandSide = 1; double rightHandSide = 1;
typename storm::storage::SparseMatrix<T>::Rows rows = labeledMdp.getTransitionMatrix().getRows(choice, choice);
for (typename storm::storage::SparseMatrix<T>::ConstIterator successorIt = rows.begin(), successorIte = rows.end(); successorIt != successorIte; ++successorIt) {
if (stateInformation.relevantStates.get(successorIt.column())) {
variables.push_back(static_cast<int>(variableInformation.stateToProbabilityVariableIndexMap.at(successorIt.column())));
coefficients.push_back(-successorIt.value());
} else if (psiStates.get(successorIt.column())) {
rightHandSide += successorIt.value();
for (auto const& successorEntry : labeledMdp.getTransitionMatrix().getRow(choice)) {
if (stateInformation.relevantStates.get(successorEntry.column())) {
variables.push_back(static_cast<int>(variableInformation.stateToProbabilityVariableIndexMap.at(successorEntry.column())));
coefficients.push_back(-successorEntry.value());
} else if (psiStates.get(successorEntry.column())) {
rightHandSide += successorEntry.value();
} }
} }
@ -609,8 +608,8 @@ namespace storm {
variables.push_back(*choiceVariableIndicesIterator); variables.push_back(*choiceVariableIndicesIterator);
coefficients.push_back(1); coefficients.push_back(1);
for (typename storm::storage::SparseMatrix<T>::ConstIndexIterator successorIt = labeledMdp.getTransitionMatrix().constColumnIteratorBegin(problematicChoice); successorIt != labeledMdp.getTransitionMatrix().constColumnIteratorEnd(problematicChoice); ++successorIt) {
variables.push_back(variableInformation.problematicTransitionToVariableIndexMap.at(std::make_pair(stateListPair.first, *successorIt)));
for (auto const& successorEntry : labeledMdp.getTransitionMatrix().getRow(problematicChoice)) {
variables.push_back(variableInformation.problematicTransitionToVariableIndexMap.at(std::make_pair(stateListPair.first, successorEntry.column())));
coefficients.push_back(-1); coefficients.push_back(-1);
} }
@ -621,15 +620,15 @@ namespace storm {
for (auto state : stateInformation.problematicStates) { for (auto state : stateInformation.problematicStates) {
for (auto problematicChoice : choiceInformation.problematicChoicesForProblematicStates.at(state)) { for (auto problematicChoice : choiceInformation.problematicChoicesForProblematicStates.at(state)) {
for (typename storm::storage::SparseMatrix<T>::ConstIndexIterator successorIt = labeledMdp.getTransitionMatrix().constColumnIteratorBegin(problematicChoice); successorIt != labeledMdp.getTransitionMatrix().constColumnIteratorEnd(problematicChoice); ++successorIt) {
for (auto const& successorEntry : labeledMdp.getTransitionMatrix().getRow(state)) {
std::vector<uint_fast64_t> variables; std::vector<uint_fast64_t> variables;
std::vector<double> coefficients; std::vector<double> coefficients;
variables.push_back(variableInformation.problematicStateToVariableIndexMap.at(state)); variables.push_back(variableInformation.problematicStateToVariableIndexMap.at(state));
coefficients.push_back(1); coefficients.push_back(1);
variables.push_back(variableInformation.problematicStateToVariableIndexMap.at(*successorIt));
variables.push_back(variableInformation.problematicStateToVariableIndexMap.at(successorEntry.column()));
coefficients.push_back(-1); coefficients.push_back(-1);
variables.push_back(variableInformation.problematicTransitionToVariableIndexMap.at(std::make_pair(state, *successorIt)));
variables.push_back(variableInformation.problematicTransitionToVariableIndexMap.at(std::make_pair(state, successorEntry.column())));
coefficients.push_back(1); coefficients.push_back(1);
solver.addConstraint("UnproblematicStateReachable" + std::to_string(numberOfConstraintsCreated), variables, coefficients, storm::solver::LpSolver::LESS, 1); solver.addConstraint("UnproblematicStateReachable" + std::to_string(numberOfConstraintsCreated), variables, coefficients, storm::solver::LpSolver::LESS, 1);
@ -684,8 +683,8 @@ namespace storm {
std::list<uint_fast64_t>::const_iterator choiceVariableIndicesIterator = variableInformation.stateToChoiceVariablesIndexMap.at(state).begin(); std::list<uint_fast64_t>::const_iterator choiceVariableIndicesIterator = variableInformation.stateToChoiceVariablesIndexMap.at(state).begin();
for (auto choice : choiceInformation.relevantChoicesForRelevantStates.at(state)) { for (auto choice : choiceInformation.relevantChoicesForRelevantStates.at(state)) {
bool psiStateReachableInOneStep = false; bool psiStateReachableInOneStep = false;
for (typename storm::storage::SparseMatrix<T>::ConstIndexIterator successorIt = labeledMdp.getTransitionMatrix().constColumnIteratorBegin(choice); successorIt != labeledMdp.getTransitionMatrix().constColumnIteratorEnd(choice); ++successorIt) {
if (psiStates.get(*successorIt)) {
for (auto const& successorEntry : labeledMdp.getTransitionMatrix().getRow(choice)) {
if (psiStates.get(successorEntry.column())) {
psiStateReachableInOneStep = true; psiStateReachableInOneStep = true;
} }
} }
@ -697,9 +696,9 @@ namespace storm {
variables.push_back(static_cast<int>(*choiceVariableIndicesIterator)); variables.push_back(static_cast<int>(*choiceVariableIndicesIterator));
coefficients.push_back(1); coefficients.push_back(1);
for (typename storm::storage::SparseMatrix<T>::ConstIndexIterator successorIt = labeledMdp.getTransitionMatrix().constColumnIteratorBegin(choice); successorIt != labeledMdp.getTransitionMatrix().constColumnIteratorEnd(choice); ++successorIt) {
if (state != *successorIt && stateInformation.relevantStates.get(*successorIt)) {
std::list<uint_fast64_t> const& successorChoiceVariableIndices = variableInformation.stateToChoiceVariablesIndexMap.at(*successorIt);
for (auto const& successorEntry : labeledMdp.getTransitionMatrix().getRow(choice)) {
if (state != successorEntry.column() && stateInformation.relevantStates.get(successorEntry.column())) {
std::list<uint_fast64_t> const& successorChoiceVariableIndices = variableInformation.stateToChoiceVariablesIndexMap.at(successorEntry.column());
for (auto choiceVariableIndex : successorChoiceVariableIndices) { for (auto choiceVariableIndex : successorChoiceVariableIndices) {
variables.push_back(choiceVariableIndex); variables.push_back(choiceVariableIndex);
@ -727,9 +726,9 @@ namespace storm {
// Compute the set of predecessors. // Compute the set of predecessors.
std::unordered_set<uint_fast64_t> predecessors; std::unordered_set<uint_fast64_t> predecessors;
for (typename storm::storage::SparseMatrix<T>::ConstIndexIterator predecessorIt = backwardTransitions.constColumnIteratorBegin(state); predecessorIt != backwardTransitions.constColumnIteratorEnd(state); ++predecessorIt) {
if (state != *predecessorIt) {
predecessors.insert(*predecessorIt);
for (auto const& predecessorEntry : backwardTransitions.getRow(state)) {
if (state != predecessorEntry.column()) {
predecessors.insert(predecessorEntry.column());
} }
} }
@ -744,8 +743,8 @@ namespace storm {
bool choiceTargetsCurrentState = false; bool choiceTargetsCurrentState = false;
// Check if the current choice targets the current state. // Check if the current choice targets the current state.
for (typename storm::storage::SparseMatrix<T>::ConstIndexIterator successorIt = labeledMdp.getTransitionMatrix().constColumnIteratorBegin(relevantChoice); successorIt != labeledMdp.getTransitionMatrix().constColumnIteratorEnd(relevantChoice); ++successorIt) {
if (state == *successorIt) {
for (auto const& successorEntry : labeledMdp.getTransitionMatrix().getRow(relevantChoice)) {
if (state == successorEntry.column()) {
choiceTargetsCurrentState = true; choiceTargetsCurrentState = true;
break; break;
} }
@ -789,9 +788,9 @@ namespace storm {
std::unordered_set<uint_fast64_t> predecessors; std::unordered_set<uint_fast64_t> predecessors;
for (auto psiState : psiStates) { for (auto psiState : psiStates) {
// Compute the set of predecessors. // Compute the set of predecessors.
for (typename storm::storage::SparseMatrix<T>::ConstIndexIterator predecessorIt = backwardTransitions.constColumnIteratorBegin(psiState); predecessorIt != backwardTransitions.constColumnIteratorEnd(psiState); ++predecessorIt) {
if (psiState != *predecessorIt) {
predecessors.insert(*predecessorIt);
for (auto const& predecessorEntry : backwardTransitions.getRow(psiState)) {
if (psiState != predecessorEntry.column()) {
predecessors.insert(predecessorEntry.column());
} }
} }
} }
@ -807,8 +806,8 @@ namespace storm {
bool choiceTargetsPsiState = false; bool choiceTargetsPsiState = false;
// Check if the current choice targets the current state. // Check if the current choice targets the current state.
for (typename storm::storage::SparseMatrix<T>::ConstIndexIterator successorIt = labeledMdp.getTransitionMatrix().constColumnIteratorBegin(relevantChoice); successorIt != labeledMdp.getTransitionMatrix().constColumnIteratorEnd(relevantChoice); ++successorIt) {
if (psiStates.get(*successorIt)) {
for (auto const& successorEntry : labeledMdp.getTransitionMatrix().getRow(relevantChoice)) {
if (psiStates.get(successorEntry.column())) {
choiceTargetsPsiState = true; choiceTargetsPsiState = true;
break; break;
} }

12
src/counterexamples/PathBasedSubsystemGenerator.h

@ -67,8 +67,7 @@ public:
distances[init].second = (T) 1; distances[init].second = (T) 1;
} }
typename storm::storage::SparseMatrix<T>::ConstRowIterator rowIt = transMat.begin(init);
for(auto trans = rowIt.begin() ; trans != rowIt.end(); ++trans) {
for(auto& trans : transMat.getRow(init)) {
//save transition only if it's no 'virtual transition of prob 0 and it doesn't go from init state to init state. //save transition only if it's no 'virtual transition of prob 0 and it doesn't go from init state to init state.
if(trans.value() != (T) 0 && !subSysStates.get(trans.column())) { if(trans.value() != (T) 0 && !subSysStates.get(trans.column())) {
//new state? //new state?
@ -114,8 +113,7 @@ public:
// Same goes for forbidden states since they may not be used on a path, except as last node. // Same goes for forbidden states since they may not be used on a path, except as last node.
if(!subSysStates.get(activeState.first) && allowedStates.get(activeState.first)) { if(!subSysStates.get(activeState.first) && allowedStates.get(activeState.first)) {
// Look at all neighbors // Look at all neighbors
typename storm::storage::SparseMatrix<T>::ConstRowIterator rowIt = transMat.begin(activeState.first);
for(typename storm::storage::SparseMatrix<T>::ConstIterator trans = rowIt.begin(); trans != rowIt.end(); ++trans) {
for(auto& trans : transMat.getRow(activeState.first)) {
// Only consider the transition if it's not virtual // Only consider the transition if it's not virtual
if(trans.value() != (T) 0) { if(trans.value() != (T) 0) {
@ -182,8 +180,7 @@ public:
continue; continue;
} }
typename storm::storage::SparseMatrix<T>::ConstRowIterator rowIt = transMat.begin(init);
for(typename storm::storage::SparseMatrix<T>::ConstIterator trans = rowIt.begin(); trans != rowIt.end(); ++trans) {
for(auto& trans : transMat.getRow(init)) {
//save transition only if it's no 'virtual transition of prob 0 and it doesn't go from init state to init state. //save transition only if it's no 'virtual transition of prob 0 and it doesn't go from init state to init state.
if(trans.value() != (T) 0 && !subSysStates.get(trans.column())) { if(trans.value() != (T) 0 && !subSysStates.get(trans.column())) {
//new state? //new state?
@ -234,8 +231,7 @@ public:
// Same goes for forbidden states since they may not be used on a path, except as last node. // Same goes for forbidden states since they may not be used on a path, except as last node.
if(!subSysStates.get(activeState.first) && allowedStates.get(activeState.first)) { if(!subSysStates.get(activeState.first) && allowedStates.get(activeState.first)) {
// Look at all neighbors // Look at all neighbors
typename storm::storage::SparseMatrix<T>::ConstRowIterator rowIt = transMat.begin(activeState.first);
for(typename storm::storage::SparseMatrix<T>::ConstIterator trans = rowIt.begin(); trans != rowIt.end(); ++trans) {
for(auto& trans : transMat.getRow(activeState.first)) {
// Only consider the transition if it's not virtual // Only consider the transition if it's not virtual
if(trans.value() != (T) 0) { if(trans.value() != (T) 0) {

94
src/counterexamples/SMTMinimalCommandSetGenerator.h

@ -123,9 +123,9 @@ namespace storm {
for (uint_fast64_t row = nondeterministicChoiceIndices[state]; row < nondeterministicChoiceIndices[state + 1]; ++row) { for (uint_fast64_t row = nondeterministicChoiceIndices[state]; row < nondeterministicChoiceIndices[state + 1]; ++row) {
bool currentChoiceRelevant = false; bool currentChoiceRelevant = false;
for (typename storm::storage::SparseMatrix<T>::ConstIndexIterator successorIt = transitionMatrix.constColumnIteratorBegin(row); successorIt != transitionMatrix.constColumnIteratorEnd(row); ++successorIt) {
for (auto& entry : transitionMatrix.getRow(row)) {
// If there is a relevant successor, we need to add the labels of the current choice. // If there is a relevant successor, we need to add the labels of the current choice.
if (relevancyInformation.relevantStates.get(*successorIt) || psiStates.get(*successorIt)) {
if (relevancyInformation.relevantStates.get(entry.column()) || psiStates.get(entry.column())) {
for (auto const& label : choiceLabeling[row]) { for (auto const& label : choiceLabeling[row]) {
relevancyInformation.relevantLabels.insert(label); relevancyInformation.relevantLabels.insert(label);
} }
@ -208,25 +208,25 @@ namespace storm {
variableInformation.stateOrderVariables.push_back(context.real_const(variableName.str().c_str())); variableInformation.stateOrderVariables.push_back(context.real_const(variableName.str().c_str()));
for (auto const& relevantChoices : relevancyInformation.relevantChoicesForRelevantStates.at(state)) {
for (typename storm::storage::SparseMatrix<T>::ConstIndexIterator successorIt = transitionMatrix.constColumnIteratorBegin(relevantChoices); successorIt != transitionMatrix.constColumnIteratorEnd(relevantChoices); ++successorIt) {
for (auto const& relevantChoice : relevancyInformation.relevantChoicesForRelevantStates.at(state)) {
for (auto const& entry : transitionMatrix.getRow(relevantChoice)) {
// If the successor state is neither the state itself nor an irrelevant state, we need to add a variable for the transition. // If the successor state is neither the state itself nor an irrelevant state, we need to add a variable for the transition.
if (state != *successorIt && (relevancyInformation.relevantStates.get(*successorIt) || psiStates.get(*successorIt))) {
if (state != entry.column() && (relevancyInformation.relevantStates.get(entry.column()) || psiStates.get(entry.column()))) {
// Make sure that there is not already one variable for the state pair. This may happen because of several nondeterministic choices // Make sure that there is not already one variable for the state pair. This may happen because of several nondeterministic choices
// targeting the same state. // targeting the same state.
if (variableInformation.statePairToIndexMap.find(std::make_pair(state, *successorIt)) != variableInformation.statePairToIndexMap.end()) {
if (variableInformation.statePairToIndexMap.find(std::make_pair(state, entry.column())) != variableInformation.statePairToIndexMap.end()) {
continue; continue;
} }
// At this point we know that the state-pair does not have an associated variable. // At this point we know that the state-pair does not have an associated variable.
variableInformation.statePairToIndexMap[std::make_pair(state, *successorIt)] = variableInformation.statePairVariables.size();
variableInformation.statePairToIndexMap[std::make_pair(state, entry.column())] = variableInformation.statePairVariables.size();
// Clear contents of the stream to construct new expression name. // Clear contents of the stream to construct new expression name.
variableName.clear(); variableName.clear();
variableName.str(""); variableName.str("");
variableName << "t" << state << "_" << *successorIt;
variableName << "t" << state << "_" << entry.column();
variableInformation.statePairVariables.push_back(context.bool_const(variableName.str().c_str())); variableInformation.statePairVariables.push_back(context.bool_const(variableName.str().c_str()));
} }
@ -315,12 +315,12 @@ namespace storm {
// Iterate over successors and add relevant choices of relevant successors to the following label set. // Iterate over successors and add relevant choices of relevant successors to the following label set.
bool canReachTargetState = false; bool canReachTargetState = false;
for (typename storm::storage::SparseMatrix<T>::ConstIndexIterator successorIt = transitionMatrix.constColumnIteratorBegin(currentChoice), successorIte = transitionMatrix.constColumnIteratorEnd(currentChoice); successorIt != successorIte; ++successorIt) {
if (relevancyInformation.relevantStates.get(*successorIt)) {
for (auto relevantChoice : relevancyInformation.relevantChoicesForRelevantStates.at(*successorIt)) {
for (auto const& entry : transitionMatrix.getRow(currentChoice)) {
if (relevancyInformation.relevantStates.get(entry.column())) {
for (auto relevantChoice : relevancyInformation.relevantChoicesForRelevantStates.at(entry.column())) {
followingLabels[choiceLabeling[currentChoice]].insert(choiceLabeling[currentChoice]); followingLabels[choiceLabeling[currentChoice]].insert(choiceLabeling[currentChoice]);
} }
} else if (psiStates.get(*successorIt)) {
} else if (psiStates.get(entry.column())) {
canReachTargetState = true; canReachTargetState = true;
} }
} }
@ -334,12 +334,12 @@ namespace storm {
// Iterate over predecessors and add all choices that target the current state to the preceding // Iterate over predecessors and add all choices that target the current state to the preceding
// label set of all labels of all relevant choices of the current state. // label set of all labels of all relevant choices of the current state.
for (typename storm::storage::SparseMatrix<T>::ConstIndexIterator predecessorIt = backwardTransitions.constColumnIteratorBegin(currentState), predecessorIte = backwardTransitions.constColumnIteratorEnd(currentState); predecessorIt != predecessorIte; ++predecessorIt) {
if (relevancyInformation.relevantStates.get(*predecessorIt)) {
for (auto predecessorChoice : relevancyInformation.relevantChoicesForRelevantStates.at(*predecessorIt)) {
for (auto const& predecessorEntry : backwardTransitions.getRow(currentState)) {
if (relevancyInformation.relevantStates.get(predecessorEntry.column())) {
for (auto predecessorChoice : relevancyInformation.relevantChoicesForRelevantStates.at(predecessorEntry.column())) {
bool choiceTargetsCurrentState = false; bool choiceTargetsCurrentState = false;
for (typename storm::storage::SparseMatrix<T>::ConstIndexIterator successorIt = transitionMatrix.constColumnIteratorBegin(predecessorChoice), successorIte = transitionMatrix.constColumnIteratorEnd(predecessorChoice); successorIt != successorIte; ++successorIt) {
if (*successorIt == currentState) {
for (auto const& successorEntry : transitionMatrix.getRow(predecessorChoice)) {
if (successorEntry.column() == currentState) {
choiceTargetsCurrentState = true; choiceTargetsCurrentState = true;
} }
} }
@ -580,12 +580,12 @@ namespace storm {
// Iterate over predecessors and add all choices that target the current state to the preceding // Iterate over predecessors and add all choices that target the current state to the preceding
// label set of all labels of all relevant choices of the current state. // label set of all labels of all relevant choices of the current state.
for (typename storm::storage::SparseMatrix<T>::ConstIndexIterator predecessorIt = backwardTransitions.constColumnIteratorBegin(currentState), predecessorIte = backwardTransitions.constColumnIteratorEnd(currentState); predecessorIt != predecessorIte; ++predecessorIt) {
if (relevancyInformation.relevantStates.get(*predecessorIt)) {
for (auto predecessorChoice : relevancyInformation.relevantChoicesForRelevantStates.at(*predecessorIt)) {
for (auto const& predecessorEntry : backwardTransitions.getRow(currentState)) {
if (relevancyInformation.relevantStates.get(predecessorEntry.column())) {
for (auto predecessorChoice : relevancyInformation.relevantChoicesForRelevantStates.at(predecessorEntry.column())) {
bool choiceTargetsCurrentState = false; bool choiceTargetsCurrentState = false;
for (typename storm::storage::SparseMatrix<T>::ConstIndexIterator successorIt = transitionMatrix.constColumnIteratorBegin(predecessorChoice), successorIte = transitionMatrix.constColumnIteratorEnd(predecessorChoice); successorIt != successorIte; ++successorIt) {
if (*successorIt == currentState) {
for (auto const& successorEntry : transitionMatrix.getRow(predecessorChoice)) {
if (successorEntry.column() == currentState) {
choiceTargetsCurrentState = true; choiceTargetsCurrentState = true;
} }
} }
@ -912,17 +912,17 @@ namespace storm {
if (!labeledMdp.getInitialStates().get(relevantState)) { if (!labeledMdp.getInitialStates().get(relevantState)) {
// Assert the constraints (1). // Assert the constraints (1).
storm::storage::VectorSet<uint_fast64_t> relevantPredecessors; storm::storage::VectorSet<uint_fast64_t> relevantPredecessors;
for (typename storm::storage::SparseMatrix<T>::ConstIndexIterator predecessorIt = backwardTransitions.constColumnIteratorBegin(relevantState), predecessorIte = backwardTransitions.constColumnIteratorEnd(relevantState); predecessorIt != predecessorIte; ++predecessorIt) {
if (relevantState != *predecessorIt && relevancyInformation.relevantStates.get(*predecessorIt)) {
relevantPredecessors.insert(*predecessorIt);
for (auto const& predecessorEntry : backwardTransitions.getRow(relevantState)) {
if (relevantState != predecessorEntry.column() && relevancyInformation.relevantStates.get(predecessorEntry.column())) {
relevantPredecessors.insert(predecessorEntry.column());
} }
} }
storm::storage::VectorSet<uint_fast64_t> relevantSuccessors; storm::storage::VectorSet<uint_fast64_t> relevantSuccessors;
for (auto const& relevantChoice : relevancyInformation.relevantChoicesForRelevantStates.at(relevantState)) { for (auto const& relevantChoice : relevancyInformation.relevantChoicesForRelevantStates.at(relevantState)) {
for (typename storm::storage::SparseMatrix<T>::ConstIndexIterator successorIt = transitionMatrix.constColumnIteratorBegin(relevantChoice); successorIt != transitionMatrix.constColumnIteratorEnd(relevantChoice); ++successorIt) {
if (relevantState != *successorIt && (relevancyInformation.relevantStates.get(*successorIt) || psiStates.get(*successorIt))) {
relevantSuccessors.insert(*successorIt);
for (auto const& successorEntry : transitionMatrix.getRow(relevantChoice)) {
if (relevantState != successorEntry.column() && (relevancyInformation.relevantStates.get(successorEntry.column()) || psiStates.get(successorEntry.column()))) {
relevantSuccessors.insert(successorEntry.column());
} }
} }
} }
@ -940,9 +940,9 @@ namespace storm {
// Assert the constraints (2). // Assert the constraints (2).
storm::storage::VectorSet<uint_fast64_t> relevantSuccessors; storm::storage::VectorSet<uint_fast64_t> relevantSuccessors;
for (auto const& relevantChoice : relevancyInformation.relevantChoicesForRelevantStates.at(relevantState)) { for (auto const& relevantChoice : relevancyInformation.relevantChoicesForRelevantStates.at(relevantState)) {
for (typename storm::storage::SparseMatrix<T>::ConstIndexIterator successorIt = transitionMatrix.constColumnIteratorBegin(relevantChoice); successorIt != transitionMatrix.constColumnIteratorEnd(relevantChoice); ++successorIt) {
if (relevantState != *successorIt && (relevancyInformation.relevantStates.get(*successorIt) || psiStates.get(*successorIt))) {
relevantSuccessors.insert(*successorIt);
for (auto const& successorEntry : transitionMatrix.getRow(relevantChoice)) {
if (relevantState != successorEntry.column() && (relevancyInformation.relevantStates.get(successorEntry.column()) || psiStates.get(successorEntry.column()))) {
relevantSuccessors.insert(successorEntry.column());
} }
} }
} }
@ -964,8 +964,8 @@ namespace storm {
// Assert constraint for (1). // Assert constraint for (1).
storm::storage::VectorSet<uint_fast64_t> choicesForStatePair; storm::storage::VectorSet<uint_fast64_t> choicesForStatePair;
for (auto const& relevantChoice : relevancyInformation.relevantChoicesForRelevantStates.at(sourceState)) { for (auto const& relevantChoice : relevancyInformation.relevantChoicesForRelevantStates.at(sourceState)) {
for (typename storm::storage::SparseMatrix<T>::ConstIndexIterator successorIt = transitionMatrix.constColumnIteratorBegin(relevantChoice); successorIt != transitionMatrix.constColumnIteratorEnd(relevantChoice); ++successorIt) {
if (*successorIt == targetState) {
for (auto const& successorEntry : transitionMatrix.getRow(relevantChoice)) {
if (successorEntry.column() == targetState) {
choicesForStatePair.insert(relevantChoice); choicesForStatePair.insert(relevantChoice);
} }
} }
@ -1399,14 +1399,14 @@ namespace storm {
for (uint_fast64_t currentChoice = nondeterministicChoiceIndices[currentState]; currentChoice < nondeterministicChoiceIndices[currentState + 1]; ++currentChoice) { for (uint_fast64_t currentChoice = nondeterministicChoiceIndices[currentState]; currentChoice < nondeterministicChoiceIndices[currentState + 1]; ++currentChoice) {
bool choiceTargetsRelevantState = false; bool choiceTargetsRelevantState = false;
for (typename storm::storage::SparseMatrix<T>::ConstIndexIterator successorIt = transitionMatrix.constColumnIteratorBegin(currentChoice), successorIte = transitionMatrix.constColumnIteratorEnd(currentChoice); successorIt != successorIte; ++successorIt) {
if (relevancyInformation.relevantStates.get(*successorIt) && currentState != *successorIt) {
for (auto const& successorEntry : transitionMatrix.getRow(currentChoice)) {
if (relevancyInformation.relevantStates.get(successorEntry.column()) && currentState != successorEntry.column()) {
choiceTargetsRelevantState = true; choiceTargetsRelevantState = true;
if (!reachableStates.get(*successorIt)) {
reachableStates.set(*successorIt, true);
stack.push_back(*successorIt);
if (!reachableStates.get(successorEntry.column())) {
reachableStates.set(successorEntry.column());
stack.push_back(successorEntry.column());
} }
} else if (psiStates.get(*successorIt)) {
} else if (psiStates.get(successorEntry.column())) {
targetStateIsReachable = true; targetStateIsReachable = true;
} }
} }
@ -1442,8 +1442,8 @@ namespace storm {
bool isBorderChoice = false; bool isBorderChoice = false;
// Determine whether the state has the option to leave the reachable state space and go to the unreachable relevant states. // Determine whether the state has the option to leave the reachable state space and go to the unreachable relevant states.
for (typename storm::storage::SparseMatrix<T>::ConstIndexIterator successorIt = originalMdp.getTransitionMatrix().constColumnIteratorBegin(currentChoice), successorIte = originalMdp.getTransitionMatrix().constColumnIteratorEnd(currentChoice); successorIt != successorIte; ++successorIt) {
if (unreachableRelevantStates.get(*successorIt)) {
for (auto const& successorEntry : originalMdp.getTransitionMatrix().getRow(currentChoice)) {
if (unreachableRelevantStates.get(successorEntry.column())) {
isBorderChoice = true; isBorderChoice = true;
} }
} }
@ -1525,14 +1525,14 @@ namespace storm {
for (uint_fast64_t currentChoice = nondeterministicChoiceIndices[currentState]; currentChoice < nondeterministicChoiceIndices[currentState + 1]; ++currentChoice) { for (uint_fast64_t currentChoice = nondeterministicChoiceIndices[currentState]; currentChoice < nondeterministicChoiceIndices[currentState + 1]; ++currentChoice) {
bool choiceTargetsRelevantState = false; bool choiceTargetsRelevantState = false;
for (typename storm::storage::SparseMatrix<T>::ConstIndexIterator successorIt = transitionMatrix.constColumnIteratorBegin(currentChoice), successorIte = transitionMatrix.constColumnIteratorEnd(currentChoice); successorIt != successorIte; ++successorIt) {
if (relevancyInformation.relevantStates.get(*successorIt) && currentState != *successorIt) {
for (auto const& successorEntry : transitionMatrix.getRow(currentChoice)) {
if (relevancyInformation.relevantStates.get(successorEntry.column()) && currentState != successorEntry.column()) {
choiceTargetsRelevantState = true; choiceTargetsRelevantState = true;
if (!reachableStates.get(*successorIt)) {
reachableStates.set(*successorIt, true);
stack.push_back(*successorIt);
if (!reachableStates.get(successorEntry.column())) {
reachableStates.set(successorEntry.column(), true);
stack.push_back(successorEntry.column());
} }
} else if (psiStates.get(*successorIt)) {
} else if (psiStates.get(successorEntry.column())) {
targetStateIsReachable = true; targetStateIsReachable = true;
} }
} }

11
src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h

@ -94,8 +94,7 @@ namespace storm {
// Digitize aMarkovian. Based on whether the transition is a self-loop or not, we apply the two digitization rules. // Digitize aMarkovian. Based on whether the transition is a self-loop or not, we apply the two digitization rules.
uint_fast64_t rowIndex = 0; uint_fast64_t rowIndex = 0;
for (auto state : markovianNonGoalStates) { for (auto state : markovianNonGoalStates) {
typename storm::storage::SparseMatrix<ValueType>::MutableRows row = aMarkovian.getMutableRow(rowIndex);
for (auto element : row) {
for (auto& element : aMarkovian.getRow(rowIndex)) {
ValueType eTerm = std::exp(-exitRates[state] * delta); ValueType eTerm = std::exp(-exitRates[state] * delta);
if (element.column() == rowIndex) { if (element.column() == rowIndex) {
element.value() = (storm::utility::constantOne<ValueType>() - eTerm) * element.value() + eTerm; element.value() = (storm::utility::constantOne<ValueType>() - eTerm) * element.value() + eTerm;
@ -109,8 +108,7 @@ namespace storm {
// Digitize aMarkovianToProbabilistic. As there are no self-loops in this case, we only need to apply the digitization formula for regular successors. // Digitize aMarkovianToProbabilistic. As there are no self-loops in this case, we only need to apply the digitization formula for regular successors.
rowIndex = 0; rowIndex = 0;
for (auto state : markovianNonGoalStates) { for (auto state : markovianNonGoalStates) {
typename storm::storage::SparseMatrix<ValueType>::MutableRows row = aMarkovianToProbabilistic.getMutableRow(rowIndex);
for (auto element : row) {
for (auto element : aMarkovianToProbabilistic.getRow(rowIndex)) {
element.value() = (1 - std::exp(-exitRates[state] * delta)) * element.value(); element.value() = (1 - std::exp(-exitRates[state] * delta)) * element.value();
} }
++rowIndex; ++rowIndex;
@ -121,14 +119,13 @@ namespace storm {
std::vector<ValueType> bMarkovian(markovianNonGoalStates.getNumberOfSetBits()); std::vector<ValueType> bMarkovian(markovianNonGoalStates.getNumberOfSetBits());
// Compute the two fixed right-hand side vectors, one for Markovian states and one for the probabilistic ones. // Compute the two fixed right-hand side vectors, one for Markovian states and one for the probabilistic ones.
std::vector<ValueType> bProbabilisticFixed = transitionMatrix.getConstrainedRowSumVector(probabilisticNonGoalStates, nondeterministicChoiceIndices, goalStates, aProbabilistic.getRowCount());
std::vector<ValueType> bProbabilisticFixed = transitionMatrix.getConstrainedRowSumVector(probabilisticNonGoalStates, nondeterministicChoiceIndices, goalStates);
std::vector<ValueType> bMarkovianFixed; std::vector<ValueType> bMarkovianFixed;
bMarkovianFixed.reserve(markovianNonGoalStates.getNumberOfSetBits()); bMarkovianFixed.reserve(markovianNonGoalStates.getNumberOfSetBits());
for (auto state : markovianNonGoalStates) { for (auto state : markovianNonGoalStates) {
bMarkovianFixed.push_back(storm::utility::constantZero<ValueType>()); bMarkovianFixed.push_back(storm::utility::constantZero<ValueType>());
typename storm::storage::SparseMatrix<ValueType>::Rows row = transitionMatrix.getRow(nondeterministicChoiceIndices[state]);
for (auto element : row) {
for (auto element : transitionMatrix.getRow(nondeterministicChoiceIndices[state])) {
if (goalStates.get(element.column())) { if (goalStates.get(element.column())) {
bMarkovianFixed.back() += (1 - std::exp(-exitRates[state] * delta)) * element.value(); bMarkovianFixed.back() += (1 - std::exp(-exitRates[state] * delta)) * element.value();
} }

7
src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h

@ -104,7 +104,6 @@ public:
* checker. If the qualitative flag is set, exact probabilities might not be computed. * checker. If the qualitative flag is set, exact probabilities might not be computed.
*/ */
virtual std::vector<Type> checkBoundedUntil(storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, uint_fast64_t stepBound, bool qualitative) const { virtual std::vector<Type> checkBoundedUntil(storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, uint_fast64_t stepBound, bool qualitative) const {
std::vector<Type> result(this->getModel().getNumberOfStates()); std::vector<Type> result(this->getModel().getNumberOfStates());
// If we identify the states that have probability 0 of reaching the target states, we can exclude them in the // If we identify the states that have probability 0 of reaching the target states, we can exclude them in the
@ -122,7 +121,7 @@ public:
storm::utility::vector::setVectorValues(result, statesWithProbabilityGreater0, Type(0.5)); storm::utility::vector::setVectorValues(result, statesWithProbabilityGreater0, Type(0.5));
} else { } else {
// In this case we have have to compute the probabilities. // In this case we have have to compute the probabilities.
// We can eliminate the rows and columns from the original transition probability matrix that have probability 0. // We can eliminate the rows and columns from the original transition probability matrix that have probability 0.
storm::storage::SparseMatrix<Type> submatrix = this->getModel().getTransitionMatrix().getSubmatrix(statesWithProbabilityGreater0); storm::storage::SparseMatrix<Type> submatrix = this->getModel().getTransitionMatrix().getSubmatrix(statesWithProbabilityGreater0);
@ -192,9 +191,7 @@ public:
* checker. If the qualitative flag is set, exact probabilities might not be computed. * checker. If the qualitative flag is set, exact probabilities might not be computed.
*/ */
virtual std::vector<Type> checkBoundedEventually(storm::property::prctl::BoundedEventually<Type> const& formula, bool qualitative) const { virtual std::vector<Type> checkBoundedEventually(storm::property::prctl::BoundedEventually<Type> const& formula, bool qualitative) const {
// Create equivalent temporary bounded until formula and check it.
storm::property::prctl::BoundedUntil<Type> temporaryBoundedUntilFormula(new storm::property::prctl::Ap<Type>("true"), formula.getChild().clone(), formula.getBound());
return this->checkBoundedUntil(temporaryBoundedUntilFormula, qualitative);
return this->checkBoundedUntil(storm::storage::BitVector(this->getModel().getNumberOfStates(), true), formula.getChild().check(*this), formula.getBound(), qualitative);
} }
/*! /*!

2
src/modelchecker/prctl/SparseMdpPrctlModelChecker.h

@ -323,7 +323,7 @@ namespace storm {
// Prepare the right-hand side of the equation system. For entry i this corresponds to // Prepare the right-hand side of the equation system. For entry i this corresponds to
// the accumulated probability of going from state i to some 'yes' state. // the accumulated probability of going from state i to some 'yes' state.
std::vector<Type> b = transitionMatrix.getConstrainedRowSumVector(maybeStates, nondeterministicChoiceIndices, statesWithProbability1, submatrix.getRowCount());
std::vector<Type> b = transitionMatrix.getConstrainedRowSumVector(maybeStates, nondeterministicChoiceIndices, statesWithProbability1);
// Create vector for results for maybe states. // Create vector for results for maybe states.
std::vector<Type> x(maybeStates.getNumberOfSetBits()); std::vector<Type> x(maybeStates.getNumberOfSetBits());

19
src/models/AbstractDeterministicModel.h

@ -71,18 +71,10 @@ class AbstractDeterministicModel: public AbstractModel<T> {
// Intentionally left empty. // Intentionally left empty.
} }
virtual typename storm::storage::SparseMatrix<T>::Rows getRows(uint_fast64_t state) const override {
virtual typename storm::storage::SparseMatrix<T>::const_rows getRows(uint_fast64_t state) const override {
return this->transitionMatrix.getRows(state, state); return this->transitionMatrix.getRows(state, state);
} }
virtual typename storm::storage::SparseMatrix<T>::ConstRowIterator rowIteratorBegin(uint_fast64_t state) const override {
return this->transitionMatrix.begin(state);
}
virtual typename storm::storage::SparseMatrix<T>::ConstRowIterator rowIteratorEnd(uint_fast64_t state) const override {
return this->transitionMatrix.end(state);
}
/*! /*!
* Calculates a hash over all values contained in this Model. * Calculates a hash over all values contained in this Model.
* @return size_t A Hash Value * @return size_t A Hash Value
@ -97,10 +89,11 @@ class AbstractDeterministicModel: public AbstractModel<T> {
// Simply iterate over all transitions and draw the arrows with probability information attached. // Simply iterate over all transitions and draw the arrows with probability information attached.
auto rowIt = this->transitionMatrix.begin(); auto rowIt = this->transitionMatrix.begin();
for (uint_fast64_t i = 0; i < this->transitionMatrix.getRowCount(); ++i, ++rowIt) { for (uint_fast64_t i = 0; i < this->transitionMatrix.getRowCount(); ++i, ++rowIt) {
for (auto transitionIt = rowIt.begin(), transitionIte = rowIt.end(); transitionIt != transitionIte; ++transitionIt) {
if (transitionIt.value() != storm::utility::constantZero<T>()) {
if (subsystem == nullptr || subsystem->get(transitionIt.column())) {
outStream << "\t" << i << " -> " << transitionIt.column() << " [ label= \"" << transitionIt.value() << "\" ];" << std::endl;
typename storm::storage::SparseMatrix<T>::const_rows row = this->transitionMatrix.getRow(i);
for (auto& transition : row) {
if (transition.value() != storm::utility::constantZero<T>()) {
if (subsystem == nullptr || subsystem->get(transition.column())) {
outStream << "\t" << i << " -> " << transition.column() << " [ label= \"" << transition.value() << "\" ];" << std::endl;
} }
} }
} }

24
src/models/AbstractModel.h

@ -208,23 +208,7 @@ class AbstractModel: public std::enable_shared_from_this<AbstractModel<T>> {
* @param state The state for which to retrieve the rows. * @param state The state for which to retrieve the rows.
* @return An object representing the matrix rows associated with the given state. * @return An object representing the matrix rows associated with the given state.
*/ */
virtual typename storm::storage::SparseMatrix<T>::Rows getRows(uint_fast64_t state) const = 0;
/*!
* Returns an iterator to the successors of the given state.
*
* @param state The state for which to return the iterator.
* @return An iterator to the successors of the given state.
*/
virtual typename storm::storage::SparseMatrix<T>::ConstRowIterator rowIteratorBegin(uint_fast64_t state) const = 0;
/*!
* Returns an iterator pointing to the element past the successors of the given state.
*
* @param state The state for which to return the iterator.
* @return An iterator pointing to the element past the successors of the given state.
*/
virtual typename storm::storage::SparseMatrix<T>::ConstRowIterator rowIteratorEnd(uint_fast64_t state) const = 0;
virtual typename storm::storage::SparseMatrix<T>::const_rows getRows(uint_fast64_t state) const = 0;
/*! /*!
* Returns the state space size of the model. * Returns the state space size of the model.
@ -239,7 +223,7 @@ class AbstractModel: public std::enable_shared_from_this<AbstractModel<T>> {
* @return The number of (non-zero) transitions of the model. * @return The number of (non-zero) transitions of the model.
*/ */
virtual uint_fast64_t getNumberOfTransitions() const { virtual uint_fast64_t getNumberOfTransitions() const {
return this->getTransitionMatrix().getNonZeroEntryCount();
return this->getTransitionMatrix().getEntryCount();
} }
/*! /*!
@ -383,13 +367,13 @@ class AbstractModel: public std::enable_shared_from_this<AbstractModel<T>> {
*/ */
virtual size_t getHash() const { virtual size_t getHash() const {
std::size_t result = 0; std::size_t result = 0;
boost::hash_combine(result, transitionMatrix.getHash());
boost::hash_combine(result, transitionMatrix.hash());
boost::hash_combine(result, stateLabeling.getHash()); boost::hash_combine(result, stateLabeling.getHash());
if (stateRewardVector) { if (stateRewardVector) {
boost::hash_combine(result, storm::utility::Hash<T>::getHash(stateRewardVector.get())); boost::hash_combine(result, storm::utility::Hash<T>::getHash(stateRewardVector.get()));
} }
if (transitionRewardMatrix) { if (transitionRewardMatrix) {
boost::hash_combine(result, transitionRewardMatrix.get().getHash());
boost::hash_combine(result, transitionRewardMatrix.get().hash());
} }
return result; return result;
} }

37
src/models/AbstractNondeterministicModel.h

@ -110,18 +110,10 @@ namespace storm {
return nondeterministicChoiceIndices; return nondeterministicChoiceIndices;
} }
virtual typename storm::storage::SparseMatrix<T>::Rows getRows(uint_fast64_t state) const override {
virtual typename storm::storage::SparseMatrix<T>::const_rows getRows(uint_fast64_t state) const override {
return this->transitionMatrix.getRows(nondeterministicChoiceIndices[state], nondeterministicChoiceIndices[state + 1] - 1); return this->transitionMatrix.getRows(nondeterministicChoiceIndices[state], nondeterministicChoiceIndices[state + 1] - 1);
} }
virtual typename storm::storage::SparseMatrix<T>::ConstRowIterator rowIteratorBegin(uint_fast64_t state) const override {
return this->transitionMatrix.begin(nondeterministicChoiceIndices[state]);
}
virtual typename storm::storage::SparseMatrix<T>::ConstRowIterator rowIteratorEnd(uint_fast64_t state) const override {
return this->transitionMatrix.end(nondeterministicChoiceIndices[state + 1] - 1);
}
/*! /*!
* Retrieves the backward transition relation of the model, i.e. a set of transitions * Retrieves the backward transition relation of the model, i.e. a set of transitions
* between states that correspond to the reversed transition relation of this model. * between states that correspond to the reversed transition relation of this model.
@ -140,7 +132,7 @@ namespace storm {
// First, we need to count how many backward transitions each state has. // First, we need to count how many backward transitions each state has.
for (uint_fast64_t i = 0; i < numberOfStates; ++i) { for (uint_fast64_t i = 0; i < numberOfStates; ++i) {
typename storm::storage::SparseMatrix<T>::Rows rows = this->getRows(i);
typename storm::storage::SparseMatrix<T>::const_rows rows = this->getRows(i);
for (auto const& transition : rows) { for (auto const& transition : rows) {
if (transition.value() > 0) { if (transition.value() > 0) {
++rowIndications[transition.column() + 1]; ++rowIndications[transition.column() + 1];
@ -160,7 +152,7 @@ namespace storm {
// Now we are ready to actually fill in the list of predecessors for // 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. // every state. Again, we start by considering all but the last row.
for (uint_fast64_t i = 0; i < numberOfStates; ++i) { for (uint_fast64_t i = 0; i < numberOfStates; ++i) {
typename storm::storage::SparseMatrix<T>::Rows rows = this->getRows(i);
typename storm::storage::SparseMatrix<T>::const_rows rows = this->getRows(i);
for (auto& transition : rows) { for (auto& transition : rows) {
if (transition.value() > 0) { if (transition.value() > 0) {
values[nextIndices[transition.column()]] = transition.value(); values[nextIndices[transition.column()]] = transition.value();
@ -169,11 +161,7 @@ namespace storm {
} }
} }
storm::storage::SparseMatrix<T> backwardTransitionMatrix(numberOfStates, numberOfStates,
numberOfTransitions,
std::move(rowIndications),
std::move(columnIndications),
std::move(values));
storm::storage::SparseMatrix<T> backwardTransitionMatrix(numberOfStates, std::move(rowIndications), std::move(columnIndications), std::move(values));
return backwardTransitionMatrix; return backwardTransitionMatrix;
} }
@ -209,16 +197,17 @@ namespace storm {
AbstractModel<T>::writeDotToStream(outStream, includeLabeling, subsystem, firstValue, secondValue, stateColoring, colors, scheduler, false); AbstractModel<T>::writeDotToStream(outStream, includeLabeling, subsystem, firstValue, secondValue, stateColoring, colors, scheduler, false);
// Write the probability distributions for all the states. // Write the probability distributions for all the states.
auto rowIt = this->transitionMatrix.begin();
for (uint_fast64_t state = 0, highestStateIndex = this->getNumberOfStates() - 1; state <= highestStateIndex; ++state) { for (uint_fast64_t state = 0, highestStateIndex = this->getNumberOfStates() - 1; state <= highestStateIndex; ++state) {
uint_fast64_t rowCount = nondeterministicChoiceIndices[state + 1] - nondeterministicChoiceIndices[state]; uint_fast64_t rowCount = nondeterministicChoiceIndices[state + 1] - nondeterministicChoiceIndices[state];
bool highlightChoice = true; bool highlightChoice = true;
// For this, we need to iterate over all available nondeterministic choices in the current state. // For this, we need to iterate over all available nondeterministic choices in the current state.
for (uint_fast64_t row = 0; row < rowCount; ++row, ++rowIt) {
for (uint_fast64_t choice = 0; choice < rowCount; ++choice) {
typename storm::storage::SparseMatrix<T>::const_rows row = this->transitionMatrix.getRow(nondeterministicChoiceIndices[state] + choice);
if (scheduler != nullptr) { if (scheduler != nullptr) {
// If the scheduler picked the current choice, we will not make it dotted, but highlight it. // If the scheduler picked the current choice, we will not make it dotted, but highlight it.
if ((*scheduler)[state] == row) {
if ((*scheduler)[state] == choice) {
highlightChoice = true; highlightChoice = true;
} else { } else {
highlightChoice = false; highlightChoice = false;
@ -227,7 +216,7 @@ namespace storm {
// For each nondeterministic choice, we draw an arrow to an intermediate node to better display // For each nondeterministic choice, we draw an arrow to an intermediate node to better display
// the grouping of transitions. // the grouping of transitions.
outStream << "\t\"" << state << "c" << row << "\" [shape = \"point\"";
outStream << "\t\"" << state << "c" << choice << "\" [shape = \"point\"";
// If we were given a scheduler to highlight, we do so now. // If we were given a scheduler to highlight, we do so now.
if (scheduler != nullptr) { if (scheduler != nullptr) {
@ -237,7 +226,7 @@ namespace storm {
} }
outStream << "];" << std::endl; outStream << "];" << std::endl;
outStream << "\t" << state << " -> \"" << state << "c" << row << "\"";
outStream << "\t" << state << " -> \"" << state << "c" << choice << "\"";
// If we were given a scheduler to highlight, we do so now. // If we were given a scheduler to highlight, we do so now.
if (scheduler != nullptr) { if (scheduler != nullptr) {
@ -250,9 +239,9 @@ namespace storm {
outStream << ";" << std::endl; outStream << ";" << std::endl;
// Now draw all probabilitic arcs that belong to this nondeterminstic choice. // Now draw all probabilitic arcs that belong to this nondeterminstic choice.
for (auto transitionIt = rowIt.begin(), transitionIte = rowIt.end(); transitionIt != transitionIte; ++transitionIt) {
if (subsystem == nullptr || subsystem->get(transitionIt.column())) {
outStream << "\t\"" << state << "c" << row << "\" -> " << transitionIt.column() << " [ label= \"" << transitionIt.value() << "\" ]";
for (auto const& transition : row) {
if (subsystem == nullptr || subsystem->get(transition.column())) {
outStream << "\t\"" << state << "c" << choice << "\" -> " << transition.column() << " [ label= \"" << transition.value() << "\" ]";
// If we were given a scheduler to highlight, we do so now. // If we were given a scheduler to highlight, we do so now.
if (scheduler != nullptr) { if (scheduler != nullptr) {

48
src/models/Dtmc.h

@ -159,19 +159,18 @@ public:
} }
// 1. Get all necessary information from the old transition matrix // 1. Get all necessary information from the old transition matrix
storm::storage::SparseMatrix<T> const & origMat = this->getTransitionMatrix();
storm::storage::SparseMatrix<T> const& origMat = this->getTransitionMatrix();
// Iterate over all rows. Count the number of all transitions from the old system to be // Iterate over all rows. Count the number of all transitions from the old system to be
// transfered to the new one. Also build a mapping from the state number of the old system // transfered to the new one. Also build a mapping from the state number of the old system
// to the state number of the new system. // to the state number of the new system.
uint_fast64_t subSysTransitionCount = 0; uint_fast64_t subSysTransitionCount = 0;
uint_fast64_t row = 0;
uint_fast64_t newRow = 0; uint_fast64_t newRow = 0;
std::vector<uint_fast64_t> stateMapping; std::vector<uint_fast64_t> stateMapping;
for(auto iter = origMat.begin(); iter != origMat.end(); ++iter) {
for(uint_fast64_t row = 0; row < origMat.getRowCount(); ++row) {
if(subSysStates.get(row)){ if(subSysStates.get(row)){
for(auto colIter = iter.begin(); colIter != iter.end(); ++colIter) {
if(subSysStates.get(colIter.column())) {
for(auto& entry : origMat.getRow(row)) {
if(subSysStates.get(entry.column())) {
subSysTransitionCount++; subSysTransitionCount++;
} }
} }
@ -180,7 +179,6 @@ public:
} else { } else {
stateMapping.push_back((uint_fast64_t) -1); stateMapping.push_back((uint_fast64_t) -1);
} }
row++;
} }
// 2. Construct transition matrix // 2. Construct transition matrix
@ -188,40 +186,37 @@ public:
// Take all states indicated by the vector as well as one additional state s_b as target of // Take all states indicated by the vector as well as one additional state s_b as target of
// all transitions that target a state that is not kept. // all transitions that target a state that is not kept.
uint_fast64_t const newStateCount = subSysStates.getNumberOfSetBits() + 1; uint_fast64_t const newStateCount = subSysStates.getNumberOfSetBits() + 1;
storm::storage::SparseMatrix<T> newMat(newStateCount);
// The number of transitions of the new Dtmc is the number of transitions transfered
// The number of transitions of the new Dtmc is the number of transitions transfered
// from the old one plus one transition for each state to s_b. // from the old one plus one transition for each state to s_b.
newMat.initialize(subSysTransitionCount + newStateCount);
storm::storage::SparseMatrix<T> newMat(newStateCount, subSysTransitionCount + newStateCount);
// Now fill the matrix. // Now fill the matrix.
newRow = 0; newRow = 0;
row = 0;
T rest = 0; T rest = 0;
for(auto iter = origMat.begin(); iter != origMat.end(); ++iter) {
for(uint_fast64_t row = 0; row < origMat.getRowCount(); ++row) {
if(subSysStates.get(row)){ if(subSysStates.get(row)){
// Transfer transitions // Transfer transitions
for(auto colIter = iter.begin(); colIter != iter.end(); ++colIter) {
if(subSysStates.get(colIter.column())) {
newMat.addNextValue(newRow, stateMapping[colIter.column()], colIter.value());
for(auto& entry : origMat.getRow(row)) {
if(subSysStates.get(entry.column())) {
newMat.addNextValue(newRow, stateMapping[entry.column()], entry.value());
} else { } else {
rest += colIter.value();
rest += entry.value();
} }
} }
// Insert the transition taking care of the remaining outgoing probability. // Insert the transition taking care of the remaining outgoing probability.
newMat.addNextValue(newRow, newStateCount - 1, rest); newMat.addNextValue(newRow, newStateCount - 1, rest);
rest = (T) 0;
rest = storm::utility::constantZero<T>();
newRow++; newRow++;
} }
row++;
} }
// Insert last transition: self loop on s_b // Insert last transition: self loop on s_b
newMat.addNextValue(newStateCount - 1, newStateCount - 1, (T) 1);
newMat.addNextValue(newStateCount - 1, newStateCount - 1, storm::utility::constantOne<T>());
newMat.finalize(false);
newMat.finalize();
// 3. Take care of the labeling. // 3. Take care of the labeling.
storm::models::AtomicPropositionsLabeling newLabeling = storm::models::AtomicPropositionsLabeling(this->getStateLabeling(), subSysStates); storm::models::AtomicPropositionsLabeling newLabeling = storm::models::AtomicPropositionsLabeling(this->getStateLabeling(), subSysStates);
@ -250,27 +245,24 @@ public:
boost::optional<storm::storage::SparseMatrix<T>> newTransitionRewards; boost::optional<storm::storage::SparseMatrix<T>> newTransitionRewards;
if(this->hasTransitionRewards()) { if(this->hasTransitionRewards()) {
storm::storage::SparseMatrix<T> newTransRewards(newStateCount);
newTransRewards.initialize(subSysTransitionCount + newStateCount);
storm::storage::SparseMatrix<T> newTransRewards(newStateCount, subSysTransitionCount + newStateCount);
// Copy the rewards for the kept states // Copy the rewards for the kept states
newRow = 0; newRow = 0;
row = 0;
for(auto iter = this->getTransitionRewardMatrix().begin(); iter != this->getTransitionRewardMatrix().end(); ++iter) {
for(uint_fast64_t row = 0; row < this->getTransitionRewardMatrix().getRowCount(); ++row) {
if(subSysStates.get(row)){ if(subSysStates.get(row)){
// Transfer transition rewards // Transfer transition rewards
for(auto colIter = iter.begin(); colIter != iter.end(); ++colIter) {
if(subSysStates.get(colIter.column())) {
newTransRewards.addNextValue(newRow, stateMapping[colIter.column()], colIter.value());
for(auto& entry : this->getTransitionRewardMatrix().getRow(row)) {
if(subSysStates.get(entry.column())) {
newTransRewards.addNextValue(newRow, stateMapping[entry.column()], entry.value());
} }
} }
// Insert the reward (e.g. 0) for the transition taking care of the remaining outgoing probability. // Insert the reward (e.g. 0) for the transition taking care of the remaining outgoing probability.
newTransRewards.addNextValue(newRow, newStateCount - 1, (T) 0);
newTransRewards.addNextValue(newRow, newStateCount - 1, storm::utility::constantZero<T>());
newRow++; newRow++;
} }
row++;
} }
newTransitionRewards = newTransRewards; newTransitionRewards = newTransRewards;

42
src/models/MarkovAutomaton.h

@ -127,8 +127,7 @@ namespace storm {
uint_fast64_t newNumberOfRows = this->getNumberOfChoices() - numberOfHybridStates; uint_fast64_t newNumberOfRows = this->getNumberOfChoices() - numberOfHybridStates;
// Create the matrix for the new transition relation and the corresponding nondeterministic choice vector. // Create the matrix for the new transition relation and the corresponding nondeterministic choice vector.
storm::storage::SparseMatrix<T> newTransitionMatrix(newNumberOfRows, this->getNumberOfStates());
newTransitionMatrix.initialize();
storm::storage::SparseMatrix<T> newTransitionMatrix;
std::vector<uint_fast64_t> newNondeterministicChoiceIndices(this->getNumberOfStates() + 1); std::vector<uint_fast64_t> newNondeterministicChoiceIndices(this->getNumberOfStates() + 1);
// Now copy over all choices that need to be kept. // Now copy over all choices that need to be kept.
@ -142,19 +141,15 @@ namespace storm {
// Record the new beginning of choices of this state. // Record the new beginning of choices of this state.
newNondeterministicChoiceIndices[state] = currentChoice; newNondeterministicChoiceIndices[state] = currentChoice;
typename storm::storage::SparseMatrix<T>::ConstRowIterator rowIt = this->transitionMatrix.begin(this->nondeterministicChoiceIndices[state]), rowIte = this->transitionMatrix.end(this->nondeterministicChoiceIndices[state + 1] - 1);
// If we are currently treating a hybrid state, we need to skip its first choice. // If we are currently treating a hybrid state, we need to skip its first choice.
if (this->isHybridState(state)) { if (this->isHybridState(state)) {
++rowIt;
// Remove the Markovian state marking. // Remove the Markovian state marking.
this->markovianStates.set(state, false); this->markovianStates.set(state, false);
} }
for (; rowIt != rowIte; ++rowIt) {
for (typename storm::storage::SparseMatrix<T>::ConstIterator succIt = rowIt.begin(), succIte = rowIt.end(); succIt != succIte; ++succIt) {
newTransitionMatrix.insertNextValue(currentChoice, succIt.column(), succIt.value());
for (uint_fast64_t row = this->nondeterministicChoiceIndices[state] + (this->isHybridState(state) ? 1 : 0); row < this->nondeterministicChoiceIndices[state + 1]; ++row) {
for (auto const& entry : this->transitionMatrix.getRow(row)) {
newTransitionMatrix.addNextValue(currentChoice, entry.column(), entry.value());
} }
++currentChoice; ++currentChoice;
} }
@ -194,16 +189,17 @@ namespace storm {
AbstractModel<T>::writeDotToStream(outStream, includeLabeling, subsystem, firstValue, secondValue, stateColoring, colors, scheduler, false); AbstractModel<T>::writeDotToStream(outStream, includeLabeling, subsystem, firstValue, secondValue, stateColoring, colors, scheduler, false);
// Write the probability distributions for all the states. // Write the probability distributions for all the states.
auto rowIt = this->transitionMatrix.begin();
for (uint_fast64_t state = 0, highestStateIndex = this->getNumberOfStates() - 1; state <= highestStateIndex; ++state) { for (uint_fast64_t state = 0, highestStateIndex = this->getNumberOfStates() - 1; state <= highestStateIndex; ++state) {
uint_fast64_t rowCount = this->getNondeterministicChoiceIndices()[state + 1] - this->getNondeterministicChoiceIndices()[state]; uint_fast64_t rowCount = this->getNondeterministicChoiceIndices()[state + 1] - this->getNondeterministicChoiceIndices()[state];
bool highlightChoice = true; bool highlightChoice = true;
// For this, we need to iterate over all available nondeterministic choices in the current state. // For this, we need to iterate over all available nondeterministic choices in the current state.
for (uint_fast64_t row = 0; row < rowCount; ++row, ++rowIt) {
for (uint_fast64_t choice = 0; choice < rowCount; ++choice) {
typename storm::storage::SparseMatrix<T>::const_rows row = this->transitionMatrix.getRow(choice);
if (scheduler != nullptr) { if (scheduler != nullptr) {
// If the scheduler picked the current choice, we will not make it dotted, but highlight it. // If the scheduler picked the current choice, we will not make it dotted, but highlight it.
if ((*scheduler)[state] == row) {
if ((*scheduler)[state] == choice) {
highlightChoice = true; highlightChoice = true;
} else { } else {
highlightChoice = false; highlightChoice = false;
@ -212,10 +208,10 @@ namespace storm {
// If it's not a Markovian state or the current row is the first choice for this state, then we // If it's not a Markovian state or the current row is the first choice for this state, then we
// are dealing with a probabilitic choice. // are dealing with a probabilitic choice.
if (!markovianStates.get(state) || row != 0) {
if (!markovianStates.get(state) || choice != 0) {
// For each nondeterministic choice, we draw an arrow to an intermediate node to better display // For each nondeterministic choice, we draw an arrow to an intermediate node to better display
// the grouping of transitions. // the grouping of transitions.
outStream << "\t\"" << state << "c" << row << "\" [shape = \"point\"";
outStream << "\t\"" << state << "c" << choice << "\" [shape = \"point\"";
// If we were given a scheduler to highlight, we do so now. // If we were given a scheduler to highlight, we do so now.
if (scheduler != nullptr) { if (scheduler != nullptr) {
@ -225,7 +221,7 @@ namespace storm {
} }
outStream << "];" << std::endl; outStream << "];" << std::endl;
outStream << "\t" << state << " -> \"" << state << "c" << row << "\"";
outStream << "\t" << state << " -> \"" << state << "c" << choice << "\"";
// If we were given a scheduler to highlight, we do so now. // If we were given a scheduler to highlight, we do so now.
if (scheduler != nullptr) { if (scheduler != nullptr) {
@ -238,9 +234,9 @@ namespace storm {
outStream << ";" << std::endl; outStream << ";" << std::endl;
// Now draw all probabilitic arcs that belong to this nondeterminstic choice. // Now draw all probabilitic arcs that belong to this nondeterminstic choice.
for (auto transitionIt = rowIt.begin(), transitionIte = rowIt.end(); transitionIt != transitionIte; ++transitionIt) {
if (subsystem == nullptr || subsystem->get(transitionIt.column())) {
outStream << "\t\"" << state << "c" << row << "\" -> " << transitionIt.column() << " [ label= \"" << transitionIt.value() << "\" ]";
for (auto& transition : row) {
if (subsystem == nullptr || subsystem->get(transition.column())) {
outStream << "\t\"" << state << "c" << choice << "\" -> " << transition.column() << " [ label= \"" << transition.value() << "\" ]";
// If we were given a scheduler to highlight, we do so now. // If we were given a scheduler to highlight, we do so now.
if (scheduler != nullptr) { if (scheduler != nullptr) {
@ -255,9 +251,9 @@ namespace storm {
} }
} else { } else {
// In this case we are emitting a Markovian choice, so draw the arrows directly to the target states. // In this case we are emitting a Markovian choice, so draw the arrows directly to the target states.
for (auto transitionIt = rowIt.begin(), transitionIte = rowIt.end(); transitionIt != transitionIte; ++transitionIt) {
if (subsystem == nullptr || subsystem->get(transitionIt.column())) {
outStream << "\t\"" << state << "\" -> " << transitionIt.column() << " [ label= \"" << transitionIt.value() << " (" << this->exitRates[state] << ")\" ]";
for (auto& transition : row) {
if (subsystem == nullptr || subsystem->get(transition.column())) {
outStream << "\t\"" << state << "\" -> " << transition.column() << " [ label= \"" << transition.value() << " (" << this->exitRates[state] << ")\" ]";
} }
} }
} }
@ -276,8 +272,8 @@ namespace storm {
*/ */
void turnRatesToProbabilities() { void turnRatesToProbabilities() {
for (auto state : this->markovianStates) { for (auto state : this->markovianStates) {
for (typename storm::storage::SparseMatrix<T>::ValueIterator valIt = this->transitionMatrix.valueIteratorBegin(this->getNondeterministicChoiceIndices()[state]), valIte = this->transitionMatrix.valueIteratorEnd(this->getNondeterministicChoiceIndices()[state]); valIt != valIte; ++valIt) {
*valIt = *valIt / this->exitRates[state];
for (typename storm::storage::SparseMatrix<T>::iterator it = this->transitionMatrix.begin(this->getNondeterministicChoiceIndices()[state]), ite = this->transitionMatrix.begin(this->getNondeterministicChoiceIndices()[state + 1]); it != ite; ++it) {
it.value() /= this->exitRates[state];
} }
} }
} }

10
src/models/Mdp.h

@ -144,7 +144,6 @@ public:
std::vector<storm::storage::VectorSet<uint_fast64_t>> const& choiceLabeling = this->getChoiceLabeling(); std::vector<storm::storage::VectorSet<uint_fast64_t>> const& choiceLabeling = this->getChoiceLabeling();
storm::storage::SparseMatrix<T> transitionMatrix; storm::storage::SparseMatrix<T> transitionMatrix;
transitionMatrix.initialize();
std::vector<uint_fast64_t> nondeterministicChoiceIndices; std::vector<uint_fast64_t> nondeterministicChoiceIndices;
std::vector<storm::storage::VectorSet<uint_fast64_t>> newChoiceLabeling; std::vector<storm::storage::VectorSet<uint_fast64_t>> newChoiceLabeling;
@ -161,9 +160,8 @@ public:
nondeterministicChoiceIndices.push_back(currentRow); nondeterministicChoiceIndices.push_back(currentRow);
} }
stateHasValidChoice = true; stateHasValidChoice = true;
typename storm::storage::SparseMatrix<T>::Rows row = this->getTransitionMatrix().getRows(choice, choice);
for (typename storm::storage::SparseMatrix<T>::ConstIterator rowIt = row.begin(), rowIte = row.end(); rowIt != rowIte; ++rowIt) {
transitionMatrix.insertNextValue(currentRow, rowIt.column(), rowIt.value(), true);
for (auto const& entry : this->getTransitionMatrix().getRow(choice)) {
transitionMatrix.addNextValue(currentRow, entry.column(), entry.value());
} }
newChoiceLabeling.emplace_back(choiceLabeling[choice]); newChoiceLabeling.emplace_back(choiceLabeling[choice]);
++currentRow; ++currentRow;
@ -173,12 +171,12 @@ public:
// If no choice of the current state may be taken, we insert a self-loop to the state instead. // If no choice of the current state may be taken, we insert a self-loop to the state instead.
if (!stateHasValidChoice) { if (!stateHasValidChoice) {
nondeterministicChoiceIndices.push_back(currentRow); nondeterministicChoiceIndices.push_back(currentRow);
transitionMatrix.insertNextValue(currentRow, state, storm::utility::constantOne<T>(), true);
transitionMatrix.addNextValue(currentRow, state, storm::utility::constantOne<T>());
newChoiceLabeling.emplace_back(); newChoiceLabeling.emplace_back();
++currentRow; ++currentRow;
} }
} }
transitionMatrix.finalize(true);
transitionMatrix.finalize();
nondeterministicChoiceIndices.push_back(currentRow); nondeterministicChoiceIndices.push_back(currentRow);
Mdp<T> restrictedMdp(std::move(transitionMatrix), storm::models::AtomicPropositionsLabeling(this->getStateLabeling()), std::move(nondeterministicChoiceIndices), this->hasStateRewards() ? boost::optional<std::vector<T>>(this->getStateRewardVector()) : boost::optional<std::vector<T>>(), this->hasTransitionRewards() ? boost::optional<storm::storage::SparseMatrix<T>>(this->getTransitionRewardMatrix()) : boost::optional<storm::storage::SparseMatrix<T>>(), boost::optional<std::vector<storm::storage::VectorSet<uint_fast64_t>>>(newChoiceLabeling)); Mdp<T> restrictedMdp(std::move(transitionMatrix), storm::models::AtomicPropositionsLabeling(this->getStateLabeling()), std::move(nondeterministicChoiceIndices), this->hasStateRewards() ? boost::optional<std::vector<T>>(this->getStateRewardVector()) : boost::optional<std::vector<T>>(), this->hasTransitionRewards() ? boost::optional<storm::storage::SparseMatrix<T>>(this->getTransitionRewardMatrix()) : boost::optional<storm::storage::SparseMatrix<T>>(), boost::optional<std::vector<storm::storage::VectorSet<uint_fast64_t>>>(newChoiceLabeling));

7
src/parser/DeterministicSparseTransitionParser.cpp

@ -201,12 +201,7 @@ storm::storage::SparseMatrix<double> DeterministicSparseTransitionParser(std::st
* The number of non-zero elements is computed by firstPass(). * The number of non-zero elements is computed by firstPass().
*/ */
LOG4CPLUS_INFO(logger, "Attempting to create matrix of size " << (maxStateId+1) << " x " << (maxStateId+1) << "."); LOG4CPLUS_INFO(logger, "Attempting to create matrix of size " << (maxStateId+1) << " x " << (maxStateId+1) << ".");
storm::storage::SparseMatrix<double> resultMatrix(maxStateId + 1);
resultMatrix.initialize(nonZeroEntryCount);
if (!resultMatrix.isInitialized()) {
LOG4CPLUS_ERROR(logger, "Could not create matrix of size " << (maxStateId+1) << " x " << (maxStateId+1) << ".");
throw std::bad_alloc();
}
storm::storage::SparseMatrix<double> resultMatrix(maxStateId + 1, nonZeroEntryCount);
int_fast64_t row, lastRow = -1, col; int_fast64_t row, lastRow = -1, col;
double val; double val;

3
src/parser/MarkovAutomatonSparseTransitionParser.h

@ -39,8 +39,7 @@ namespace storm {
*/ */
struct ResultType { struct ResultType {
ResultType(FirstPassResult const& firstPassResult) : transitionMatrix(firstPassResult.numberOfChoices, firstPassResult.highestStateIndex + 1), nondeterministicChoiceIndices(firstPassResult.highestStateIndex + 2), markovianChoices(firstPassResult.numberOfChoices), markovianStates(firstPassResult.highestStateIndex + 1), exitRates(firstPassResult.highestStateIndex + 1) {
transitionMatrix.initialize(firstPassResult.numberOfNonzeroEntries);
ResultType(FirstPassResult const& firstPassResult) : transitionMatrix(firstPassResult.numberOfChoices, firstPassResult.highestStateIndex + 1, firstPassResult.numberOfNonzeroEntries), nondeterministicChoiceIndices(firstPassResult.highestStateIndex + 2), markovianChoices(firstPassResult.numberOfChoices), markovianStates(firstPassResult.highestStateIndex + 1), exitRates(firstPassResult.highestStateIndex + 1) {
// Intentionally left empty. // Intentionally left empty.
} }

8
src/parser/NondeterministicSparseTransitionParser.cpp

@ -264,13 +264,7 @@ NondeterministicSparseTransitionParserResult_t NondeterministicSparseTransitionP
* Those two values, as well as the number of nonzero elements, was been calculated in the first run. * 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 " << choices << " x " << (maxnode+1) << " with " << nonzero << " entries."); LOG4CPLUS_INFO(logger, "Attempting to create matrix of size " << choices << " x " << (maxnode+1) << " with " << nonzero << " entries.");
storm::storage::SparseMatrix<double> matrix(choices, maxnode + 1);
matrix.initialize(nonzero);
if (!matrix.isInitialized()) {
LOG4CPLUS_ERROR(logger, "Could not create matrix of size " << choices << " x " << (maxnode+1) << ".");
throw std::bad_alloc();
}
storm::storage::SparseMatrix<double> matrix(choices, maxnode + 1, nonzero);
/* /*
* Create row mapping. * Create row mapping.

11
src/solver/AbstractNondeterministicLinearEquationSolver.h

@ -80,8 +80,7 @@ namespace storm {
* @returns The solution vector x of the system of linear equations as the content of the parameter x. * @returns The solution vector x of the system of linear equations as the content of the parameter x.
*/ */
virtual void solveEquationSystem(bool minimize, storm::storage::SparseMatrix<Type> const& A, std::vector<Type>& x, std::vector<Type> const& b, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, std::vector<Type>* multiplyResult = nullptr, std::vector<Type>* newX = nullptr) const { virtual void solveEquationSystem(bool minimize, storm::storage::SparseMatrix<Type> const& A, std::vector<Type>& x, std::vector<Type> const& b, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, std::vector<Type>* multiplyResult = nullptr, std::vector<Type>* newX = nullptr) const {
// LOG4CPLUS_INFO(logger, "Starting iterative solver.");
// Set up the environment for the power method. // Set up the environment for the power method.
bool multiplyResultMemoryProvided = true; bool multiplyResultMemoryProvided = true;
if (multiplyResult == nullptr) { if (multiplyResult == nullptr) {
@ -137,14 +136,6 @@ namespace storm {
if (!multiplyResultMemoryProvided) { if (!multiplyResultMemoryProvided) {
delete multiplyResult; delete multiplyResult;
} }
// // Check if the solver converged and issue a warning otherwise.
// if (converged) {
// LOG4CPLUS_INFO(logger, "Iterative solver converged after " << iterations << " iterations.");
// } else {
// LOG4CPLUS_WARN(logger, "Iterative solver did not converge.");
// }
} }
protected: protected:

14
src/storage/MaximalEndComponentDecomposition.cpp

@ -82,8 +82,8 @@ namespace storm {
for (uint_fast64_t choice = nondeterministicChoiceIndices[state]; choice < nondeterministicChoiceIndices[state + 1]; ++choice) { for (uint_fast64_t choice = nondeterministicChoiceIndices[state]; choice < nondeterministicChoiceIndices[state + 1]; ++choice) {
bool choiceContainedInMEC = true; bool choiceContainedInMEC = true;
for (typename storm::storage::SparseMatrix<ValueType>::ConstIndexIterator successorIt = transitionMatrix.constColumnIteratorBegin(choice), successorIte = transitionMatrix.constColumnIteratorEnd(choice); successorIt != successorIte; ++successorIt) {
if (!scc.contains(*successorIt)) {
for (auto& entry : transitionMatrix.getRow(choice)) {
if (!scc.contains(entry.column())) {
choiceContainedInMEC = false; choiceContainedInMEC = false;
break; break;
} }
@ -108,9 +108,9 @@ namespace storm {
// Now check which states should be reconsidered, because successors of them were removed. // Now check which states should be reconsidered, because successors of them were removed.
statesToCheck.clear(); statesToCheck.clear();
for (auto state : statesToRemove) { for (auto state : statesToRemove) {
for (typename storm::storage::SparseMatrix<ValueType>::ConstIndexIterator predIt = backwardTransitions.constColumnIteratorBegin(state), predIte = backwardTransitions.constColumnIteratorEnd(state); predIt != predIte; ++predIt) {
if (scc.contains(*predIt)) {
statesToCheck.set(*predIt);
for (auto& entry : transitionMatrix.getRow(state)) {
if (scc.contains(entry.column())) {
statesToCheck.set(entry.column());
} }
} }
} }
@ -144,8 +144,8 @@ namespace storm {
std::vector<uint_fast64_t> containedChoices; std::vector<uint_fast64_t> containedChoices;
for (uint_fast64_t choice = nondeterministicChoiceIndices[state]; choice < nondeterministicChoiceIndices[state + 1]; ++choice) { for (uint_fast64_t choice = nondeterministicChoiceIndices[state]; choice < nondeterministicChoiceIndices[state + 1]; ++choice) {
bool choiceContained = true; bool choiceContained = true;
for (typename storm::storage::SparseMatrix<ValueType>::ConstIndexIterator successorIt = transitionMatrix.constColumnIteratorBegin(choice), successorIte = transitionMatrix.constColumnIteratorEnd(choice); successorIt != successorIte; ++successorIt) {
if (!mecStateSet.contains(*successorIt)) {
for (auto& entry : transitionMatrix.getRow(choice)) {
if (!mecStateSet.contains(entry.column())) {
choiceContained = false; choiceContained = false;
break; break;
} }

332
src/storage/SparseMatrix.cpp

@ -101,7 +101,7 @@ namespace storm {
} }
template<typename T> template<typename T>
SparseMatrix<T>::SparseMatrix(uint_fast64_t rows, uint_fast64_t columns, uint_fast64_t entries) : rowCount(rows), columnCount(columns), entryCount(entries), internalStatus(UNINITIALIZED), valueStorage(), columnIndications(), rowIndications(), currentEntryCount(0), lastRow(0), lastColumn(0) {
SparseMatrix<T>::SparseMatrix(uint_fast64_t rows, uint_fast64_t columns, uint_fast64_t entries) : rowCount(rows), columnCount(columns), entryCount(entries), valueStorage(), columnIndications(), rowIndications(), internalStatus(UNINITIALIZED), currentEntryCount(0), lastRow(0), lastColumn(0) {
storagePreallocated = rows != 0 && columns != 0 && entries != 0; storagePreallocated = rows != 0 && columns != 0 && entries != 0;
prepareInternalStorage(); prepareInternalStorage();
} }
@ -128,6 +128,11 @@ namespace storm {
other.lastRow = 0; other.lastRow = 0;
other.lastColumn = 0; other.lastColumn = 0;
} }
template<typename T>
SparseMatrix<T>::SparseMatrix(uint_fast64_t columnCount, std::vector<uint_fast64_t> const& rowIndications, std::vector<uint_fast64_t> const& columnIndications, std::vector<T> const& values) : rowCount(rowIndications.size() - 1), columnCount(columnCount), entryCount(values.size()), valueStorage(values), columnIndications(columnIndications), rowIndications(rowIndications), internalStatus(INITIALIZED), currentEntryCount(0), lastRow(0), lastColumn(0) {
// Intentionally left empty.
}
template<typename T> template<typename T>
SparseMatrix<T>::SparseMatrix(uint_fast64_t columnCount, std::vector<uint_fast64_t>&& rowIndications, std::vector<uint_fast64_t>&& columnIndications, std::vector<T>&& values) : rowCount(rowIndications.size() - 1), columnCount(columnCount), entryCount(values.size()), valueStorage(std::move(values)), columnIndications(std::move(columnIndications)), rowIndications(std::move(rowIndications)), internalStatus(INITIALIZED), currentEntryCount(0), lastRow(0), lastColumn(0) { SparseMatrix<T>::SparseMatrix(uint_fast64_t columnCount, std::vector<uint_fast64_t>&& rowIndications, std::vector<uint_fast64_t>&& columnIndications, std::vector<T>&& values) : rowCount(rowIndications.size() - 1), columnCount(columnCount), entryCount(values.size()), valueStorage(std::move(values)), columnIndications(std::move(columnIndications)), rowIndications(std::move(rowIndications)), internalStatus(INITIALIZED), currentEntryCount(0), lastRow(0), lastColumn(0) {
@ -155,6 +160,27 @@ namespace storm {
return *this; return *this;
} }
template<typename T>
SparseMatrix<T>& SparseMatrix<T>::operator=(SparseMatrix<T>&& other) {
// Only perform assignment if source and target are not the same.
if (this != &other) {
rowCount = other.rowCount;
columnCount = other.columnCount;
entryCount = other.entryCount;
valueStorage = std::move(other.valueStorage);
columnIndications = std::move(other.columnIndications);
rowIndications = std::move(other.rowIndications);
internalStatus = other.internalStatus;
currentEntryCount = other.currentEntryCount;
lastRow = other.lastRow;
lastColumn = other.lastColumn;
}
return *this;
}
template<typename T> template<typename T>
void SparseMatrix<T>::addNextValue(uint_fast64_t row, uint_fast64_t column, T const& value) { void SparseMatrix<T>::addNextValue(uint_fast64_t row, uint_fast64_t column, T const& value) {
// Depending on whether the internal data storage was preallocated or not, adding the value is done somewhat // Depending on whether the internal data storage was preallocated or not, adding the value is done somewhat
@ -168,12 +194,12 @@ namespace storm {
// Check that we did not move backwards wrt. the row. // Check that we did not move backwards wrt. the row.
if (row < lastRow) { if (row < lastRow) {
throw storm::exceptions::InvalidArgumentException() << "Illegal call to SparseMatrix::addNextValue: adding an element in row " << row << ", but an element in row " << lastRow << " has already been added." << std::endl;
throw storm::exceptions::InvalidArgumentException() << "Illegal call to SparseMatrix::addNextValue: adding an element in row " << row << ", but an element in row " << lastRow << " has already been added.";
} }
// Check that we did not move backwards wrt. to column. // Check that we did not move backwards wrt. to column.
if (row == lastRow && column < lastColumn) { if (row == lastRow && column < lastColumn) {
throw storm::exceptions::InvalidArgumentException() << "Illegal call to SparseMatrix::addNextValue: adding an element in column " << column << " in row " << row << ", but an element in column " << lastColumn << " has already been added in that row." << std::endl;
throw storm::exceptions::InvalidArgumentException() << "Illegal call to SparseMatrix::addNextValue: adding an element in column " << column << " in row " << row << ", but an element in column " << lastColumn << " has already been added in that row.";
} }
// If we switched to another row, we have to adjust the missing entries in the row indices vector. // If we switched to another row, we have to adjust the missing entries in the row indices vector.
@ -203,6 +229,8 @@ namespace storm {
} else { } else {
valueStorage.push_back(value); valueStorage.push_back(value);
columnIndications.push_back(column); columnIndications.push_back(column);
columnCount = column + 1;
rowCount = row + 1;
} }
} }
@ -295,6 +323,8 @@ namespace storm {
// one given by the parameter and set all subsequent elements of this row to zero. // one given by the parameter and set all subsequent elements of this row to zero.
*valuePtr = storm::utility::constantOne<T>(); *valuePtr = storm::utility::constantOne<T>();
*columnPtr = column; *columnPtr = column;
++valuePtr;
++columnPtr;
for (; valuePtr != valuePtrEnd; ++valuePtr) { for (; valuePtr != valuePtrEnd; ++valuePtr) {
*valuePtr = storm::utility::constantZero<T>(); *valuePtr = storm::utility::constantZero<T>();
*columnPtr = 0; *columnPtr = 0;
@ -531,7 +561,7 @@ namespace storm {
uint_fast64_t rowCount = this->columnCount; uint_fast64_t rowCount = this->columnCount;
uint_fast64_t columnCount = this->rowCount; uint_fast64_t columnCount = this->rowCount;
uint_fast64_t entryCount = this->nonZeroEntryCount;
uint_fast64_t entryCount = this->entryCount;
std::vector<uint_fast64_t> rowIndications(rowCount + 1); std::vector<uint_fast64_t> rowIndications(rowCount + 1);
std::vector<uint_fast64_t> columnIndications(entryCount); std::vector<uint_fast64_t> columnIndications(entryCount);
@ -539,8 +569,7 @@ namespace storm {
// First, we need to count how many entries each column has. // First, we need to count how many entries each column has.
for (uint_fast64_t i = 0; i < this->rowCount; ++i) { for (uint_fast64_t i = 0; i < this->rowCount; ++i) {
typename storm::storage::SparseMatrix<T>::Rows rows = this->getRow(i);
for (auto const& transition : rows) {
for (auto const& transition : this->getRow(i)) {
if (transition.value() > 0) { if (transition.value() > 0) {
++rowIndications[transition.column() + 1]; ++rowIndications[transition.column() + 1];
} }
@ -559,8 +588,7 @@ namespace storm {
// Now we are ready to actually fill in the values of the transposed matrix. // Now we are ready to actually fill in the values of the transposed matrix.
for (uint_fast64_t i = 0; i < this->rowCount; ++i) { for (uint_fast64_t i = 0; i < this->rowCount; ++i) {
typename storm::storage::SparseMatrix<T>::Rows rows = this->getRow(i);
for (auto& transition : rows) {
for (auto& transition : this->getRow(i)) {
if (transition.value() > 0) { if (transition.value() > 0) {
values[nextIndices[transition.column()]] = transition.value(); values[nextIndices[transition.column()]] = transition.value();
columnIndications[nextIndices[transition.column()]++] = i; columnIndications[nextIndices[transition.column()]++] = i;
@ -568,11 +596,7 @@ namespace storm {
} }
} }
storm::storage::SparseMatrix<T> transposedMatrix(rowCount, colCount,
nonZeroEntryCount,
std::move(rowIndications),
std::move(columnIndications),
std::move(values));
storm::storage::SparseMatrix<T> transposedMatrix(columnCount, std::move(rowIndications), std::move(columnIndications), std::move(values));
return transposedMatrix; return transposedMatrix;
} }
@ -616,11 +640,10 @@ namespace storm {
} }
template<typename T> template<typename T>
void SparseMatrix<T>::negateAllNonDiagonalElements() {
// Check if the matrix is square, because only then it makes sense to perform this
// transformation.
void SparseMatrix<T>::negateAllNonDiagonalEntries() {
// Check if the matrix is square, because only then it makes sense to perform this transformation.
if (this->getRowCount() != this->getColumnCount()) { if (this->getRowCount() != this->getColumnCount()) {
throw storm::exceptions::InvalidArgumentException() << "SparseMatrix::invertDiagonal requires the Matrix to be square!";
throw storm::exceptions::InvalidArgumentException() << "Illegal call to SparseMatrix::invertDiagonal: matrix is non-square.";
} }
// Iterate over all rows and negate all the elements that are not on the diagonal. // Iterate over all rows and negate all the elements that are not on the diagonal.
@ -629,7 +652,27 @@ namespace storm {
uint_fast64_t rowEnd = rowIndications[row + 1]; uint_fast64_t rowEnd = rowIndications[row + 1];
while (rowStart < rowEnd) { while (rowStart < rowEnd) {
if (columnIndications[rowStart] != row) { if (columnIndications[rowStart] != row) {
valueStorage[rowStart] = - valueStorage[rowStart];
valueStorage[rowStart] = -valueStorage[rowStart];
}
++rowStart;
}
}
}
template<typename T>
void SparseMatrix<T>::deleteDiagonalEntries() {
// Check if the matrix is square, because only then it makes sense to perform this transformation.
if (this->getRowCount() != this->getColumnCount()) {
throw storm::exceptions::InvalidArgumentException() << "Illegal call to SparseMatrix::deleteDiagonalEntries: matrix is non-square.";
}
// Iterate over all rows and negate all the elements that are not on the diagonal.
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] = storm::utility::constantZero<T>();
} }
++rowStart; ++rowStart;
} }
@ -638,23 +681,28 @@ namespace storm {
template<typename T> template<typename T>
typename std::pair<storm::storage::SparseMatrix<T>, storm::storage::SparseMatrix<T>> SparseMatrix<T>::getJacobiDecomposition() const { typename std::pair<storm::storage::SparseMatrix<T>, storm::storage::SparseMatrix<T>> SparseMatrix<T>::getJacobiDecomposition() const {
uint_fast64_t rowCount = this->getRowCount();
uint_fast64_t colCount = this->getColumnCount();
if (rowCount != colCount) {
throw storm::exceptions::InvalidArgumentException() << "SparseMatrix::getJacobiDecomposition requires the Matrix to be square.";
if (rowCount != columnCount) {
throw storm::exceptions::InvalidArgumentException() << "Illegal call to SparseMatrix::invertDiagonal: matrix is non-square.";
} }
storm::storage::SparseMatrix<T> resultLU(*this); storm::storage::SparseMatrix<T> resultLU(*this);
storm::storage::SparseMatrix<T> resultDinv(rowCount, colCount);
// no entries apart from those on the diagonal (rowCount)
resultDinv.initialize(rowCount);
resultLU.deleteDiagonalEntries();
// constant 1 for diagonal inversion
T constOne = storm::utility::constantOne<T>();
storm::storage::SparseMatrix<T> resultDinv(rowCount, columnCount, rowCount);
// copy diagonal entries to other matrix
for (uint_fast64_t i = 0; i < rowCount; ++i) {
resultDinv.addNextValue(i, i, constOne / resultLU.getValue(i, i));
resultLU.getValue(i, i) = storm::utility::constantZero<T>();
// Copy entries to the appropriate matrices.
for (uint_fast64_t rowNumber = 0; rowNumber < rowCount; ++rowNumber) {
// Because the matrix may have several entries on the diagonal, we need to sum them before we are able
// to invert the entry.
T diagonalValue = storm::utility::constantZero<T>();
for (const_iterator rowIt = this->begin(rowNumber), rowIte = this->end(rowNumber); rowIt != rowIte; ++rowIt) {
if (rowIt.column() == rowNumber) {
diagonalValue += rowIt.value();
} else if (rowIt.column() > rowNumber) {
break;
}
}
resultDinv.addNextValue(rowNumber, rowNumber, storm::utility::constantOne<T>() / diagonalValue);
} }
resultDinv.finalize(); resultDinv.finalize();
@ -663,12 +711,11 @@ namespace storm {
template<typename T> template<typename T>
std::vector<T> SparseMatrix<T>::getPointwiseProductRowSumVector(storm::storage::SparseMatrix<T> const& otherMatrix) const { std::vector<T> SparseMatrix<T>::getPointwiseProductRowSumVector(storm::storage::SparseMatrix<T> const& otherMatrix) const {
// Prepare result.
std::vector<T> result(rowCount, storm::utility::constantZero<T>()); std::vector<T> result(rowCount, storm::utility::constantZero<T>());
// Iterate over all elements of the current matrix and either continue with the next element
// 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.
// Iterate over all elements of the current matrix and either continue with the next element 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) { for (uint_fast64_t row = 0; row < rowCount && row < otherMatrix.rowCount; ++row) {
for (uint_fast64_t element = rowIndications[row], nextOtherElement = otherMatrix.rowIndications[row]; element < rowIndications[row + 1] && nextOtherElement < otherMatrix.rowIndications[row + 1]; ++element) { 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]) { if (columnIndications[element] < otherMatrix.columnIndications[nextOtherElement]) {
@ -692,13 +739,19 @@ namespace storm {
#ifdef STORM_HAVE_INTELTBB #ifdef STORM_HAVE_INTELTBB
tbb::parallel_for(tbb::blocked_range<uint_fast64_t>(0, result.size()), tbbHelper_MatrixRowVectorScalarProduct<storm::storage::SparseMatrix<T>, std::vector<T>, T>(this, &vector, &result)); tbb::parallel_for(tbb::blocked_range<uint_fast64_t>(0, result.size()), tbbHelper_MatrixRowVectorScalarProduct<storm::storage::SparseMatrix<T>, std::vector<T>, T>(this, &vector, &result));
#else #else
ConstRowIterator rowIt = this->begin();
for (auto resultIt = result.begin(), resultIte = result.end(); resultIt != resultIte; ++resultIt, ++rowIt) {
*resultIt = storm::utility::constantZero<T>();
typename std::vector<T>::const_iterator valueIterator = valueStorage.begin();
typename std::vector<T>::const_iterator valueIteratorEnd;
typename std::vector<uint_fast64_t>::const_iterator columnIterator = columnIndications.begin();
typename std::vector<uint_fast64_t>::const_iterator rowIterator = rowIndications.begin();
typename std::vector<uint_fast64_t>::const_iterator rowIteratorEnd = rowIndications.end();
typename std::vector<T>::iterator resultIterator = result.begin();
typename std::vector<T>::iterator resultIteratorEnd = result.end();
for (; resultIterator != resultIteratorEnd; ++rowIterator, ++resultIterator) {
*resultIterator = storm::utility::constantZero<T>();
for (auto elementIt = rowIt.begin(), elementIte = rowIt.end(); elementIt != elementIte; ++elementIt) {
*resultIt += elementIt.value() * vector[elementIt.column()];
for (valueIteratorEnd = valueIterator + (*(rowIterator + 1) - *rowIterator); valueIterator != valueIteratorEnd; ++valueIterator, ++columnIterator) {
*resultIterator += *valueIterator * vector[*columnIterator];
} }
} }
#endif #endif
@ -707,95 +760,74 @@ namespace storm {
template<typename T> template<typename T>
uint_fast64_t SparseMatrix<T>::getSizeInMemory() const { uint_fast64_t SparseMatrix<T>::getSizeInMemory() const {
uint_fast64_t size = sizeof(*this); uint_fast64_t size = sizeof(*this);
// Add value_storage size. // Add value_storage size.
size += sizeof(T) * valueStorage.capacity(); size += sizeof(T) * valueStorage.capacity();
// Add column_indications size. // Add column_indications size.
size += sizeof(uint_fast64_t) * columnIndications.capacity(); size += sizeof(uint_fast64_t) * columnIndications.capacity();
// Add row_indications size. // Add row_indications size.
size += sizeof(uint_fast64_t) * rowIndications.capacity(); size += sizeof(uint_fast64_t) * rowIndications.capacity();
return size; return size;
} }
template<typename T> template<typename T>
typename SparseMatrix<T>::Rows SparseMatrix<T>::getRows(uint_fast64_t startRow, uint_fast64_t endRow) const {
return Rows(this->valueStorage.data() + this->rowIndications[startRow], this->columnIndications.data() + this->rowIndications[startRow], this->rowIndications[endRow + 1] - this->rowIndications[startRow]);
}
template<typename T>
typename SparseMatrix<T>::MutableRows SparseMatrix<T>::getMutableRows(uint_fast64_t startRow, uint_fast64_t endRow) {
return MutableRows(this->valueStorage.data() + this->rowIndications[startRow], this->columnIndications.data() + this->rowIndications[startRow], this->rowIndications[endRow + 1] - this->rowIndications[startRow]);
typename SparseMatrix<T>::const_rows SparseMatrix<T>::getRows(uint_fast64_t startRow, uint_fast64_t endRow) const {
return const_rows(this->valueStorage.data() + this->rowIndications[startRow], this->columnIndications.data() + this->rowIndications[startRow], this->rowIndications[endRow + 1] - this->rowIndications[startRow]);
} }
template<typename T> template<typename T>
typename SparseMatrix<T>::MutableRows SparseMatrix<T>::getMutableRow(uint_fast64_t row) {
return getMutableRows(row, row);
typename SparseMatrix<T>::rows SparseMatrix<T>::getRows(uint_fast64_t startRow, uint_fast64_t endRow) {
return rows(this->valueStorage.data() + this->rowIndications[startRow], this->columnIndications.data() + this->rowIndications[startRow], this->rowIndications[endRow + 1] - this->rowIndications[startRow]);
} }
template<typename T> template<typename T>
typename SparseMatrix<T>::Rows SparseMatrix<T>::getRow(uint_fast64_t row) const {
typename SparseMatrix<T>::const_rows SparseMatrix<T>::getRow(uint_fast64_t row) const {
return getRows(row, row); return getRows(row, row);
} }
template<typename T>
typename SparseMatrix<T>::ConstRowIterator SparseMatrix<T>::begin(uint_fast64_t initialRow) const {
return ConstRowIterator(this->valueStorage.data(), this->columnIndications.data(), this->rowIndications.data() + initialRow);
}
template<typename T>
typename SparseMatrix<T>::ConstRowIterator SparseMatrix<T>::end() const {
return ConstRowIterator(this->valueStorage.data(), this->columnIndications.data(), this->rowIndications.data() + rowCount);
}
template<typename T>
typename SparseMatrix<T>::ConstRowIterator SparseMatrix<T>::end(uint_fast64_t row) const {
return ConstRowIterator(this->valueStorage.data(), this->columnIndications.data(), this->rowIndications.data() + row + 1);
}
template<typename T>
typename SparseMatrix<T>::ConstIndexIterator SparseMatrix<T>::constColumnIteratorBegin(uint_fast64_t row) const {
return &(this->columnIndications[0]) + this->rowIndications[row];
}
template<typename T> template<typename T>
typename SparseMatrix<T>::ConstIndexIterator SparseMatrix<T>::constColumnIteratorEnd() const {
return &(this->columnIndications[0]) + this->rowIndications[rowCount];
typename SparseMatrix<T>::rows SparseMatrix<T>::getRow(uint_fast64_t row) {
return getRows(row, row);
} }
template<typename T> template<typename T>
typename SparseMatrix<T>::ConstIndexIterator SparseMatrix<T>::constColumnIteratorEnd(uint_fast64_t row) const {
return &(this->columnIndications[0]) + this->rowIndications[row + 1];
typename SparseMatrix<T>::const_iterator SparseMatrix<T>::begin(uint_fast64_t row) const {
return const_iterator(this->valueStorage.data() + this->rowIndications[row], this->columnIndications.data() + this->rowIndications[row]);
} }
template<typename T> template<typename T>
typename SparseMatrix<T>::ConstValueIterator SparseMatrix<T>::constValueIteratorBegin(uint_fast64_t row) const {
return &(this->valueStorage[0]) + this->rowIndications[row];
typename SparseMatrix<T>::iterator SparseMatrix<T>::begin(uint_fast64_t row) {
return iterator(this->valueStorage.data() + this->rowIndications[row], this->columnIndications.data() + this->rowIndications[row]);
} }
template<typename T> template<typename T>
typename SparseMatrix<T>::ConstValueIterator SparseMatrix<T>::constValueIteratorEnd() const {
return &(this->valueStorage[0]) + this->rowIndications[rowCount];
typename SparseMatrix<T>::const_iterator SparseMatrix<T>::end(uint_fast64_t row) const {
return const_iterator(this->valueStorage.data() + this->rowIndications[row + 1], this->columnIndications.data() + this->rowIndications[row + 1]);
} }
template<typename T> template<typename T>
typename SparseMatrix<T>::ConstValueIterator SparseMatrix<T>::constValueIteratorEnd(uint_fast64_t row) const {
return &(this->valueStorage[0]) + this->rowIndications[row + 1];
typename SparseMatrix<T>::iterator SparseMatrix<T>::end(uint_fast64_t row) {
return iterator(this->valueStorage.data() + this->rowIndications[row + 1], this->columnIndications.data() + this->rowIndications[row + 1]);
} }
template<typename T> template<typename T>
typename SparseMatrix<T>::ValueIterator SparseMatrix<T>::valueIteratorBegin(uint_fast64_t row) {
return &(this->valueStorage[0]) + this->rowIndications[row];
typename SparseMatrix<T>::const_iterator SparseMatrix<T>::end() const {
return const_iterator(this->valueStorage.data() + this->rowIndications[rowCount], this->columnIndications.data() + this->rowIndications[rowCount]);
} }
template<typename T> template<typename T>
typename SparseMatrix<T>::ValueIterator SparseMatrix<T>::valueIteratorEnd(uint_fast64_t row) {
return &(this->valueStorage[0]) + this->rowIndications[row + 1];
typename SparseMatrix<T>::iterator SparseMatrix<T>::end() {
return iterator(this->valueStorage.data() + this->rowIndications[rowCount], this->columnIndications.data() + this->rowIndications[rowCount]);
} }
template<typename T> template<typename T>
T SparseMatrix<T>::getRowSum(uint_fast64_t row) const { T SparseMatrix<T>::getRowSum(uint_fast64_t row) const {
T sum = storm::utility::constantZero<T>(); T sum = storm::utility::constantZero<T>();
for (auto it = this->constValueIteratorBegin(row), ite = this->constValueIteratorEnd(row); it != ite; ++it) {
sum += *it;
for (typename std::vector<T>::const_iterator valueIterator = valueStorage.begin() + rowIndications[row], valueIteratorEnd = valueStorage.begin() + rowIndications[row + 1]; valueIterator != valueIteratorEnd; ++valueIterator) {
sum += *valueIterator;
} }
return sum; return sum;
} }
@ -809,8 +841,7 @@ namespace storm {
// Check the subset property for all rows individually. // Check the subset property for all rows individually.
for (uint_fast64_t row = 0; row < this->getRowCount(); ++row) { for (uint_fast64_t row = 0; row < this->getRowCount(); ++row) {
for (uint_fast64_t elem = rowIndications[row], elem2 = matrix.rowIndications[row]; elem < rowIndications[row + 1] && elem < matrix.rowIndications[row + 1]; ++elem) { for (uint_fast64_t elem = rowIndications[row], elem2 = matrix.rowIndications[row]; elem < rowIndications[row + 1] && elem < matrix.rowIndications[row + 1]; ++elem) {
// Skip over all entries of the other matrix that are before the current entry in
// the current matrix.
// Skip over all entries of the other matrix that are before the current entry in the current matrix.
while (elem2 < matrix.rowIndications[row + 1] && matrix.columnIndications[elem2] < columnIndications[elem]) { while (elem2 < matrix.rowIndications[row + 1] && matrix.columnIndications[elem2] < columnIndications[elem]) {
++elem2; ++elem2;
} }
@ -823,73 +854,51 @@ namespace storm {
} }
template<typename T> template<typename T>
std::string SparseMatrix<T>::toString(std::vector<uint_fast64_t> const* rowGroupIndices) const {
std::stringstream result;
uint_fast64_t currentNondeterministicChoiceIndex = 0;
std::ostream& operator<<(std::ostream& out, SparseMatrix<T> const& matrix) {
// Print column numbers in header. // Print column numbers in header.
result << "\t\t";
for (uint_fast64_t i = 0; i < colCount; ++i) {
result << i << "\t";
out << "\t\t";
for (uint_fast64_t i = 0; i < matrix.columnCount; ++i) {
out << i << "\t";
} }
result << std::endl;
out << std::endl;
// Iterate over all rows. // Iterate over all rows.
for (uint_fast64_t i = 0; i < rowCount; ++i) {
uint_fast64_t nextIndex = rowIndications[i];
// If we need to group rows, print a dashed line in case we have moved to the next group of rows.
if (rowGroupIndices != nullptr) {
if (i == (*rowGroupIndices)[currentNondeterministicChoiceIndex]) {
if (i != 0) {
result << "\t(\t";
for (uint_fast64_t j = 0; j < colCount - 2; ++j) {
result << "----";
if (j == 1) {
result << "\t" << currentNondeterministicChoiceIndex << "\t";
}
}
result << "\t)" << std::endl;
}
++currentNondeterministicChoiceIndex;
}
}
for (uint_fast64_t i = 0; i < matrix.rowCount; ++i) {
uint_fast64_t nextIndex = matrix.rowIndications[i];
// Print the actual row. // Print the actual row.
result << i << "\t(\t";
out << i << "\t(\t";
uint_fast64_t currentRealIndex = 0; uint_fast64_t currentRealIndex = 0;
while (currentRealIndex < colCount) {
if (nextIndex < rowIndications[i + 1] && currentRealIndex == columnIndications[nextIndex]) {
result << std::setprecision(8) << valueStorage[nextIndex] << "\t";
while (currentRealIndex < matrix.columnCount) {
if (nextIndex < matrix.rowIndications[i + 1] && currentRealIndex == matrix.columnIndications[nextIndex]) {
out << matrix.valueStorage[nextIndex] << "\t";
++nextIndex; ++nextIndex;
} else { } else {
result << "0\t";
out << "0\t";
} }
++currentRealIndex; ++currentRealIndex;
} }
result << "\t)\t" << i << std::endl;
out << "\t)\t" << i << std::endl;
} }
// Print column numbers in footer. // Print column numbers in footer.
result << "\t\t";
for (uint_fast64_t i = 0; i < colCount; ++i) {
result << i << "\t";
out << "\t\t";
for (uint_fast64_t i = 0; i < matrix.columnCount; ++i) {
out << i << "\t";
} }
result << std::endl;
out << std::endl;
// Return final result.
return result.str();
return out;
} }
template<typename T> template<typename T>
std::size_t SparseMatrix<T>::getHash() const {
std::size_t SparseMatrix<T>::hash() const {
std::size_t result = 0; std::size_t result = 0;
boost::hash_combine(result, rowCount); boost::hash_combine(result, rowCount);
boost::hash_combine(result, colCount);
boost::hash_combine(result, nonZeroEntryCount);
boost::hash_combine(result, currentSize);
boost::hash_combine(result, lastRow);
boost::hash_combine(result, columnCount);
boost::hash_combine(result, entryCount);
boost::hash_combine(result, internalStatus);
boost::hash_combine(result, boost::hash_range(valueStorage.begin(), valueStorage.end())); boost::hash_combine(result, boost::hash_range(valueStorage.begin(), valueStorage.end()));
boost::hash_combine(result, boost::hash_range(columnIndications.begin(), columnIndications.end())); boost::hash_combine(result, boost::hash_range(columnIndications.begin(), columnIndications.end()));
boost::hash_combine(result, boost::hash_range(rowIndications.begin(), rowIndications.end())); boost::hash_combine(result, boost::hash_range(rowIndications.begin(), rowIndications.end()));
@ -898,44 +907,23 @@ namespace storm {
} }
template<typename T> template<typename T>
void SparseMatrix<T>::triggerErrorState() {
setState(MatrixStatus::Error);
}
template<typename T>
void SparseMatrix<T>::setState(const MatrixStatus new_state) {
internalStatus = (internalStatus == MatrixStatus::Error) ? internalStatus : new_state;
}
template<typename T>
bool SparseMatrix<T>::prepareInternalStorage(bool initializeElements) {
if (initializeElements) {
// Set up the arrays for the elements that are not on the diagonal.
valueStorage.resize(nonZeroEntryCount, storm::utility::constantZero<T>());
columnIndications.resize(nonZeroEntryCount, 0);
// Set up the rowIndications 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 {
// If it was not requested to initialize the elements, we simply reserve the space.
valueStorage.reserve(nonZeroEntryCount);
columnIndications.reserve(nonZeroEntryCount);
rowIndications.reserve(rowCount + 1);
return true;
void SparseMatrix<T>::prepareInternalStorage() {
// Only allocate the memory if the dimensions of the matrix are already known.
if (storagePreallocated) {
valueStorage = std::vector<T>(entryCount, storm::utility::constantZero<T>());
columnIndications = std::vector<uint_fast64_t>(entryCount, 0);
rowIndications = std::vector<uint_fast64_t>(rowCount + 1, 0);
} }
} }
// Explicit instantiations of specializations of this template here.
// Explicitly instantiate the matrix and the nested classes.
template class SparseMatrix<double>::BaseIterator<double const>;
template class SparseMatrix<double>::BaseIterator<double>;
template class SparseMatrix<double>; template class SparseMatrix<double>;
template class SparseMatrix<int>::BaseIterator<int const>;
template class SparseMatrix<int>::BaseIterator<int>;
template class SparseMatrix<int>; template class SparseMatrix<int>;
// Functions of the tbbHelper_MatrixRowVectorScalarProduct friend class.
#ifdef STORM_HAVE_INTELTBB #ifdef STORM_HAVE_INTELTBB
template <typename M, typename V, typename T> template <typename M, typename V, typename T>

20
src/storage/SparseMatrix.h

@ -269,6 +269,16 @@ namespace storm {
*/ */
SparseMatrix(SparseMatrix<T>&& other); SparseMatrix(SparseMatrix<T>&& other);
/*!
* Constructs a sparse matrix by copying the given contents.
*
* @param columnCount The number of columns of the matrix.
* @param rowIndications The row indications vector of the matrix to be constructed.
* @param columnIndications The column indications vector of the matrix to be constructed.
* @param values The vector containing the values of the entries in the matrix.
*/
SparseMatrix(uint_fast64_t columnCount, std::vector<uint_fast64_t> const& rowIndications, std::vector<uint_fast64_t> const& columnIndications, std::vector<T> const& values);
/*! /*!
* Constructs a sparse matrix by moving the given contents. * Constructs a sparse matrix by moving the given contents.
* *
@ -468,6 +478,11 @@ namespace storm {
*/ */
void negateAllNonDiagonalEntries(); void negateAllNonDiagonalEntries();
/*!
* Sets all diagonal elements to zero.
*/
void deleteDiagonalEntries();
/*! /*!
* Calculates the Jacobi decomposition of this sparse matrix. For this operation, the matrix must be square. * Calculates the Jacobi decomposition of this sparse matrix. For this operation, the matrix must be square.
* *
@ -592,8 +607,9 @@ namespace storm {
* @return True iff the current matrix is a submatrix of the given matrix. * @return True iff the current matrix is a submatrix of the given matrix.
*/ */
bool isSubmatrixOf(SparseMatrix<T> const& matrix) const; bool isSubmatrixOf(SparseMatrix<T> const& matrix) const;
friend std::ostream& operator<<(std::ostream& out, BitVector const& bitVector);
template<typename TPrime>
friend std::ostream& operator<<(std::ostream& out, SparseMatrix<TPrime> const& matrix);
/*! /*!
* Returns the size of the matrix in memory measured in bytes. * Returns the size of the matrix in memory measured in bytes.

4
src/storage/StronglyConnectedComponentDecomposition.cpp

@ -91,7 +91,7 @@ namespace storm {
// all successors of a particular state are considered. // all successors of a particular state are considered.
std::vector<uint_fast64_t> recursionStateStack; std::vector<uint_fast64_t> recursionStateStack;
recursionStateStack.reserve(lowlinks.size()); recursionStateStack.reserve(lowlinks.size());
std::vector<typename storm::storage::SparseMatrix<ValueType>::ConstIterator> recursionIteratorStack;
std::vector<typename storm::storage::SparseMatrix<ValueType>::const_iterator> recursionIteratorStack;
recursionIteratorStack.reserve(lowlinks.size()); recursionIteratorStack.reserve(lowlinks.size());
std::vector<bool> statesInStack(lowlinks.size()); std::vector<bool> statesInStack(lowlinks.size());
@ -114,7 +114,7 @@ namespace storm {
recursionStepForward: recursionStepForward:
while (!recursionStateStack.empty()) { while (!recursionStateStack.empty()) {
uint_fast64_t currentState = recursionStateStack.back(); uint_fast64_t currentState = recursionStateStack.back();
typename storm::storage::SparseMatrix<ValueType>::ConstIterator successorIt = recursionIteratorStack.back();
typename storm::storage::SparseMatrix<ValueType>::const_iterator successorIt = recursionIteratorStack.back();
// Perform the treatment of newly discovered state as defined by Tarjan's algorithm. // Perform the treatment of newly discovered state as defined by Tarjan's algorithm.
visitedStates.set(currentState, true); visitedStates.set(currentState, true);

16
src/utility/counterexamples.h

@ -34,9 +34,9 @@ namespace storm {
// Initially, put all predecessors of target states in the worklist and empty the analysis information them. // Initially, put all predecessors of target states in the worklist and empty the analysis information them.
for (auto state : psiStates) { for (auto state : psiStates) {
analysisInformation[state] = std::set<uint_fast64_t>(); analysisInformation[state] = std::set<uint_fast64_t>();
for (typename storm::storage::SparseMatrix<T>::ConstIndexIterator predecessorIt = backwardTransitions.constColumnIteratorBegin(state), predecessorIte = backwardTransitions.constColumnIteratorEnd(state); predecessorIt != predecessorIte; ++predecessorIt) {
if (*predecessorIt != state) {
worklist.push(std::make_pair(*predecessorIt, state));
for (auto& predecessorEntry : backwardTransitions.getRow(state)) {
if (predecessorEntry.column() != state) {
worklist.push(std::make_pair(predecessorEntry.column(), state));
} }
} }
} }
@ -56,8 +56,8 @@ namespace storm {
storm::storage::VectorSet<uint_fast64_t> tmpIntersection; storm::storage::VectorSet<uint_fast64_t> tmpIntersection;
bool choiceTargetsTargetState = false; bool choiceTargetsTargetState = false;
for (typename storm::storage::SparseMatrix<T>::ConstIndexIterator successorIt = transitionMatrix.constColumnIteratorBegin(currentChoice), successorIte = transitionMatrix.constColumnIteratorEnd(currentChoice); successorIt != successorIte; ++successorIt) {
if (*successorIt == targetState) {
for (auto& entry : transitionMatrix.getRow(currentChoice)) {
if (entry.column() == targetState) {
choiceTargetsTargetState = true; choiceTargetsTargetState = true;
break; break;
} }
@ -76,10 +76,10 @@ namespace storm {
// If the analysis information changed, we need to update it and put all the predecessors of this // If the analysis information changed, we need to update it and put all the predecessors of this
// state in the worklist. // state in the worklist.
if (analysisInformation[currentState].size() != analysisInformationSizeBefore) { if (analysisInformation[currentState].size() != analysisInformationSizeBefore) {
for (typename storm::storage::SparseMatrix<T>::ConstIndexIterator predecessorIt = backwardTransitions.constColumnIteratorBegin(currentState), predecessorIte = backwardTransitions.constColumnIteratorEnd(currentState); predecessorIt != predecessorIte; ++predecessorIt) {
for (auto& predecessorEntry : backwardTransitions.getRow(currentState)) {
// Only put the predecessor in the worklist if it's not already a target state. // Only put the predecessor in the worklist if it's not already a target state.
if (!psiStates.get(*predecessorIt)) {
worklist.push(std::make_pair(*predecessorIt, currentState));
if (!psiStates.get(predecessorEntry.column())) {
worklist.push(std::make_pair(predecessorEntry.column(), currentState));
} }
} }
} }

105
src/utility/graph.h

@ -81,17 +81,17 @@ namespace storm {
stepStack.pop_back(); stepStack.pop_back();
} }
for (auto predecessorIt = backwardTransitions.constColumnIteratorBegin(currentState), predecessorIte = backwardTransitions.constColumnIteratorEnd(currentState); predecessorIt != predecessorIte; ++predecessorIt) {
if (phiStates.get(*predecessorIt) && (!statesWithProbabilityGreater0.get(*predecessorIt) || (useStepBound && remainingSteps[*predecessorIt] < currentStepBound - 1))) {
for (auto& entry : backwardTransitions.getRow(currentState)) {
if (phiStates.get(entry.column()) && (!statesWithProbabilityGreater0.get(entry.column()) || (useStepBound && remainingSteps[entry.column()] < currentStepBound - 1))) {
// If we don't have a bound on the number of steps to take, just add the state to the stack. // If we don't have a bound on the number of steps to take, just add the state to the stack.
if (!useStepBound) { if (!useStepBound) {
statesWithProbabilityGreater0.set(*predecessorIt, true);
stack.push_back(*predecessorIt);
statesWithProbabilityGreater0.set(entry.column(), true);
stack.push_back(entry.column());
} else if (currentStepBound > 0) { } else if (currentStepBound > 0) {
// If there is at least one more step to go, we need to push the state and the new number of steps. // If there is at least one more step to go, we need to push the state and the new number of steps.
remainingSteps[*predecessorIt] = currentStepBound - 1;
statesWithProbabilityGreater0.set(*predecessorIt, true);
stack.push_back(*predecessorIt);
remainingSteps[entry.column()] = currentStepBound - 1;
statesWithProbabilityGreater0.set(entry.column(), true);
stack.push_back(entry.column());
stepStack.push_back(currentStepBound - 1); stepStack.push_back(currentStepBound - 1);
} }
} }
@ -212,17 +212,17 @@ namespace storm {
stepStack.pop_back(); stepStack.pop_back();
} }
for (auto predecessorIt = backwardTransitions.constColumnIteratorBegin(currentState), predecessorIte = backwardTransitions.constColumnIteratorEnd(currentState); predecessorIt != predecessorIte; ++predecessorIt) {
if (phiStates.get(*predecessorIt) && (!statesWithProbabilityGreater0.get(*predecessorIt) || (useStepBound && remainingSteps[*predecessorIt] < currentStepBound - 1))) {
for (auto& entry : backwardTransitions.getRow(currentState)) {
if (phiStates.get(entry.column()) && (!statesWithProbabilityGreater0.get(entry.column()) || (useStepBound && remainingSteps[entry.column()] < currentStepBound - 1))) {
// If we don't have a bound on the number of steps to take, just add the state to the stack. // If we don't have a bound on the number of steps to take, just add the state to the stack.
if (!useStepBound) { if (!useStepBound) {
statesWithProbabilityGreater0.set(*predecessorIt, true);
stack.push_back(*predecessorIt);
statesWithProbabilityGreater0.set(entry.column(), true);
stack.push_back(entry.column());
} else if (currentStepBound > 0) { } else if (currentStepBound > 0) {
// If there is at least one more step to go, we need to push the state and the new number of steps. // If there is at least one more step to go, we need to push the state and the new number of steps.
remainingSteps[*predecessorIt] = currentStepBound - 1;
statesWithProbabilityGreater0.set(*predecessorIt, true);
stack.push_back(*predecessorIt);
remainingSteps[entry.column()] = currentStepBound - 1;
statesWithProbabilityGreater0.set(entry.column(), true);
stack.push_back(entry.column());
stepStack.push_back(currentStepBound - 1); stepStack.push_back(currentStepBound - 1);
} }
} }
@ -291,14 +291,14 @@ namespace storm {
currentState = stack.back(); currentState = stack.back();
stack.pop_back(); stack.pop_back();
for(auto predecessorIt = backwardTransitions.constColumnIteratorBegin(currentState), predecessorIte = backwardTransitions.constColumnIteratorEnd(currentState); predecessorIt != predecessorIte; ++predecessorIt) {
if (phiStates.get(*predecessorIt) && !nextStates.get(*predecessorIt)) {
for (auto& predecessorEntry : backwardTransitions.getRow(currentState)) {
if (phiStates.get(predecessorEntry.column()) && !nextStates.get(predecessorEntry.column())) {
// Check whether the predecessor has only successors in the current state set for one of the // Check whether the predecessor has only successors in the current state set for one of the
// nondeterminstic choices. // nondeterminstic choices.
for (auto row = nondeterministicChoiceIndices[*predecessorIt]; row < nondeterministicChoiceIndices[*predecessorIt + 1]; ++row) {
for (auto row = nondeterministicChoiceIndices[predecessorEntry.column()]; row < nondeterministicChoiceIndices[predecessorEntry.column() + 1]; ++row) {
bool allSuccessorsInCurrentStates = true; bool allSuccessorsInCurrentStates = true;
for (auto targetIt = transitionMatrix.constColumnIteratorBegin(row), targetIte = transitionMatrix.constColumnIteratorEnd(row); targetIt != targetIte; ++targetIt) {
if (!currentStates.get(*targetIt)) {
for (auto& targetEntry : transitionMatrix.getRow(row)) {
if (!currentStates.get(targetEntry.column())) {
allSuccessorsInCurrentStates = false; allSuccessorsInCurrentStates = false;
break; break;
} }
@ -308,8 +308,8 @@ namespace storm {
// add it to the set of states for the next iteration and perform a backward search from // add it to the set of states for the next iteration and perform a backward search from
// that state. // that state.
if (allSuccessorsInCurrentStates) { if (allSuccessorsInCurrentStates) {
nextStates.set(*predecessorIt, true);
stack.push_back(*predecessorIt);
nextStates.set(predecessorEntry.column(), true);
stack.push_back(predecessorEntry.column());
break; break;
} }
} }
@ -402,15 +402,15 @@ namespace storm {
stepStack.pop_back(); stepStack.pop_back();
} }
for(auto predecessorIt = backwardTransitions.constColumnIteratorBegin(currentState), predecessorIte = backwardTransitions.constColumnIteratorEnd(currentState); predecessorIt != predecessorIte; ++predecessorIt) {
if (phiStates.get(*predecessorIt) && (!statesWithProbabilityGreater0.get(*predecessorIt) || (useStepBound && remainingSteps[*predecessorIt] < currentStepBound - 1))) {
for(auto& predecessorEntry : backwardTransitions.getRow(currentState)) {
if (phiStates.get(predecessorEntry.column()) && (!statesWithProbabilityGreater0.get(predecessorEntry.column()) || (useStepBound && remainingSteps[predecessorEntry.column()] < currentStepBound - 1))) {
// Check whether the predecessor has at least one successor in the current state set for every // Check whether the predecessor has at least one successor in the current state set for every
// nondeterministic choice. // nondeterministic choice.
bool addToStatesWithProbabilityGreater0 = true; bool addToStatesWithProbabilityGreater0 = true;
for (auto row = nondeterministicChoiceIndices[*predecessorIt]; row < nondeterministicChoiceIndices[*predecessorIt + 1]; ++row) {
for (auto row = nondeterministicChoiceIndices[predecessorEntry.column()]; row < nondeterministicChoiceIndices[predecessorEntry.column() + 1]; ++row) {
bool hasAtLeastOneSuccessorWithProbabilityGreater0 = false; bool hasAtLeastOneSuccessorWithProbabilityGreater0 = false;
for (auto successorIt = transitionMatrix.constColumnIteratorBegin(row), successorIte = transitionMatrix.constColumnIteratorEnd(row); successorIt != successorIte; ++successorIt) {
if (statesWithProbabilityGreater0.get(*successorIt)) {
for (auto& successorEntry : transitionMatrix.getRow(row)) {
if (statesWithProbabilityGreater0.get(successorEntry.column())) {
hasAtLeastOneSuccessorWithProbabilityGreater0 = true; hasAtLeastOneSuccessorWithProbabilityGreater0 = true;
break; break;
} }
@ -426,13 +426,13 @@ namespace storm {
if (addToStatesWithProbabilityGreater0) { if (addToStatesWithProbabilityGreater0) {
// If we don't have a bound on the number of steps to take, just add the state to the stack. // If we don't have a bound on the number of steps to take, just add the state to the stack.
if (!useStepBound) { if (!useStepBound) {
statesWithProbabilityGreater0.set(*predecessorIt, true);
stack.push_back(*predecessorIt);
statesWithProbabilityGreater0.set(predecessorEntry.column(), true);
stack.push_back(predecessorEntry.column());
} else if (currentStepBound > 0) { } else if (currentStepBound > 0) {
// If there is at least one more step to go, we need to push the state and the new number of steps. // If there is at least one more step to go, we need to push the state and the new number of steps.
remainingSteps[*predecessorIt] = currentStepBound - 1;
statesWithProbabilityGreater0.set(*predecessorIt, true);
stack.push_back(*predecessorIt);
remainingSteps[predecessorEntry.column()] = currentStepBound - 1;
statesWithProbabilityGreater0.set(predecessorEntry.column(), true);
stack.push_back(predecessorEntry.column());
stepStack.push_back(currentStepBound - 1); stepStack.push_back(currentStepBound - 1);
} }
} }
@ -502,17 +502,15 @@ namespace storm {
currentState = stack.back(); currentState = stack.back();
stack.pop_back(); stack.pop_back();
for(auto predecessorIt = backwardTransitions.constColumnIteratorBegin(currentState), predecessorIte = backwardTransitions.constColumnIteratorEnd(currentState); predecessorIt != predecessorIte; ++predecessorIt) {
if (phiStates.get(*predecessorIt) && !nextStates.get(*predecessorIt)) {
for(auto& predecessorEntry : backwardTransitions.getRow(currentState)) {
if (phiStates.get(predecessorEntry.column()) && !nextStates.get(predecessorEntry.column())) {
// Check whether the predecessor has only successors in the current state set for all of the // Check whether the predecessor has only successors in the current state set for all of the
// nondeterminstic choices. // nondeterminstic choices.
bool allSuccessorsInCurrentStatesForAllChoices = true; bool allSuccessorsInCurrentStatesForAllChoices = true;
for (auto row = nondeterministicChoiceIndices[*predecessorIt]; row < nondeterministicChoiceIndices[*predecessorIt + 1]; ++row) {
for (auto successorIt = transitionMatrix.constColumnIteratorBegin(row), successorIte = transitionMatrix.constColumnIteratorEnd(row); successorIt != successorIte; ++successorIt) {
if (!currentStates.get(*successorIt)) {
allSuccessorsInCurrentStatesForAllChoices = false;
goto afterCheckLoop;
}
for (auto& successorEntry : transitionMatrix.getRows(nondeterministicChoiceIndices[predecessorEntry.column()], nondeterministicChoiceIndices[predecessorEntry.column() + 1] - 1)) {
if (!currentStates.get(successorEntry.column())) {
allSuccessorsInCurrentStatesForAllChoices = false;
goto afterCheckLoop;
} }
} }
@ -521,8 +519,8 @@ namespace storm {
// add it to the set of states for the next iteration and perform a backward search from // add it to the set of states for the next iteration and perform a backward search from
// that state. // that state.
if (allSuccessorsInCurrentStatesForAllChoices) { if (allSuccessorsInCurrentStatesForAllChoices) {
nextStates.set(*predecessorIt, true);
stack.push_back(*predecessorIt);
nextStates.set(predecessorEntry.column(), true);
stack.push_back(predecessorEntry.column());
} }
} }
} }
@ -541,7 +539,6 @@ namespace storm {
template <typename T> template <typename T>
std::pair<storm::storage::BitVector, storm::storage::BitVector> performProb01Min(storm::storage::SparseMatrix<T> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::SparseMatrix<T> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { std::pair<storm::storage::BitVector, storm::storage::BitVector> performProb01Min(storm::storage::SparseMatrix<T> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::SparseMatrix<T> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) {
std::pair<storm::storage::BitVector, storm::storage::BitVector> result; std::pair<storm::storage::BitVector, storm::storage::BitVector> result;
result.first = performProb0E(transitionMatrix, nondeterministicChoiceIndices, backwardTransitions, phiStates, psiStates); result.first = performProb0E(transitionMatrix, nondeterministicChoiceIndices, backwardTransitions, phiStates, psiStates);
result.second = performProb1A(transitionMatrix, nondeterministicChoiceIndices, backwardTransitions, phiStates, psiStates); result.second = performProb1A(transitionMatrix, nondeterministicChoiceIndices, backwardTransitions, phiStates, psiStates);
return result; return result;
@ -584,7 +581,7 @@ namespace storm {
// Prepare the stacks needed for recursion. // Prepare the stacks needed for recursion.
std::vector<uint_fast64_t> recursionStack; std::vector<uint_fast64_t> recursionStack;
recursionStack.reserve(matrix.getRowCount()); recursionStack.reserve(matrix.getRowCount());
std::vector<typename storm::storage::SparseMatrix<T>::ConstIndexIterator> iteratorRecursionStack;
std::vector<typename storm::storage::SparseMatrix<T>::const_iterator> iteratorRecursionStack;
iteratorRecursionStack.reserve(numberOfStates); iteratorRecursionStack.reserve(numberOfStates);
// Perform a depth-first search over the given transitions and record states in the reverse order they were visited. // Perform a depth-first search over the given transitions and record states in the reverse order they were visited.
@ -592,27 +589,23 @@ namespace storm {
for (uint_fast64_t state = 0; state < numberOfStates; ++state) { for (uint_fast64_t state = 0; state < numberOfStates; ++state) {
if (!visitedStates.get(state)) { if (!visitedStates.get(state)) {
recursionStack.push_back(state); recursionStack.push_back(state);
iteratorRecursionStack.push_back(matrix.constColumnIteratorBegin(state));
iteratorRecursionStack.push_back(matrix.begin(state));
recursionStepForward: recursionStepForward:
while (!recursionStack.empty()) { while (!recursionStack.empty()) {
uint_fast64_t currentState = recursionStack.back(); uint_fast64_t currentState = recursionStack.back();
typename storm::storage::SparseMatrix<T>::ConstIndexIterator successorIt = iteratorRecursionStack.back();
typename storm::storage::SparseMatrix<T>::const_iterator successorIterator = iteratorRecursionStack.back();
visitedStates.set(currentState, true); visitedStates.set(currentState, true);
recursionStepBackward: recursionStepBackward:
for (; successorIt != matrix.constColumnIteratorEnd(currentState); ++successorIt) {
if (!visitedStates.get(*successorIt)) {
for (; successorIterator != matrix.end(currentState); ++successorIterator) {
if (!visitedStates.get(successorIterator.column())) {
// Put unvisited successor on top of our recursion stack and remember that. // Put unvisited successor on top of our recursion stack and remember that.
recursionStack.push_back(*successorIt);
// Save current iterator position so we can continue where we left off later.
iteratorRecursionStack.pop_back();
iteratorRecursionStack.push_back(successorIt + 1);
recursionStack.push_back(successorIterator.column());
// Also, put initial value for iterator on corresponding recursion stack. // Also, put initial value for iterator on corresponding recursion stack.
iteratorRecursionStack.push_back(matrix.constColumnIteratorBegin(*successorIt));
iteratorRecursionStack.push_back(matrix.begin(successorIterator.column()));
goto recursionStepForward; goto recursionStepForward;
} }
@ -630,7 +623,7 @@ namespace storm {
// original recursive call. // original recursive call.
if (recursionStack.size() > 0) { if (recursionStack.size() > 0) {
currentState = recursionStack.back(); currentState = recursionStack.back();
successorIt = iteratorRecursionStack.back();
successorIterator = iteratorRecursionStack.back();
goto recursionStepBackward; goto recursionStepBackward;
} }
@ -674,7 +667,7 @@ namespace storm {
// Set the probability to 1 for all starting states. // Set the probability to 1 for all starting states.
#ifdef LINUX #ifdef LINUX
boost::container::set<std::pair<T, uint_fast64_t>, DistanceCompare<T>> probabilityStateSet;
boost::container::set<std::pair<T, uint_fast64_t>, DistanceCompare<T>> probabilityStateSet;
#else #else
std::set<std::pair<T, uint_fast64_t>, DistanceCompare<T>> probabilityStateSet; std::set<std::pair<T, uint_fast64_t>, DistanceCompare<T>> probabilityStateSet;
#endif #endif
@ -690,7 +683,7 @@ namespace storm {
probabilityStateSet.erase(probabilityStateSet.begin()); probabilityStateSet.erase(probabilityStateSet.begin());
// Now check the new distances for all successors of the current state. // Now check the new distances for all successors of the current state.
typename storm::storage::SparseMatrix<T>::Rows row = transitions.getRows(probabilityStatePair.second, probabilityStatePair.second);
typename storm::storage::SparseMatrix<T>::Rows row = transitions.getRow(probabilityStatePair.second);
for (auto& transition : row) { for (auto& transition : row) {
// Only follow the transition if it lies within the filtered states. // Only follow the transition if it lies within the filtered states.
if (filterStates != nullptr && filterStates->get(transition.column())) { if (filterStates != nullptr && filterStates->get(transition.column())) {

6
src/utility/matrix.h

@ -31,13 +31,13 @@ namespace storm {
} }
// If a valid choice for this state is defined, we copy over the corresponding entries. // If a valid choice for this state is defined, we copy over the corresponding entries.
typename storm::storage::SparseMatrix<T>::Rows selectedRow = transitionMatrix.getRow(choice);
typename storm::storage::SparseMatrix<T>::const_rows selectedRow = transitionMatrix.getRow(choice);
for (auto entry : selectedRow) { for (auto entry : selectedRow) {
result.insertNextValue(state, entry.column(), entry.value());
result.addNextValue(state, entry.column(), entry.value());
} }
} else { } else {
// If no valid choice for the state is defined, we insert a self-loop. // If no valid choice for the state is defined, we insert a self-loop.
result.insertNextValue(state, state, storm::utility::constantOne<T>());
result.addNextValue(state, state, storm::utility::constantOne<T>());
} }
} }

17
src/utility/vector.h

@ -1,7 +1,6 @@
#ifndef STORM_UTILITY_VECTOR_H_ #ifndef STORM_UTILITY_VECTOR_H_
#define STORM_UTILITY_VECTOR_H_ #define STORM_UTILITY_VECTOR_H_
#include "Eigen/Core"
#include "constants.h" #include "constants.h"
#include <iostream> #include <iostream>
#include <algorithm> #include <algorithm>
@ -43,21 +42,7 @@ namespace storm {
vector[position] = value; vector[position] = value;
} }
} }
/*!
* Sets the provided value at the provided positions in the given vector.
*
* @param vector The vector in which the value is to be set.
* @param positions The positions at which the value is to be set.
* @param value The value that is to be set.
*/
template<class T>
void setVectorValues(Eigen::Matrix<T, -1, 1, 0, -1, 1>& eigenVector, storm::storage::BitVector const& positions, T value) {
for (auto position : positions) {
eigenVector(position, 0) = value;
}
}
/*! /*!
* Selects the elements from a vector at the specified positions and writes them consecutively into another vector. * Selects the elements from a vector at the specified positions and writes them consecutively into another vector.
* @param vector The vector into which the selected elements are to be written. * @param vector The vector into which the selected elements are to be written.

79
test/functional/eigen/EigenSparseMatrixTest.cpp

@ -1,79 +0,0 @@
#include "gtest/gtest.h"
#include "Eigen/Sparse"
#include "src/exceptions/InvalidArgumentException.h"
#include <cstdint>
TEST(EigenSparseMatrixTest, BasicReadWriteTest) {
// 25 rows, 50 non zero entries
Eigen::SparseMatrix<int, 1> esm(25, 25);
int values[50] = {
0, 1, 2, 3, 4, 5, 6, 7, 8, 9,
10, 11, 12, 13, 14, 15, 16, 17, 18, 19,
20, 21, 22, 23, 24, 25, 26, 27, 28, 29,
30, 31, 32, 33, 34, 35, 36, 37, 38, 39,
40, 41, 42, 43, 44, 45, 46, 47, 48, 49
};
int position_row[50] = {
2, 2, 2, 2, 2, 2, 2, 2, 2, 2,
2, 2, 2, 2, 2, 2, 2, 2, 2, 2,
2, 2, 2, 2, /* first row empty, one full row 25 minus the diagonal entry */
4, 4, /* one empty row, then first and last column */
13, 13, 13, 13, /* a few empty rows, middle columns */
24, 24, 24, 24, 24, 24, 24, 24, 24, 24,
24, 24, 24, 24, 24, 24, 24, 24, 24, 24 /* second to last row */
};
int position_col[50] = {
1, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 14, 15, 16, 17, 18, 19, 20,
21, 22, 23, 24, 25, /* first row empty, one full row a 25 */
1, 25, /* one empty row, then first and last column */
16, 17, 18, 19, /* a few empty rows, middle columns */
2, 3, 4, 5, 6, 7, 8, 9, 10, 11,
14, 15, 16, 17, 18, 19, 20, 21, 22, 23 /* second to last row */
};
typedef Eigen::Triplet<double> ETd;
std::vector<ETd> tripletList;
tripletList.reserve(50);
for (int i = 0; i < 50; ++i) {
ASSERT_NO_THROW(tripletList.push_back(ETd(position_row[i] - 1, position_col[i] - 1, values[i])));
}
ASSERT_NO_THROW(esm.setFromTriplets(tripletList.begin(), tripletList.end()));
for (int i = 0; i < 50; ++i) {
Eigen::SparseMatrix<int, 1>::InnerIterator it(esm, position_row[i] - 1);
ASSERT_EQ(values[i], esm.coeff(position_row[i] - 1, position_col[i] - 1));
}
// test for a few of the empty rows
for (int row = 15; row < 24; ++row) {
for (int col = 1; col <= 25; ++col) {
ASSERT_EQ(0, esm.coeff(row - 1, col - 1));
}
}
}
TEST(EigenSparseMatrixTest, BoundaryTest) {
Eigen::SparseMatrix<int, 1> esm(10, 10);
esm.reserve(100);
int values[100];
for (uint_fast32_t i = 0; i < 100; ++i) {
values[i] = i;
}
for (uint_fast32_t row = 0; row < 10; ++row) {
for (uint_fast32_t col = 0; col < 10; ++col) {
ASSERT_NO_THROW(esm.insert(row, col) = values[row * 10 + col]);
}
}
for (uint_fast32_t row = 0; row < 10; ++row) {
for (uint_fast32_t col = 0; col < 10; ++col) {
ASSERT_EQ(values[row * 10 + col], esm.coeff(row, col));
}
}
}

1
test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp

@ -116,7 +116,6 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, SynchronousLeader) {
storm::parser::AutoParser<double> parser(STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader4_8.tra", STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader4_8.lab", "", STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader4_8.pick.trans.rew"); storm::parser::AutoParser<double> parser(STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader4_8.tra", STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader4_8.lab", "", STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader4_8.pick.trans.rew");
ASSERT_EQ(parser.getType(), storm::models::DTMC); ASSERT_EQ(parser.getType(), storm::models::DTMC);
std::shared_ptr<storm::models::Dtmc<double>> dtmc = parser.getModel<storm::models::Dtmc<double>>(); std::shared_ptr<storm::models::Dtmc<double>> dtmc = parser.getModel<storm::models::Dtmc<double>>();
ASSERT_EQ(dtmc->getNumberOfStates(), 12400ull); ASSERT_EQ(dtmc->getNumberOfStates(), 12400ull);

77
test/functional/parser/ReadTraFileTest.cpp

@ -1,77 +0,0 @@
/*
* ReadTraFileTest.cpp
*
* Created on: 16.08.2012
* Author: Thomas Heinemann
*/
#include "gtest/gtest.h"
#include "storm-config.h"
#include "src/storage/SparseMatrix.h"
#include "src/parser/DeterministicSparseTransitionParser.h"
#include "src/exceptions/FileIoException.h"
#include "src/exceptions/WrongFormatException.h"
TEST(ReadTraFileTest, NonExistingFileTest) {
//No matter what happens, please don't create a file with the name "nonExistingFile.not"! :-)
ASSERT_THROW(storm::parser::DeterministicSparseTransitionParser(STORM_CPP_TESTS_BASE_PATH "/nonExistingFile.not"), storm::exceptions::FileIoException);
}
/* The following test case is based on one of the original MRMC test cases
*/
TEST(ReadTraFileTest, ParseFileTest1) {
storm::storage::SparseMatrix<double> result = storm::parser::DeterministicSparseTransitionParser(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/csl_general_input_01.tra");
double val = 0.0;
ASSERT_TRUE(result.getValue(0, 0, &val));
ASSERT_EQ(val, 0.0);
ASSERT_TRUE(result.getValue(0, 1, &val));
ASSERT_EQ(val, 1.0);
ASSERT_TRUE(result.getValue(1, 1, &val));
ASSERT_EQ(val, 0.080645161290322580645161290322581);
ASSERT_TRUE(result.getValue(1, 2, &val));
ASSERT_EQ(val, 0.080645161290322580645161290322581);
//Transition 1->3 was not set in the file, so it is not to appear in the matrix!
ASSERT_FALSE(result.getValue(1, 3, &val));
ASSERT_EQ(val, 0);
ASSERT_TRUE(result.getValue(2, 1, &val));
ASSERT_EQ(val, 0.04032258064516129032258064516129);
ASSERT_TRUE(result.getValue(2, 2, &val));
ASSERT_EQ(val, 0.04032258064516129032258064516129);
ASSERT_TRUE(result.getValue(2, 3, &val));
ASSERT_EQ(val, 0.04032258064516129032258064516129);
ASSERT_TRUE(result.getValue(2, 4, &val));
ASSERT_EQ(val, 0.04032258064516129032258064516129);
ASSERT_TRUE(result.getValue(3, 2, &val));
ASSERT_EQ(val, 0.0806451612903225806451612903225812);
ASSERT_TRUE(result.getValue(3, 3, &val));
ASSERT_EQ(val, 0.0);
ASSERT_TRUE(result.getValue(3, 4, &val));
ASSERT_EQ(val, 0.080645161290322580645161290322581);
ASSERT_TRUE(result.getValue(4, 4, &val));
ASSERT_EQ(val, 0.0);
}
TEST(ReadTraFileTest, WrongFormatTestHeader1) {
ASSERT_THROW(storm::parser::DeterministicSparseTransitionParser(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/wrong_format_header1.tra"), storm::exceptions::WrongFormatException);
}
TEST(ReadTraFileTest, WrongFormatTestHeader2) {
ASSERT_THROW(storm::parser::DeterministicSparseTransitionParser(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/wrong_format_header2.tra"), storm::exceptions::WrongFormatException);
}
TEST(ReadTraFileTest, WrongFormatTestTransition) {
ASSERT_THROW(storm::parser::DeterministicSparseTransitionParser(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/wrong_format_transition.tra"), storm::exceptions::WrongFormatException);
}

386
test/functional/storage/SparseMatrixTest.cpp

@ -1,386 +0,0 @@
#include "gtest/gtest.h"
#include "src/storage/SparseMatrix.h"
#include "src/exceptions/InvalidArgumentException.h"
#include "src/exceptions/OutOfRangeException.h"
#include "src/adapters/EigenAdapter.h"
#include "src/adapters/StormAdapter.h"
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::SparseMatrix<int>::MatrixStatus::Error);
delete ssm;
}
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::SparseMatrix<int>::MatrixStatus::Error);
delete ssm;
}
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::SparseMatrix<int>::MatrixStatus::Initialized);
ASSERT_THROW(ssm->addNextValue(-1, 1, 1), storm::exceptions::OutOfRangeException);
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::SparseMatrix<int>::MatrixStatus::Error);
ASSERT_THROW(ssm->addNextValue(6, 1, 1), storm::exceptions::OutOfRangeException);
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::SparseMatrix<int>::MatrixStatus::Error);
delete ssm;
}
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::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::SparseMatrix<int>::MatrixStatus::Initialized);
ASSERT_THROW(ssm->finalize(), storm::exceptions::InvalidStateException);
ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix<int>::MatrixStatus::Error);
delete ssm;
}
TEST(SparseMatrixTest, Test) {
// 25 rows, 50 non zero entries
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,
10, 11, 12, 13, 14, 15, 16, 17, 18, 19,
20, 21, 22, 23, 24, 25, 26, 27, 28, 29,
30, 31, 32, 33, 34, 35, 36, 37, 38, 39,
40, 41, 42, 43, 44, 45, 46, 47, 48, 49
};
int position_row[50] = {
2, 2, 2, 2, 2, 2, 2, 2, 2, 2,
2, 2, 2, 2, 2, 2, 2, 2, 2, 2,
2, 2, 2, 2, /* first row empty, one full row 25 minus the diagonal entry */
4, 4, /* one empty row, then first and last column */
13, 13, 13, 13, /* a few empty rows, middle columns */
24, 24, 24, 24, 24, 24, 24, 24, 24, 24,
24, 24, 24, 24, 24, 24, 24, 24, 24, 24 /* second to last row */
};
int position_col[50] = {
1, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 14, 15, 16, 17, 18, 19, 20,
21, 22, 23, 24, 25, /* first row empty, one full row a 25 */
1, 25, /* one empty row, then first and last column */
16, 17, 18, 19, /* a few empty rows, middle columns */
2, 3, 4, 5, 6, 7, 8, 9, 10, 11,
14, 15, 16, 17, 18, 19, 20, 21, 22, 23 /* second to last row */
};
int row_sums[25] = {};
for (int i = 0; i < 50; ++i) {
row_sums[position_row[i]] += values[i];
}
ASSERT_NO_THROW(ssm->initialize(50));
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::SparseMatrix<int>::MatrixStatus::Initialized);
ASSERT_NO_THROW(ssm->finalize());
ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix<int>::MatrixStatus::ReadReady);
int target;
for (int i = 0; i < 50; ++i) {
ASSERT_TRUE(ssm->getValue(position_row[i], position_col[i], &target));
ASSERT_EQ(values[i], target);
}
// test for a few of the empty rows
for (int row = 15; row < 24; ++row) {
for (int col = 1; col <= 25; ++col) {
target = 1;
ASSERT_FALSE(ssm->getValue(row, col, &target));
ASSERT_EQ(0, target);
}
}
ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix<int>::MatrixStatus::ReadReady);
// Test Row Sums
for (int row = 0; row < 25; ++row) {
ASSERT_EQ(row_sums[row], ssm->getRowSum(row));
}
delete ssm;
}
TEST(SparseMatrixTest, ConversionFromDenseEigen_ColMajor_SparseMatrixTest) {
// 10 rows, 100 non zero entries
Eigen::SparseMatrix<int> esm(10, 10);
for (int row = 0; row < 10; ++row) {
for (int col = 0; col < 10; ++col) {
esm.insert(row, col) = row * 10 + col;
}
}
// make compressed, important for initialize()
esm.makeCompressed();
storm::storage::SparseMatrix<int> *ssm = nullptr;
ASSERT_NO_THROW(ssm = storm::adapters::StormAdapter::toStormSparseMatrix(esm));
ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix<int>::MatrixStatus::ReadReady);
int target = -1;
for (int row = 0; row < 10; ++row) {
for (int col = 0; col < 10; ++col) {
ASSERT_TRUE(ssm->getValue(row, col, &target));
ASSERT_EQ(target, row * 10 + col);
}
}
delete ssm;
}
TEST(SparseMatrixTest, ConversionFromDenseEigen_RowMajor_SparseMatrixTest) {
// 10 rows, 100 non zero entries
Eigen::SparseMatrix<int, Eigen::RowMajor> esm(10, 10);
for (int row = 0; row < 10; ++row) {
for (int col = 0; col < 10; ++col) {
esm.insert(row, col) = row * 10 + col;
}
}
// make compressed, important for initialize()
esm.makeCompressed();
storm::storage::SparseMatrix<int> *ssm = nullptr;
ASSERT_NO_THROW(ssm = storm::adapters::StormAdapter::toStormSparseMatrix(esm));
ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix<int>::MatrixStatus::ReadReady);
int target = -1;
for (int row = 0; row < 10; ++row) {
for (int col = 0; col < 10; ++col) {
ASSERT_TRUE(ssm->getValue(row, col, &target));
ASSERT_EQ(target, row * 10 + col);
}
}
delete ssm;
}
TEST(SparseMatrixTest, ConversionFromSparseEigen_ColMajor_SparseMatrixTest) {
// 10 rows, 15 non zero entries
Eigen::SparseMatrix<int> 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, 1, 1));
tripletList.push_back(IntTriplet(1, 2, 2));
tripletList.push_back(IntTriplet(1, 3, 3));
tripletList.push_back(IntTriplet(1, 4, 4));
tripletList.push_back(IntTriplet(1, 5, 5));
tripletList.push_back(IntTriplet(1, 6, 6));
tripletList.push_back(IntTriplet(1, 7, 7));
tripletList.push_back(IntTriplet(1, 8, 8));
tripletList.push_back(IntTriplet(1, 9, 9));
tripletList.push_back(IntTriplet(4, 3, 10));
tripletList.push_back(IntTriplet(4, 6, 11));
tripletList.push_back(IntTriplet(4, 9, 12));
tripletList.push_back(IntTriplet(6, 0, 13));
tripletList.push_back(IntTriplet(8, 9, 14));
esm.setFromTriplets(tripletList.begin(), tripletList.end());
// make compressed, important for initialize()
esm.makeCompressed();
storm::storage::SparseMatrix<int> *ssm = nullptr;
ASSERT_NO_THROW(ssm = storm::adapters::StormAdapter::toStormSparseMatrix(esm));
ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix<int>::MatrixStatus::ReadReady);
int target = -1;
for (auto &coeff: tripletList) {
ASSERT_TRUE(ssm->getValue(coeff.row(), coeff.col(), &target));
ASSERT_EQ(target, coeff.value());
}
delete ssm;
}
TEST(SparseMatrixTest, ConversionFromSparseEigen_RowMajor_SparseMatrixTest) {
// 10 rows, 15 non zero entries
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, 15));
tripletList.push_back(IntTriplet(1, 1, 1));
tripletList.push_back(IntTriplet(1, 2, 2));
tripletList.push_back(IntTriplet(1, 3, 3));
tripletList.push_back(IntTriplet(1, 4, 4));
tripletList.push_back(IntTriplet(1, 5, 5));
tripletList.push_back(IntTriplet(1, 6, 6));
tripletList.push_back(IntTriplet(1, 7, 7));
tripletList.push_back(IntTriplet(1, 8, 8));
tripletList.push_back(IntTriplet(1, 9, 9));
tripletList.push_back(IntTriplet(4, 3, 10));
tripletList.push_back(IntTriplet(4, 6, 11));
tripletList.push_back(IntTriplet(4, 9, 12));
tripletList.push_back(IntTriplet(6, 0, 13));
tripletList.push_back(IntTriplet(8, 9, 14));
esm.setFromTriplets(tripletList.begin(), tripletList.end());
// make compressed, important for initialize()
esm.makeCompressed();
storm::storage::SparseMatrix<int> *ssm = nullptr;
ASSERT_NO_THROW(ssm = storm::adapters::StormAdapter::toStormSparseMatrix(esm));
ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix<int>::MatrixStatus::ReadReady);
int target = -1;
for (auto &coeff: tripletList) {
bool retVal = ssm->getValue(coeff.row(), coeff.col(), &target);
ASSERT_TRUE(retVal);
ASSERT_EQ(target, coeff.value());
}
delete ssm;
}
TEST(SparseMatrixTest, ConversionToSparseEigen_RowMajor_SparseMatrixTest) {
int values[100];
storm::storage::SparseMatrix<int> *ssm = new storm::storage::SparseMatrix<int>(10);
for (uint_fast32_t i = 0; i < 100; ++i) {
values[i] = i;
}
ASSERT_NO_THROW(ssm->initialize(100));
ASSERT_EQ(ssm->getState(), storm::storage::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::SparseMatrix<int>::MatrixStatus::Initialized);
ASSERT_NO_THROW(ssm->finalize());
ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix<int>::MatrixStatus::ReadReady);
Eigen::SparseMatrix<int, Eigen::RowMajor, int_fast32_t>* esm = storm::adapters::EigenAdapter::toEigenSparseMatrix<int>(*ssm);
for (uint_fast32_t row = 0; row < 10; ++row) {
for (uint_fast32_t col = 0; col < 10; ++col) {
ASSERT_EQ(values[row * 10 + col], esm->coeff(row, col));
}
}
delete esm;
delete ssm;
}
#ifdef STORM_USE_TBB
TEST(SparseMatrixTest, TBBMatrixMultTest) {
storm::storage::SparseMatrix<double> matrix(10, 10);
ASSERT_NO_THROW(matrix.initialize(100));
double values[100];
std::vector<double> x;
x.resize(10);
for (uint_fast64_t i = 0; i < 100; ++i) {
values[i] = i + 1.0;
if (i < 10) {
x[i] = 1.0;
}
matrix.addNextValue(i / 10, i % 10, values[i]);
}
ASSERT_NO_THROW(matrix.finalize());
ASSERT_EQ(matrix.getState(), storm::storage::SparseMatrix<double>::MatrixStatus::ReadReady);
std::vector<double> result;
result.resize(10);
matrix.multiplyWithVector(x, result);
for (uint_fast64_t i = 0; i < 10; ++i) {
double rowSum = 0.0;
for (uint_fast64_t j = 0; j < 10; ++j) {
rowSum += values[10 * i + j];
}
ASSERT_EQ(rowSum, result.at(i));
}
}
TEST(SparseMatrixTest, TBBSparseMatrixMultTest) {
storm::storage::SparseMatrix<double> matrix(10, 10);
ASSERT_NO_THROW(matrix.initialize(50));
double values[100];
std::vector<double> x;
x.resize(10);
for (uint_fast64_t i = 0; i < 100; ++i) {
if (i % 2 == 0) {
values[i] = i + 1.0;
matrix.addNextValue(i / 10, i % 10, i + 1.0);
} else {
values[i] = 0.0;
}
if (i < 10) {
x[i] = 1.0;
}
}
ASSERT_NO_THROW(matrix.finalize());
ASSERT_EQ(matrix.getState(), storm::storage::SparseMatrix<double>::MatrixStatus::ReadReady);
std::vector<double> result;
result.resize(10);
matrix.multiplyWithVector(x, result);
for (uint_fast64_t i = 0; i < 10; ++i) {
double rowSum = 0.0;
for (uint_fast64_t j = 0; j < 10; ++j) {
rowSum += values[10 * i + j];
}
ASSERT_EQ(rowSum, result.at(i));
}
}
#endif // STORM_USE_TBB

100
test/functional/storage/adapters/EigenAdapterTest.cpp

@ -1,100 +0,0 @@
#include "gtest/gtest.h"
#include "Eigen/Sparse"
#include "src/adapters/EigenAdapter.h"
#include "src/exceptions/InvalidArgumentException.h"
#include <cstdint>
#define STORM_EIGENADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE 5
#define STORM_EIGENADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE 5
TEST(EigenAdapterTest, SimpleDenseSquareCopy) {
// 5 rows
storm::storage::SparseMatrix<double> sm(STORM_EIGENADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE);
double values[STORM_EIGENADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE * STORM_EIGENADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE];
sm.initialize(STORM_EIGENADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE * STORM_EIGENADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE);
int row = 0;
int col = 0;
for (int i = 0; i < STORM_EIGENADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE * STORM_EIGENADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE; ++i) {
values[i] = static_cast<double>(i + 1);
sm.addNextValue(row, col, values[i]);
++col;
if (col == STORM_EIGENADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE) {
++row;
col = 0;
}
}
sm.finalize();
auto esm = storm::adapters::EigenAdapter::toEigenSparseMatrix(sm);
ASSERT_EQ(esm->rows(), STORM_EIGENADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE);
ASSERT_EQ(esm->cols(), STORM_EIGENADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE);
ASSERT_EQ(esm->nonZeros(), STORM_EIGENADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE * STORM_EIGENADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE);
row = 0;
col = 0;
for (int i = 0; i < STORM_EIGENADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE * STORM_EIGENADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE; ++i) {
ASSERT_EQ(values[i], esm->coeff(row, col));
++col;
if (col == STORM_EIGENADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE) {
++row;
col = 0;
}
}
delete esm;
}
TEST(EigenAdapterTest, SimpleSparseSquareCopy) {
// 5 rows
storm::storage::SparseMatrix<double> sm(STORM_EIGENADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE);
double values[STORM_EIGENADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE * STORM_EIGENADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE];
sm.initialize((STORM_EIGENADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE * STORM_EIGENADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE + 1) / 2);
int row = 0;
int col = 0;
bool everySecondElement = true;
for (int i = 0; i < STORM_EIGENADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE * STORM_EIGENADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE; ++i) {
values[i] = static_cast<double>(i + 1);
if (everySecondElement) {
sm.addNextValue(row, col, values[i]);
}
everySecondElement = !everySecondElement;
++col;
if (col == STORM_EIGENADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE) {
++row;
col = 0;
}
}
sm.finalize();
auto esm = storm::adapters::EigenAdapter::toEigenSparseMatrix(sm);
ASSERT_EQ(esm->rows(), STORM_EIGENADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE);
ASSERT_EQ(esm->cols(), STORM_EIGENADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE);
ASSERT_EQ(esm->nonZeros(), (STORM_EIGENADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE * STORM_EIGENADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE + 1) / 2);
row = 0;
col = 0;
everySecondElement = true;
for (int i = 0; i < STORM_EIGENADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE * STORM_EIGENADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE; ++i) {
if (everySecondElement) {
ASSERT_EQ(values[i], esm->coeff(row, col));
}
everySecondElement = !everySecondElement;
++col;
if (col == STORM_EIGENADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE) {
++row;
col = 0;
}
}
delete esm;
}

111
test/functional/storage/adapters/GmmAdapterTest.cpp

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

104
test/functional/storage/adapters/StormAdapterTest.cpp

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

BIN
util/checklist/storage.ods

Loading…
Cancel
Save