diff --git a/CMakeLists.txt b/CMakeLists.txt index d5d8d8872..31d82172c 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -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. set (CLANG ON) # 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) set(CLANG_STDLIB libstdc++) message(STATUS "StoRM - Linking against libstdc++") diff --git a/src/adapters/GmmxxAdapter.h b/src/adapters/GmmxxAdapter.h index 5b20df4d9..f0fb9cf9e 100644 --- a/src/adapters/GmmxxAdapter.h +++ b/src/adapters/GmmxxAdapter.h @@ -40,13 +40,21 @@ public: // Copy Row Indications 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 values; + values.reserve(matrix.getEntryCount()); + std::vector 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."); return result; @@ -59,6 +67,7 @@ public: template static gmm::csr_matrix* toGmmxxSparseMatrix(storm::storage::SparseMatrix&& matrix) { uint_fast64_t realNonZeros = matrix.getEntryCount(); + std::cout << "here?!" << std::endl; LOG4CPLUS_DEBUG(logger, "Converting matrix with " << realNonZeros << " non-zeros to gmm++ format."); // Prepare the resulting matrix. @@ -71,91 +80,25 @@ public: // Move Row Indications result->jc.~vectorType_ull_t(); // Call Destructor inplace 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)); - + + // Copy columns and values. + std::vector values; + values.reserve(matrix.getEntryCount()); + std::vector 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."); 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 - static storm::storage::SparseMatrix* fromGmmxxSparseMatrix(gmm::csr_matrix 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* result = new storm::storage::SparseMatrix(matrix.nrows(), matrix.ncols()); - - // Set internal NonZero Counter - result->nonZeroEntryCount = realNonZeros; - result->setState(result->Initialized); - - if (!result->prepareInternalStorage(false)) { - LOG4CPLUS_ERROR(logger, "Unable to allocate internal storage while converting GMM++ Matrix to Storm."); - delete result; - return nullptr; - } else { - - // Copy Row Indications - std::copy(matrix.jc.begin(), matrix.jc.end(), std::back_inserter(result->rowIndications)); - // Copy Columns Indications - std::copy(matrix.ir.begin(), matrix.ir.end(), std::back_inserter(result->columnIndications)); - // And do the same thing with the actual values. - std::copy(matrix.pr.begin(), matrix.pr.end(), std::back_inserter(result->valueStorage)); - - result->currentSize = realNonZeros; - result->lastRow = matrix.nrows() - 1; - } - - result->finalize(); - - 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 - static storm::storage::SparseMatrix* fromGmmxxSparseMatrix(gmm::csr_matrix && 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* result = new storm::storage::SparseMatrix(matrix.nrows(), matrix.ncols()); - - // Set internal NonZero Counter - result->nonZeroEntryCount = realNonZeros; - result->setState(result->Initialized); - - // Move Row Indications - result->rowIndications = std::vector(std::move(matrix.jc)); - // Move Columns Indications - result->columnIndications = std::vector(std::move(matrix.ir)); - // And do the same thing with the actual values. - result->valueStorage = std::vector(std::move(matrix.pr)); - - result->currentSize = realNonZeros; - result->lastRow = matrix.nrows() - 1; - - result->finalize(); - - LOG4CPLUS_DEBUG(logger, "Done converting matrix to storm format."); - - return result; - } }; } //namespace adapters diff --git a/src/counterexamples/MILPMinimalLabelSetGenerator.h b/src/counterexamples/MILPMinimalLabelSetGenerator.h index df5611577..bb135b43f 100644 --- a/src/counterexamples/MILPMinimalLabelSetGenerator.h +++ b/src/counterexamples/MILPMinimalLabelSetGenerator.h @@ -131,7 +131,7 @@ namespace storm { bool allSuccessorsProblematic = true; for (auto const& successorEntry : transitionMatrix.getRow(row)) { // 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]) { result.allRelevantLabels.insert(label); } @@ -140,7 +140,7 @@ namespace storm { result.relevantChoicesForRelevantStates[state].push_back(row); } } - if (!stateInformation.problematicStates.get(successorEntry.column())) { + if (!stateInformation.problematicStates.get(successorEntry.first)) { allSuccessorsProblematic = false; } } @@ -304,11 +304,11 @@ namespace storm { std::list const& relevantChoicesForState = choiceInformation.relevantChoicesForRelevantStates.at(state); for (uint_fast64_t row : relevantChoicesForState) { 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.clear(); - variableNameBuffer << "r" << successorEntry.column(); + variableNameBuffer << "r" << successorEntry.first; resultingMap[state] = solver.createContinuousVariable(variableNameBuffer.str(), storm::solver::LpSolver::BOUNDED, 0, 1, 0); ++numberOfVariablesCreated; } @@ -338,11 +338,11 @@ namespace storm { std::list const& relevantChoicesForState = choiceInformation.relevantChoicesForRelevantStates.at(state); for (uint_fast64_t row : relevantChoicesForState) { for (auto const& successorEntry : labeledMdp.getTransitionMatrix().getRow(row)) { - if (stateInformation.relevantStates.get(successorEntry.column())) { + if (stateInformation.relevantStates.get(successorEntry.first)) { variableNameBuffer.str(""); 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; } } @@ -551,11 +551,11 @@ namespace storm { double rightHandSide = 1; for (auto const& successorEntry : labeledMdp.getTransitionMatrix().getRow(choice)) { - if (stateInformation.relevantStates.get(successorEntry.column())) { - variables.push_back(static_cast(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(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); 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); } @@ -626,9 +626,9 @@ namespace storm { variables.push_back(variableInformation.problematicStateToVariableIndexMap.at(state)); coefficients.push_back(1); - variables.push_back(variableInformation.problematicStateToVariableIndexMap.at(successorEntry.column())); + variables.push_back(variableInformation.problematicStateToVariableIndexMap.at(successorEntry.first)); 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); 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)) { bool psiStateReachableInOneStep = false; for (auto const& successorEntry : labeledMdp.getTransitionMatrix().getRow(choice)) { - if (psiStates.get(successorEntry.column())) { + if (psiStates.get(successorEntry.first)) { psiStateReachableInOneStep = true; } } @@ -697,8 +697,8 @@ namespace storm { coefficients.push_back(1); for (auto const& successorEntry : labeledMdp.getTransitionMatrix().getRow(choice)) { - if (state != successorEntry.column() && stateInformation.relevantStates.get(successorEntry.column())) { - std::list const& successorChoiceVariableIndices = variableInformation.stateToChoiceVariablesIndexMap.at(successorEntry.column()); + if (state != successorEntry.first && stateInformation.relevantStates.get(successorEntry.first)) { + std::list const& successorChoiceVariableIndices = variableInformation.stateToChoiceVariablesIndexMap.at(successorEntry.first); for (auto choiceVariableIndex : successorChoiceVariableIndices) { variables.push_back(choiceVariableIndex); @@ -727,8 +727,8 @@ namespace storm { // Compute the set of predecessors. std::unordered_set predecessors; 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. for (auto const& successorEntry : labeledMdp.getTransitionMatrix().getRow(relevantChoice)) { - if (state == successorEntry.column()) { + if (state == successorEntry.first) { choiceTargetsCurrentState = true; break; } @@ -789,8 +789,8 @@ namespace storm { for (auto psiState : psiStates) { // Compute the set of predecessors. 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. for (auto const& successorEntry : labeledMdp.getTransitionMatrix().getRow(relevantChoice)) { - if (psiStates.get(successorEntry.column())) { + if (psiStates.get(successorEntry.first)) { choiceTargetsPsiState = true; break; } diff --git a/src/counterexamples/PathBasedSubsystemGenerator.h b/src/counterexamples/PathBasedSubsystemGenerator.h index 1676de7ef..c00fe0c4d 100644 --- a/src/counterexamples/PathBasedSubsystemGenerator.h +++ b/src/counterexamples/PathBasedSubsystemGenerator.h @@ -67,33 +67,33 @@ public: 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. - if(trans.value() != (T) 0 && !subSysStates.get(trans.column())) { + if(trans.second != (T) 0 && !subSysStates.get(trans.first)) { //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(trans.column(), distances[trans.column()].second)); + activeSet.insert(std::pair(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 //And the distance can be improved by using this transition. //find state in set, remove it, reenter it with new and correct values. - auto range = activeSet.equal_range(std::pair(trans.column(), distances[trans.column()].second)); + auto range = activeSet.equal_range(std::pair(trans.first, distances[trans.first].second)); for(;range.first != range.second; range.first++) { - if(trans.column() == range.first->first) { + if(trans.first == range.first->first) { activeSet.erase(range.first); 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(trans.column(), trans.value())); + activeSet.insert(std::pair(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. if(!subSysStates.get(activeState.first) && allowedStates.get(activeState.first)) { // 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 - 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 - if(distances[trans.column()].second == (T)-1) { + if(distances[trans.first].second == (T)-1) { //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 - activeSet.insert(std::pair(trans.column(), distance)); + activeSet.insert(std::pair(trans.first, distance)); } - else if(distances[trans.column()].second < distance ){ + else if(distances[trans.first].second < distance ){ //This state has already been discovered //And the distance can be improved by using this transition. //find state in set, remove it, reenter it with new and correct values. - auto range = activeSet.equal_range(std::pair(trans.column(), distances[trans.column()].second)); + auto range = activeSet.equal_range(std::pair(trans.first, distances[trans.first].second)); for(;range.first != range.second; range.first++) { - if(trans.column() == range.first->first) { + if(trans.first == range.first->first) { activeSet.erase(range.first); break; } } - distances[trans.column()].first = activeState.first; - distances[trans.column()].second = distance; - activeSet.insert(std::pair(trans.column(), distance)); + distances[trans.first].first = activeState.first; + distances[trans.first].second = distance; + activeSet.insert(std::pair(trans.first, distance)); } } } @@ -180,35 +180,35 @@ public: 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. - if(trans.value() != (T) 0 && !subSysStates.get(trans.column())) { + if(trans.second != (T) 0 && !subSysStates.get(trans.first)) { //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) - 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(trans.column(), distances[trans.column()].second)); + activeSet.insert(std::pair(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 //And the distance can be improved by using this transition. //find state in set, remove it, reenter it with new and correct values. - auto range = activeSet.equal_range(std::pair(trans.column(), distances[trans.column()].second)); + auto range = activeSet.equal_range(std::pair(trans.first, distances[trans.first].second)); for(;range.first != range.second; range.first++) { - if(trans.column() == range.first->first) { + if(trans.first == range.first->first) { activeSet.erase(range.first); break; } } //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(trans.column(), trans.value())); + activeSet.insert(std::pair(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. if(!subSysStates.get(activeState.first) && allowedStates.get(activeState.first)) { // 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 - 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 - if(distances[trans.column()].second == (T)-1) { + if(distances[trans.first].second == (T)-1) { //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 - activeSet.insert(std::pair(trans.column(), distance)); + activeSet.insert(std::pair(trans.first, distance)); } - else if(distances[trans.column()].second < distance ){ + else if(distances[trans.first].second < distance ){ //This state has already been discovered //And the distance can be improved by using this transition. //find state in set, remove it, reenter it with new and correct values. - auto range = activeSet.equal_range(std::pair(trans.column(), distances[trans.column()].second)); + auto range = activeSet.equal_range(std::pair(trans.first, distances[trans.first].second)); for(;range.first != range.second; range.first++) { - if(trans.column() == range.first->first) { + if(trans.first == range.first->first) { activeSet.erase(range.first); break; } } - distances[trans.column()].first = activeState.first; - distances[trans.column()].second = distance; - activeSet.insert(std::pair(trans.column(), distance)); + distances[trans.first].first = activeState.first; + distances[trans.first].second = distance; + activeSet.insert(std::pair(trans.first, distance)); } } } diff --git a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h index 3edfba9b8..4668abded 100644 --- a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h +++ b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h @@ -96,10 +96,10 @@ namespace storm { for (auto state : markovianNonGoalStates) { for (auto& element : aMarkovian.getRow(rowIndex)) { ValueType eTerm = std::exp(-exitRates[state] * delta); - if (element.column() == rowIndex) { - element.value() = (storm::utility::constantOne() - eTerm) * element.value() + eTerm; + if (element.first == rowIndex) { + element.second = (storm::utility::constantOne() - eTerm) * element.second + eTerm; } else { - element.value() = (storm::utility::constantOne() - eTerm) * element.value(); + element.second = (storm::utility::constantOne() - eTerm) * element.second; } } ++rowIndex; @@ -109,7 +109,7 @@ namespace storm { rowIndex = 0; for (auto state : markovianNonGoalStates) { 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; } @@ -126,8 +126,8 @@ namespace storm { bMarkovianFixed.push_back(storm::utility::constantZero()); 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::Rows row = transitionMatrix.getRow(choice); 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. - sspMatrix.insertNextValue(currentChoice, statesNotInMecsBeforeIndex[element.column()], element.value(), true); + sspMatrix.insertNextValue(currentChoice, statesNotInMecsBeforeIndex[element.first], element.second, true); } else { // 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. - auxiliaryStateToProbabilityMap[stateToMecIndexMap[element.column()]] += element.value(); + auxiliaryStateToProbabilityMap[stateToMecIndexMap[element.first]] += element.second; } } @@ -350,13 +350,13 @@ namespace storm { typename storm::storage::SparseMatrix::Rows row = transitionMatrix.getRow(choice); 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. - sspMatrix.insertNextValue(currentChoice, statesNotInMecsBeforeIndex[element.column()], element.value(), true); + sspMatrix.insertNextValue(currentChoice, statesNotInMecsBeforeIndex[element.first], element.second, true); } else { // 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. - auxiliaryStateToProbabilityMap[stateToMecIndexMap[element.column()]] += element.value(); + auxiliaryStateToProbabilityMap[stateToMecIndexMap[element.first]] += element.second; } } @@ -456,8 +456,8 @@ namespace storm { typename storm::storage::SparseMatrix::Rows row = transitionMatrix.getRow(nondeterministicChoiceIndices[state]); 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); @@ -476,8 +476,8 @@ namespace storm { typename storm::storage::SparseMatrix::Rows row = transitionMatrix.getRow(choice); 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()); diff --git a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h index 98e1c2e73..26461f665 100644 --- a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h +++ b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h @@ -264,7 +264,9 @@ public: // 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. + LOG4CPLUS_INFO(logger, "Running Prob01."); std::pair 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 statesWithProbability1 = std::move(statesWithProbability01.second); diff --git a/src/models/AbstractDeterministicModel.h b/src/models/AbstractDeterministicModel.h index 926dd484b..0d9abec5e 100644 --- a/src/models/AbstractDeterministicModel.h +++ b/src/models/AbstractDeterministicModel.h @@ -90,10 +90,10 @@ class AbstractDeterministicModel: public AbstractModel { auto rowIt = this->transitionMatrix.begin(); for (uint_fast64_t i = 0; i < this->transitionMatrix.getRowCount(); ++i, ++rowIt) { typename storm::storage::SparseMatrix::const_rows row = this->transitionMatrix.getRow(i); - for (auto& transition : row) { - if (transition.value() != storm::utility::constantZero()) { - 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()) { + if (subsystem == nullptr || subsystem->get(transition.first)) { + outStream << "\t" << i << " -> " << transition.first << " [ label= \"" << transition.second << "\" ];" << std::endl; } } } diff --git a/src/models/AbstractModel.h b/src/models/AbstractModel.h index d222350c6..fa1731f10 100644 --- a/src/models/AbstractModel.h +++ b/src/models/AbstractModel.h @@ -170,7 +170,7 @@ class AbstractModel: public std::enable_shared_from_this> { storm::storage::VectorSet allTargetBlocks; for (auto state : block) { 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. if (targetBlock != currentBlockIndex) { diff --git a/src/models/AbstractNondeterministicModel.h b/src/models/AbstractNondeterministicModel.h index 344109f44..f2a515bc2 100644 --- a/src/models/AbstractNondeterministicModel.h +++ b/src/models/AbstractNondeterministicModel.h @@ -134,8 +134,8 @@ namespace storm { for (uint_fast64_t i = 0; i < numberOfStates; ++i) { typename storm::storage::SparseMatrix::const_rows rows = this->getRows(i); 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. for (uint_fast64_t i = 0; i < numberOfStates; ++i) { typename storm::storage::SparseMatrix::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. 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 (scheduler != nullptr) { diff --git a/src/models/Dtmc.h b/src/models/Dtmc.h index bf3654498..4ccbda8b4 100644 --- a/src/models/Dtmc.h +++ b/src/models/Dtmc.h @@ -169,8 +169,8 @@ public: std::vector stateMapping; for(uint_fast64_t row = 0; row < origMat.getRowCount(); ++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++; } } @@ -198,10 +198,10 @@ public: if(subSysStates.get(row)){ // Transfer transitions 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 { - rest += entry.value(); + rest += entry.second; } } @@ -253,8 +253,8 @@ public: if(subSysStates.get(row)){ // Transfer transition rewards 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); } } diff --git a/src/models/MarkovAutomaton.h b/src/models/MarkovAutomaton.h index b52cc9701..547bd7dce 100644 --- a/src/models/MarkovAutomaton.h +++ b/src/models/MarkovAutomaton.h @@ -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 (auto const& entry : this->transitionMatrix.getRow(row)) { - newTransitionMatrix.addNextValue(currentChoice, entry.column(), entry.value()); + newTransitionMatrix.addNextValue(currentChoice, entry.first, entry.second); } ++currentChoice; } @@ -234,9 +234,9 @@ namespace storm { outStream << ";" << std::endl; // 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 (scheduler != nullptr) { @@ -251,9 +251,9 @@ namespace storm { } } else { // 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() { for (auto state : this->markovianStates) { - for (typename storm::storage::SparseMatrix::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]; } } } diff --git a/src/parser/DeterministicSparseTransitionParser.cpp b/src/parser/DeterministicSparseTransitionParser.cpp index e436ebbce..223f0b218 100644 --- a/src/parser/DeterministicSparseTransitionParser.cpp +++ b/src/parser/DeterministicSparseTransitionParser.cpp @@ -226,9 +226,9 @@ storm::storage::SparseMatrix DeterministicSparseTransitionParser(std::st if ((lastRow != -1) && (!rowHadDiagonalEntry)) { if (insertDiagonalEntriesIfMissing && !isRewardMatrix) { resultMatrix.addNextValue(lastRow, lastRow, storm::utility::constantZero()); - 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) { - 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 rowHadDiagonalEntry = true; @@ -238,9 +238,9 @@ storm::storage::SparseMatrix DeterministicSparseTransitionParser(std::st if (fixDeadlocks && !isRewardMatrix) { resultMatrix.addNextValue(skippedRow, skippedRow, storm::utility::constantOne()); 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) { - 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. } } @@ -254,9 +254,9 @@ storm::storage::SparseMatrix DeterministicSparseTransitionParser(std::st rowHadDiagonalEntry = true; if (insertDiagonalEntriesIfMissing && !isRewardMatrix) { resultMatrix.addNextValue(row, row, storm::utility::constantZero()); - 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) { - 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 DeterministicSparseTransitionParser(std::st if (!rowHadDiagonalEntry) { if (insertDiagonalEntriesIfMissing && !isRewardMatrix) { resultMatrix.addNextValue(lastRow, lastRow, storm::utility::constantZero()); - 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) { - 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."); } } diff --git a/src/storage/MaximalEndComponentDecomposition.cpp b/src/storage/MaximalEndComponentDecomposition.cpp index ed329c6ba..e47d6537a 100644 --- a/src/storage/MaximalEndComponentDecomposition.cpp +++ b/src/storage/MaximalEndComponentDecomposition.cpp @@ -82,8 +82,8 @@ namespace storm { for (uint_fast64_t choice = nondeterministicChoiceIndices[state]; choice < nondeterministicChoiceIndices[state + 1]; ++choice) { 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; break; } @@ -108,9 +108,9 @@ namespace storm { // Now check which states should be reconsidered, because successors of them were removed. statesToCheck.clear(); 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 containedChoices; for (uint_fast64_t choice = nondeterministicChoiceIndices[state]; choice < nondeterministicChoiceIndices[state + 1]; ++choice) { 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; break; } diff --git a/src/storage/SparseMatrix.cpp b/src/storage/SparseMatrix.cpp index f0185eb9a..6b9601f6f 100644 --- a/src/storage/SparseMatrix.cpp +++ b/src/storage/SparseMatrix.cpp @@ -9,47 +9,47 @@ extern log4cplus::Logger logger; namespace storm { namespace storage { - + template - SparseMatrix::rows::rows(std::pair* columnAndValuePtr, uint_fast64_t entryCount) : columnAndValuePtr(columnAndValuePtr), entryCount(entryCount) { + SparseMatrix::rows::rows(iterator begin, uint_fast64_t entryCount) : beginIterator(begin), entryCount(entryCount) { // Intentionally left empty. } template typename SparseMatrix::iterator SparseMatrix::rows::begin() { - return columnAndValuePtr; + return beginIterator; } template typename SparseMatrix::iterator SparseMatrix::rows::end() { - return columnAndValuePtr + entryCount; + return beginIterator + entryCount; } - + template - SparseMatrix::const_rows::const_rows(std::pair const* columnAndValuePtr, uint_fast64_t entryCount) : columnAndValuePtr(columnAndValuePtr), entryCount(entryCount) { + SparseMatrix::const_rows::const_rows(const_iterator begin, uint_fast64_t entryCount) : beginIterator(begin), entryCount(entryCount) { // Intentionally left empty. } template typename SparseMatrix::const_iterator SparseMatrix::const_rows::begin() const { - return columnAndValuePtr; + return beginIterator; } template typename SparseMatrix::const_iterator SparseMatrix::const_rows::end() const { - return columnAndValuePtr + entryCount; + return beginIterator + entryCount; } template SparseMatrix::SparseMatrix(uint_fast64_t rows, uint_fast64_t columns, uint_fast64_t entries) : rowCountSet(rows != 0), rowCount(rows), columnCountSet(columns != 0), columnCount(columns), entryCount(entries), storagePreallocated(rows != 0 && columns != 0 && entries != 0), columnsAndValues(), rowIndications(), internalStatus(UNINITIALIZED), currentEntryCount(0), lastRow(0), lastColumn(0) { prepareInternalStorage(); } - + template SparseMatrix::SparseMatrix(SparseMatrix const& other) : rowCountSet(other.rowCountSet), rowCount(other.rowCount), columnCountSet(other.columnCountSet), columnCount(other.columnCount), entryCount(other.entryCount), storagePreallocated(other.storagePreallocated), columnsAndValues(other.columnsAndValues), rowIndications(other.rowIndications), internalStatus(other.internalStatus), currentEntryCount(other.currentEntryCount), lastRow(other.lastRow), lastColumn(other.lastColumn) { // Intentionally left empty. } - + template SparseMatrix::SparseMatrix(SparseMatrix&& other) : rowCountSet(other.rowCountSet), rowCount(other.rowCount), columnCountSet(other.columnCountSet), columnCount(other.columnCount), entryCount(other.entryCount), storagePreallocated(other.storagePreallocated), columnsAndValues(std::move(other.columnsAndValues)), rowIndications(std::move(other.rowIndications)), internalStatus(other.internalStatus), currentEntryCount(other.currentEntryCount), lastRow(other.lastRow), lastColumn(other.lastColumn) { // Now update the source matrix @@ -64,9 +64,9 @@ namespace storm { other.lastRow = 0; other.lastColumn = 0; } - + template - SparseMatrix::SparseMatrix(uint_fast64_t columnCount, std::vector const& rowIndications, std::vector> 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::SparseMatrix(uint_fast64_t columnCount, std::vector const& rowIndications, std::vector> 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. } @@ -87,7 +87,7 @@ namespace storm { } template - SparseMatrix::SparseMatrix(uint_fast64_t columnCount, std::vector&& rowIndications, std::vector>&& 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::SparseMatrix(uint_fast64_t columnCount, std::vector&& rowIndications, std::vector>&& 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. } @@ -198,7 +198,7 @@ namespace storm { } } } - + return equalityResult; } @@ -305,7 +305,7 @@ namespace storm { columnCount = std::max(columnCount, overridenColumnCount); } } - + entryCount = currentEntryCount; internalStatus = INITIALIZED; } @@ -359,8 +359,8 @@ namespace storm { 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 // in the vector of nonzeros otherwise. @@ -373,7 +373,7 @@ namespace storm { columnValuePtr->first = column; columnValuePtr->second = storm::utility::constantOne(); ++columnValuePtr; - for (; columnValuePtr != columnValuePtr; ++columnValuePtr) { + for (; columnValuePtr != columnValuePtrEnd; ++columnValuePtr) { columnValuePtr->first = 0; columnValuePtr->second = storm::utility::constantZero(); } @@ -383,7 +383,7 @@ namespace storm { T SparseMatrix::getConstrainedRowSum(uint_fast64_t row, storm::storage::BitVector const& constraint) const { checkReady("getConstrainedRowSum"); T result(0); - for (typename std::vector>::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)) { result += it->second; } @@ -570,7 +570,7 @@ namespace storm { template SparseMatrix SparseMatrix::transpose() const { checkReady("transpose"); - + uint_fast64_t rowCount = this->columnCount; uint_fast64_t columnCount = this->rowCount; uint_fast64_t entryCount = this->entryCount; @@ -633,7 +633,7 @@ namespace storm { T one = storm::utility::constantOne(); bool foundDiagonalElement = false; 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) { it->second = one - it->second; foundDiagonalElement = true; @@ -650,7 +650,7 @@ namespace storm { template void SparseMatrix::negateAllNonDiagonalEntries() { checkReady("negateAllNonDiagonalEntries"); - + // Check if the matrix is square, because only then it makes sense to perform this transformation. if (this->getRowCount() != this->getColumnCount()) { throw storm::exceptions::InvalidArgumentException() << "Illegal call to SparseMatrix::invertDiagonal: matrix is non-square."; @@ -658,7 +658,7 @@ namespace storm { // 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 (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) { it->second = -it->second; } @@ -669,7 +669,7 @@ namespace storm { template void SparseMatrix::deleteDiagonalEntries() { checkReady("deleteDiagonalEntries"); - + // Check if the matrix is square, because only then it makes sense to perform this transformation. if (this->getRowCount() != this->getColumnCount()) { throw storm::exceptions::InvalidArgumentException() << "Illegal call to SparseMatrix::deleteDiagonalEntries: matrix is non-square."; @@ -677,7 +677,7 @@ namespace storm { // 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 (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) { it->second = storm::utility::constantZero(); } @@ -688,7 +688,7 @@ namespace storm { template typename std::pair, storm::storage::SparseMatrix> SparseMatrix::getJacobiDecomposition() const { checkReady("getJacobiDecomposition"); - + if (rowCount != columnCount) { throw storm::exceptions::InvalidArgumentException() << "Illegal call to SparseMatrix::invertDiagonal: matrix is non-square."; } @@ -720,7 +720,7 @@ namespace storm { template std::vector SparseMatrix::getPointwiseProductRowSumVector(storm::storage::SparseMatrix const& otherMatrix) const { checkReady("getPointwiseProductRowSumVector"); - + std::vector result(rowCount, storm::utility::constantZero()); // Iterate over all elements of the current matrix and either continue with the next element in case the @@ -770,7 +770,7 @@ namespace storm { template uint_fast64_t SparseMatrix::getSizeInMemory() const { checkReady("getSizeInMemory"); - + uint_fast64_t size = sizeof(*this); // Add size of columns and values. @@ -785,63 +785,63 @@ namespace storm { template typename SparseMatrix::const_rows SparseMatrix::getRows(uint_fast64_t startRow, uint_fast64_t endRow) const { 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 SparseMatrix::rows SparseMatrix::getRows(uint_fast64_t startRow, uint_fast64_t endRow) { 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 SparseMatrix::const_rows SparseMatrix::getRow(uint_fast64_t row) const { checkReady("getRow"); return getRows(row, row); } - + template typename SparseMatrix::rows SparseMatrix::getRow(uint_fast64_t row) { checkReady("getRow"); return getRows(row, row); } - + template typename SparseMatrix::const_iterator SparseMatrix::begin(uint_fast64_t row) const { checkReady("begin"); - return this->columnsAndValues.begin() + this->rowIndications[row]; + return this->columnsAndValues.data() + this->rowIndications[row]; } - + template typename SparseMatrix::iterator SparseMatrix::begin(uint_fast64_t row) { checkReady("begin"); - return this->columnsAndValues.begin() + this->rowIndications[row]; + return this->columnsAndValues.data() + this->rowIndications[row]; } template typename SparseMatrix::const_iterator SparseMatrix::end(uint_fast64_t row) const { checkReady("end"); - return this->columnsAndValues.begin() + this->rowIndications[row + 1]; + return this->columnsAndValues.data() + this->rowIndications[row + 1]; } template typename SparseMatrix::iterator SparseMatrix::end(uint_fast64_t row) { checkReady("end"); - return this->columnsAndValues.begin() + this->rowIndications[row + 1]; + return this->columnsAndValues.data() + this->rowIndications[row + 1]; } - + template typename SparseMatrix::const_iterator SparseMatrix::end() const { checkReady("end"); - return this->columnsAndValues.begin() + this->rowIndications[rowCount]; + return this->columnsAndValues.data() + this->rowIndications[rowCount]; } template typename SparseMatrix::iterator SparseMatrix::end() { checkReady("end"); - return this->columnsAndValues.begin() + this->rowIndications[rowCount]; + return this->columnsAndValues.data() + this->rowIndications[rowCount]; } - + template T SparseMatrix::getRowSum(uint_fast64_t row) const { checkReady("getRowSum"); @@ -853,22 +853,21 @@ namespace storm { } template - bool SparseMatrix::isSubmatrixOf(SparseMatrix const& matrix) const { + bool SparseMatrix::isSubmatrixOf(SparseMatrix const& matrix) const { checkReady("isSubmatrixOf"); - + // Check for matching sizes. if (this->getRowCount() != matrix.getRowCount()) return false; if (this->getColumnCount() != matrix.getColumnCount()) return false; // Check the subset property for all rows individually. 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 (uint_fast64_t elem = rowIndications[row], elem2 = matrix.rowIndications[row]; elem < rowIndications[row + 1]; ++elem) { + for (const_iterator it1 = this->begin(row), ite1 = this->end(row), it2 = matrix.begin(row), ite2 = matrix.end(row); it1 != ite1; ++it1) { // 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; } - if (it2->first == ite2 || it1->first != it2->first) { + if (it2 == ite2 || it1->first != it2->first) { return false; } } @@ -879,7 +878,7 @@ namespace storm { template std::ostream& operator<<(std::ostream& out, SparseMatrix const& matrix) { matrix.checkReady("operator<<"); - + // Print column numbers in header. out << "\t\t"; for (uint_fast64_t i = 0; i < matrix.columnCount; ++i) { @@ -934,8 +933,7 @@ namespace storm { void SparseMatrix::prepareInternalStorage() { // Only allocate the memory if the dimensions of the matrix are already known. if (storagePreallocated) { - valueStorage = std::vector(entryCount, storm::utility::constantZero()); - columnIndications = std::vector(entryCount, 0); + columnsAndValues = std::vector>(entryCount, std::make_pair(0, storm::utility::constantZero())); rowIndications = std::vector(rowCount + 1, 0); } else { rowIndications.push_back(0); @@ -950,12 +948,8 @@ namespace storm { } // Explicitly instantiate the matrix and the nested classes. - template class SparseMatrix::BaseIterator; - template class SparseMatrix::BaseIterator; template class SparseMatrix; template std::ostream& operator<<(std::ostream& out, SparseMatrix const& matrix); - template class SparseMatrix::BaseIterator; - template class SparseMatrix::BaseIterator; template class SparseMatrix; template std::ostream& operator<<(std::ostream& out, SparseMatrix const& matrix); diff --git a/src/storage/SparseMatrix.h b/src/storage/SparseMatrix.h index 9406f3e79..5d5d66fa6 100644 --- a/src/storage/SparseMatrix.h +++ b/src/storage/SparseMatrix.h @@ -68,8 +68,8 @@ namespace storm { friend class tbbHelper_MatrixRowVectorScalarProduct; #endif - typedef typename std::vector>::iterator iterator; - typedef typename std::vector>::const_iterator const_iterator; + typedef std::pair* iterator; + typedef std::pair const* const_iterator; /*! * 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 * 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. */ - rows(std::pair* columnAndValuePtr, uint_fast64_t entryCount); + rows(iterator begin, uint_fast64_t entryCount); /*! * Retrieves an iterator that points to the beginning of the rows. @@ -101,7 +101,7 @@ namespace storm { private: // The pointer to the columnd and value of the first entry. - std::pair* columnAndValuePtr; + iterator beginIterator; // The number of non-zero entries in the rows. 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 * 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. */ - const_rows(std::pair 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. @@ -137,7 +137,7 @@ namespace storm { private: // The pointer to the columnd and value of the first entry. - std::pair const* columnAndValuePtr; + const_iterator beginIterator; // The number of non-zero entries in the rows. uint_fast64_t entryCount; @@ -507,7 +507,7 @@ namespace storm { * @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. */ - 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. @@ -515,7 +515,7 @@ namespace storm { * @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. */ - 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. diff --git a/src/storage/StronglyConnectedComponentDecomposition.cpp b/src/storage/StronglyConnectedComponentDecomposition.cpp index 4a43a6d44..d8c571c7b 100644 --- a/src/storage/StronglyConnectedComponentDecomposition.cpp +++ b/src/storage/StronglyConnectedComponentDecomposition.cpp @@ -127,40 +127,40 @@ namespace storm { // Now, traverse all successors of the current state. for(; successorIt != model.getRows(currentState).end(); ++successorIt) { // 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); } // 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 // 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. recursionIteratorStack.pop_back(); recursionIteratorStack.push_back(successorIt); // 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. - 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. goto recursionStepForward; 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 // can leave the SCC. - if (onlyBottomSccs && lowlinks[currentState] != lowlinks[successorIt.column()]) { + if (onlyBottomSccs && lowlinks[currentState] != lowlinks[successorIt->first]) { statesThatCanLeaveTheirScc.set(currentState); } - } else if (tarjanStackStates.get(successorIt.column())) { + } else if (tarjanStackStates.get(successorIt->first)) { // 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 // we don't need to update the bit vector of states that can leave their SCC. diff --git a/src/utility/counterexamples.h b/src/utility/counterexamples.h index 23996aaed..12358fd85 100644 --- a/src/utility/counterexamples.h +++ b/src/utility/counterexamples.h @@ -35,8 +35,8 @@ namespace storm { for (auto state : psiStates) { analysisInformation[state] = std::set(); 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; for (auto& entry : transitionMatrix.getRow(currentChoice)) { - if (entry.column() == targetState) { + if (entry.first == targetState) { choiceTargetsTargetState = true; break; } @@ -78,8 +78,8 @@ namespace storm { if (analysisInformation[currentState].size() != analysisInformationSizeBefore) { for (auto& predecessorEntry : backwardTransitions.getRow(currentState)) { // 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)); } } } diff --git a/src/utility/graph.h b/src/utility/graph.h index dfcb19e4a..c83e38c5e 100644 --- a/src/utility/graph.h +++ b/src/utility/graph.h @@ -81,17 +81,17 @@ namespace storm { 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::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 (!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) { // 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); } } @@ -212,17 +212,17 @@ namespace storm { 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 (!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) { // 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); } } @@ -291,14 +291,14 @@ namespace storm { currentState = stack.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 // 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; - 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; break; } @@ -308,8 +308,8 @@ namespace storm { // add it to the set of states for the next iteration and perform a backward search from // that state. if (allSuccessorsInCurrentStates) { - nextStates.set(predecessorEntry.column(), true); - stack.push_back(predecessorEntry.column()); + nextStates.set(predecessorEntry.first, true); + stack.push_back(predecessorEntry.first); break; } } @@ -402,15 +402,15 @@ namespace storm { 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 // nondeterministic choice. 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; - 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; break; } @@ -426,13 +426,13 @@ namespace storm { if (addToStatesWithProbabilityGreater0) { // If we don't have a bound on the number of steps to take, just add the state to the stack. 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) { // 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); } } @@ -502,13 +502,13 @@ namespace storm { currentState = stack.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 // nondeterminstic choices. 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; 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 // that state. 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: 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. - recursionStack.push_back(successorIterator.column()); + recursionStack.push_back(successorIterator.first); // 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; } @@ -684,23 +684,23 @@ namespace storm { // Now check the new distances for all successors of the current state. typename storm::storage::SparseMatrix::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. - 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. - 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. - if (newDistance > probabilities[transition.column()]) { + if (newDistance > probabilities[transition.first]) { // 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. - 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)); } } } diff --git a/src/utility/matrix.h b/src/utility/matrix.h index 47e36fb44..21bbe2fe9 100644 --- a/src/utility/matrix.h +++ b/src/utility/matrix.h @@ -32,8 +32,8 @@ namespace storm { // If a valid choice for this state is defined, we copy over the corresponding entries. typename storm::storage::SparseMatrix::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 { // If no valid choice for the state is defined, we insert a self-loop. diff --git a/test/functional/storage/SparseMatrixTest.cpp b/test/functional/storage/SparseMatrixTest.cpp index 4788e51eb..8e48b1c7b 100644 --- a/test/functional/storage/SparseMatrixTest.cpp +++ b/test/functional/storage/SparseMatrixTest.cpp @@ -494,24 +494,24 @@ TEST(SparseMatrix, Iteration) { ASSERT_NO_THROW(matrix.finalize()); 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 { ASSERT_TRUE(false); } } for (storm::storage::SparseMatrix::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 { ASSERT_TRUE(false); } diff --git a/test/performance/graph/GraphTest.cpp b/test/performance/graph/GraphTest.cpp index 8bbb44518..5bff9383a 100644 --- a/test/performance/graph/GraphTest.cpp +++ b/test/performance/graph/GraphTest.cpp @@ -21,7 +21,7 @@ TEST(GraphTest, PerformProb01) { ASSERT_EQ(prob01.first.getNumberOfSetBits(), 574016ull); ASSERT_EQ(prob01.second.getNumberOfSetBits(), 825797ull); - + prob01 = storm::utility::graph::performProb01(*dtmc, trueStates, storm::storage::BitVector(dtmc->getLabeledStates("observeOnlyTrueSender"))); ASSERT_EQ(prob01.first.getNumberOfSetBits(), 1785309ull); diff --git a/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp b/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp index c8c7e1346..c9c309d60 100644 --- a/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp +++ b/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp @@ -67,6 +67,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, SynchronousLeader) { ASSERT_EQ(parser.getType(), storm::models::DTMC); + std::shared_ptr> dtmc = parser.getModel>(); ASSERT_EQ(dtmc->getNumberOfStates(), 1312334ull); diff --git a/test/performance/storage/SparseMatrixTest.cpp b/test/performance/storage/SparseMatrixTest.cpp index c6c78d2b7..794d942ec 100644 --- a/test/performance/storage/SparseMatrixTest.cpp +++ b/test/performance/storage/SparseMatrixTest.cpp @@ -13,7 +13,7 @@ TEST(SparseMatrix, Iteration) { for (uint_fast64_t row = 0; row < matrix.getRowCount(); ++row) { for (auto const& entry : matrix.getRow(row)) { // 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); } }