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

Further work on iterators for sparse matrix. 

Former-commit-id: 8e78262161
main
dehnert 12 years ago
parent
ab5b5be1ac
commit
cf2b84b281
23 changed files with 309 additions and 369 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 2
      CMakeLists.txt
  2. 109
      src/adapters/GmmxxAdapter.h
  3. 50
      src/counterexamples/MILPMinimalLabelSetGenerator.h
  4. 100
      src/counterexamples/PathBasedSubsystemGenerator.h
  5. 32
      src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h
  6. 2
      src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h
  7. 8
      src/models/AbstractDeterministicModel.h
  8. 2
      src/models/AbstractModel.h
  9. 16
      src/models/AbstractNondeterministicModel.h
  10. 14
      src/models/Dtmc.h
  11. 18
      src/models/MarkovAutomaton.h
  12. 16
      src/parser/DeterministicSparseTransitionParser.cpp
  13. 14
      src/storage/MaximalEndComponentDecomposition.cpp
  14. 58
      src/storage/SparseMatrix.cpp
  15. 20
      src/storage/SparseMatrix.h
  16. 20
      src/storage/StronglyConnectedComponentDecomposition.cpp
  17. 10
      src/utility/counterexamples.h
  18. 98
      src/utility/graph.h
  19. 4
      src/utility/matrix.h
  20. 24
      test/functional/storage/SparseMatrixTest.cpp
  21. 1
      test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp
  22. 2
      test/performance/storage/SparseMatrixTest.cpp

2
CMakeLists.txt
View File

