From db232fe39bf256865e69f19cec2e2b9abbcb98c4 Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 6 May 2014 19:33:54 +0200 Subject: [PATCH] Moved from pair to MatrixEntry as the basic building block of the matrix. Now matrix elements can be accessed in a more readable way. Former-commit-id: f6514eb0cd627fba813d78d4626763afda0734ee --- src/adapters/GmmxxAdapter.h | 4 +- .../MILPMinimalLabelSetGenerator.h | 50 ++--- .../PathBasedSubsystemGenerator.h | 144 +++++++------- .../SparseMarkovAutomatonCslModelChecker.h | 32 +-- src/models/AbstractDeterministicModel.h | 6 +- src/models/AbstractNondeterministicModel.h | 4 +- src/models/Dtmc.h | 12 +- src/models/MarkovAutomaton.h | 12 +- .../MaximalEndComponentDecomposition.cpp | 8 +- src/storage/SparseMatrix.cpp | 137 ++++++++----- src/storage/SparseMatrix.h | 90 ++++++++- ...tronglyConnectedComponentDecomposition.cpp | 20 +- src/utility/counterexamples.h | 28 +-- src/utility/graph.h | 60 +++--- src/utility/matrix.h | 2 +- ...eterministicSparseTransitionParserTest.cpp | 168 ++++++++-------- ...kovAutomatonSparseTransitionParserTest.cpp | 48 ++--- ...eterministicSparseTransitionParserTest.cpp | 184 +++++++++--------- test/functional/storage/SparseMatrixTest.cpp | 26 +-- test/performance/storage/SparseMatrixTest.cpp | 2 +- 20 files changed, 576 insertions(+), 461 deletions(-) diff --git a/src/adapters/GmmxxAdapter.h b/src/adapters/GmmxxAdapter.h index ff35800b2..b1d2206a5 100644 --- a/src/adapters/GmmxxAdapter.h +++ b/src/adapters/GmmxxAdapter.h @@ -51,8 +51,8 @@ public: columns.reserve(matrix.getEntryCount()); for (auto const& entry : matrix) { - columns.emplace_back(entry.first); - values.emplace_back(entry.second); + columns.emplace_back(entry.getColumn()); + values.emplace_back(entry.getValue()); } std::swap(result->ir, columns); diff --git a/src/counterexamples/MILPMinimalLabelSetGenerator.h b/src/counterexamples/MILPMinimalLabelSetGenerator.h index 197db76ab..4e0f9381c 100644 --- a/src/counterexamples/MILPMinimalLabelSetGenerator.h +++ b/src/counterexamples/MILPMinimalLabelSetGenerator.h @@ -130,7 +130,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.first) || psiStates.get(successorEntry.first)) { + if (stateInformation.relevantStates.get(successorEntry.getColumn()) || psiStates.get(successorEntry.getColumn())) { for (auto const& label : choiceLabeling[row]) { result.allRelevantLabels.insert(label); } @@ -139,7 +139,7 @@ namespace storm { result.relevantChoicesForRelevantStates[state].push_back(row); } } - if (!stateInformation.problematicStates.get(successorEntry.first)) { + if (!stateInformation.problematicStates.get(successorEntry.getColumn())) { allSuccessorsProblematic = false; } } @@ -297,11 +297,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.first)) { - if (resultingMap.find(successorEntry.first) == resultingMap.end()) { + if (stateInformation.relevantStates.get(successorEntry.getColumn())) { + if (resultingMap.find(successorEntry.getColumn()) == resultingMap.end()) { variableNameBuffer.str(""); variableNameBuffer.clear(); - variableNameBuffer << "r" << successorEntry.first; + variableNameBuffer << "r" << successorEntry.getColumn(); resultingMap[state] = solver.createContinuousVariable(variableNameBuffer.str(), storm::solver::LpSolver::BOUNDED, 0, 1, 0); ++numberOfVariablesCreated; } @@ -330,11 +330,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.first)) { + if (stateInformation.relevantStates.get(successorEntry.getColumn())) { variableNameBuffer.str(""); variableNameBuffer.clear(); - variableNameBuffer << "t" << state << "to" << successorEntry.first; - resultingMap[std::make_pair(state, successorEntry.first)] = solver.createBinaryVariable(variableNameBuffer.str(), 0); + variableNameBuffer << "t" << state << "to" << successorEntry.getColumn(); + resultingMap[std::make_pair(state, successorEntry.getColumn())] = solver.createBinaryVariable(variableNameBuffer.str(), 0); ++numberOfVariablesCreated; } } @@ -544,11 +544,11 @@ namespace storm { double rightHandSide = 1; for (auto const& successorEntry : labeledMdp.getTransitionMatrix().getRow(choice)) { - 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; + if (stateInformation.relevantStates.get(successorEntry.getColumn())) { + variables.push_back(static_cast(variableInformation.stateToProbabilityVariableIndexMap.at(successorEntry.getColumn()))); + coefficients.push_back(-successorEntry.getValue()); + } else if (psiStates.get(successorEntry.getColumn())) { + rightHandSide += successorEntry.getValue(); } } @@ -602,7 +602,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.first))); + variables.push_back(variableInformation.problematicTransitionToVariableIndexMap.at(std::make_pair(stateListPair.first, successorEntry.getColumn()))); coefficients.push_back(-1); } @@ -619,9 +619,9 @@ namespace storm { variables.push_back(variableInformation.problematicStateToVariableIndexMap.at(state)); coefficients.push_back(1); - variables.push_back(variableInformation.problematicStateToVariableIndexMap.at(successorEntry.first)); + variables.push_back(variableInformation.problematicStateToVariableIndexMap.at(successorEntry.getColumn())); coefficients.push_back(-1); - variables.push_back(variableInformation.problematicTransitionToVariableIndexMap.at(std::make_pair(state, successorEntry.first))); + variables.push_back(variableInformation.problematicTransitionToVariableIndexMap.at(std::make_pair(state, successorEntry.getColumn()))); coefficients.push_back(1); solver.addConstraint("UnproblematicStateReachable" + std::to_string(numberOfConstraintsCreated), variables, coefficients, storm::solver::LpSolver::LESS, 1); @@ -677,7 +677,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.first)) { + if (psiStates.get(successorEntry.getColumn())) { psiStateReachableInOneStep = true; } } @@ -690,8 +690,8 @@ namespace storm { coefficients.push_back(1); for (auto const& successorEntry : labeledMdp.getTransitionMatrix().getRow(choice)) { - if (state != successorEntry.first && stateInformation.relevantStates.get(successorEntry.first)) { - std::list const& successorChoiceVariableIndices = variableInformation.stateToChoiceVariablesIndexMap.at(successorEntry.first); + if (state != successorEntry.getColumn() && stateInformation.relevantStates.get(successorEntry.getColumn())) { + std::list const& successorChoiceVariableIndices = variableInformation.stateToChoiceVariablesIndexMap.at(successorEntry.getColumn()); for (auto choiceVariableIndex : successorChoiceVariableIndices) { variables.push_back(choiceVariableIndex); @@ -720,8 +720,8 @@ namespace storm { // Compute the set of predecessors. std::unordered_set predecessors; for (auto const& predecessorEntry : backwardTransitions.getRow(state)) { - if (state != predecessorEntry.first) { - predecessors.insert(predecessorEntry.first); + if (state != predecessorEntry.getColumn()) { + predecessors.insert(predecessorEntry.getColumn()); } } @@ -737,7 +737,7 @@ namespace storm { // Check if the current choice targets the current state. for (auto const& successorEntry : labeledMdp.getTransitionMatrix().getRow(relevantChoice)) { - if (state == successorEntry.first) { + if (state == successorEntry.getColumn()) { choiceTargetsCurrentState = true; break; } @@ -782,8 +782,8 @@ namespace storm { for (auto psiState : psiStates) { // Compute the set of predecessors. for (auto const& predecessorEntry : backwardTransitions.getRow(psiState)) { - if (psiState != predecessorEntry.first) { - predecessors.insert(predecessorEntry.first); + if (psiState != predecessorEntry.getColumn()) { + predecessors.insert(predecessorEntry.getColumn()); } } } @@ -800,7 +800,7 @@ namespace storm { // Check if the current choice targets the current state. for (auto const& successorEntry : labeledMdp.getTransitionMatrix().getRow(relevantChoice)) { - if (psiStates.get(successorEntry.first)) { + if (psiStates.get(successorEntry.getColumn())) { choiceTargetsPsiState = true; break; } diff --git a/src/counterexamples/PathBasedSubsystemGenerator.h b/src/counterexamples/PathBasedSubsystemGenerator.h index 11e24d00d..2325eebe8 100644 --- a/src/counterexamples/PathBasedSubsystemGenerator.h +++ b/src/counterexamples/PathBasedSubsystemGenerator.h @@ -69,31 +69,31 @@ public: 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.second != (T) 0 && !subSysStates.get(trans.first)) { + if(trans.getValue() != (T) 0 && !subSysStates.get(trans.getColumn())) { //new state? - if(distances[trans.first].second == (T) -1) { - distances[trans.first].first = init; - distances[trans.first].second = trans.second; + if(distances[trans.getColumn()].second == (T) -1) { + distances[trans.getColumn()].first = init; + distances[trans.getColumn()].second = trans.getValue(); - activeSet.insert(std::pair(trans.first, distances[trans.first].second)); + activeSet.insert(std::pair(trans.getColumn(), distances[trans.getColumn()].second)); } - else if(distances[trans.first].second < trans.second){ + else if(distances[trans.getColumn()].second < trans.getValue()){ //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.first, distances[trans.first].second)); + auto range = activeSet.equal_range(std::pair(trans.getColumn(), distances[trans.getColumn()].second)); for(;range.first != range.second; range.first++) { - if(trans.first == range.first->first) { + if(trans.getColumn() == range.first->first) { activeSet.erase(range.first); break; } } - distances[trans.first].first = init; - distances[trans.first].second = trans.second; + distances[trans.getColumn()].first = init; + distances[trans.getColumn()].second = trans.getValue(); - activeSet.insert(std::pair(trans.first, trans.second)); + activeSet.insert(std::pair(trans.getColumn(), trans.getValue())); } } } @@ -115,36 +115,36 @@ public: // Look at all neighbors for(auto const& trans : transMat.getRow(activeState.first)) { // Only consider the transition if it's not virtual - if(trans.second != (T) 0) { + if(trans.getValue() != (T) 0) { - T distance = activeState.second * trans.second; + T distance = activeState.second * trans.getValue(); //not discovered or initial terminal state - if(distances[trans.first].second == (T)-1) { + if(distances[trans.getColumn()].second == (T)-1) { //New state discovered -> save it - distances[trans.first].first = activeState.first; - distances[trans.first].second = distance; + distances[trans.getColumn()].first = activeState.first; + distances[trans.getColumn()].second = distance; // push newly discovered state into activeSet - activeSet.insert(std::pair(trans.first, distance)); + activeSet.insert(std::pair(trans.getColumn(), distance)); } - else if(distances[trans.first].second < distance ){ + else if(distances[trans.getColumn()].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.first, distances[trans.first].second)); + auto range = activeSet.equal_range(std::pair(trans.getColumn(), distances[trans.getColumn()].second)); for(;range.first != range.second; range.first++) { - if(trans.first == range.first->first) { + if(trans.getColumn() == range.first->first) { activeSet.erase(range.first); break; } } - distances[trans.first].first = activeState.first; - distances[trans.first].second = distance; - activeSet.insert(std::pair(trans.first, distance)); + distances[trans.getColumn()].first = activeState.first; + distances[trans.getColumn()].second = distance; + activeSet.insert(std::pair(trans.getColumn(), distance)); } } } @@ -182,33 +182,33 @@ public: 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.second != (T) 0 && !subSysStates.get(trans.first)) { + if(trans.getValue() != (T) 0 && !subSysStates.get(trans.getColumn())) { //new state? - if(distances[trans.first].second == (T) -1) { + if(distances[trans.getColumn()].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.first].first = init; - distances[trans.first].second = trans.second * (itDistances[init].second == -1 ? 1 : itDistances[init].second); + distances[trans.getColumn()].first = init; + distances[trans.getColumn()].second = trans.getValue() * (itDistances[init].second == -1 ? 1 : itDistances[init].second); - activeSet.insert(std::pair(trans.first, distances[trans.first].second)); + activeSet.insert(std::pair(trans.getColumn(), distances[trans.getColumn()].second)); } - else if(distances[trans.first].second < trans.second * itDistances[init].second){ + else if(distances[trans.getColumn()].second < trans.getValue() * 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.first, distances[trans.first].second)); + auto range = activeSet.equal_range(std::pair(trans.getColumn(), distances[trans.getColumn()].second)); for(;range.first != range.second; range.first++) { - if(trans.first == range.first->first) { + if(trans.getColumn() == 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.first].first = init; - distances[trans.first].second = trans.second * (itDistances[init].second == -1 ? 1 : itDistances[init].second); + distances[trans.getColumn()].first = init; + distances[trans.getColumn()].second = trans.getValue() * (itDistances[init].second == -1 ? 1 : itDistances[init].second); - activeSet.insert(std::pair(trans.first, trans.second)); + activeSet.insert(std::pair(trans.getColumn(), trans.getValue())); } } } @@ -225,7 +225,7 @@ public: activeSet.erase(--activeSet.end()); // Always stop at first target/terminal state - //if(terminalStates.get(activeState.first) || subSysStates.get(activeState.first)) break; + //if(terminalStates.get(activeState.getColumn()) || subSysStates.get(activeState.getColumn())) break; // If this is an initial state, do not consider its outgoing transitions, since all relevant ones have already been considered // Same goes for forbidden states since they may not be used on a path, except as last node. @@ -233,36 +233,36 @@ public: // Look at all neighbors for(auto const& trans : transMat.getRow(activeState.first)) { // Only consider the transition if it's not virtual - if(trans.second != (T) 0) { + if(trans.getValue() != (T) 0) { - T distance = activeState.second * trans.second; + T distance = activeState.second * trans.getValue(); //not discovered or initial terminal state - if(distances[trans.first].second == (T)-1) { + if(distances[trans.getColumn()].second == (T)-1) { //New state discovered -> save it - distances[trans.first].first = activeState.first; - distances[trans.first].second = distance; + distances[trans.getColumn()].first = activeState.first; + distances[trans.getColumn()].second = distance; // push newly discovered state into activeSet - activeSet.insert(std::pair(trans.first, distance)); + activeSet.insert(std::pair(trans.getColumn(), distance)); } - else if(distances[trans.first].second < distance ){ + else if(distances[trans.getColumn()].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.first, distances[trans.first].second)); + auto range = activeSet.equal_range(std::pair(trans.getColumn(), distances[trans.getColumn()].second)); for(;range.first != range.second; range.first++) { - if(trans.first == range.first->first) { + if(trans.getColumn() == range.first->first) { activeSet.erase(range.first); break; } } - distances[trans.first].first = activeState.first; - distances[trans.first].second = distance; - activeSet.insert(std::pair(trans.first, distance)); + distances[trans.getColumn()].first = activeState.first; + distances[trans.getColumn()].second = distance; + activeSet.insert(std::pair(trans.getColumn(), distance)); } } } @@ -292,8 +292,8 @@ public: // if there is a terminal state that is an initial state then prob == 1 and return if(initStates.get(*target)){ - distances[*target].first = *target; - distances[*target].second = (T) 1; + distances[*target].getColumn() = *target; + distances[*target].getValue() = (T) 1; return; } @@ -302,19 +302,19 @@ public: //only use if allowed and not in subsys and not terminal if(allowedStates.get(*iter) && !subSysStates.get(*iter) && !terminalStates.get(*iter)) { //new state? - if(distances[*iter].second == (T) -1) { + if(distances[*iter].getValue() == (T) -1) { // save as discovered and push into active set - distances[*iter].first = *target; //successor - distances[*iter].second = transMat.getValue(*iter, *target); //prob of shortest path + distances[*iter].getColumn() = *target; //successor + distances[*iter].getValue() = transMat.getValue(*iter, *target); //prob of shortest path activeSet.insert(std::pair(*iter, probabilities[*iter])); //prob of reaching some terminal state from pred. } else { // state was already discovered // is this the better transition? - if(distances[*iter].second > transMat.getValue(*iter, *target)) { - distances[*iter].first = *target; - distances[*iter].second = transMat.getValue(*iter, *target); + if(distances[*iter].getValue() > transMat.getValue(*iter, *target)) { + distances[*iter].getColumn() = *target; + distances[*iter].getValue() = transMat.getValue(*iter, *target); } } } @@ -328,19 +328,19 @@ public: //only use if allowed and not in subsys and not terminal if(allowedStates.get(*iter) && !subSysStates.get(*iter) && !terminalStates.get(*iter)) { //new state? - if(distances[*iter].second == (T) -1) { + if(distances[*iter].getValue() == (T) -1) { // save as discovered and push into active set - distances[*iter].first = *sysState; //successor - distances[*iter].second = transMat.getValue(*iter, *sysState); //prob of shortest path + distances[*iter].getColumn() = *sysState; //successor + distances[*iter].getValue() = transMat.getValue(*iter, *sysState); //prob of shortest path activeSet.insert(std::pair(*iter, probabilities[*iter])); //prob of reaching some terminal state from pred. } else { // state was already discovered // is this the better transition? - if(distances[*iter].second > transMat.getValue(*iter, *sysState)) { - distances[*iter].first = *sysState; - distances[*iter].second = transMat.getValue(*iter, *sysState); + if(distances[*iter].getValue() > transMat.getValue(*iter, *sysState)) { + distances[*iter].getColumn() = *sysState; + distances[*iter].getValue() = transMat.getValue(*iter, *sysState); } } } @@ -355,7 +355,7 @@ public: while(!activeSet.empty()) { // copy here since using a reference leads to segfault state = *(--activeSet.end()); - activeState = state.first; + activeState = state.getColumn(); activeSet.erase(--activeSet.end()); //stop on the first subsys/init state @@ -368,19 +368,19 @@ public: //only if transition is not "virtual" and no selfloop if(*iter != activeState && transMat.getValue(*iter, activeState) != (T) 0) { //new state? - if(distances[*iter].second == (T) -1) { + if(distances[*iter].getValue() == (T) -1) { // save as discovered and push into active set - distances[*iter].first = activeState; - distances[*iter].second = transMat.getValue(*iter, activeState) * distances[activeState].second; + distances[*iter].getColumn() = activeState; + distances[*iter].getValue() = transMat.getValue(*iter, activeState) * distances[activeState].getValue(); activeSet.insert(std::pair(*iter, probabilities[*iter])); } else { // state was already discovered // is this the better transition? - if(distances[*iter].second < transMat.getValue(*iter, activeState) * distances[activeState].second) { - distances[*iter].first = activeState; - distances[*iter].second = transMat.getValue(*iter, activeState) * distances[activeState].second; + if(distances[*iter].getValue() < transMat.getValue(*iter, activeState) * distances[activeState].getValue()) { + distances[*iter].getColumn() = activeState; + distances[*iter].getValue() = transMat.getValue(*iter, activeState) * distances[activeState].getValue(); } } } @@ -389,15 +389,15 @@ public: } //get path probability - probability = distances[activeState].second; + probability = distances[activeState].getValue(); if(probability == (T) -1) probability = 1; // iterate over the successors until reaching the end of the finite path shortestPath.push_back(activeState); - activeState = distances[activeState].first; + activeState = distances[activeState].getColumn(); while(!terminalStates.get(activeState) && !subSysStates.get(activeState)) { shortestPath.push_back(activeState); - activeState = distances[activeState].first; + activeState = distances[activeState].getColumn(); } shortestPath.push_back(activeState); } @@ -482,7 +482,7 @@ public: shortestPath.push_back(bestIndex); //At last compensate for the distance between init and source state - probability = itSearch ? probability : probability / itDistances[bestIndex].second; + probability = itSearch ? probability : probability / itDistances[bestIndex].first; } private: diff --git a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h index a4cd0844a..aab76f807 100644 --- a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h +++ b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h @@ -103,10 +103,10 @@ namespace storm { for (auto state : markovianNonGoalStates) { for (auto& element : aMarkovian.getRow(rowIndex)) { ValueType eTerm = std::exp(-exitRates[state] * delta); - if (element.first == rowIndex) { - element.second = (storm::utility::constantOne() - eTerm) * element.second + eTerm; + if (element.getColumn() == rowIndex) { + element.getValue() = (storm::utility::constantOne() - eTerm) * element.getValue() + eTerm; } else { - element.second = (storm::utility::constantOne() - eTerm) * element.second; + element.getValue() = (storm::utility::constantOne() - eTerm) * element.getValue(); } } ++rowIndex; @@ -116,7 +116,7 @@ namespace storm { rowIndex = 0; for (auto state : markovianNonGoalStates) { for (auto& element : aMarkovianToProbabilistic.getRow(rowIndex)) { - element.second = (1 - std::exp(-exitRates[state] * delta)) * element.second; + element.getValue() = (1 - std::exp(-exitRates[state] * delta)) * element.getValue(); } ++rowIndex; } @@ -133,8 +133,8 @@ namespace storm { bMarkovianFixed.push_back(storm::utility::constantZero()); for (auto& element : transitionMatrix.getRowGroup(state)) { - if (goalStates.get(element.first)) { - bMarkovianFixed.back() += (1 - std::exp(-exitRates[state] * delta)) * element.second; + if (goalStates.get(element.getColumn())) { + bMarkovianFixed.back() += (1 - std::exp(-exitRates[state] * delta)) * element.getValue(); } } } @@ -314,13 +314,13 @@ namespace storm { b.push_back(storm::utility::constantZero()); for (auto element : transitionMatrix.getRow(choice)) { - if (statesNotContainedInAnyMec.get(element.first)) { + if (statesNotContainedInAnyMec.get(element.getColumn())) { // If the target state is not contained in an MEC, we can copy over the entry. - sspMatrixBuilder.addNextValue(currentChoice, statesNotInMecsBeforeIndex[element.first], element.second); + sspMatrixBuilder.addNextValue(currentChoice, statesNotInMecsBeforeIndex[element.getColumn()], element.getValue()); } 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.first]] += element.second; + auxiliaryStateToProbabilityMap[stateToMecIndexMap[element.getColumn()]] += element.getValue(); } } @@ -350,13 +350,13 @@ namespace storm { b.push_back(storm::utility::constantZero()); for (auto element : transitionMatrix.getRow(choice)) { - if (statesNotContainedInAnyMec.get(element.first)) { + if (statesNotContainedInAnyMec.get(element.getColumn())) { // If the target state is not contained in an MEC, we can copy over the entry. - sspMatrixBuilder.addNextValue(currentChoice, statesNotInMecsBeforeIndex[element.first], element.second); + sspMatrixBuilder.addNextValue(currentChoice, statesNotInMecsBeforeIndex[element.getColumn()], element.getValue()); } 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.first]] += element.second; + auxiliaryStateToProbabilityMap[stateToMecIndexMap[element.getColumn()]] += element.getValue(); } } @@ -453,8 +453,8 @@ namespace storm { coefficients.push_back(1); for (auto element : transitionMatrix.getRow(nondeterministicChoiceIndices[state])) { - variables.push_back(stateToVariableIndexMap.at(element.first)); - coefficients.push_back(-element.second); + variables.push_back(stateToVariableIndexMap.at(element.getColumn())); + coefficients.push_back(-element.getValue()); } variables.push_back(lraValueVariableIndex); @@ -472,8 +472,8 @@ namespace storm { coefficients.push_back(1); for (auto element : transitionMatrix.getRow(choice)) { - variables.push_back(stateToVariableIndexMap.at(element.first)); - coefficients.push_back(-element.second); + variables.push_back(stateToVariableIndexMap.at(element.getColumn())); + coefficients.push_back(-element.getValue()); } 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/models/AbstractDeterministicModel.h b/src/models/AbstractDeterministicModel.h index c72b914de..88e0d1006 100644 --- a/src/models/AbstractDeterministicModel.h +++ b/src/models/AbstractDeterministicModel.h @@ -87,9 +87,9 @@ class AbstractDeterministicModel: public AbstractModel { 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 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; + if (transition.getValue() != storm::utility::constantZero()) { + if (subsystem == nullptr || subsystem->get(transition.getColumn())) { + outStream << "\t" << i << " -> " << transition.getColumn() << " [ label= \"" << transition.getValue() << "\" ];" << std::endl; } } } diff --git a/src/models/AbstractNondeterministicModel.h b/src/models/AbstractNondeterministicModel.h index 0058377a6..3a738cbe6 100644 --- a/src/models/AbstractNondeterministicModel.h +++ b/src/models/AbstractNondeterministicModel.h @@ -189,8 +189,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.first)) { - outStream << "\t\"" << state << "c" << choice << "\" -> " << transition.first << " [ label= \"" << transition.second << "\" ]"; + if (subsystem == nullptr || subsystem->get(transition.getColumn())) { + outStream << "\t\"" << state << "c" << choice << "\" -> " << transition.getColumn() << " [ label= \"" << transition.getValue() << "\" ]"; // 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 b599774f9..eb0e669dd 100644 --- a/src/models/Dtmc.h +++ b/src/models/Dtmc.h @@ -170,7 +170,7 @@ public: for(uint_fast64_t row = 0; row < origMat.getRowCount(); ++row) { if(subSysStates.get(row)){ for(auto const& entry : origMat.getRow(row)) { - if(subSysStates.get(entry.first)) { + if(subSysStates.get(entry.getColumn())) { subSysTransitionCount++; } } @@ -198,10 +198,10 @@ public: if(subSysStates.get(row)){ // Transfer transitions for(auto& entry : origMat.getRow(row)) { - if(subSysStates.get(entry.first)) { - newMatBuilder.addNextValue(newRow, stateMapping[entry.first], entry.second); + if(subSysStates.get(entry.getColumn())) { + newMatBuilder.addNextValue(newRow, stateMapping[entry.getColumn()], entry.getValue()); } else { - rest += entry.second; + rest += entry.getValue(); } } @@ -251,8 +251,8 @@ public: if(subSysStates.get(row)){ // Transfer transition rewards for(auto& entry : this->getTransitionRewardMatrix().getRow(row)) { - if(subSysStates.get(entry.first)) { - newTransRewardsBuilder.addNextValue(newRow, stateMapping[entry.first], entry.second); + if(subSysStates.get(entry.getColumn())) { + newTransRewardsBuilder.addNextValue(newRow, stateMapping[entry.getColumn()], entry.getValue()); } } diff --git a/src/models/MarkovAutomaton.h b/src/models/MarkovAutomaton.h index 22b6ab13f..89ce7ccee 100644 --- a/src/models/MarkovAutomaton.h +++ b/src/models/MarkovAutomaton.h @@ -147,7 +147,7 @@ namespace storm { for (uint_fast64_t row = this->getTransitionMatrix().getRowGroupIndices()[state] + (this->isHybridState(state) ? 1 : 0); row < this->getTransitionMatrix().getRowGroupIndices()[state + 1]; ++row) { for (auto const& entry : this->transitionMatrix.getRow(row)) { - newTransitionMatrixBuilder.addNextValue(currentChoice, entry.first, entry.second); + newTransitionMatrixBuilder.addNextValue(currentChoice, entry.getColumn(), entry.getValue()); } ++currentChoice; } @@ -220,8 +220,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.first)) { - outStream << "\t\"" << state << "c" << choice << "\" -> " << transition.first << " [ label= \"" << transition.second << "\" ]"; + if (subsystem == nullptr || subsystem->get(transition.getColumn())) { + outStream << "\t\"" << state << "c" << choice << "\" -> " << transition.getColumn() << " [ label= \"" << transition.getValue() << "\" ]"; // If we were given a scheduler to highlight, we do so now. if (scheduler != nullptr) { @@ -237,8 +237,8 @@ namespace storm { } else { // In this case we are emitting a Markovian choice, so draw the arrows directly to the target states. for (auto const& transition : row) { - if (subsystem == nullptr || subsystem->get(transition.first)) { - outStream << "\t\"" << state << "\" -> " << transition.first << " [ label= \"" << transition.second << " (" << this->exitRates[state] << ")\" ]"; + if (subsystem == nullptr || subsystem->get(transition.getColumn())) { + outStream << "\t\"" << state << "\" -> " << transition.getColumn() << " [ label= \"" << transition.getValue() << " (" << this->exitRates[state] << ")\" ]"; } } } @@ -259,7 +259,7 @@ namespace storm { void turnRatesToProbabilities() { for (auto state : this->markovianStates) { for (auto& transition : this->transitionMatrix.getRowGroup(state)) { - transition.second /= this->exitRates[state]; + transition.getValue() /= this->exitRates[state]; } } } diff --git a/src/storage/MaximalEndComponentDecomposition.cpp b/src/storage/MaximalEndComponentDecomposition.cpp index 56ebbd34c..0f6a44f65 100644 --- a/src/storage/MaximalEndComponentDecomposition.cpp +++ b/src/storage/MaximalEndComponentDecomposition.cpp @@ -88,7 +88,7 @@ namespace storm { for (uint_fast64_t choice = nondeterministicChoiceIndices[state]; choice < nondeterministicChoiceIndices[state + 1]; ++choice) { bool choiceContainedInMEC = true; for (auto const& entry : transitionMatrix.getRow(choice)) { - if (scc.find(entry.first) == scc.end()) { + if (scc.find(entry.getColumn()) == scc.end()) { choiceContainedInMEC = false; break; } @@ -116,8 +116,8 @@ namespace storm { statesToCheck.clear(); for (auto state : statesToRemove) { for (auto const& entry : backwardTransitions.getRow(state)) { - if (scc.find(entry.first) != scc.end()) { - statesToCheck.set(entry.first); + if (scc.find(entry.getColumn()) != scc.end()) { + statesToCheck.set(entry.getColumn()); } } } @@ -154,7 +154,7 @@ namespace storm { for (uint_fast64_t choice = nondeterministicChoiceIndices[state]; choice < nondeterministicChoiceIndices[state + 1]; ++choice) { bool choiceContained = true; for (auto const& entry : transitionMatrix.getRow(choice)) { - if (mecStateSet.find(entry.first) == mecStateSet.end()) { + if (mecStateSet.find(entry.getColumn()) == mecStateSet.end()) { choiceContained = false; break; } diff --git a/src/storage/SparseMatrix.cpp b/src/storage/SparseMatrix.cpp index e4d719006..c6bfd0214 100644 --- a/src/storage/SparseMatrix.cpp +++ b/src/storage/SparseMatrix.cpp @@ -17,6 +17,41 @@ extern log4cplus::Logger logger; namespace storm { namespace storage { + template + MatrixEntry::MatrixEntry(uint_fast64_t column, T value) : entry(column, value) { + // Intentionally left empty. + } + + template + MatrixEntry::MatrixEntry(std::pair&& pair) : entry(std::move(pair)) { + // Intentionally left empty. + } + + template + uint_fast64_t const& MatrixEntry::getColumn() const { + return this->entry.first; + } + + template + uint_fast64_t& MatrixEntry::getColumn() { + return this->entry.first; + } + + template + T const& MatrixEntry::getValue() const { + return this->entry.second; + } + + template + T& MatrixEntry::getValue() { + return this->entry.second; + } + + template + std::pair const& MatrixEntry::getColumnValuePair() const { + return this->entry; + } + template SparseMatrixBuilder::SparseMatrixBuilder(uint_fast64_t rows, uint_fast64_t columns, uint_fast64_t entries, bool hasCustomRowGrouping, uint_fast64_t rowGroups) : rowCountSet(rows != 0), rowCount(rows), columnCountSet(columns != 0), columnCount(columns), entryCount(entries), hasCustomRowGrouping(hasCustomRowGrouping), rowGroupCountSet(rowGroups != 0), rowGroupCount(rowGroups), rowGroupIndices(), storagePreallocated(rows != 0 && columns != 0 && entries != 0), columnsAndValues(), rowIndications(), currentEntryCount(0), lastRow(0), lastColumn(0), currentRowGroup(0) { this->prepareInternalStorage(); @@ -168,7 +203,7 @@ namespace storm { void SparseMatrixBuilder::prepareInternalStorage() { // Only allocate the memory for the matrix contents if the dimensions of the matrix are already known. if (storagePreallocated) { - columnsAndValues = std::vector>(entryCount, std::make_pair(0, storm::utility::constantZero())); + columnsAndValues = std::vector>(entryCount, MatrixEntry(0, storm::utility::constantZero())); rowIndications = std::vector(rowCount + 1, 0); } else { rowIndications.push_back(0); @@ -236,18 +271,18 @@ namespace storm { } template - SparseMatrix::SparseMatrix(uint_fast64_t columnCount, std::vector const& rowIndications, std::vector> const& columnsAndValues, std::vector const& rowGroupIndices) : rowCount(rowIndications.size() - 1), columnCount(columnCount), entryCount(columnsAndValues.size()), nonzeroEntryCount(0), columnsAndValues(columnsAndValues), rowIndications(rowIndications), rowGroupIndices(rowGroupIndices) { + SparseMatrix::SparseMatrix(uint_fast64_t columnCount, std::vector const& rowIndications, std::vector> const& columnsAndValues, std::vector const& rowGroupIndices) : rowCount(rowIndications.size() - 1), columnCount(columnCount), entryCount(columnsAndValues.size()), nonzeroEntryCount(0), columnsAndValues(columnsAndValues), rowIndications(rowIndications), rowGroupIndices(rowGroupIndices) { for (auto const& element : *this) { - if (element.second != storm::utility::constantZero()) { + if (element.getValue() != storm::utility::constantZero()) { ++this->nonzeroEntryCount; } } } template - SparseMatrix::SparseMatrix(uint_fast64_t columnCount, std::vector&& rowIndications, std::vector>&& columnsAndValues, std::vector&& rowGroupIndices) : rowCount(rowIndications.size() - 1), columnCount(columnCount), entryCount(columnsAndValues.size()), nonzeroEntryCount(0), columnsAndValues(std::move(columnsAndValues)), rowIndications(std::move(rowIndications)), rowGroupIndices(std::move(rowGroupIndices)) { + SparseMatrix::SparseMatrix(uint_fast64_t columnCount, std::vector&& rowIndications, std::vector>&& columnsAndValues, std::vector&& rowGroupIndices) : rowCount(rowIndications.size() - 1), columnCount(columnCount), entryCount(columnsAndValues.size()), nonzeroEntryCount(0), columnsAndValues(std::move(columnsAndValues)), rowIndications(std::move(rowIndications)), rowGroupIndices(std::move(rowGroupIndices)) { for (auto const& element : *this) { - if (element.second != storm::utility::constantZero()) { + if (element.getValue() != storm::utility::constantZero()) { ++this->nonzeroEntryCount; } } @@ -304,17 +339,17 @@ namespace storm { for (uint_fast64_t row = 0; row < this->getRowCount(); ++row) { for (const_iterator it1 = this->begin(row), ite1 = this->end(row), it2 = other.begin(row), ite2 = other.end(row); it1 != ite1 && it2 != ite2; ++it1, ++it2) { // Skip over all zero entries in both matrices. - while (it1 != ite1 && it1->second == storm::utility::constantZero()) { + while (it1 != ite1 && it1->getValue() == storm::utility::constantZero()) { ++it1; } - while (it2 != ite2 && it2->second == storm::utility::constantZero()) { + while (it2 != ite2 && it2->getValue() == storm::utility::constantZero()) { ++it2; } if ((it1 == ite1) || (it2 == ite2)) { equalityResult = (it1 == ite1) ^ (it2 == ite2); break; } else { - if (it1->first != it2->first || it1->second != it2->second) { + if (it1->getColumn() != it2->getColumn() || it1->getValue() != it2->getValue()) { equalityResult = false; break; } @@ -389,12 +424,12 @@ namespace storm { // If there is at least one entry in this row, we can just set it to one, modify its column value to the // one given by the parameter and set all subsequent elements of this row to zero. - columnValuePtr->first = column; - columnValuePtr->second = storm::utility::constantOne(); + columnValuePtr->getColumn() = column; + columnValuePtr->getValue() = storm::utility::constantOne(); ++columnValuePtr; for (; columnValuePtr != columnValuePtrEnd; ++columnValuePtr) { - columnValuePtr->first = 0; - columnValuePtr->second = storm::utility::constantZero(); + columnValuePtr->getColumn() = 0; + columnValuePtr->getValue() = storm::utility::constantZero(); } } @@ -402,8 +437,8 @@ namespace storm { T SparseMatrix::getConstrainedRowSum(uint_fast64_t row, storm::storage::BitVector const& constraint) const { T result(0); for (const_iterator it = this->begin(row), ite = this->end(row); it != ite; ++it) { - if (constraint.get(it->first)) { - result += it->second; + if (constraint.get(it->getColumn())) { + result += it->getValue(); } } return result; @@ -457,10 +492,10 @@ namespace storm { bool foundDiagonalElement = false; for (const_iterator it = this->begin(i), ite = this->end(i); it != ite; ++it) { - if (columnConstraint.get(it->first)) { + if (columnConstraint.get(it->getColumn())) { ++subEntries; - if (index == it->first) { + if (index == it->getColumn()) { foundDiagonalElement = true; } } @@ -507,14 +542,14 @@ namespace storm { bool insertedDiagonalElement = false; for (const_iterator it = this->begin(i), ite = this->end(i); it != ite; ++it) { - if (columnConstraint.get(it->first)) { - if (index == it->first) { + if (columnConstraint.get(it->getColumn())) { + if (index == it->getColumn()) { insertedDiagonalElement = true; - } else if (insertDiagonalEntries && !insertedDiagonalElement && it->first > index) { + } else if (insertDiagonalEntries && !insertedDiagonalElement && it->getColumn() > index) { matrixBuilder.addNextValue(rowCount, bitsSetBeforeIndex[index], storm::utility::constantZero()); insertedDiagonalElement = true; } - matrixBuilder.addNextValue(rowCount, bitsSetBeforeIndex[it->first], it->second); + matrixBuilder.addNextValue(rowCount, bitsSetBeforeIndex[it->getColumn()], it->getValue()); } } if (insertDiagonalEntries && !insertedDiagonalElement) { @@ -540,7 +575,7 @@ namespace storm { // Iterate through that row and count the number of slots we have to reserve for copying. bool foundDiagonalElement = false; for (const_iterator it = this->begin(rowToCopy), ite = this->end(rowToCopy); it != ite; ++it) { - if (it->first == rowGroupIndex) { + if (it->getColumn() == rowGroupIndex) { foundDiagonalElement = true; } ++subEntries; @@ -562,13 +597,13 @@ namespace storm { // there is no entry yet. bool insertedDiagonalElement = false; for (const_iterator it = this->begin(rowToCopy), ite = this->end(rowToCopy); it != ite; ++it) { - if (it->first == rowGroupIndex) { + if (it->getColumn() == rowGroupIndex) { insertedDiagonalElement = true; - } else if (insertDiagonalEntries && !insertedDiagonalElement && it->first > rowGroupIndex) { + } else if (insertDiagonalEntries && !insertedDiagonalElement && it->getColumn() > rowGroupIndex) { matrixBuilder.addNextValue(rowGroupIndex, rowGroupIndex, storm::utility::constantZero()); insertedDiagonalElement = true; } - matrixBuilder.addNextValue(rowGroupIndex, it->first, it->second); + matrixBuilder.addNextValue(rowGroupIndex, it->getColumn(), it->getValue()); } if (insertDiagonalEntries && !insertedDiagonalElement) { matrixBuilder.addNextValue(rowGroupIndex, rowGroupIndex, storm::utility::constantZero()); @@ -586,13 +621,13 @@ namespace storm { uint_fast64_t entryCount = this->getEntryCount(); std::vector rowIndications(rowCount + 1); - std::vector> columnsAndValues(entryCount); + std::vector> columnsAndValues(entryCount); // First, we need to count how many entries each column has. for (uint_fast64_t group = 0; group < columnCount; ++group) { for (auto const& transition : joinGroups ? this->getRowGroup(group) : this->getRow(group)) { - if (transition.second != storm::utility::constantZero()) { - ++rowIndications[transition.first + 1]; + if (transition.getValue() != storm::utility::constantZero()) { + ++rowIndications[transition.getColumn() + 1]; } } } @@ -610,9 +645,9 @@ namespace storm { // Now we are ready to actually fill in the values of the transposed matrix. for (uint_fast64_t group = 0; group < columnCount; ++group) { for (auto const& transition : joinGroups ? this->getRowGroup(group) : this->getRow(group)) { - if (transition.second != storm::utility::constantZero()) { - columnsAndValues[nextIndices[transition.first]] = std::make_pair(group, transition.second); - nextIndices[transition.first]++; + if (transition.getValue() != storm::utility::constantZero()) { + columnsAndValues[nextIndices[transition.getColumn()]] = std::make_pair(group, transition.getValue()); + nextIndices[transition.getColumn()]++; } } } @@ -641,8 +676,8 @@ namespace storm { bool foundDiagonalElement = false; for (uint_fast64_t group = 0; group < this->getRowGroupCount(); ++group) { for (auto& entry : this->getRowGroup(group)) { - if (entry.first == group) { - entry.second = one - entry.second; + if (entry.getColumn() == group) { + entry.getValue() = one - entry.getValue(); foundDiagonalElement = true; } } @@ -659,8 +694,8 @@ namespace storm { // Iterate over all row groups and negate all the elements that are not on the diagonal. for (uint_fast64_t group = 0; group < this->getRowGroupCount(); ++group) { for (auto& entry : this->getRowGroup(group)) { - if (entry.first != group) { - entry.second = -entry.second; + if (entry.getColumn() != group) { + entry.getValue() = -entry.getValue(); } } } @@ -671,8 +706,8 @@ namespace storm { // Iterate over all rows and negate all the elements that are not on the diagonal. for (uint_fast64_t group = 0; group < this->getRowGroupCount(); ++group) { for (auto& entry : this->getRowGroup(group)) { - if (entry.first == group) { - entry.second = storm::utility::constantZero(); + if (entry.getColumn() == group) { + entry.getValue() = storm::utility::constantZero(); } } } @@ -695,9 +730,9 @@ namespace storm { // to invert the entry. T diagonalValue = storm::utility::constantZero(); for (const_iterator it = this->begin(rowNumber), ite = this->end(rowNumber); it != ite; ++it) { - if (it->first == rowNumber) { - diagonalValue += it->second; - } else if (it->first > rowNumber) { + if (it->getColumn() == rowNumber) { + diagonalValue += it->getValue(); + } else if (it->getColumn() > rowNumber) { break; } } @@ -716,13 +751,13 @@ namespace storm { // add the result to the corresponding position in the vector. for (uint_fast64_t row = 0; row < rowCount && row < otherMatrix.rowCount; ++row) { for (const_iterator it1 = this->begin(row), ite1 = this->end(row), it2 = otherMatrix.begin(row), ite2 = otherMatrix.end(row); it1 != ite1 && it2 != ite2; ++it1) { - if (it1->first < it2->first) { + if (it1->getColumn() < it2->getColumn()) { continue; } else { // If the precondition of this method (i.e. that the given matrix is a submatrix // of the current one) was fulfilled, we know now that the two elements are in // the same column, so we can multiply and add them to the row sum vector. - result[row] += it2->second * it1->second; + result[row] += it2->getValue() * it1->getValue(); ++it2; } } @@ -750,7 +785,7 @@ namespace storm { *resultIterator = storm::utility::constantZero(); for (ite = this->begin() + *(rowIterator + 1); it != ite; ++it) { - *resultIterator += it->second * vector[it->first]; + *resultIterator += it->getValue() * vector[it->getColumn()]; } } }); @@ -765,7 +800,7 @@ namespace storm { *resultIterator = storm::utility::constantZero(); for (ite = this->begin() + *(rowIterator + 1); it != ite; ++it) { - *resultIterator += it->second * vector[it->first]; + *resultIterator += it->getValue() * vector[it->getColumn()]; } } #endif @@ -776,7 +811,7 @@ namespace storm { uint_fast64_t size = sizeof(*this); // Add size of columns and values. - size += sizeof(std::pair) * columnsAndValues.capacity(); + size += sizeof(MatrixEntry) * columnsAndValues.capacity(); // Add row_indications size. size += sizeof(uint_fast64_t) * rowIndications.capacity(); @@ -848,7 +883,7 @@ namespace storm { T SparseMatrix::getRowSum(uint_fast64_t row) const { T sum = storm::utility::constantZero(); for (const_iterator it = this->begin(row), ite = this->end(row); it != ite; ++it) { - sum += it->second; + sum += it->getValue(); } return sum; } @@ -864,10 +899,10 @@ namespace storm { 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) { // Skip over all entries of the other matrix that are before the current entry in the current matrix. - while (it2 != ite2 && it2->first < it1->first) { + while (it2 != ite2 && it2->getColumn() < it1->getColumn()) { ++it2; } - if (it2 == ite2 || it1->first != it2->first) { + if (it2 == ite2 || it1->getColumn() != it2->getColumn()) { return false; } } @@ -894,8 +929,8 @@ namespace storm { out << i << "\t(\t"; uint_fast64_t currentRealIndex = 0; while (currentRealIndex < matrix.columnCount) { - if (nextIndex < matrix.rowIndications[i + 1] && currentRealIndex == matrix.columnsAndValues[nextIndex].first) { - out << matrix.columnsAndValues[nextIndex].second << "\t"; + if (nextIndex < matrix.rowIndications[i + 1] && currentRealIndex == matrix.columnsAndValues[nextIndex].getColumn()) { + out << matrix.columnsAndValues[nextIndex].getValue() << "\t"; ++nextIndex; } else { out << "0\t"; @@ -930,10 +965,12 @@ namespace storm { return result; } - // Explicitly instantiate the builder and the matrix. + // Explicitly instantiate the entry, builder and the matrix. + template class MatrixEntry; template class SparseMatrixBuilder; template class SparseMatrix; template std::ostream& operator<<(std::ostream& out, SparseMatrix const& matrix); + template class MatrixEntry; template class SparseMatrixBuilder; 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 b8b8b80d3..b60cbdc16 100644 --- a/src/storage/SparseMatrix.h +++ b/src/storage/SparseMatrix.h @@ -8,6 +8,7 @@ #include "src/storage/BitVector.h" #include "src/utility/constants.h" +#include "src/utility/OsDetection.h" #include "src/exceptions/InvalidArgumentException.h" #include "src/exceptions/OutOfRangeException.h" @@ -27,6 +28,83 @@ namespace storm { // Forward declare matrix class. template class SparseMatrix; + template + class MatrixEntry { + public: + /*! + * Constructs a matrix entry with the given column and value. + * + * @param column The column of the matrix entry. + * @param value The value of the matrix entry. + */ + MatrixEntry(uint_fast64_t column, T value); + + /*! + * Move-constructs the matrix entry fro the given column-value pair. + * + * @param pair The column-value pair from which to move-construct the matrix entry. + */ + MatrixEntry(std::pair&& pair); + + MatrixEntry() = default; + MatrixEntry(MatrixEntry const& other) = default; + MatrixEntry& operator=(MatrixEntry const& other) = default; +#ifndef WINDOWS + MatrixEntry(MatrixEntry&& other) = default; + MatrixEntry& operator=(MatrixEntry&& other) = default; +#endif + + /*! + * Retrieves the column of the matrix entry. + * + * @return The column of the matrix entry. + */ + uint_fast64_t const& getColumn() const; + + /*! + * Retrieves the column of the matrix entry. + * + * @return The column of the matrix entry. + */ + uint_fast64_t& getColumn(); + + /*! + * Retrieves the value of the matrix entry. + * + * @return The value of the matrix entry. + */ + T const& getValue() const; + + /*! + * Retrieves the value of the matrix entry. + * + * @return The value of the matrix entry. + */ + T& getValue(); + + /*! + * Retrieves a pair of column and value that characterizes this entry. + * + * @return A column-value pair that characterizes this entry. + */ + std::pair const& getColumnValuePair() const; + + private: + // The actual matrix entry. + std::pair entry; + }; + + /*! + * Computes the hash value of a matrix entry. + */ + template + std::size_t hash_value(MatrixEntry const& matrixEntry) { + std::size_t seed = 0; + boost::hash_combine(seed, matrixEntry.getColumn()); + boost::hash_combine(seed, matrixEntry.getValue()); + return seed; + } + /*! * A class that can be used to build a sparse matrix by adding value by value. */ @@ -128,7 +206,7 @@ namespace storm { bool storagePreallocated; // The storage for the columns and values of all entries in the matrix. - std::vector> columnsAndValues; + std::vector> columnsAndValues; // A vector containing the indices at which each given row begins. This index is to be interpreted as an // index in the valueStorage and the columnIndications vectors. Put differently, the values of the entries @@ -175,8 +253,8 @@ namespace storm { friend class storm::adapters::EigenAdapter; friend class storm::adapters::StormAdapter; - typedef typename std::vector>::iterator iterator; - typedef typename std::vector>::const_iterator const_iterator; + typedef typename std::vector>::iterator iterator; + typedef typename std::vector>::const_iterator const_iterator; /*! * This class represents a number of consecutive rows of the matrix. @@ -284,7 +362,7 @@ namespace storm { * @param columnsAndValues The vector containing the columns and values of the entries in the matrix. * @param rowGroupIndices The vector representing the row groups in the matrix. */ - SparseMatrix(uint_fast64_t columnCount, std::vector const& rowIndications, std::vector> const& columnsAndValues, std::vector const& rowGroupIndices); + SparseMatrix(uint_fast64_t columnCount, std::vector const& rowIndications, std::vector> const& columnsAndValues, std::vector const& rowGroupIndices); /*! * Constructs a sparse matrix by moving the given contents. @@ -294,7 +372,7 @@ namespace storm { * @param columnsAndValues The vector containing the columns and values of the entries in the matrix. * @param rowGroupIndices The vector representing the row groups in the matrix. */ - SparseMatrix(uint_fast64_t columnCount, std::vector&& rowIndications, std::vector>&& columnsAndValues, std::vector&& rowGroupIndices); + SparseMatrix(uint_fast64_t columnCount, std::vector&& rowIndications, std::vector>&& columnsAndValues, std::vector&& rowGroupIndices); /*! * Assigns the contents of the given matrix to the current one by deep-copying its contents. @@ -662,7 +740,7 @@ namespace storm { uint_fast64_t nonzeroEntryCount; // The storage for the columns and values of all entries in the matrix. - std::vector> columnsAndValues; + std::vector> columnsAndValues; // A vector containing the indices at which each given row begins. This index is to be interpreted as an // index in the valueStorage and the columnIndications vectors. Put differently, the values of the entries diff --git a/src/storage/StronglyConnectedComponentDecomposition.cpp b/src/storage/StronglyConnectedComponentDecomposition.cpp index 6e9f08386..b14559bcb 100644 --- a/src/storage/StronglyConnectedComponentDecomposition.cpp +++ b/src/storage/StronglyConnectedComponentDecomposition.cpp @@ -114,33 +114,33 @@ 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->first) { + if (dropNaiveSccs && currentState == successorIt->getColumn()) { 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->first)) { - if (!visitedStates.get(successorIt->first)) { + if (subsystem.get(successorIt->getColumn())) { + if (!visitedStates.get(successorIt->getColumn())) { // 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->first); - statesInStack[successorIt->first] = true; + recursionStateStack.push_back(successorIt->getColumn()); + statesInStack[successorIt->getColumn()] = true; // Also, put initial value for iterator on corresponding recursion stack. - recursionIteratorStack.push_back(model.getRows(successorIt->first).begin()); + recursionIteratorStack.push_back(model.getRows(successorIt->getColumn()).begin()); // Perform the actual recursion step in an iterative way. goto recursionStepForward; recursionStepBackward: - lowlinks[currentState] = std::min(lowlinks[currentState], lowlinks[successorIt->first]); - } else if (tarjanStackStates.get(successorIt->first)) { + lowlinks[currentState] = std::min(lowlinks[currentState], lowlinks[successorIt->getColumn()]); + } else if (tarjanStackStates.get(successorIt->getColumn())) { // Update the lowlink of the current state. - lowlinks[currentState] = std::min(lowlinks[currentState], stateIndices[successorIt->first]); + lowlinks[currentState] = std::min(lowlinks[currentState], stateIndices[successorIt->getColumn()]); } } } @@ -165,7 +165,7 @@ namespace storm { if (onlyBottomSccs) { for (auto const& state : scc) { for (auto const& successor : model.getRows(state)) { - if (scc.find(successor.first) == scc.end()) { + if (scc.find(successor.getColumn()) == scc.end()) { isBottomScc = false; break; } diff --git a/src/utility/counterexamples.h b/src/utility/counterexamples.h index 23b5b372e..8b233e402 100644 --- a/src/utility/counterexamples.h +++ b/src/utility/counterexamples.h @@ -36,8 +36,8 @@ namespace storm { // for (auto state : psiStates) { // analysisInformation[state] = boost::container::flat_set(); // for (auto const& predecessorEntry : backwardTransitions.getRow(state)) { -// if (predecessorEntry.first != state && !psiStates.get(predecessorEntry.first)) { -// worklist.push(std::make_pair(predecessorEntry.first, state)); +// if (predecessorEntry.getColumn() != state && !psiStates.get(predecessorEntry.getColumn())) { +// worklist.push(std::make_pair(predecessorEntry.getColumn(), state)); // } // } // } @@ -57,7 +57,7 @@ namespace storm { // bool choiceTargetsTargetState = false; // // for (auto& entry : transitionMatrix.getRow(currentChoice)) { -// if (entry.first == targetState) { +// if (entry.getColumn() == targetState) { // choiceTargetsTargetState = true; // break; // } @@ -79,8 +79,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.first)) { -// worklist.push(std::make_pair(predecessorEntry.first, currentState)); +// if (!psiStates.get(predecessorEntry.getColumn())) { +// worklist.push(std::make_pair(predecessorEntry.getColumn(), currentState)); // } // } // } @@ -96,9 +96,9 @@ namespace storm { for (auto state : psiStates) { analysisInformation[state] = boost::container::flat_set(); for (auto const& predecessorEntry : backwardTransitions.getRow(state)) { - if (predecessorEntry.first != state && !statesInWorkList.get(predecessorEntry.first) && !psiStates.get(predecessorEntry.first)) { - worklist.push(predecessorEntry.first); - statesInWorkList.set(predecessorEntry.first); + if (predecessorEntry.getColumn() != state && !statesInWorkList.get(predecessorEntry.getColumn()) && !psiStates.get(predecessorEntry.getColumn())) { + worklist.push(predecessorEntry.getColumn()); + statesInWorkList.set(predecessorEntry.getColumn()); markedStates.set(state); } } @@ -116,7 +116,7 @@ namespace storm { bool modifiedChoice = false; for (auto const& entry : transitionMatrix.getRow(currentChoice)) { - if (markedStates.get(entry.first)) { + if (markedStates.get(entry.getColumn())) { modifiedChoice = true; break; } @@ -127,9 +127,9 @@ namespace storm { // and the choice labels. if (modifiedChoice) { for (auto const& entry : transitionMatrix.getRow(currentChoice)) { - if (markedStates.get(entry.first)) { + if (markedStates.get(entry.getColumn())) { boost::container::flat_set tmpIntersection; - std::set_intersection(analysisInformation[currentState].begin(), analysisInformation[currentState].end(), analysisInformation[entry.first].begin(), analysisInformation[entry.first].end(), std::inserter(tmpIntersection, tmpIntersection.begin())); + std::set_intersection(analysisInformation[currentState].begin(), analysisInformation[currentState].end(), analysisInformation[entry.getColumn()].begin(), analysisInformation[entry.getColumn()].end(), std::inserter(tmpIntersection, tmpIntersection.begin())); std::set_intersection(analysisInformation[currentState].begin(), analysisInformation[currentState].end(), choiceLabeling[currentChoice].begin(), choiceLabeling[currentChoice].end(), std::inserter(tmpIntersection, tmpIntersection.begin())); analysisInformation[currentState] = std::move(tmpIntersection); } @@ -142,9 +142,9 @@ namespace storm { if (analysisInformation[currentState].size() != analysisInformationSizeBefore) { for (auto const& predecessorEntry : backwardTransitions.getRow(currentState)) { // Only put the predecessor in the worklist if it's not already a target state. - if (!psiStates.get(predecessorEntry.first) && !statesInWorkList.get(predecessorEntry.first)) { - worklist.push(predecessorEntry.first); - statesInWorkList.set(predecessorEntry.first); + if (!psiStates.get(predecessorEntry.getColumn()) && !statesInWorkList.get(predecessorEntry.getColumn())) { + worklist.push(predecessorEntry.getColumn()); + statesInWorkList.set(predecessorEntry.getColumn()); } } markedStates.set(currentState, true); diff --git a/src/utility/graph.h b/src/utility/graph.h index 01d0a7f4f..3d0d95fb1 100644 --- a/src/utility/graph.h +++ b/src/utility/graph.h @@ -79,16 +79,16 @@ namespace storm { } for (typename storm::storage::SparseMatrix::const_iterator entryIt = backwardTransitions.begin(currentState), entryIte = backwardTransitions.end(currentState); entryIt != entryIte; ++entryIt) { - if (phiStates[entryIt->first] && (!statesWithProbabilityGreater0.get(entryIt->first) || (useStepBound && remainingSteps[entryIt->first] < currentStepBound - 1))) { + if (phiStates[entryIt->getColumn()] && (!statesWithProbabilityGreater0.get(entryIt->getColumn()) || (useStepBound && remainingSteps[entryIt->getColumn()] < 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(entryIt->first, true); - stack.push_back(entryIt->first); + statesWithProbabilityGreater0.set(entryIt->getColumn(), true); + stack.push_back(entryIt->getColumn()); } 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[entryIt->first] = currentStepBound - 1; - statesWithProbabilityGreater0.set(entryIt->first, true); - stack.push_back(entryIt->first); + remainingSteps[entryIt->getColumn()] = currentStepBound - 1; + statesWithProbabilityGreater0.set(entryIt->getColumn(), true); + stack.push_back(entryIt->getColumn()); stepStack.push_back(currentStepBound - 1); } } @@ -211,16 +211,16 @@ namespace storm { } 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 (phiStates.get(entryIt->getColumn()) && (!statesWithProbabilityGreater0.get(entryIt->getColumn()) || (useStepBound && remainingSteps[entryIt->getColumn()] < 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(entryIt->first, true); - stack.push_back(entryIt->first); + statesWithProbabilityGreater0.set(entryIt->getColumn(), true); + stack.push_back(entryIt->getColumn()); } 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[entryIt->first] = currentStepBound - 1; - statesWithProbabilityGreater0.set(entryIt->first, true); - stack.push_back(entryIt->first); + remainingSteps[entryIt->getColumn()] = currentStepBound - 1; + statesWithProbabilityGreater0.set(entryIt->getColumn(), true); + stack.push_back(entryIt->getColumn()); stepStack.push_back(currentStepBound - 1); } } @@ -290,13 +290,13 @@ namespace storm { stack.pop_back(); for (typename storm::storage::SparseMatrix::const_iterator predecessorEntryIt = backwardTransitions.begin(currentState), predecessorEntryIte = backwardTransitions.end(currentState); predecessorEntryIt != predecessorEntryIte; ++predecessorEntryIt) { - if (phiStates.get(predecessorEntryIt->first) && !nextStates.get(predecessorEntryIt->first)) { + if (phiStates.get(predecessorEntryIt->getColumn()) && !nextStates.get(predecessorEntryIt->getColumn())) { // Check whether the predecessor has only successors in the current state set for one of the // nondeterminstic choices. - for (uint_fast64_t row = nondeterministicChoiceIndices[predecessorEntryIt->first]; row < nondeterministicChoiceIndices[predecessorEntryIt->first + 1]; ++row) { + for (uint_fast64_t row = nondeterministicChoiceIndices[predecessorEntryIt->getColumn()]; row < nondeterministicChoiceIndices[predecessorEntryIt->getColumn() + 1]; ++row) { bool allSuccessorsInCurrentStates = true; for (typename storm::storage::SparseMatrix::const_iterator successorEntryIt = transitionMatrix.begin(row), successorEntryIte = transitionMatrix.end(row); successorEntryIt != successorEntryIte; ++successorEntryIt) { - if (!currentStates.get(successorEntryIt->first)) { + if (!currentStates.get(successorEntryIt->getColumn())) { allSuccessorsInCurrentStates = false; break; } @@ -306,8 +306,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(predecessorEntryIt->first, true); - stack.push_back(predecessorEntryIt->first); + nextStates.set(predecessorEntryIt->getColumn(), true); + stack.push_back(predecessorEntryIt->getColumn()); break; } } @@ -401,14 +401,14 @@ namespace storm { } for(typename storm::storage::SparseMatrix::const_iterator predecessorEntryIt = backwardTransitions.begin(currentState), predecessorEntryIte = backwardTransitions.end(currentState); predecessorEntryIt != predecessorEntryIte; ++predecessorEntryIt) { - if (phiStates.get(predecessorEntryIt->first) && (!statesWithProbabilityGreater0.get(predecessorEntryIt->first) || (useStepBound && remainingSteps[predecessorEntryIt->first] < currentStepBound - 1))) { + if (phiStates.get(predecessorEntryIt->getColumn()) && (!statesWithProbabilityGreater0.get(predecessorEntryIt->getColumn()) || (useStepBound && remainingSteps[predecessorEntryIt->getColumn()] < currentStepBound - 1))) { // Check whether the predecessor has at least one successor in the current state set for every // nondeterministic choice. bool addToStatesWithProbabilityGreater0 = true; - for (uint_fast64_t row = nondeterministicChoiceIndices[predecessorEntryIt->first]; row < nondeterministicChoiceIndices[predecessorEntryIt->first + 1]; ++row) { + for (uint_fast64_t row = nondeterministicChoiceIndices[predecessorEntryIt->getColumn()]; row < nondeterministicChoiceIndices[predecessorEntryIt->getColumn() + 1]; ++row) { bool hasAtLeastOneSuccessorWithProbabilityGreater0 = false; for (typename storm::storage::SparseMatrix::const_iterator successorEntryIt = transitionMatrix.begin(row), successorEntryIte = transitionMatrix.end(row); successorEntryIt != successorEntryIte; ++successorEntryIt) { - if (statesWithProbabilityGreater0.get(successorEntryIt->first)) { + if (statesWithProbabilityGreater0.get(successorEntryIt->getColumn())) { hasAtLeastOneSuccessorWithProbabilityGreater0 = true; break; } @@ -424,13 +424,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(predecessorEntryIt->first, true); - stack.push_back(predecessorEntryIt->first); + statesWithProbabilityGreater0.set(predecessorEntryIt->getColumn(), true); + stack.push_back(predecessorEntryIt->getColumn()); } 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[predecessorEntryIt->first] = currentStepBound - 1; - statesWithProbabilityGreater0.set(predecessorEntryIt->first, true); - stack.push_back(predecessorEntryIt->first); + remainingSteps[predecessorEntryIt->getColumn()] = currentStepBound - 1; + statesWithProbabilityGreater0.set(predecessorEntryIt->getColumn(), true); + stack.push_back(predecessorEntryIt->getColumn()); stepStack.push_back(currentStepBound - 1); } } @@ -501,12 +501,12 @@ namespace storm { stack.pop_back(); for(typename storm::storage::SparseMatrix::const_iterator predecessorEntryIt = backwardTransitions.begin(currentState), predecessorEntryIte = backwardTransitions.end(currentState); predecessorEntryIt != predecessorEntryIte; ++predecessorEntryIt) { - if (phiStates.get(predecessorEntryIt->first) && !nextStates.get(predecessorEntryIt->first)) { + if (phiStates.get(predecessorEntryIt->getColumn()) && !nextStates.get(predecessorEntryIt->getColumn())) { // Check whether the predecessor has only successors in the current state set for all of the // nondeterminstic choices. bool allSuccessorsInCurrentStatesForAllChoices = true; - for (typename storm::storage::SparseMatrix::const_iterator successorEntryIt = transitionMatrix.begin(nondeterministicChoiceIndices[predecessorEntryIt->first]), successorEntryIte = transitionMatrix.begin(nondeterministicChoiceIndices[predecessorEntryIt->first + 1]); successorEntryIt != successorEntryIte; ++successorEntryIt) { - if (!currentStates.get(successorEntryIt->first)) { + for (typename storm::storage::SparseMatrix::const_iterator successorEntryIt = transitionMatrix.begin(nondeterministicChoiceIndices[predecessorEntryIt->getColumn()]), successorEntryIte = transitionMatrix.begin(nondeterministicChoiceIndices[predecessorEntryIt->getColumn() + 1]); successorEntryIt != successorEntryIte; ++successorEntryIt) { + if (!currentStates.get(successorEntryIt->getColumn())) { allSuccessorsInCurrentStatesForAllChoices = false; goto afterCheckLoop; } @@ -517,8 +517,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(predecessorEntryIt->first, true); - stack.push_back(predecessorEntryIt->first); + nextStates.set(predecessorEntryIt->getColumn(), true); + stack.push_back(predecessorEntryIt->getColumn()); } } } diff --git a/src/utility/matrix.h b/src/utility/matrix.h index 446fb413f..1027e7e42 100644 --- a/src/utility/matrix.h +++ b/src/utility/matrix.h @@ -32,7 +32,7 @@ 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 const& entry : selectedRow) { - matrixBuilder.addNextValue(state, entry.first, entry.second); + matrixBuilder.addNextValue(state, entry.getColumn(), entry.getValue()); } } else { // If no valid choice for the state is defined, we insert a self-loop. diff --git a/test/functional/parser/DeterministicSparseTransitionParserTest.cpp b/test/functional/parser/DeterministicSparseTransitionParserTest.cpp index 2b301a1e7..89c5c9c6e 100644 --- a/test/functional/parser/DeterministicSparseTransitionParserTest.cpp +++ b/test/functional/parser/DeterministicSparseTransitionParserTest.cpp @@ -35,68 +35,68 @@ TEST(DeterministicSparseTransitionParserTest, BasicTransitionsParsing) { // Test every entry of the matrix. storm::storage::SparseMatrix::const_iterator cIter = transitionMatrix.begin(0); - ASSERT_EQ(0, cIter->first); - ASSERT_EQ(0, cIter->second); + ASSERT_EQ(0, cIter->getColumn()); + ASSERT_EQ(0, cIter->getValue()); cIter++; - ASSERT_EQ(1, cIter->first); - ASSERT_EQ(1, cIter->second); + ASSERT_EQ(1, cIter->getColumn()); + ASSERT_EQ(1, cIter->getValue()); cIter++; - ASSERT_EQ(1, cIter->first); - ASSERT_EQ(0, cIter->second); + ASSERT_EQ(1, cIter->getColumn()); + ASSERT_EQ(0, cIter->getValue()); cIter++; - ASSERT_EQ(2, cIter->first); - ASSERT_EQ(0.5, cIter->second); + ASSERT_EQ(2, cIter->getColumn()); + ASSERT_EQ(0.5, cIter->getValue()); cIter++; - ASSERT_EQ(3, cIter->first); - ASSERT_EQ(0.5, cIter->second); + ASSERT_EQ(3, cIter->getColumn()); + ASSERT_EQ(0.5, cIter->getValue()); cIter++; - ASSERT_EQ(2, cIter->first); - ASSERT_EQ(0, cIter->second); + ASSERT_EQ(2, cIter->getColumn()); + ASSERT_EQ(0, cIter->getValue()); cIter++; - ASSERT_EQ(3, cIter->first); - ASSERT_EQ(0.4, cIter->second); + ASSERT_EQ(3, cIter->getColumn()); + ASSERT_EQ(0.4, cIter->getValue()); cIter++; - ASSERT_EQ(4, cIter->first); - ASSERT_EQ(0.4, cIter->second); + ASSERT_EQ(4, cIter->getColumn()); + ASSERT_EQ(0.4, cIter->getValue()); cIter++; - ASSERT_EQ(5, cIter->first); - ASSERT_EQ(0.2, cIter->second); + ASSERT_EQ(5, cIter->getColumn()); + ASSERT_EQ(0.2, cIter->getValue()); cIter++; - ASSERT_EQ(3, cIter->first); - ASSERT_EQ(1, cIter->second); + ASSERT_EQ(3, cIter->getColumn()); + ASSERT_EQ(1, cIter->getValue()); cIter++; - ASSERT_EQ(3, cIter->first); - ASSERT_EQ(1, cIter->second); + ASSERT_EQ(3, cIter->getColumn()); + ASSERT_EQ(1, cIter->getValue()); cIter++; - ASSERT_EQ(4, cIter->first); - ASSERT_EQ(0, cIter->second); + ASSERT_EQ(4, cIter->getColumn()); + ASSERT_EQ(0, cIter->getValue()); cIter++; - ASSERT_EQ(3, cIter->first); - ASSERT_EQ(0.1, cIter->second); + ASSERT_EQ(3, cIter->getColumn()); + ASSERT_EQ(0.1, cIter->getValue()); cIter++; - ASSERT_EQ(4, cIter->first); - ASSERT_EQ(0.1, cIter->second); + ASSERT_EQ(4, cIter->getColumn()); + ASSERT_EQ(0.1, cIter->getValue()); cIter++; - ASSERT_EQ(5, cIter->first); - ASSERT_EQ(0.1, cIter->second); + ASSERT_EQ(5, cIter->getColumn()); + ASSERT_EQ(0.1, cIter->getValue()); cIter++; - ASSERT_EQ(6, cIter->first); - ASSERT_EQ(0.7, cIter->second); + ASSERT_EQ(6, cIter->getColumn()); + ASSERT_EQ(0.7, cIter->getValue()); cIter++; - ASSERT_EQ(0, cIter->first); - ASSERT_EQ(0.9, cIter->second); + ASSERT_EQ(0, cIter->getColumn()); + ASSERT_EQ(0.9, cIter->getValue()); cIter++; - ASSERT_EQ(5, cIter->first); - ASSERT_EQ(0, cIter->second); + ASSERT_EQ(5, cIter->getColumn()); + ASSERT_EQ(0, cIter->getValue()); cIter++; - ASSERT_EQ(6, cIter->first); - ASSERT_EQ(0.1, cIter->second); + ASSERT_EQ(6, cIter->getColumn()); + ASSERT_EQ(0.1, cIter->getValue()); cIter++; - ASSERT_EQ(6, cIter->first); - ASSERT_EQ(0.224653, cIter->second); + ASSERT_EQ(6, cIter->getColumn()); + ASSERT_EQ(0.224653, cIter->getValue()); cIter++; - ASSERT_EQ(7, cIter->first); - ASSERT_EQ(0.775347, cIter->second); + ASSERT_EQ(7, cIter->getColumn()); + ASSERT_EQ(0.775347, cIter->getValue()); } TEST(DeterministicSparseTransitionParserTest, BasicTransitionsRewardsParsing) { @@ -112,56 +112,56 @@ TEST(DeterministicSparseTransitionParserTest, BasicTransitionsRewardsParsing) { // Test every entry of the matrix. storm::storage::SparseMatrix::const_iterator cIter = rewardMatrix.begin(0); - ASSERT_EQ(1, cIter->first); - ASSERT_EQ(10, cIter->second); + ASSERT_EQ(1, cIter->getColumn()); + ASSERT_EQ(10, cIter->getValue()); cIter++; - ASSERT_EQ(2, cIter->first); - ASSERT_EQ(5, cIter->second); + ASSERT_EQ(2, cIter->getColumn()); + ASSERT_EQ(5, cIter->getValue()); cIter++; - ASSERT_EQ(3, cIter->first); - ASSERT_EQ(5.5, cIter->second); + ASSERT_EQ(3, cIter->getColumn()); + ASSERT_EQ(5.5, cIter->getValue()); cIter++; - ASSERT_EQ(3, cIter->first); - ASSERT_EQ(21.4, cIter->second); + ASSERT_EQ(3, cIter->getColumn()); + ASSERT_EQ(21.4, cIter->getValue()); cIter++; - ASSERT_EQ(4, cIter->first); - ASSERT_EQ(4, cIter->second); + ASSERT_EQ(4, cIter->getColumn()); + ASSERT_EQ(4, cIter->getValue()); cIter++; - ASSERT_EQ(5, cIter->first); - ASSERT_EQ(2, cIter->second); + ASSERT_EQ(5, cIter->getColumn()); + ASSERT_EQ(2, cIter->getValue()); cIter++; - ASSERT_EQ(3, cIter->first); - ASSERT_EQ(1, cIter->second); + ASSERT_EQ(3, cIter->getColumn()); + ASSERT_EQ(1, cIter->getValue()); cIter++; - ASSERT_EQ(3, cIter->first); - ASSERT_EQ(1, cIter->second); + ASSERT_EQ(3, cIter->getColumn()); + ASSERT_EQ(1, cIter->getValue()); cIter++; - ASSERT_EQ(3, cIter->first); - ASSERT_EQ(0.1, cIter->second); + ASSERT_EQ(3, cIter->getColumn()); + ASSERT_EQ(0.1, cIter->getValue()); cIter++; - ASSERT_EQ(4, cIter->first); - ASSERT_EQ(1.1, cIter->second); + ASSERT_EQ(4, cIter->getColumn()); + ASSERT_EQ(1.1, cIter->getValue()); cIter++; - ASSERT_EQ(5, cIter->first); - ASSERT_EQ(9.5, cIter->second); + ASSERT_EQ(5, cIter->getColumn()); + ASSERT_EQ(9.5, cIter->getValue()); cIter++; - ASSERT_EQ(6, cIter->first); - ASSERT_EQ(6.7, cIter->second); + ASSERT_EQ(6, cIter->getColumn()); + ASSERT_EQ(6.7, cIter->getValue()); cIter++; - ASSERT_EQ(0, cIter->first); - ASSERT_EQ(1, cIter->second); + ASSERT_EQ(0, cIter->getColumn()); + ASSERT_EQ(1, cIter->getValue()); cIter++; - ASSERT_EQ(5, cIter->first); - ASSERT_EQ(0, cIter->second); + ASSERT_EQ(5, cIter->getColumn()); + ASSERT_EQ(0, cIter->getValue()); cIter++; - ASSERT_EQ(6, cIter->first); - ASSERT_EQ(12, cIter->second); + ASSERT_EQ(6, cIter->getColumn()); + ASSERT_EQ(12, cIter->getValue()); cIter++; - ASSERT_EQ(6, cIter->first); - ASSERT_EQ(35.224653, cIter->second); + ASSERT_EQ(6, cIter->getColumn()); + ASSERT_EQ(35.224653, cIter->getValue()); cIter++; - ASSERT_EQ(7, cIter->first); - ASSERT_EQ(9.875347, cIter->second); + ASSERT_EQ(7, cIter->getColumn()); + ASSERT_EQ(9.875347, cIter->getValue()); } @@ -201,17 +201,17 @@ TEST(DeterministicSparseTransitionParserTest, FixDeadlocks) { ASSERT_EQ(23, transitionMatrix.getEntryCount()); storm::storage::SparseMatrix::const_iterator cIter = transitionMatrix.begin(7); - ASSERT_EQ(7, cIter->first); - ASSERT_EQ(1, cIter->second); + ASSERT_EQ(7, cIter->getColumn()); + ASSERT_EQ(1, cIter->getValue()); cIter++; - ASSERT_EQ(6, cIter->first); - ASSERT_EQ(0.224653, cIter->second); + ASSERT_EQ(6, cIter->getColumn()); + ASSERT_EQ(0.224653, cIter->getValue()); cIter++; - ASSERT_EQ(7, cIter->first); - ASSERT_EQ(0.775347, cIter->second); + ASSERT_EQ(7, cIter->getColumn()); + ASSERT_EQ(0.775347, cIter->getValue()); cIter++; - ASSERT_EQ(8, cIter->first); - ASSERT_EQ(0, cIter->second); + ASSERT_EQ(8, cIter->getColumn()); + ASSERT_EQ(0, cIter->getValue()); } TEST(DeterministicSparseTransitionParserTest, DontFixDeadlocks) { diff --git a/test/functional/parser/MarkovAutomatonSparseTransitionParserTest.cpp b/test/functional/parser/MarkovAutomatonSparseTransitionParserTest.cpp index 81c2ccfb8..38b152cd4 100644 --- a/test/functional/parser/MarkovAutomatonSparseTransitionParserTest.cpp +++ b/test/functional/parser/MarkovAutomatonSparseTransitionParserTest.cpp @@ -79,29 +79,29 @@ TEST(MarkovAutomatonSparseTransitionParserTest, BasicParsing) { // Finally, test the transition matrix itself. storm::storage::SparseMatrix::const_iterator cIter = transitionMatrix.begin(0); - ASSERT_EQ(2, cIter->second); + ASSERT_EQ(2, cIter->getValue()); cIter++; - ASSERT_EQ(1, cIter->second); + ASSERT_EQ(1, cIter->getValue()); cIter++; - ASSERT_EQ(1, cIter->second); + ASSERT_EQ(1, cIter->getValue()); cIter++; - ASSERT_EQ(2, cIter->second); + ASSERT_EQ(2, cIter->getValue()); cIter++; - ASSERT_EQ(4, cIter->second); + ASSERT_EQ(4, cIter->getValue()); cIter++; - ASSERT_EQ(8, cIter->second); + ASSERT_EQ(8, cIter->getValue()); cIter++; - ASSERT_EQ(0.5, cIter->second); + ASSERT_EQ(0.5, cIter->getValue()); cIter++; - ASSERT_EQ(0.5, cIter->second); + ASSERT_EQ(0.5, cIter->getValue()); cIter++; - ASSERT_EQ(1, cIter->second); + ASSERT_EQ(1, cIter->getValue()); cIter++; - ASSERT_EQ(0.5, cIter->second); + ASSERT_EQ(0.5, cIter->getValue()); cIter++; - ASSERT_EQ(0.5, cIter->second); + ASSERT_EQ(0.5, cIter->getValue()); cIter++; - ASSERT_EQ(1, cIter->second); + ASSERT_EQ(1, cIter->getValue()); cIter++; ASSERT_EQ(transitionMatrix.end(), cIter); } @@ -157,29 +157,29 @@ TEST(MarkovAutomatonSparseTransitionParserTest, Whitespaces) { // Finally, test the transition matrix itself. storm::storage::SparseMatrix::const_iterator cIter = transitionMatrix.begin(0); - ASSERT_EQ(2, cIter->second); + ASSERT_EQ(2, cIter->getValue()); cIter++; - ASSERT_EQ(1, cIter->second); + ASSERT_EQ(1, cIter->getValue()); cIter++; - ASSERT_EQ(1, cIter->second); + ASSERT_EQ(1, cIter->getValue()); cIter++; - ASSERT_EQ(2, cIter->second); + ASSERT_EQ(2, cIter->getValue()); cIter++; - ASSERT_EQ(4, cIter->second); + ASSERT_EQ(4, cIter->getValue()); cIter++; - ASSERT_EQ(8, cIter->second); + ASSERT_EQ(8, cIter->getValue()); cIter++; - ASSERT_EQ(0.5, cIter->second); + ASSERT_EQ(0.5, cIter->getValue()); cIter++; - ASSERT_EQ(0.5, cIter->second); + ASSERT_EQ(0.5, cIter->getValue()); cIter++; - ASSERT_EQ(1, cIter->second); + ASSERT_EQ(1, cIter->getValue()); cIter++; - ASSERT_EQ(0.5, cIter->second); + ASSERT_EQ(0.5, cIter->getValue()); cIter++; - ASSERT_EQ(0.5, cIter->second); + ASSERT_EQ(0.5, cIter->getValue()); cIter++; - ASSERT_EQ(1, cIter->second); + ASSERT_EQ(1, cIter->getValue()); cIter++; ASSERT_EQ(transitionMatrix.end(), cIter); } diff --git a/test/functional/parser/NondeterministicSparseTransitionParserTest.cpp b/test/functional/parser/NondeterministicSparseTransitionParserTest.cpp index 21240a9dd..9494c983f 100644 --- a/test/functional/parser/NondeterministicSparseTransitionParserTest.cpp +++ b/test/functional/parser/NondeterministicSparseTransitionParserTest.cpp @@ -48,71 +48,71 @@ TEST(NondeterministicSparseTransitionParserTest, BasicTransitionsParsing) { // Test every entry of the matrix. storm::storage::SparseMatrix::const_iterator cIter = result.begin(0); - ASSERT_EQ(0, cIter->first); - ASSERT_EQ(0.9, cIter->second); + ASSERT_EQ(0, cIter->getColumn()); + ASSERT_EQ(0.9, cIter->getValue()); cIter++; - ASSERT_EQ(1, cIter->first); - ASSERT_EQ(0.1, cIter->second); + ASSERT_EQ(1, cIter->getColumn()); + ASSERT_EQ(0.1, cIter->getValue()); cIter++; - ASSERT_EQ(1, cIter->first); - ASSERT_EQ(0.2, cIter->second); + ASSERT_EQ(1, cIter->getColumn()); + ASSERT_EQ(0.2, cIter->getValue()); cIter++; - ASSERT_EQ(2, cIter->first); - ASSERT_EQ(0.2, cIter->second); + ASSERT_EQ(2, cIter->getColumn()); + ASSERT_EQ(0.2, cIter->getValue()); cIter++; - ASSERT_EQ(3, cIter->first); - ASSERT_EQ(0.2, cIter->second); + ASSERT_EQ(3, cIter->getColumn()); + ASSERT_EQ(0.2, cIter->getValue()); cIter++; - ASSERT_EQ(4, cIter->first); - ASSERT_EQ(0.2, cIter->second); + ASSERT_EQ(4, cIter->getColumn()); + ASSERT_EQ(0.2, cIter->getValue()); cIter++; - ASSERT_EQ(5, cIter->first); - ASSERT_EQ(0.2, cIter->second); + ASSERT_EQ(5, cIter->getColumn()); + ASSERT_EQ(0.2, cIter->getValue()); cIter++; - ASSERT_EQ(5, cIter->first); - ASSERT_EQ(1, cIter->second); + ASSERT_EQ(5, cIter->getColumn()); + ASSERT_EQ(1, cIter->getValue()); cIter++; - ASSERT_EQ(0, cIter->first); - ASSERT_EQ(0.1, cIter->second); + ASSERT_EQ(0, cIter->getColumn()); + ASSERT_EQ(0.1, cIter->getValue()); cIter++; - ASSERT_EQ(4, cIter->first); - ASSERT_EQ(0.9, cIter->second); + ASSERT_EQ(4, cIter->getColumn()); + ASSERT_EQ(0.9, cIter->getValue()); cIter++; - ASSERT_EQ(2, cIter->first); - ASSERT_EQ(1, cIter->second); + ASSERT_EQ(2, cIter->getColumn()); + ASSERT_EQ(1, cIter->getValue()); cIter++; - ASSERT_EQ(2, cIter->first); - ASSERT_EQ(0.5, cIter->second); + ASSERT_EQ(2, cIter->getColumn()); + ASSERT_EQ(0.5, cIter->getValue()); cIter++; - ASSERT_EQ(3, cIter->first); - ASSERT_EQ(0.5, cIter->second); + ASSERT_EQ(3, cIter->getColumn()); + ASSERT_EQ(0.5, cIter->getValue()); cIter++; - ASSERT_EQ(2, cIter->first); - ASSERT_EQ(1, cIter->second); + ASSERT_EQ(2, cIter->getColumn()); + ASSERT_EQ(1, cIter->getValue()); cIter++; - ASSERT_EQ(2, cIter->first); - ASSERT_EQ(0.001, cIter->second); + ASSERT_EQ(2, cIter->getColumn()); + ASSERT_EQ(0.001, cIter->getValue()); cIter++; - ASSERT_EQ(3, cIter->first); - ASSERT_EQ(0.999, cIter->second); + ASSERT_EQ(3, cIter->getColumn()); + ASSERT_EQ(0.999, cIter->getValue()); cIter++; - ASSERT_EQ(1, cIter->first); - ASSERT_EQ(0.7, cIter->second); + ASSERT_EQ(1, cIter->getColumn()); + ASSERT_EQ(0.7, cIter->getValue()); cIter++; - ASSERT_EQ(4, cIter->first); - ASSERT_EQ(0.3, cIter->second); + ASSERT_EQ(4, cIter->getColumn()); + ASSERT_EQ(0.3, cIter->getValue()); cIter++; - ASSERT_EQ(1, cIter->first); - ASSERT_EQ(0.2, cIter->second); + ASSERT_EQ(1, cIter->getColumn()); + ASSERT_EQ(0.2, cIter->getValue()); cIter++; - ASSERT_EQ(4, cIter->first); - ASSERT_EQ(0.2, cIter->second); + ASSERT_EQ(4, cIter->getColumn()); + ASSERT_EQ(0.2, cIter->getValue()); cIter++; - ASSERT_EQ(5, cIter->first); - ASSERT_EQ(0.6, cIter->second); + ASSERT_EQ(5, cIter->getColumn()); + ASSERT_EQ(0.6, cIter->getValue()); cIter++; - ASSERT_EQ(5, cIter->first); - ASSERT_EQ(1, cIter->second); + ASSERT_EQ(5, cIter->getColumn()); + ASSERT_EQ(1, cIter->getValue()); } TEST(NondeterministicSparseTransitionParserTest, BasicTransitionsRewardsParsing) { @@ -128,56 +128,56 @@ TEST(NondeterministicSparseTransitionParserTest, BasicTransitionsRewardsParsing) // Test every entry of the matrix. storm::storage::SparseMatrix::const_iterator cIter = result.begin(0); - ASSERT_EQ(0, cIter->first); - ASSERT_EQ(1, cIter->second); + ASSERT_EQ(0, cIter->getColumn()); + ASSERT_EQ(1, cIter->getValue()); cIter++; - ASSERT_EQ(1, cIter->first); - ASSERT_EQ(30, cIter->second); + ASSERT_EQ(1, cIter->getColumn()); + ASSERT_EQ(30, cIter->getValue()); cIter++; - ASSERT_EQ(1, cIter->first); - ASSERT_EQ(15.2, cIter->second); + ASSERT_EQ(1, cIter->getColumn()); + ASSERT_EQ(15.2, cIter->getValue()); cIter++; - ASSERT_EQ(2, cIter->first); - ASSERT_EQ(75, cIter->second); + ASSERT_EQ(2, cIter->getColumn()); + ASSERT_EQ(75, cIter->getValue()); cIter++; - ASSERT_EQ(5, cIter->first); - ASSERT_EQ(2.45, cIter->second); + ASSERT_EQ(5, cIter->getColumn()); + ASSERT_EQ(2.45, cIter->getValue()); cIter++; - ASSERT_EQ(5, cIter->first); - ASSERT_EQ(1, cIter->second); + ASSERT_EQ(5, cIter->getColumn()); + ASSERT_EQ(1, cIter->getValue()); cIter++; - ASSERT_EQ(0, cIter->first); - ASSERT_EQ(0.114, cIter->second); + ASSERT_EQ(0, cIter->getColumn()); + ASSERT_EQ(0.114, cIter->getValue()); cIter++; - ASSERT_EQ(4, cIter->first); - ASSERT_EQ(90, cIter->second); + ASSERT_EQ(4, cIter->getColumn()); + ASSERT_EQ(90, cIter->getValue()); cIter++; - ASSERT_EQ(2, cIter->first); - ASSERT_EQ(1, cIter->second); + ASSERT_EQ(2, cIter->getColumn()); + ASSERT_EQ(1, cIter->getValue()); cIter++; - ASSERT_EQ(2, cIter->first); - ASSERT_EQ(55, cIter->second); + ASSERT_EQ(2, cIter->getColumn()); + ASSERT_EQ(55, cIter->getValue()); cIter++; - ASSERT_EQ(3, cIter->first); - ASSERT_EQ(87, cIter->second); + ASSERT_EQ(3, cIter->getColumn()); + ASSERT_EQ(87, cIter->getValue()); cIter++; - ASSERT_EQ(2, cIter->first); - ASSERT_EQ(13, cIter->second); + ASSERT_EQ(2, cIter->getColumn()); + ASSERT_EQ(13, cIter->getValue()); cIter++; - ASSERT_EQ(3, cIter->first); - ASSERT_EQ(999, cIter->second); + ASSERT_EQ(3, cIter->getColumn()); + ASSERT_EQ(999, cIter->getValue()); cIter++; - ASSERT_EQ(1, cIter->first); - ASSERT_EQ(0.7, cIter->second); + ASSERT_EQ(1, cIter->getColumn()); + ASSERT_EQ(0.7, cIter->getValue()); cIter++; - ASSERT_EQ(4, cIter->first); - ASSERT_EQ(0.3, cIter->second); + ASSERT_EQ(4, cIter->getColumn()); + ASSERT_EQ(0.3, cIter->getValue()); cIter++; - ASSERT_EQ(1, cIter->first); - ASSERT_EQ(0.1, cIter->second); + ASSERT_EQ(1, cIter->getColumn()); + ASSERT_EQ(0.1, cIter->getValue()); cIter++; - ASSERT_EQ(5, cIter->first); - ASSERT_EQ(6, cIter->second); + ASSERT_EQ(5, cIter->getColumn()); + ASSERT_EQ(6, cIter->getValue()); } TEST(NondeterministicSparseTransitionParserTest, Whitespaces) { @@ -224,26 +224,26 @@ TEST(NondeterministicSparseTransitionParserTest, FixDeadlocks) { storm::storage::SparseMatrix::const_iterator cIter = result.begin(8); - ASSERT_EQ(1, cIter->first); - ASSERT_EQ(0.7, cIter->second); + ASSERT_EQ(1, cIter->getColumn()); + ASSERT_EQ(0.7, cIter->getValue()); cIter++; - ASSERT_EQ(4, cIter->first); - ASSERT_EQ(0.3, cIter->second); + ASSERT_EQ(4, cIter->getColumn()); + ASSERT_EQ(0.3, cIter->getValue()); cIter++; - ASSERT_EQ(5, cIter->first); - ASSERT_EQ(1, cIter->second); + ASSERT_EQ(5, cIter->getColumn()); + ASSERT_EQ(1, cIter->getValue()); cIter++; - ASSERT_EQ(1, cIter->first); - ASSERT_EQ(0.2, cIter->second); + ASSERT_EQ(1, cIter->getColumn()); + ASSERT_EQ(0.2, cIter->getValue()); cIter++; - ASSERT_EQ(4, cIter->first); - ASSERT_EQ(0.2, cIter->second); + ASSERT_EQ(4, cIter->getColumn()); + ASSERT_EQ(0.2, cIter->getValue()); cIter++; - ASSERT_EQ(5, cIter->first); - ASSERT_EQ(0.6, cIter->second); + ASSERT_EQ(5, cIter->getColumn()); + ASSERT_EQ(0.6, cIter->getValue()); cIter++; - ASSERT_EQ(5, cIter->first); - ASSERT_EQ(1, cIter->second); + ASSERT_EQ(5, cIter->getColumn()); + ASSERT_EQ(1, cIter->getValue()); } diff --git a/test/functional/storage/SparseMatrixTest.cpp b/test/functional/storage/SparseMatrixTest.cpp index 69517a6d4..de89f4950 100644 --- a/test/functional/storage/SparseMatrixTest.cpp +++ b/test/functional/storage/SparseMatrixTest.cpp @@ -147,7 +147,7 @@ TEST(SparseMatrix, Build) { } TEST(SparseMatrix, CreationWithMovingContents) { - std::vector> columnsAndValues; + std::vector> columnsAndValues; columnsAndValues.emplace_back(1, 1.0); columnsAndValues.emplace_back(2, 1.2); columnsAndValues.emplace_back(0, 0.5); @@ -540,24 +540,24 @@ TEST(SparseMatrix, Iteration) { ASSERT_NO_THROW(matrix = matrixBuilder.build()); for (auto const& entry : matrix.getRow(4)) { - 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); + if (entry.getColumn() == 0) { + ASSERT_EQ(0.1, entry.getValue()); + } else if (entry.getColumn() == 1) { + ASSERT_EQ(0.2, entry.getValue()); + } else if (entry.getColumn() == 3) { + ASSERT_EQ(0.3, entry.getValue()); } else { ASSERT_TRUE(false); } } for (storm::storage::SparseMatrix::iterator it = matrix.begin(4), ite = matrix.end(4); it != ite; ++it) { - 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); + if (it->getColumn() == 0) { + ASSERT_EQ(0.1, it->getValue()); + } else if (it->getColumn() == 1) { + ASSERT_EQ(0.2, it->getValue()); + } else if (it->getColumn() == 3) { + ASSERT_EQ(0.3, it->getValue()); } else { ASSERT_TRUE(false); } diff --git a/test/performance/storage/SparseMatrixTest.cpp b/test/performance/storage/SparseMatrixTest.cpp index 367bd3401..b59d283af 100644 --- a/test/performance/storage/SparseMatrixTest.cpp +++ b/test/performance/storage/SparseMatrixTest.cpp @@ -15,7 +15,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.first > matrix.getColumnCount()) { + if (entry.getColumn() > matrix.getColumnCount()) { ASSERT_TRUE(false); } }