@ -144,7 +144,7 @@ else(CLANG)
# As CLANG is not set as a variable, we need to set it in case we have not matched another compiler. # As CLANG is not set as a variable, we need to set it in case we have not matched another compiler.
set (CLANG ON) set (CLANG ON)
# Set standard flags for clang # Set standard flags for clang
set (CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -funroll-loops -O4")
set (CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -funroll-loops -O3")
if(UNIX AND NOT APPLE AND NOT USE_LIBCXX) if(UNIX AND NOT APPLE AND NOT USE_LIBCXX)
set(CLANG_STDLIB libstdc++) set(CLANG_STDLIB libstdc++)
message(STATUS "StoRM - Linking against libstdc++") message(STATUS "StoRM - Linking against libstdc++")

109
src/adapters/GmmxxAdapter.h
View File

@ -40,12 +40,20 @@ public:
// 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());
// Copy Columns Indications
result->ir.resize(realNonZeros);
std::copy(matrix.columnIndications.begin(), matrix.columnIndications.end(), result->ir.begin());
// And do the same thing with the actual values.
result->pr.resize(realNonZeros);
std::copy(matrix.valueStorage.begin(), matrix.valueStorage.end(), result->pr.begin());
// Copy columns and values.
std::vector<T> values;
values.reserve(matrix.getEntryCount());
std::vector<uint_fast64_t> columns;
columns.reserve(matrix.getEntryCount());
for (auto const& entry : matrix) {
columns.emplace_back(entry.first);
values.emplace_back(entry.second);
}
std::swap(result->ir, columns);
std::swap(result->pr, values);
LOG4CPLUS_DEBUG(logger, "Done converting matrix to gmm++ format."); LOG4CPLUS_DEBUG(logger, "Done converting matrix to gmm++ format.");
@ -59,6 +67,7 @@ public:
template<class T> template<class T>
static gmm::csr_matrix<T>* toGmmxxSparseMatrix(storm::storage::SparseMatrix<T>&& matrix) { static gmm::csr_matrix<T>* toGmmxxSparseMatrix(storm::storage::SparseMatrix<T>&& matrix) {
uint_fast64_t realNonZeros = matrix.getEntryCount(); uint_fast64_t realNonZeros = matrix.getEntryCount();
std::cout << "here?!" << std::endl;
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.
@ -71,88 +80,22 @@ public:
// Move Row Indications // Move Row Indications
result->jc.~vectorType_ull_t(); // Call Destructor inplace result->jc.~vectorType_ull_t(); // Call Destructor inplace
new (&result->jc) vectorType_ull_t(std::move(*storm::utility::ConversionHelper::toUnsignedLongLong(&matrix.rowIndications))); new (&result->jc) vectorType_ull_t(std::move(*storm::utility::ConversionHelper::toUnsignedLongLong(&matrix.rowIndications)));
// Move Columns Indications
result->ir.~vectorType_ull_t(); // Call Destructor inplace
new (&result->ir) vectorType_ull_t(std::move(*storm::utility::ConversionHelper::toUnsignedLongLong(&matrix.columnIndications)));
// And do the same thing with the actual values.
result->pr.~vectorType_T_t(); // Call Destructor inplace
new (&result->pr) vectorType_T_t(std::move(matrix.valueStorage));
LOG4CPLUS_DEBUG(logger, "Done converting matrix to gmm++ format.");
return result;
}
/*!
* Converts a sparse matrix in the gmm++ format to Storm Sparse Matrix format.
* @return A pointer to a row-major sparse matrix in our format.
*/
template<class T>
static storm::storage::SparseMatrix<T>* fromGmmxxSparseMatrix(gmm::csr_matrix<T> const& matrix) {
uint_fast64_t realNonZeros = gmm::nnz(matrix);
LOG4CPLUS_DEBUG(logger, "Converting matrix with " << realNonZeros << " non-zeros from gmm++ format into Storm.");
// Prepare the resulting matrix.
storm::storage::SparseMatrix<T>* result = new storm::storage::SparseMatrix<T>(matrix.nrows(), matrix.ncols());
// Set internal NonZero Counter
result->nonZeroEntryCount = realNonZeros;
result->setState(result->Initialized);
if (!result->prepareInternalStorage(false)) {
LOG4CPLUS_ERROR(logger, "Unable to allocate internal storage while converting GMM++ Matrix to Storm.");
delete result;
return nullptr;
} else {
// Copy columns and values.
std::vector<T> values;
values.reserve(matrix.getEntryCount());
std::vector<uint_fast64_t> columns;
columns.reserve(matrix.getEntryCount());
// 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;
for (auto const& entry : matrix) {
columns.emplace_back(entry.first);
values.emplace_back(entry.second);
} }
result->finalize();
LOG4CPLUS_DEBUG(logger, "Done converting matrix to storm format.");
return result;
}
/*!
* Converts a sparse matrix in the gmm++ format to Storm Sparse Matrix format.
* @return A pointer to a row-major sparse matrix in our format.
*/
template<class T>
static storm::storage::SparseMatrix<T>* fromGmmxxSparseMatrix(gmm::csr_matrix<T> && matrix) {
uint_fast64_t realNonZeros = gmm::nnz(matrix);
LOG4CPLUS_DEBUG(logger, "Converting matrix with " << realNonZeros << " non-zeros from gmm++ format into Storm.");
std::swap(result->ir, columns);
std::swap(result->pr, values);
// 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);
// Move Row Indications
result->rowIndications = std::vector<uint_fast64_t>(std::move(matrix.jc));
// Move Columns Indications
result->columnIndications = std::vector<uint_fast64_t>(std::move(matrix.ir));
// And do the same thing with the actual values.
result->valueStorage = std::vector<T>(std::move(matrix.pr));
result->currentSize = realNonZeros;
result->lastRow = matrix.nrows() - 1;
result->finalize();
LOG4CPLUS_DEBUG(logger, "Done converting matrix to storm format.");
LOG4CPLUS_DEBUG(logger, "Done converting matrix to gmm++ format.");
return result; return result;
} }

50
src/counterexamples/MILPMinimalLabelSetGenerator.h
View File

@ -131,7 +131,7 @@ namespace storm {
bool allSuccessorsProblematic = true; bool allSuccessorsProblematic = true;
for (auto const& successorEntry : transitionMatrix.getRow(row)) { 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(successorEntry.column()) || psiStates.get(successorEntry.column())) {
if (stateInformation.relevantStates.get(successorEntry.first) || psiStates.get(successorEntry.first)) {
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(successorEntry.column())) {
if (!stateInformation.problematicStates.get(successorEntry.first)) {
allSuccessorsProblematic = false; allSuccessorsProblematic = false;
} }
} }
@ -304,11 +304,11 @@ 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 (auto const& successorEntry : labeledMdp.getTransitionMatrix().getRow(row)) { for (auto const& successorEntry : labeledMdp.getTransitionMatrix().getRow(row)) {
if (stateInformation.relevantStates.get(successorEntry.column())) {
if (resultingMap.find(successorEntry.column()) == resultingMap.end()) {
if (stateInformation.relevantStates.get(successorEntry.first)) {
if (resultingMap.find(successorEntry.first) == resultingMap.end()) {
variableNameBuffer.str(""); variableNameBuffer.str("");
variableNameBuffer.clear(); variableNameBuffer.clear();
variableNameBuffer << "r" << successorEntry.column();
variableNameBuffer << "r" << successorEntry.first;
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;
} }
@ -338,11 +338,11 @@ 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 (auto const& successorEntry : labeledMdp.getTransitionMatrix().getRow(row)) { for (auto const& successorEntry : labeledMdp.getTransitionMatrix().getRow(row)) {
if (stateInformation.relevantStates.get(successorEntry.column())) {
if (stateInformation.relevantStates.get(successorEntry.first)) {
variableNameBuffer.str(""); variableNameBuffer.str("");
variableNameBuffer.clear(); variableNameBuffer.clear();
variableNameBuffer << "t" << state << "to" << successorEntry.column();
resultingMap[std::make_pair(state, successorEntry.column())] = solver.createBinaryVariable(variableNameBuffer.str(), 0);
variableNameBuffer << "t" << state << "to" << successorEntry.first;
resultingMap[std::make_pair(state, successorEntry.first)] = solver.createBinaryVariable(variableNameBuffer.str(), 0);
++numberOfVariablesCreated; ++numberOfVariablesCreated;
} }
} }
@ -551,11 +551,11 @@ namespace storm {
double rightHandSide = 1; double rightHandSide = 1;
for (auto const& successorEntry : labeledMdp.getTransitionMatrix().getRow(choice)) { 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();
if (stateInformation.relevantStates.get(successorEntry.first)) {
variables.push_back(static_cast<int>(variableInformation.stateToProbabilityVariableIndexMap.at(successorEntry.first)));
coefficients.push_back(-successorEntry.second);
} else if (psiStates.get(successorEntry.first)) {
rightHandSide += successorEntry.second;
} }
} }
@ -609,7 +609,7 @@ namespace storm {
coefficients.push_back(1); coefficients.push_back(1);
for (auto const& successorEntry : labeledMdp.getTransitionMatrix().getRow(problematicChoice)) { for (auto const& successorEntry : labeledMdp.getTransitionMatrix().getRow(problematicChoice)) {
variables.push_back(variableInformation.problematicTransitionToVariableIndexMap.at(std::make_pair(stateListPair.first, successorEntry.column())));
variables.push_back(variableInformation.problematicTransitionToVariableIndexMap.at(std::make_pair(stateListPair.first, successorEntry.first)));
coefficients.push_back(-1); coefficients.push_back(-1);
} }
@ -626,9 +626,9 @@ namespace storm {
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(successorEntry.column()));
variables.push_back(variableInformation.problematicStateToVariableIndexMap.at(successorEntry.first));
coefficients.push_back(-1); coefficients.push_back(-1);
variables.push_back(variableInformation.problematicTransitionToVariableIndexMap.at(std::make_pair(state, successorEntry.column())));
variables.push_back(variableInformation.problematicTransitionToVariableIndexMap.at(std::make_pair(state, successorEntry.first)));
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,7 +684,7 @@ namespace storm {
for (auto choice : choiceInformation.relevantChoicesForRelevantStates.at(state)) { for (auto choice : choiceInformation.relevantChoicesForRelevantStates.at(state)) {
bool psiStateReachableInOneStep = false; bool psiStateReachableInOneStep = false;
for (auto const& successorEntry : labeledMdp.getTransitionMatrix().getRow(choice)) { for (auto const& successorEntry : labeledMdp.getTransitionMatrix().getRow(choice)) {
if (psiStates.get(successorEntry.column())) {
if (psiStates.get(successorEntry.first)) {
psiStateReachableInOneStep = true; psiStateReachableInOneStep = true;
} }
} }
@ -697,8 +697,8 @@ namespace storm {
coefficients.push_back(1); coefficients.push_back(1);
for (auto const& successorEntry : labeledMdp.getTransitionMatrix().getRow(choice)) { 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());
if (state != successorEntry.first && stateInformation.relevantStates.get(successorEntry.first)) {
std::list<uint_fast64_t> const& successorChoiceVariableIndices = variableInformation.stateToChoiceVariablesIndexMap.at(successorEntry.first);
for (auto choiceVariableIndex : successorChoiceVariableIndices) { for (auto choiceVariableIndex : successorChoiceVariableIndices) {
variables.push_back(choiceVariableIndex); variables.push_back(choiceVariableIndex);
@ -727,8 +727,8 @@ 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 (auto const& predecessorEntry : backwardTransitions.getRow(state)) { for (auto const& predecessorEntry : backwardTransitions.getRow(state)) {
if (state != predecessorEntry.column()) {
predecessors.insert(predecessorEntry.column());
if (state != predecessorEntry.first) {
predecessors.insert(predecessorEntry.first);
} }
} }
@ -744,7 +744,7 @@ namespace storm {
// Check if the current choice targets the current state. // Check if the current choice targets the current state.
for (auto const& successorEntry : labeledMdp.getTransitionMatrix().getRow(relevantChoice)) { for (auto const& successorEntry : labeledMdp.getTransitionMatrix().getRow(relevantChoice)) {
if (state == successorEntry.column()) {
if (state == successorEntry.first) {
choiceTargetsCurrentState = true; choiceTargetsCurrentState = true;
break; break;
} }
@ -789,8 +789,8 @@ namespace storm {
for (auto psiState : psiStates) { for (auto psiState : psiStates) {
// Compute the set of predecessors. // Compute the set of predecessors.
for (auto const& predecessorEntry : backwardTransitions.getRow(psiState)) { for (auto const& predecessorEntry : backwardTransitions.getRow(psiState)) {
if (psiState != predecessorEntry.column()) {
predecessors.insert(predecessorEntry.column());
if (psiState != predecessorEntry.first) {
predecessors.insert(predecessorEntry.first);
} }
} }
} }
@ -807,7 +807,7 @@ namespace storm {
// Check if the current choice targets the current state. // Check if the current choice targets the current state.
for (auto const& successorEntry : labeledMdp.getTransitionMatrix().getRow(relevantChoice)) { for (auto const& successorEntry : labeledMdp.getTransitionMatrix().getRow(relevantChoice)) {
if (psiStates.get(successorEntry.column())) {
if (psiStates.get(successorEntry.first)) {
choiceTargetsPsiState = true; choiceTargetsPsiState = true;
break; break;
} }

100
src/counterexamples/PathBasedSubsystemGenerator.h
View File

@ -67,33 +67,33 @@ public:
distances[init].second = (T) 1; distances[init].second = (T) 1;
} }
for(auto& trans : transMat.getRow(init)) {
for(auto const& 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.second != (T) 0 && !subSysStates.get(trans.first)) {
//new state? //new state?
if(distances[trans.column()].second == (T) -1) {
distances[trans.column()].first = init;
distances[trans.column()].second = trans.value();
if(distances[trans.first].second == (T) -1) {
distances[trans.first].first = init;
distances[trans.first].second = trans.second;
activeSet.insert(std::pair<uint_fast64_t, T>(trans.column(), distances[trans.column()].second));
activeSet.insert(std::pair<uint_fast64_t, T>(trans.first, distances[trans.first].second));
} }
else if(distances[trans.column()].second < trans.value()){
else if(distances[trans.first].second < trans.second){
//This state has already been discovered //This state has already been discovered
//And the distance can be improved by using this transition. //And the distance can be improved by using this transition.
//find state in set, remove it, reenter it with new and correct values. //find state in set, remove it, reenter it with new and correct values.
auto range = activeSet.equal_range(std::pair<uint_fast64_t, T>(trans.column(), distances[trans.column()].second));
auto range = activeSet.equal_range(std::pair<uint_fast64_t, T>(trans.first, distances[trans.first].second));
for(;range.first != range.second; range.first++) { for(;range.first != range.second; range.first++) {
if(trans.column() == range.first->first) {
if(trans.first == range.first->first) {
activeSet.erase(range.first); activeSet.erase(range.first);
break; break;
} }
} }
distances[trans.column()].first = init;
distances[trans.column()].second = trans.value();
distances[trans.first].first = init;
distances[trans.first].second = trans.second;
activeSet.insert(std::pair<uint_fast64_t, T>(trans.column(), trans.value()));
activeSet.insert(std::pair<uint_fast64_t, T>(trans.first, trans.second));
} }
} }
} }
@ -113,38 +113,38 @@ 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
for(auto& trans : transMat.getRow(activeState.first)) {
for(auto const& 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.second != (T) 0) {
T distance = activeState.second * trans.value();
T distance = activeState.second * trans.second;
//not discovered or initial terminal state //not discovered or initial terminal state
if(distances[trans.column()].second == (T)-1) {
if(distances[trans.first].second == (T)-1) {
//New state discovered -> save it //New state discovered -> save it
distances[trans.column()].first = activeState.first;
distances[trans.column()].second = distance;
distances[trans.first].first = activeState.first;
distances[trans.first].second = distance;
// push newly discovered state into activeSet // push newly discovered state into activeSet
activeSet.insert(std::pair<uint_fast64_t, T>(trans.column(), distance));
activeSet.insert(std::pair<uint_fast64_t, T>(trans.first, distance));
} }
else if(distances[trans.column()].second < distance ){
else if(distances[trans.first].second < distance ){
//This state has already been discovered //This state has already been discovered
//And the distance can be improved by using this transition. //And the distance can be improved by using this transition.
//find state in set, remove it, reenter it with new and correct values. //find state in set, remove it, reenter it with new and correct values.
auto range = activeSet.equal_range(std::pair<uint_fast64_t, T>(trans.column(), distances[trans.column()].second));
auto range = activeSet.equal_range(std::pair<uint_fast64_t, T>(trans.first, distances[trans.first].second));
for(;range.first != range.second; range.first++) { for(;range.first != range.second; range.first++) {
if(trans.column() == range.first->first) {
if(trans.first == range.first->first) {
activeSet.erase(range.first); activeSet.erase(range.first);
break; break;
} }
} }
distances[trans.column()].first = activeState.first;
distances[trans.column()].second = distance;
activeSet.insert(std::pair<uint_fast64_t, T>(trans.column(), distance));
distances[trans.first].first = activeState.first;
distances[trans.first].second = distance;
activeSet.insert(std::pair<uint_fast64_t, T>(trans.first, distance));
} }
} }
} }
@ -180,35 +180,35 @@ public:
continue; continue;
} }
for(auto& trans : transMat.getRow(init)) {
for(auto const& 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.second != (T) 0 && !subSysStates.get(trans.first)) {
//new state? //new state?
if(distances[trans.column()].second == (T) -1) {
if(distances[trans.first].second == (T) -1) {
//for initialization of subsys -> subsys search use prob (init -> subsys state -> found state) instead of prob(subsys state -> found state) //for initialization of subsys -> subsys search use prob (init -> subsys state -> found state) instead of prob(subsys state -> found state)
distances[trans.column()].first = init;
distances[trans.column()].second = trans.value() * (itDistances[init].second == -1 ? 1 : itDistances[init].second);
distances[trans.first].first = init;
distances[trans.first].second = trans.second * (itDistances[init].second == -1 ? 1 : itDistances[init].second);
activeSet.insert(std::pair<uint_fast64_t, T>(trans.column(), distances[trans.column()].second));
activeSet.insert(std::pair<uint_fast64_t, T>(trans.first, distances[trans.first].second));
} }
else if(distances[trans.column()].second < trans.value() * itDistances[init].second){
else if(distances[trans.first].second < trans.second * itDistances[init].second){
//This state has already been discovered //This state has already been discovered
//And the distance can be improved by using this transition. //And the distance can be improved by using this transition.
//find state in set, remove it, reenter it with new and correct values. //find state in set, remove it, reenter it with new and correct values.
auto range = activeSet.equal_range(std::pair<uint_fast64_t, T>(trans.column(), distances[trans.column()].second));
auto range = activeSet.equal_range(std::pair<uint_fast64_t, T>(trans.first, distances[trans.first].second));
for(;range.first != range.second; range.first++) { for(;range.first != range.second; range.first++) {
if(trans.column() == range.first->first) {
if(trans.first == range.first->first) {
activeSet.erase(range.first); activeSet.erase(range.first);
break; break;
} }
} }
//for initialization of subsys -> subsys search use prob (init -> subsys state -> found state) instead of prob(subsys state -> found state) //for initialization of subsys -> subsys search use prob (init -> subsys state -> found state) instead of prob(subsys state -> found state)
distances[trans.column()].first = init;
distances[trans.column()].second = trans.value() * (itDistances[init].second == -1 ? 1 : itDistances[init].second);
distances[trans.first].first = init;
distances[trans.first].second = trans.second * (itDistances[init].second == -1 ? 1 : itDistances[init].second);
activeSet.insert(std::pair<uint_fast64_t, T>(trans.column(), trans.value()));
activeSet.insert(std::pair<uint_fast64_t, T>(trans.first, trans.second));
} }
} }
} }
@ -231,38 +231,38 @@ 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
for(auto& trans : transMat.getRow(activeState.first)) {
for(auto const& 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.second != (T) 0) {
T distance = activeState.second * trans.value();
T distance = activeState.second * trans.second;
//not discovered or initial terminal state //not discovered or initial terminal state
if(distances[trans.column()].second == (T)-1) {
if(distances[trans.first].second == (T)-1) {
//New state discovered -> save it //New state discovered -> save it
distances[trans.column()].first = activeState.first;
distances[trans.column()].second = distance;
distances[trans.first].first = activeState.first;
distances[trans.first].second = distance;
// push newly discovered state into activeSet // push newly discovered state into activeSet
activeSet.insert(std::pair<uint_fast64_t, T>(trans.column(), distance));
activeSet.insert(std::pair<uint_fast64_t, T>(trans.first, distance));
} }
else if(distances[trans.column()].second < distance ){
else if(distances[trans.first].second < distance ){
//This state has already been discovered //This state has already been discovered
//And the distance can be improved by using this transition. //And the distance can be improved by using this transition.
//find state in set, remove it, reenter it with new and correct values. //find state in set, remove it, reenter it with new and correct values.
auto range = activeSet.equal_range(std::pair<uint_fast64_t, T>(trans.column(), distances[trans.column()].second));
auto range = activeSet.equal_range(std::pair<uint_fast64_t, T>(trans.first, distances[trans.first].second));
for(;range.first != range.second; range.first++) { for(;range.first != range.second; range.first++) {
if(trans.column() == range.first->first) {
if(trans.first == range.first->first) {
activeSet.erase(range.first); activeSet.erase(range.first);
break; break;
} }
} }
distances[trans.column()].first = activeState.first;
distances[trans.column()].second = distance;
activeSet.insert(std::pair<uint_fast64_t, T>(trans.column(), distance));
distances[trans.first].first = activeState.first;
distances[trans.first].second = distance;
activeSet.insert(std::pair<uint_fast64_t, T>(trans.first, distance));
} }
} }
} }

32
src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h
View File

@ -96,10 +96,10 @@ namespace storm {
for (auto state : markovianNonGoalStates) { for (auto state : markovianNonGoalStates) {
for (auto& element : aMarkovian.getRow(rowIndex)) { for (auto& element : aMarkovian.getRow(rowIndex)) {
ValueType eTerm = std::exp(-exitRates[state] * delta); ValueType eTerm = std::exp(-exitRates[state] * delta);
if (element.column() == rowIndex) {
element.value() = (storm::utility::constantOne<ValueType>() - eTerm) * element.value() + eTerm;
if (element.first == rowIndex) {
element.second = (storm::utility::constantOne<ValueType>() - eTerm) * element.second + eTerm;
} else { } else {
element.value() = (storm::utility::constantOne<ValueType>() - eTerm) * element.value();
element.second = (storm::utility::constantOne<ValueType>() - eTerm) * element.second;
} }
} }
++rowIndex; ++rowIndex;
@ -109,7 +109,7 @@ namespace storm {
rowIndex = 0; rowIndex = 0;
for (auto state : markovianNonGoalStates) { for (auto state : markovianNonGoalStates) {
for (auto element : aMarkovianToProbabilistic.getRow(rowIndex)) { for (auto element : aMarkovianToProbabilistic.getRow(rowIndex)) {
element.value() = (1 - std::exp(-exitRates[state] * delta)) * element.value();
element.second = (1 - std::exp(-exitRates[state] * delta)) * element.second;
} }
++rowIndex; ++rowIndex;
} }
@ -126,8 +126,8 @@ namespace storm {
bMarkovianFixed.push_back(storm::utility::constantZero<ValueType>()); bMarkovianFixed.push_back(storm::utility::constantZero<ValueType>());
for (auto element : transitionMatrix.getRow(nondeterministicChoiceIndices[state])) { for (auto element : transitionMatrix.getRow(nondeterministicChoiceIndices[state])) {
if (goalStates.get(element.column())) {
bMarkovianFixed.back() += (1 - std::exp(-exitRates[state] * delta)) * element.value();
if (goalStates.get(element.first)) {
bMarkovianFixed.back() += (1 - std::exp(-exitRates[state] * delta)) * element.second;
} }
} }
} }
@ -313,13 +313,13 @@ namespace storm {
typename storm::storage::SparseMatrix<ValueType>::Rows row = transitionMatrix.getRow(choice); typename storm::storage::SparseMatrix<ValueType>::Rows row = transitionMatrix.getRow(choice);
for (auto element : row) { for (auto element : row) {
if (statesNotContainedInAnyMec.get(element.column())) {
if (statesNotContainedInAnyMec.get(element.first)) {
// If the target state is not contained in an MEC, we can copy over the entry. // If the target state is not contained in an MEC, we can copy over the entry.
sspMatrix.insertNextValue(currentChoice, statesNotInMecsBeforeIndex[element.column()], element.value(), true);
sspMatrix.insertNextValue(currentChoice, statesNotInMecsBeforeIndex[element.first], element.second, true);
} else { } else {
// If the target state is contained in MEC i, we need to add the probability to the corresponding field in the vector // If the target state is contained in MEC i, we need to add the probability to the corresponding field in the vector
// so that we are able to write the cumulative probability to the MEC into the matrix. // so that we are able to write the cumulative probability to the MEC into the matrix.
auxiliaryStateToProbabilityMap[stateToMecIndexMap[element.column()]] += element.value();
auxiliaryStateToProbabilityMap[stateToMecIndexMap[element.first]] += element.second;
} }
} }
@ -350,13 +350,13 @@ namespace storm {
typename storm::storage::SparseMatrix<ValueType>::Rows row = transitionMatrix.getRow(choice); typename storm::storage::SparseMatrix<ValueType>::Rows row = transitionMatrix.getRow(choice);
for (auto element : row) { for (auto element : row) {
if (statesNotContainedInAnyMec.get(element.column())) {
if (statesNotContainedInAnyMec.get(element.first)) {
// If the target state is not contained in an MEC, we can copy over the entry. // If the target state is not contained in an MEC, we can copy over the entry.
sspMatrix.insertNextValue(currentChoice, statesNotInMecsBeforeIndex[element.column()], element.value(), true);
sspMatrix.insertNextValue(currentChoice, statesNotInMecsBeforeIndex[element.first], element.second, true);
} else { } else {
// If the target state is contained in MEC i, we need to add the probability to the corresponding field in the vector // If the target state is contained in MEC i, we need to add the probability to the corresponding field in the vector
// so that we are able to write the cumulative probability to the MEC into the matrix. // so that we are able to write the cumulative probability to the MEC into the matrix.
auxiliaryStateToProbabilityMap[stateToMecIndexMap[element.column()]] += element.value();
auxiliaryStateToProbabilityMap[stateToMecIndexMap[element.first]] += element.second;
} }
} }
@ -456,8 +456,8 @@ namespace storm {
typename storm::storage::SparseMatrix<ValueType>::Rows row = transitionMatrix.getRow(nondeterministicChoiceIndices[state]); typename storm::storage::SparseMatrix<ValueType>::Rows row = transitionMatrix.getRow(nondeterministicChoiceIndices[state]);
for (auto element : row) { for (auto element : row) {
variables.push_back(stateToVariableIndexMap.at(element.column()));
coefficients.push_back(-element.value());
variables.push_back(stateToVariableIndexMap.at(element.first));
coefficients.push_back(-element.second);
} }
variables.push_back(lraValueVariableIndex); variables.push_back(lraValueVariableIndex);
@ -476,8 +476,8 @@ namespace storm {
typename storm::storage::SparseMatrix<ValueType>::Rows row = transitionMatrix.getRow(choice); typename storm::storage::SparseMatrix<ValueType>::Rows row = transitionMatrix.getRow(choice);
for (auto element : row) { for (auto element : row) {
variables.push_back(stateToVariableIndexMap.at(element.column()));
coefficients.push_back(-element.value());
variables.push_back(stateToVariableIndexMap.at(element.first));
coefficients.push_back(-element.second);
} }
solver->addConstraint("state" + std::to_string(state), variables, coefficients, min ? storm::solver::LpSolver::LESS_EQUAL : storm::solver::LpSolver::GREATER_EQUAL, storm::utility::constantZero<ValueType>()); solver->addConstraint("state" + std::to_string(state), variables, coefficients, min ? storm::solver::LpSolver::LESS_EQUAL : storm::solver::LpSolver::GREATER_EQUAL, storm::utility::constantZero<ValueType>());

2
src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h
View File

@ -264,7 +264,9 @@ public:
// We need to identify the states which have to be taken out of the matrix, i.e. // We need to identify the states which have to be taken out of the matrix, i.e.
// all states that have probability 0 and 1 of satisfying the until-formula. // all states that have probability 0 and 1 of satisfying the until-formula.
LOG4CPLUS_INFO(logger, "Running Prob01.");
std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 = storm::utility::graph::performProb01(this->getModel(), phiStates, psiStates); std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 = storm::utility::graph::performProb01(this->getModel(), phiStates, psiStates);
LOG4CPLUS_INFO(logger, "Done running Prob01.");
storm::storage::BitVector statesWithProbability0 = std::move(statesWithProbability01.first); storm::storage::BitVector statesWithProbability0 = std::move(statesWithProbability01.first);
storm::storage::BitVector statesWithProbability1 = std::move(statesWithProbability01.second); storm::storage::BitVector statesWithProbability1 = std::move(statesWithProbability01.second);

8
src/models/AbstractDeterministicModel.h
View File

@ -90,10 +90,10 @@ class AbstractDeterministicModel: public AbstractModel<T> {
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) {
typename storm::storage::SparseMatrix<T>::const_rows row = this->transitionMatrix.getRow(i); 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;
for (auto const& transition : row) {
if (transition.second != storm::utility::constantZero<T>()) {
if (subsystem == nullptr || subsystem->get(transition.first)) {
outStream << "\t" << i << " -> " << transition.first << " [ label= \"" << transition.second << "\" ];" << std::endl;
} }
} }
} }

2
src/models/AbstractModel.h
View File

@ -170,7 +170,7 @@ class AbstractModel: public std::enable_shared_from_this<AbstractModel<T>> {
storm::storage::VectorSet<uint_fast64_t> allTargetBlocks; storm::storage::VectorSet<uint_fast64_t> allTargetBlocks;
for (auto state : block) { for (auto state : block) {
for (auto const& transitionEntry : this->getRows(state)) { for (auto const& transitionEntry : this->getRows(state)) {
uint_fast64_t targetBlock = stateToBlockMap[transitionEntry.column()];
uint_fast64_t targetBlock = stateToBlockMap[transitionEntry.first];
// We only need to consider transitions that are actually leaving the SCC. // We only need to consider transitions that are actually leaving the SCC.
if (targetBlock != currentBlockIndex) { if (targetBlock != currentBlockIndex) {

16
src/models/AbstractNondeterministicModel.h
View File

@ -134,8 +134,8 @@ namespace storm {
for (uint_fast64_t i = 0; i < numberOfStates; ++i) { for (uint_fast64_t i = 0; i < numberOfStates; ++i) {
typename storm::storage::SparseMatrix<T>::const_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) {
++rowIndications[transition.column() + 1];
if (transition.second > 0) {
++rowIndications[transition.first + 1];
} }
} }
} }
@ -153,10 +153,10 @@ namespace storm {
// 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>::const_rows rows = this->getRows(i); typename storm::storage::SparseMatrix<T>::const_rows rows = this->getRows(i);
for (auto& transition : rows) {
if (transition.value() > 0) {
values[nextIndices[transition.column()]] = transition.value();
columnIndications[nextIndices[transition.column()]++] = i;
for (auto const& transition : rows) {
if (transition.second > 0) {
values[nextIndices[transition.first]] = transition.second;
columnIndications[nextIndices[transition.first]++] = i;
} }
} }
} }
@ -240,8 +240,8 @@ namespace storm {
// Now draw all probabilitic arcs that belong to this nondeterminstic choice. // Now draw all probabilitic arcs that belong to this nondeterminstic choice.
for (auto const& transition : row) { for (auto const& transition : row) {
if (subsystem == nullptr || subsystem->get(transition.column())) {
outStream << "\t\"" << state << "c" << choice << "\" -> " << transition.column() << " [ label= \"" << transition.value() << "\" ]";
if (subsystem == nullptr || subsystem->get(transition.first)) {
outStream << "\t\"" << state << "c" << choice << "\" -> " << transition.first << " [ label= \"" << transition.second << "\" ]";
// 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) {

14
src/models/Dtmc.h
View File

@ -169,8 +169,8 @@ public:
std::vector<uint_fast64_t> stateMapping; std::vector<uint_fast64_t> stateMapping;
for(uint_fast64_t row = 0; row < origMat.getRowCount(); ++row) { for(uint_fast64_t row = 0; row < origMat.getRowCount(); ++row) {
if(subSysStates.get(row)){ if(subSysStates.get(row)){
for(auto& entry : origMat.getRow(row)) {
if(subSysStates.get(entry.column())) {
for(auto const& entry : origMat.getRow(row)) {
if(subSysStates.get(entry.first)) {
subSysTransitionCount++; subSysTransitionCount++;
} }
} }
@ -198,10 +198,10 @@ public:
if(subSysStates.get(row)){ if(subSysStates.get(row)){
// Transfer transitions // Transfer transitions
for(auto& entry : origMat.getRow(row)) { for(auto& entry : origMat.getRow(row)) {
if(subSysStates.get(entry.column())) {
newMat.addNextValue(newRow, stateMapping[entry.column()], entry.value());
if(subSysStates.get(entry.first)) {
newMat.addNextValue(newRow, stateMapping[entry.first], entry.second);
} else { } else {
rest += entry.value();
rest += entry.second;
} }
} }
@ -253,8 +253,8 @@ public:
if(subSysStates.get(row)){ if(subSysStates.get(row)){
// Transfer transition rewards // Transfer transition rewards
for(auto& entry : this->getTransitionRewardMatrix().getRow(row)) { for(auto& entry : this->getTransitionRewardMatrix().getRow(row)) {
if(subSysStates.get(entry.column())) {
newTransRewards.addNextValue(newRow, stateMapping[entry.column()], entry.value());
if(subSysStates.get(entry.first)) {
newTransRewards.addNextValue(newRow, stateMapping[entry.first], entry.second);
} }
} }

18
src/models/MarkovAutomaton.h
View File

@ -149,7 +149,7 @@ namespace storm {
for (uint_fast64_t row = this->nondeterministicChoiceIndices[state] + (this->isHybridState(state) ? 1 : 0); row < this->nondeterministicChoiceIndices[state + 1]; ++row) { 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)) { for (auto const& entry : this->transitionMatrix.getRow(row)) {
newTransitionMatrix.addNextValue(currentChoice, entry.column(), entry.value());
newTransitionMatrix.addNextValue(currentChoice, entry.first, entry.second);
} }
++currentChoice; ++currentChoice;
} }
@ -234,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& transition : row) {
if (subsystem == nullptr || subsystem->get(transition.column())) {
outStream << "\t\"" << state << "c" << choice << "\" -> " << transition.column() << " [ label= \"" << transition.value() << "\" ]";
for (auto const& transition : row) {
if (subsystem == nullptr || subsystem->get(transition.first)) {
outStream << "\t\"" << state << "c" << choice << "\" -> " << transition.first << " [ label= \"" << transition.second << "\" ]";
// 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) {
@ -251,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& transition : row) {
if (subsystem == nullptr || subsystem->get(transition.column())) {
outStream << "\t\"" << state << "\" -> " << transition.column() << " [ label= \"" << transition.value() << " (" << this->exitRates[state] << ")\" ]";
for (auto const& transition : row) {
if (subsystem == nullptr || subsystem->get(transition.first)) {
outStream << "\t\"" << state << "\" -> " << transition.first << " [ label= \"" << transition.second << " (" << this->exitRates[state] << ")\" ]";
} }
} }
} }
@ -272,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>::iterator it = this->transitionMatrix.begin(this->getNondeterministicChoiceIndices()[state]), ite = this->transitionMatrix.begin(this->getNondeterministicChoiceIndices()[state + 1]); it != ite; ++it) {
it.value() /= this->exitRates[state];
for (auto& transition : this->transitionMatrix.getRow(this->getNondeterministicChoiceIndices()[state])) {
transition.second /= this->exitRates[state];
} }
} }
} }

16
src/parser/DeterministicSparseTransitionParser.cpp
View File

@ -226,9 +226,9 @@ storm::storage::SparseMatrix<double> DeterministicSparseTransitionParser(std::st
if ((lastRow != -1) && (!rowHadDiagonalEntry)) { if ((lastRow != -1) && (!rowHadDiagonalEntry)) {
if (insertDiagonalEntriesIfMissing && !isRewardMatrix) { if (insertDiagonalEntriesIfMissing && !isRewardMatrix) {
resultMatrix.addNextValue(lastRow, lastRow, storm::utility::constantZero<double>()); resultMatrix.addNextValue(lastRow, lastRow, storm::utility::constantZero<double>());
LOG4CPLUS_DEBUG(logger, "While parsing " << filename << ": state " << lastRow << " has no transition to itself. Inserted a 0-transition. (1)");
// LOG4CPLUS_DEBUG(logger, "While parsing " << filename << ": state " << lastRow << " has no transition to itself. Inserted a 0-transition. (1)");
} else if (!isRewardMatrix) { } else if (!isRewardMatrix) {
LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": state " << lastRow << " has no transition to itself.");
// LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": state " << lastRow << " has no transition to itself.");
} }
// No increment for lastRow // No increment for lastRow
rowHadDiagonalEntry = true; rowHadDiagonalEntry = true;
@ -238,9 +238,9 @@ storm::storage::SparseMatrix<double> DeterministicSparseTransitionParser(std::st
if (fixDeadlocks && !isRewardMatrix) { if (fixDeadlocks && !isRewardMatrix) {
resultMatrix.addNextValue(skippedRow, skippedRow, storm::utility::constantOne<double>()); resultMatrix.addNextValue(skippedRow, skippedRow, storm::utility::constantOne<double>());
rowHadDiagonalEntry = true; rowHadDiagonalEntry = true;
LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": state " << skippedRow << " has no outgoing transitions. A self-loop was inserted.");
// LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": state " << skippedRow << " has no outgoing transitions. A self-loop was inserted.");
} else if (!isRewardMatrix) { } else if (!isRewardMatrix) {
LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": state " << skippedRow << " has no outgoing transitions.");
// LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": state " << skippedRow << " has no outgoing transitions.");
// FIXME Why no exception at this point? This will break the App. // FIXME Why no exception at this point? This will break the App.
} }
} }
@ -254,9 +254,9 @@ storm::storage::SparseMatrix<double> DeterministicSparseTransitionParser(std::st
rowHadDiagonalEntry = true; rowHadDiagonalEntry = true;
if (insertDiagonalEntriesIfMissing && !isRewardMatrix) { if (insertDiagonalEntriesIfMissing && !isRewardMatrix) {
resultMatrix.addNextValue(row, row, storm::utility::constantZero<double>()); resultMatrix.addNextValue(row, row, storm::utility::constantZero<double>());
LOG4CPLUS_DEBUG(logger, "While parsing " << filename << ": state " << row << " has no transition to itself. Inserted a 0-transition. (2)");
// LOG4CPLUS_DEBUG(logger, "While parsing " << filename << ": state " << row << " has no transition to itself. Inserted a 0-transition. (2)");
} else if (!isRewardMatrix) { } else if (!isRewardMatrix) {
LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": state " << row << " has no transition to itself.");
// LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": state " << row << " has no transition to itself.");
} }
} }
@ -267,9 +267,9 @@ storm::storage::SparseMatrix<double> DeterministicSparseTransitionParser(std::st
if (!rowHadDiagonalEntry) { if (!rowHadDiagonalEntry) {
if (insertDiagonalEntriesIfMissing && !isRewardMatrix) { if (insertDiagonalEntriesIfMissing && !isRewardMatrix) {
resultMatrix.addNextValue(lastRow, lastRow, storm::utility::constantZero<double>()); resultMatrix.addNextValue(lastRow, lastRow, storm::utility::constantZero<double>());
LOG4CPLUS_DEBUG(logger, "While parsing " << filename << ": state " << lastRow << " has no transition to itself. Inserted a 0-transition. (3)");
// LOG4CPLUS_DEBUG(logger, "While parsing " << filename << ": state " << lastRow << " has no transition to itself. Inserted a 0-transition. (3)");
} else if (!isRewardMatrix) { } else if (!isRewardMatrix) {
LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": state " << lastRow << " has no transition to itself.");
// LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": state " << lastRow << " has no transition to itself.");
} }
} }

14
src/storage/MaximalEndComponentDecomposition.cpp
View File

@ -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 (auto& entry : transitionMatrix.getRow(choice)) {
if (!scc.contains(entry.column())) {
for (auto const& entry : transitionMatrix.getRow(choice)) {
if (!scc.contains(entry.first)) {
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 (auto& entry : transitionMatrix.getRow(state)) {
if (scc.contains(entry.column())) {
statesToCheck.set(entry.column());
for (auto const& entry : transitionMatrix.getRow(state)) {
if (scc.contains(entry.first)) {
statesToCheck.set(entry.first);
} }
} }
} }
@ -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 (auto& entry : transitionMatrix.getRow(choice)) {
if (!mecStateSet.contains(entry.column())) {
for (auto const& entry : transitionMatrix.getRow(choice)) {
if (!mecStateSet.contains(entry.first)) {
choiceContained = false; choiceContained = false;
break; break;
} }

58
src/storage/SparseMatrix.cpp
View File

@ -11,33 +11,33 @@ namespace storm {
namespace storage { namespace storage {
template<typename T> template<typename T>
SparseMatrix<T>::rows::rows(std::pair<uint_fast64_t, T>* columnAndValuePtr, uint_fast64_t entryCount) : columnAndValuePtr(columnAndValuePtr), entryCount(entryCount) {
SparseMatrix<T>::rows::rows(iterator begin, uint_fast64_t entryCount) : beginIterator(begin), entryCount(entryCount) {
// Intentionally left empty. // Intentionally left empty.
} }
template<typename T> template<typename T>
typename SparseMatrix<T>::iterator SparseMatrix<T>::rows::begin() { typename SparseMatrix<T>::iterator SparseMatrix<T>::rows::begin() {
return columnAndValuePtr;
return beginIterator;
} }
template<typename T> template<typename T>
typename SparseMatrix<T>::iterator SparseMatrix<T>::rows::end() { typename SparseMatrix<T>::iterator SparseMatrix<T>::rows::end() {
return columnAndValuePtr + entryCount;
return beginIterator + entryCount;
} }
template<typename T> template<typename T>
SparseMatrix<T>::const_rows::const_rows(std::pair<uint_fast64_t, T> const* columnAndValuePtr, uint_fast64_t entryCount) : columnAndValuePtr(columnAndValuePtr), entryCount(entryCount) {
SparseMatrix<T>::const_rows::const_rows(const_iterator begin, uint_fast64_t entryCount) : beginIterator(begin), entryCount(entryCount) {
// Intentionally left empty. // Intentionally left empty.
} }
template<typename T> template<typename T>
typename SparseMatrix<T>::const_iterator SparseMatrix<T>::const_rows::begin() const { typename SparseMatrix<T>::const_iterator SparseMatrix<T>::const_rows::begin() const {
return columnAndValuePtr;
return beginIterator;
} }
template<typename T> template<typename T>
typename SparseMatrix<T>::const_iterator SparseMatrix<T>::const_rows::end() const { typename SparseMatrix<T>::const_iterator SparseMatrix<T>::const_rows::end() const {
return columnAndValuePtr + entryCount;
return beginIterator + entryCount;
} }
template<typename T> template<typename T>
@ -66,7 +66,7 @@ namespace storm {
} }
template<typename T> template<typename T>
SparseMatrix<T>::SparseMatrix(uint_fast64_t columnCount, std::vector<uint_fast64_t> const& rowIndications, std::vector<std::pair<uint_fast64_t, T>> const& columnsAndValues) : rowCount(rowIndications.size() - 1), columnCount(columnCount), entryCount(values.size()), storagePreallocated(true), columnsAndValues(columnsAndValues), rowIndications(rowIndications), internalStatus(INITIALIZED), currentEntryCount(0), lastRow(0), lastColumn(0) {
SparseMatrix<T>::SparseMatrix(uint_fast64_t columnCount, std::vector<uint_fast64_t> const& rowIndications, std::vector<std::pair<uint_fast64_t, T>> const& columnsAndValues) : rowCount(rowIndications.size() - 1), columnCount(columnCount), entryCount(columnsAndValues.size()), storagePreallocated(true), columnsAndValues(columnsAndValues), rowIndications(rowIndications), internalStatus(INITIALIZED), currentEntryCount(0), lastRow(0), lastColumn(0) {
// Intentionally left empty. // Intentionally left empty.
} }
@ -87,7 +87,7 @@ namespace storm {
} }
template<typename T> template<typename T>
SparseMatrix<T>::SparseMatrix(uint_fast64_t columnCount, std::vector<uint_fast64_t>&& rowIndications, std::vector<std::pair<uint_fast64_t, T>>&& columnsAndValues) : rowCount(rowIndications.size() - 1), columnCount(columnCount), entryCount(values.size()), storagePreallocated(true), columnsAndValues(std::move(columnsAndValues)), 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<std::pair<uint_fast64_t, T>>&& columnsAndValues) : rowCount(rowIndications.size() - 1), columnCount(columnCount), entryCount(columnsAndValues.size()), storagePreallocated(true), columnsAndValues(std::move(columnsAndValues)), rowIndications(std::move(rowIndications)), internalStatus(INITIALIZED), currentEntryCount(0), lastRow(0), lastColumn(0) {
// Intentionally left empty. // Intentionally left empty.
} }
@ -359,8 +359,8 @@ namespace storm {
throw storm::exceptions::OutOfRangeException() << "Illegal call to SparseMatrix::makeRowAbsorbing: access to row " << row << " is out of bounds."; throw storm::exceptions::OutOfRangeException() << "Illegal call to SparseMatrix::makeRowAbsorbing: access to row " << row << " is out of bounds.";
} }
const_iterator columnValuePtr = columnsAndValues.begin() + rowIndications[row];
const_iterator columnValuePtrEnd = columnsAndValues.begin() + rowIndications[row + 1];
iterator columnValuePtr = this->begin(row);
iterator columnValuePtrEnd = this->end(row);
// If the row has no elements in it, we cannot make it absorbing, because we would need to move all elements // If the row has no elements in it, we cannot make it absorbing, because we would need to move all elements
// in the vector of nonzeros otherwise. // in the vector of nonzeros otherwise.
@ -373,7 +373,7 @@ namespace storm {
columnValuePtr->first = column; columnValuePtr->first = column;
columnValuePtr->second = storm::utility::constantOne<T>(); columnValuePtr->second = storm::utility::constantOne<T>();
++columnValuePtr; ++columnValuePtr;
for (; columnValuePtr != columnValuePtr; ++columnValuePtr) {
for (; columnValuePtr != columnValuePtrEnd; ++columnValuePtr) {
columnValuePtr->first = 0; columnValuePtr->first = 0;
columnValuePtr->second = storm::utility::constantZero<T>(); columnValuePtr->second = storm::utility::constantZero<T>();
} }
@ -383,7 +383,7 @@ namespace storm {
T SparseMatrix<T>::getConstrainedRowSum(uint_fast64_t row, storm::storage::BitVector const& constraint) const { T SparseMatrix<T>::getConstrainedRowSum(uint_fast64_t row, storm::storage::BitVector const& constraint) const {
checkReady("getConstrainedRowSum"); checkReady("getConstrainedRowSum");
T result(0); T result(0);
for (typename std::vector<std::pair<uint_fast64_t, T>>::const_iterator it = this->begin(row), ite = this->end(row); it != ite; ++it) {
for (const_iterator it = this->begin(row), ite = this->end(row); it != ite; ++it) {
if (constraint.get(it->first)) { if (constraint.get(it->first)) {
result += it->second; result += it->second;
} }
@ -633,7 +633,7 @@ namespace storm {
T one = storm::utility::constantOne<T>(); T one = storm::utility::constantOne<T>();
bool foundDiagonalElement = false; bool foundDiagonalElement = false;
for (uint_fast64_t row = 0; row < rowCount; ++row) { for (uint_fast64_t row = 0; row < rowCount; ++row) {
for (const_iterator it = this->begin(row), ite = this->end(row); it != ite; ++it) {
for (iterator it = this->begin(row), ite = this->end(row); it != ite; ++it) {
if (it->first == row) { if (it->first == row) {
it->second = one - it->second; it->second = one - it->second;
foundDiagonalElement = true; foundDiagonalElement = true;
@ -658,7 +658,7 @@ namespace storm {
// 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.
for (uint_fast64_t row = 0; row < rowCount; ++row) { for (uint_fast64_t row = 0; row < rowCount; ++row) {
for (const_iterator it = this->begin(row), ite = this->end(row); it != ite; ++it) {
for (iterator it = this->begin(row), ite = this->end(row); it != ite; ++it) {
if (it->first != row) { if (it->first != row) {
it->second = -it->second; it->second = -it->second;
} }
@ -677,7 +677,7 @@ namespace storm {
// 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.
for (uint_fast64_t row = 0; row < rowCount; ++row) { for (uint_fast64_t row = 0; row < rowCount; ++row) {
for (const_iterator it = this->begin(row), ite = this->end(row); it != ite; ++it) {
for (iterator it = this->begin(row), ite = this->end(row); it != ite; ++it) {
if (it->first == row) { if (it->first == row) {
it->second = storm::utility::constantZero<T>(); it->second = storm::utility::constantZero<T>();
} }
@ -785,13 +785,13 @@ namespace storm {
template<typename T> template<typename T>
typename SparseMatrix<T>::const_rows SparseMatrix<T>::getRows(uint_fast64_t startRow, uint_fast64_t endRow) const { typename SparseMatrix<T>::const_rows SparseMatrix<T>::getRows(uint_fast64_t startRow, uint_fast64_t endRow) const {
checkReady("getRows"); checkReady("getRows");
return const_rows(this->valueStorage.data() + this->rowIndications[startRow], this->columnIndications.data() + this->rowIndications[startRow], this->rowIndications[endRow + 1] - this->rowIndications[startRow]);
return const_rows(this->columnsAndValues.data() + this->rowIndications[startRow], this->rowIndications[endRow + 1] - this->rowIndications[startRow]);
} }
template<typename T> template<typename T>
typename SparseMatrix<T>::rows SparseMatrix<T>::getRows(uint_fast64_t startRow, uint_fast64_t endRow) { typename SparseMatrix<T>::rows SparseMatrix<T>::getRows(uint_fast64_t startRow, uint_fast64_t endRow) {
checkReady("getRows"); checkReady("getRows");
return rows(this->valueStorage.data() + this->rowIndications[startRow], this->columnIndications.data() + this->rowIndications[startRow], this->rowIndications[endRow + 1] - this->rowIndications[startRow]);
return rows(this->columnsAndValues.data() + this->rowIndications[startRow], this->rowIndications[endRow + 1] - this->rowIndications[startRow]);
} }
template<typename T> template<typename T>
@ -809,37 +809,37 @@ namespace storm {
template<typename T> template<typename T>
typename SparseMatrix<T>::const_iterator SparseMatrix<T>::begin(uint_fast64_t row) const { typename SparseMatrix<T>::const_iterator SparseMatrix<T>::begin(uint_fast64_t row) const {
checkReady("begin"); checkReady("begin");
return this->columnsAndValues.begin() + this->rowIndications[row];
return this->columnsAndValues.data() + this->rowIndications[row];
} }
template<typename T> template<typename T>
typename SparseMatrix<T>::iterator SparseMatrix<T>::begin(uint_fast64_t row) { typename SparseMatrix<T>::iterator SparseMatrix<T>::begin(uint_fast64_t row) {
checkReady("begin"); checkReady("begin");
return this->columnsAndValues.begin() + this->rowIndications[row];
return this->columnsAndValues.data() + this->rowIndications[row];
} }
template<typename T> template<typename T>
typename SparseMatrix<T>::const_iterator SparseMatrix<T>::end(uint_fast64_t row) const { typename SparseMatrix<T>::const_iterator SparseMatrix<T>::end(uint_fast64_t row) const {
checkReady("end"); checkReady("end");
return this->columnsAndValues.begin() + this->rowIndications[row + 1];
return this->columnsAndValues.data() + this->rowIndications[row + 1];
} }
template<typename T> template<typename T>
typename SparseMatrix<T>::iterator SparseMatrix<T>::end(uint_fast64_t row) { typename SparseMatrix<T>::iterator SparseMatrix<T>::end(uint_fast64_t row) {
checkReady("end"); checkReady("end");
return this->columnsAndValues.begin() + this->rowIndications[row + 1];
return this->columnsAndValues.data() + this->rowIndications[row + 1];
} }
template<typename T> template<typename T>
typename SparseMatrix<T>::const_iterator SparseMatrix<T>::end() const { typename SparseMatrix<T>::const_iterator SparseMatrix<T>::end() const {
checkReady("end"); checkReady("end");
return this->columnsAndValues.begin() + this->rowIndications[rowCount];
return this->columnsAndValues.data() + this->rowIndications[rowCount];
} }
template<typename T> template<typename T>
typename SparseMatrix<T>::iterator SparseMatrix<T>::end() { typename SparseMatrix<T>::iterator SparseMatrix<T>::end() {
checkReady("end"); checkReady("end");
return this->columnsAndValues.begin() + this->rowIndications[rowCount];
return this->columnsAndValues.data() + this->rowIndications[rowCount];
} }
template<typename T> template<typename T>
@ -863,12 +863,11 @@ 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 (const_iterator it1 = this->begin(row), ite1 = this->end(row), it2 = matrix.begin(row), ite2 = matrix.end(row); it1 != ite1; ++it1) { for (const_iterator it1 = this->begin(row), ite1 = this->end(row), it2 = matrix.begin(row), ite2 = matrix.end(row); it1 != ite1; ++it1) {
for (uint_fast64_t elem = rowIndications[row], elem2 = matrix.rowIndications[row]; elem < 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 (it2->first != ite2 && it2->first < it1->first) {
while (it2 != ite2 && it2->first < it1->first) {
++it2; ++it2;
} }
if (it2->first == ite2 || it1->first != it2->first) {
if (it2 == ite2 || it1->first != it2->first) {
return false; return false;
} }
} }
@ -934,8 +933,7 @@ namespace storm {
void SparseMatrix<T>::prepareInternalStorage() { void SparseMatrix<T>::prepareInternalStorage() {
// Only allocate the memory if the dimensions of the matrix are already known. // Only allocate the memory if the dimensions of the matrix are already known.
if (storagePreallocated) { if (storagePreallocated) {
valueStorage = std::vector<T>(entryCount, storm::utility::constantZero<T>());
columnIndications = std::vector<uint_fast64_t>(entryCount, 0);
columnsAndValues = std::vector<std::pair<uint_fast64_t, T>>(entryCount, std::make_pair(0, storm::utility::constantZero<T>()));
rowIndications = std::vector<uint_fast64_t>(rowCount + 1, 0); rowIndications = std::vector<uint_fast64_t>(rowCount + 1, 0);
} else { } else {
rowIndications.push_back(0); rowIndications.push_back(0);
@ -950,12 +948,8 @@ namespace storm {
} }
// Explicitly instantiate the matrix and the nested classes. // 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 std::ostream& operator<<(std::ostream& out, SparseMatrix<double> const& matrix); template std::ostream& operator<<(std::ostream& out, SparseMatrix<double> const& matrix);
template class SparseMatrix<int>::BaseIterator<int const>;
template class SparseMatrix<int>::BaseIterator<int>;
template class SparseMatrix<int>; template class SparseMatrix<int>;
template std::ostream& operator<<(std::ostream& out, SparseMatrix<int> const& matrix); template std::ostream& operator<<(std::ostream& out, SparseMatrix<int> const& matrix);

20
src/storage/SparseMatrix.h
View File

@ -68,8 +68,8 @@ namespace storm {
friend class tbbHelper_MatrixRowVectorScalarProduct; friend class tbbHelper_MatrixRowVectorScalarProduct;
#endif #endif
typedef typename std::vector<std::pair<uint_fast64_t, T>>::iterator iterator;
typedef typename std::vector<std::pair<uint_fast64_t, T>>::const_iterator const_iterator;
typedef std::pair<uint_fast64_t, T>* iterator;
typedef std::pair<uint_fast64_t, T> const* const_iterator;
/*! /*!
* This class represents a number of consecutive rows of the matrix. * This class represents a number of consecutive rows of the matrix.
@ -80,10 +80,10 @@ namespace storm {
* Constructs an object that represents the rows defined by the value of the first entry, the column * Constructs an object that represents the rows defined by the value of the first entry, the column
* of the first entry and the number of entries in this row set. * of the first entry and the number of entries in this row set.
* *
* @param columnAndValuePtr A pointer to the columnd and value of the first entry of the rows.
* @param begin An iterator that points to the beginning of the row.
* @param entryCount The number of entrys in the rows. * @param entryCount The number of entrys in the rows.
*/ */
rows(std::pair<uint_fast64_t, T>* columnAndValuePtr, uint_fast64_t entryCount);
rows(iterator begin, uint_fast64_t entryCount);
/*! /*!
* Retrieves an iterator that points to the beginning of the rows. * Retrieves an iterator that points to the beginning of the rows.
@ -101,7 +101,7 @@ namespace storm {
private: private:
// The pointer to the columnd and value of the first entry. // The pointer to the columnd and value of the first entry.
std::pair<uint_fast64_t, T>* columnAndValuePtr;
iterator beginIterator;
// The number of non-zero entries in the rows. // The number of non-zero entries in the rows.
uint_fast64_t entryCount; uint_fast64_t entryCount;
@ -116,10 +116,10 @@ namespace storm {
* Constructs an object that represents the rows defined by the value of the first entry, the column * Constructs an object that represents the rows defined by the value of the first entry, the column
* of the first entry and the number of entries in this row set. * of the first entry and the number of entries in this row set.
* *
* @param columnAndValuePtr A pointer to the columnd and value of the first entry of the rows.
* @param begin An iterator that points to the beginning of the row.
* @param entryCount The number of entrys in the rows. * @param entryCount The number of entrys in the rows.
*/ */
const_rows(std::pair<uint_fast64_t, T> const* columnAndValuePtr, uint_fast64_t entryCount);
const_rows(const_iterator begin, uint_fast64_t entryCount);
/*! /*!
* Retrieves an iterator that points to the beginning of the rows. * Retrieves an iterator that points to the beginning of the rows.
@ -137,7 +137,7 @@ namespace storm {
private: private:
// The pointer to the columnd and value of the first entry. // The pointer to the columnd and value of the first entry.
std::pair<uint_fast64_t, T> const* columnAndValuePtr;
const_iterator beginIterator;
// The number of non-zero entries in the rows. // The number of non-zero entries in the rows.
uint_fast64_t entryCount; uint_fast64_t entryCount;
@ -507,7 +507,7 @@ namespace storm {
* @param row The row past the end of which the iterator has to point. * @param row The row past the end of which the iterator has to point.
* @return An iterator that points past the end of the given row. * @return An iterator that points past the end of the given row.
*/ */
const_iterator end(uint_fast64_t row = 0) const;
const_iterator end(uint_fast64_t row) const;
/*! /*!
* Retrieves an iterator that points past the end of the given row. * Retrieves an iterator that points past the end of the given row.
@ -515,7 +515,7 @@ namespace storm {
* @param row The row past the end of which the iterator has to point. * @param row The row past the end of which the iterator has to point.
* @return An iterator that points past the end of the given row. * @return An iterator that points past the end of the given row.
*/ */
iterator end(uint_fast64_t row = 0);
iterator end(uint_fast64_t row);
/*! /*!
* Retrieves an iterator that points past the end of the last row of the matrix. * Retrieves an iterator that points past the end of the last row of the matrix.

20
src/storage/StronglyConnectedComponentDecomposition.cpp
View File

@ -127,40 +127,40 @@ namespace storm {
// Now, traverse all successors of the current state. // Now, traverse all successors of the current state.
for(; successorIt != model.getRows(currentState).end(); ++successorIt) { for(; successorIt != model.getRows(currentState).end(); ++successorIt) {
// Record if the current state has a self-loop if we are to drop naive SCCs later. // Record if the current state has a self-loop if we are to drop naive SCCs later.
if (dropNaiveSccs && currentState == successorIt.column()) {
if (dropNaiveSccs && currentState == successorIt->first) {
statesWithSelfloop.set(currentState, true); statesWithSelfloop.set(currentState, true);
} }
// If we have not visited the successor already, we need to perform the procedure // If we have not visited the successor already, we need to perform the procedure
// recursively on the newly found state, but only if it belongs to the subsystem in // recursively on the newly found state, but only if it belongs to the subsystem in
// which we are interested. // which we are interested.
if (subsystem.get(successorIt.column())) {
if (!visitedStates.get(successorIt.column())) {
if (subsystem.get(successorIt->first)) {
if (!visitedStates.get(successorIt->first)) {
// Save current iterator position so we can continue where we left off later. // Save current iterator position so we can continue where we left off later.
recursionIteratorStack.pop_back(); recursionIteratorStack.pop_back();
recursionIteratorStack.push_back(successorIt); recursionIteratorStack.push_back(successorIt);
// Put unvisited successor on top of our recursion stack and remember that. // Put unvisited successor on top of our recursion stack and remember that.
recursionStateStack.push_back(successorIt.column());
statesInStack[successorIt.column()] = true;
recursionStateStack.push_back(successorIt->first);
statesInStack[successorIt->first] = true;
// Also, put initial value for iterator on corresponding recursion stack. // Also, put initial value for iterator on corresponding recursion stack.
recursionIteratorStack.push_back(model.getRows(successorIt.column()).begin());
recursionIteratorStack.push_back(model.getRows(successorIt->first).begin());
// Perform the actual recursion step in an iterative way. // Perform the actual recursion step in an iterative way.
goto recursionStepForward; goto recursionStepForward;
recursionStepBackward: recursionStepBackward:
lowlinks[currentState] = std::min(lowlinks[currentState], lowlinks[successorIt.column()]);
lowlinks[currentState] = std::min(lowlinks[currentState], lowlinks[successorIt->first]);
// If we are interested in bottom SCCs only, we need to check whether the current state // If we are interested in bottom SCCs only, we need to check whether the current state
// can leave the SCC. // can leave the SCC.
if (onlyBottomSccs && lowlinks[currentState] != lowlinks[successorIt.column()]) {
if (onlyBottomSccs && lowlinks[currentState] != lowlinks[successorIt->first]) {
statesThatCanLeaveTheirScc.set(currentState); statesThatCanLeaveTheirScc.set(currentState);
} }
} else if (tarjanStackStates.get(successorIt.column())) {
} else if (tarjanStackStates.get(successorIt->first)) {
// Update the lowlink of the current state. // Update the lowlink of the current state.
lowlinks[currentState] = std::min(lowlinks[currentState], stateIndices[successorIt.column()]);
lowlinks[currentState] = std::min(lowlinks[currentState], stateIndices[successorIt->first]);
// Since it is known that in this case, the successor state is in the same SCC as the current state // Since it is known that in this case, the successor state is in the same SCC as the current state
// we don't need to update the bit vector of states that can leave their SCC. // we don't need to update the bit vector of states that can leave their SCC.

10
src/utility/counterexamples.h
View File

@ -35,8 +35,8 @@ namespace storm {
for (auto state : psiStates) { for (auto state : psiStates) {
analysisInformation[state] = std::set<uint_fast64_t>(); analysisInformation[state] = std::set<uint_fast64_t>();
for (auto& predecessorEntry : backwardTransitions.getRow(state)) { for (auto& predecessorEntry : backwardTransitions.getRow(state)) {
if (predecessorEntry.column() != state) {
worklist.push(std::make_pair(predecessorEntry.column(), state));
if (predecessorEntry.first != state) {
worklist.push(std::make_pair(predecessorEntry.first, state));
} }
} }
} }
@ -57,7 +57,7 @@ namespace storm {
bool choiceTargetsTargetState = false; bool choiceTargetsTargetState = false;
for (auto& entry : transitionMatrix.getRow(currentChoice)) { for (auto& entry : transitionMatrix.getRow(currentChoice)) {
if (entry.column() == targetState) {
if (entry.first == targetState) {
choiceTargetsTargetState = true; choiceTargetsTargetState = true;
break; break;
} }
@ -78,8 +78,8 @@ namespace storm {
if (analysisInformation[currentState].size() != analysisInformationSizeBefore) { if (analysisInformation[currentState].size() != analysisInformationSizeBefore) {
for (auto& predecessorEntry : backwardTransitions.getRow(currentState)) { 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(predecessorEntry.column())) {
worklist.push(std::make_pair(predecessorEntry.column(), currentState));
if (!psiStates.get(predecessorEntry.first)) {
worklist.push(std::make_pair(predecessorEntry.first, currentState));
} }
} }
} }

98
src/utility/graph.h
View File

@ -81,17 +81,17 @@ namespace storm {
stepStack.pop_back(); stepStack.pop_back();
} }
for (auto& entry : backwardTransitions.getRow(currentState)) {
if (phiStates.get(entry.column()) && (!statesWithProbabilityGreater0.get(entry.column()) || (useStepBound && remainingSteps[entry.column()] < currentStepBound - 1))) {
for (typename storm::storage::SparseMatrix<T>::const_iterator entryIt = backwardTransitions.begin(currentState), entryIte = backwardTransitions.end(currentState); entryIt != entryIte; ++entryIt) {
if (phiStates.get(entryIt->first) && (!statesWithProbabilityGreater0.get(entryIt->first) || (useStepBound && remainingSteps[entryIt->first] < 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(entry.column(), true);
stack.push_back(entry.column());
statesWithProbabilityGreater0.set(entryIt->first, true);
stack.push_back(entryIt->first);
} 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[entry.column()] = currentStepBound - 1;
statesWithProbabilityGreater0.set(entry.column(), true);
stack.push_back(entry.column());
remainingSteps[entryIt->first] = currentStepBound - 1;
statesWithProbabilityGreater0.set(entryIt->first, true);
stack.push_back(entryIt->first);
stepStack.push_back(currentStepBound - 1); stepStack.push_back(currentStepBound - 1);
} }
} }
@ -212,17 +212,17 @@ namespace storm {
stepStack.pop_back(); stepStack.pop_back();
} }
for (auto& entry : backwardTransitions.getRow(currentState)) {
if (phiStates.get(entry.column()) && (!statesWithProbabilityGreater0.get(entry.column()) || (useStepBound && remainingSteps[entry.column()] < currentStepBound - 1))) {
for (auto const& entry : backwardTransitions.getRow(currentState)) {
if (phiStates.get(entry.first) && (!statesWithProbabilityGreater0.get(entry.first) || (useStepBound && remainingSteps[entry.first] < 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(entry.column(), true);
stack.push_back(entry.column());
statesWithProbabilityGreater0.set(entry.first, true);
stack.push_back(entry.first);
} 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[entry.column()] = currentStepBound - 1;
statesWithProbabilityGreater0.set(entry.column(), true);
stack.push_back(entry.column());
remainingSteps[entry.first] = currentStepBound - 1;
statesWithProbabilityGreater0.set(entry.first, true);
stack.push_back(entry.first);
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& predecessorEntry : backwardTransitions.getRow(currentState)) {
if (phiStates.get(predecessorEntry.column()) && !nextStates.get(predecessorEntry.column())) {
for (auto const& predecessorEntry : backwardTransitions.getRow(currentState)) {
if (phiStates.get(predecessorEntry.first) && !nextStates.get(predecessorEntry.first)) {
// 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[predecessorEntry.column()]; row < nondeterministicChoiceIndices[predecessorEntry.column() + 1]; ++row) {
for (auto row = nondeterministicChoiceIndices[predecessorEntry.first]; row < nondeterministicChoiceIndices[predecessorEntry.first + 1]; ++row) {
bool allSuccessorsInCurrentStates = true; bool allSuccessorsInCurrentStates = true;
for (auto& targetEntry : transitionMatrix.getRow(row)) {
if (!currentStates.get(targetEntry.column())) {
for (auto const& targetEntry : transitionMatrix.getRow(row)) {
if (!currentStates.get(targetEntry.first)) {
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(predecessorEntry.column(), true);
stack.push_back(predecessorEntry.column());
nextStates.set(predecessorEntry.first, true);
stack.push_back(predecessorEntry.first);
break; break;
} }
} }
@ -402,15 +402,15 @@ namespace storm {
stepStack.pop_back(); stepStack.pop_back();
} }
for(auto& predecessorEntry : backwardTransitions.getRow(currentState)) {
if (phiStates.get(predecessorEntry.column()) && (!statesWithProbabilityGreater0.get(predecessorEntry.column()) || (useStepBound && remainingSteps[predecessorEntry.column()] < currentStepBound - 1))) {
for(auto const& predecessorEntry : backwardTransitions.getRow(currentState)) {
if (phiStates.get(predecessorEntry.first) && (!statesWithProbabilityGreater0.get(predecessorEntry.first) || (useStepBound && remainingSteps[predecessorEntry.first] < 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[predecessorEntry.column()]; row < nondeterministicChoiceIndices[predecessorEntry.column() + 1]; ++row) {
for (auto row = nondeterministicChoiceIndices[predecessorEntry.first]; row < nondeterministicChoiceIndices[predecessorEntry.first + 1]; ++row) {
bool hasAtLeastOneSuccessorWithProbabilityGreater0 = false; bool hasAtLeastOneSuccessorWithProbabilityGreater0 = false;
for (auto& successorEntry : transitionMatrix.getRow(row)) {
if (statesWithProbabilityGreater0.get(successorEntry.column())) {
for (auto const& successorEntry : transitionMatrix.getRow(row)) {
if (statesWithProbabilityGreater0.get(successorEntry.first)) {
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(predecessorEntry.column(), true);
stack.push_back(predecessorEntry.column());
statesWithProbabilityGreater0.set(predecessorEntry.first, true);
stack.push_back(predecessorEntry.first);
} 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[predecessorEntry.column()] = currentStepBound - 1;
statesWithProbabilityGreater0.set(predecessorEntry.column(), true);
stack.push_back(predecessorEntry.column());
remainingSteps[predecessorEntry.first] = currentStepBound - 1;
statesWithProbabilityGreater0.set(predecessorEntry.first, true);
stack.push_back(predecessorEntry.first);
stepStack.push_back(currentStepBound - 1); stepStack.push_back(currentStepBound - 1);
} }
} }
@ -502,13 +502,13 @@ namespace storm {
currentState = stack.back(); currentState = stack.back();
stack.pop_back(); stack.pop_back();
for(auto& predecessorEntry : backwardTransitions.getRow(currentState)) {
if (phiStates.get(predecessorEntry.column()) && !nextStates.get(predecessorEntry.column())) {
for(auto const& predecessorEntry : backwardTransitions.getRow(currentState)) {
if (phiStates.get(predecessorEntry.first) && !nextStates.get(predecessorEntry.first)) {
// 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& successorEntry : transitionMatrix.getRows(nondeterministicChoiceIndices[predecessorEntry.column()], nondeterministicChoiceIndices[predecessorEntry.column() + 1] - 1)) {
if (!currentStates.get(successorEntry.column())) {
for (auto const& successorEntry : transitionMatrix.getRows(nondeterministicChoiceIndices[predecessorEntry.first], nondeterministicChoiceIndices[predecessorEntry.first + 1] - 1)) {
if (!currentStates.get(successorEntry.first)) {
allSuccessorsInCurrentStatesForAllChoices = false; allSuccessorsInCurrentStatesForAllChoices = false;
goto afterCheckLoop; goto afterCheckLoop;
} }
@ -519,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(predecessorEntry.column(), true);
stack.push_back(predecessorEntry.column());
nextStates.set(predecessorEntry.first, true);
stack.push_back(predecessorEntry.first);
} }
} }
} }
@ -600,12 +600,12 @@ namespace storm {
recursionStepBackward: recursionStepBackward:
for (; successorIterator != matrix.end(currentState); ++successorIterator) { for (; successorIterator != matrix.end(currentState); ++successorIterator) {
if (!visitedStates.get(successorIterator.column())) {
if (!visitedStates.get(successorIterator.first)) {
// 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(successorIterator.column());
recursionStack.push_back(successorIterator.first);
// Also, put initial value for iterator on corresponding recursion stack. // Also, put initial value for iterator on corresponding recursion stack.
iteratorRecursionStack.push_back(matrix.begin(successorIterator.column()));
iteratorRecursionStack.push_back(matrix.begin(successorIterator.first));
goto recursionStepForward; goto recursionStepForward;
} }
@ -684,23 +684,23 @@ namespace storm {
// 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.getRow(probabilityStatePair.second); typename storm::storage::SparseMatrix<T>::Rows row = transitions.getRow(probabilityStatePair.second);
for (auto& transition : row) {
for (auto const& 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.first)) {
// Calculate the distance we achieve when we take the path to the successor via the current state. // Calculate the distance we achieve when we take the path to the successor via the current state.
T newDistance = probabilityStatePair.first * transition.value();
T newDistance = probabilityStatePair.first * transition.second;
// We found a cheaper way to get to the target state of the transition. // We found a cheaper way to get to the target state of the transition.
if (newDistance > probabilities[transition.column()]) {
if (newDistance > probabilities[transition.first]) {
// Remove the old distance. // Remove the old distance.
if (probabilities[transition.column()] != noPredecessorValue) {
probabilityStateSet.erase(std::make_pair(probabilities[transition.column()], transition.column()));
if (probabilities[transition.first] != noPredecessorValue) {
probabilityStateSet.erase(std::make_pair(probabilities[transition.first], transition.first));
} }
// Set and add the new distance. // Set and add the new distance.
probabilities[transition.column()] = newDistance;
predecessors[transition.column()] = probabilityStatePair.second;
probabilityStateSet.insert(std::make_pair(newDistance, transition.column()));
probabilities[transition.first] = newDistance;
predecessors[transition.first] = probabilityStatePair.second;
probabilityStateSet.insert(std::make_pair(newDistance, transition.first));
} }
} }
} }

4
src/utility/matrix.h
View File

@ -32,8 +32,8 @@ 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>::const_rows selectedRow = transitionMatrix.getRow(choice); typename storm::storage::SparseMatrix<T>::const_rows selectedRow = transitionMatrix.getRow(choice);
for (auto entry : selectedRow) {
result.addNextValue(state, entry.column(), entry.value());
for (auto const& entry : selectedRow) {
result.addNextValue(state, entry.first, entry.second);
} }
} 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.

24
test/functional/storage/SparseMatrixTest.cpp
View File

@ -494,24 +494,24 @@ TEST(SparseMatrix, Iteration) {
ASSERT_NO_THROW(matrix.finalize()); ASSERT_NO_THROW(matrix.finalize());
for (auto const& entry : matrix.getRow(4)) { for (auto const& entry : matrix.getRow(4)) {
if (entry.column() == 0) {
ASSERT_EQ(0.1, entry.value());
} else if (entry.column() == 1) {
ASSERT_EQ(0.2, entry.value());
} else if (entry.column() == 3) {
ASSERT_EQ(0.3, entry.value());
if (entry.first == 0) {
ASSERT_EQ(0.1, entry.second);
} else if (entry.first == 1) {
ASSERT_EQ(0.2, entry.second);
} else if (entry.first == 3) {
ASSERT_EQ(0.3, entry.second);
} else { } else {
ASSERT_TRUE(false); ASSERT_TRUE(false);
} }
} }
for (storm::storage::SparseMatrix<double>::iterator it = matrix.begin(4), ite = matrix.end(4); it != ite; ++it) { for (storm::storage::SparseMatrix<double>::iterator it = matrix.begin(4), ite = matrix.end(4); it != ite; ++it) {
if (it.column() == 0) {
ASSERT_EQ(0.1, it.value());
} else if (it.column() == 1) {
ASSERT_EQ(0.2, it.value());
} else if (it.column() == 3) {
ASSERT_EQ(0.3, it.value());
if (it->first == 0) {
ASSERT_EQ(0.1, it->second);
} else if (it->first == 1) {
ASSERT_EQ(0.2, it->second);
} else if (it->first == 3) {
ASSERT_EQ(0.3, it->second);
} else { } else {
ASSERT_TRUE(false); ASSERT_TRUE(false);
} }

1
test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp
View File

@ -67,6 +67,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, SynchronousLeader) {
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(), 1312334ull); ASSERT_EQ(dtmc->getNumberOfStates(), 1312334ull);

2
test/performance/storage/SparseMatrixTest.cpp
View File

@ -13,7 +13,7 @@ TEST(SparseMatrix, Iteration) {
for (uint_fast64_t row = 0; row < matrix.getRowCount(); ++row) { for (uint_fast64_t row = 0; row < matrix.getRowCount(); ++row) {
for (auto const& entry : matrix.getRow(row)) { for (auto const& entry : matrix.getRow(row)) {
// The following can never be true, but prevents the compiler from optimizing away the loop. // The following can never be true, but prevents the compiler from optimizing away the loop.
if (entry.column() > matrix.getColumnCount()) {
if (entry.first > matrix.getColumnCount()) {
ASSERT_TRUE(false); ASSERT_TRUE(false);
} }
} }

Write Preview
Loading…
Cancel
Save