From a26f63be30793a230d0ed515d14871fa18d09d7f Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 6 Dec 2013 18:58:35 +0100 Subject: [PATCH] Finished reworking the sparse matrix implementation. Adapted all other classes to the (partially) new API of the matrix. Former-commit-id: 2c3b5a5bc31a0227be839612b5e8105bc449d52d --- src/adapters/EigenAdapter.h | 66 --- src/adapters/ExplicitModelAdapter.h | 31 +- src/adapters/GmmxxAdapter.h | 10 +- src/adapters/StormAdapter.h | 25 +- .../MILPMinimalLabelSetGenerator.h | 75 ++-- .../PathBasedSubsystemGenerator.h | 12 +- .../SMTMinimalCommandSetGenerator.h | 94 ++--- .../SparseMarkovAutomatonCslModelChecker.h | 11 +- .../prctl/SparseDtmcPrctlModelChecker.h | 7 +- .../prctl/SparseMdpPrctlModelChecker.h | 2 +- src/models/AbstractDeterministicModel.h | 19 +- src/models/AbstractModel.h | 24 +- src/models/AbstractNondeterministicModel.h | 37 +- src/models/Dtmc.h | 48 +-- src/models/MarkovAutomaton.h | 42 +- src/models/Mdp.h | 10 +- .../DeterministicSparseTransitionParser.cpp | 7 +- .../MarkovAutomatonSparseTransitionParser.h | 3 +- ...NondeterministicSparseTransitionParser.cpp | 8 +- ...ractNondeterministicLinearEquationSolver.h | 11 +- .../MaximalEndComponentDecomposition.cpp | 14 +- src/storage/SparseMatrix.cpp | 332 ++++++++------- src/storage/SparseMatrix.h | 20 +- ...tronglyConnectedComponentDecomposition.cpp | 4 +- src/utility/counterexamples.h | 16 +- src/utility/graph.h | 105 +++-- src/utility/matrix.h | 6 +- src/utility/vector.h | 17 +- .../eigen/EigenSparseMatrixTest.cpp | 79 ---- .../GmmxxDtmcPrctlModelCheckerTest.cpp | 1 - test/functional/parser/ReadTraFileTest.cpp | 77 ---- test/functional/storage/SparseMatrixTest.cpp | 386 ------------------ .../storage/adapters/EigenAdapterTest.cpp | 100 ----- .../storage/adapters/GmmAdapterTest.cpp | 111 ----- .../storage/adapters/StormAdapterTest.cpp | 104 ----- util/checklist/storage.ods | Bin 18619 -> 18701 bytes 36 files changed, 428 insertions(+), 1486 deletions(-) delete mode 100644 src/adapters/EigenAdapter.h delete mode 100644 test/functional/eigen/EigenSparseMatrixTest.cpp delete mode 100644 test/functional/parser/ReadTraFileTest.cpp delete mode 100644 test/functional/storage/SparseMatrixTest.cpp delete mode 100644 test/functional/storage/adapters/EigenAdapterTest.cpp delete mode 100644 test/functional/storage/adapters/GmmAdapterTest.cpp delete mode 100644 test/functional/storage/adapters/StormAdapterTest.cpp diff --git a/src/adapters/EigenAdapter.h b/src/adapters/EigenAdapter.h deleted file mode 100644 index 68f2ba588..000000000 --- a/src/adapters/EigenAdapter.h +++ /dev/null @@ -1,66 +0,0 @@ -/* - * EigenAdapter.h - * - * Created on: 21.01.2013 - * Author: Philipp Berger - */ - -#ifndef STORM_ADAPTERS_EIGENADAPTER_H_ -#define STORM_ADAPTERS_EIGENADAPTER_H_ - -#include "src/storage/SparseMatrix.h" -#include "Eigen/Sparse" - -#include "log4cplus/logger.h" -#include "log4cplus/loggingmacros.h" - -#include "src/utility/OsDetection.h" - -extern log4cplus::Logger logger; - -namespace storm { - -namespace adapters { - -class EigenAdapter { -public: - /*! - * Converts a sparse matrix into the sparse matrix in the eigen format. - * @return A pointer to a row-major sparse matrix in eigen format. - */ - template - static Eigen::SparseMatrix* toEigenSparseMatrix(storm::storage::SparseMatrix const& matrix) { - uint_fast64_t realNonZeros = matrix.getNonZeroEntryCount(); - LOG4CPLUS_DEBUG(logger, "Converting matrix with " << realNonZeros << " non-zeros to Eigen format."); - - // Prepare the resulting matrix. - Eigen::SparseMatrix* result = new Eigen::SparseMatrix(static_cast(matrix.rowCount), static_cast(matrix.colCount)); - - result->resizeNonZeros(static_cast(realNonZeros)); - //result->reserve(realNonZeros); -#ifdef WINDOWS -# pragma warning(push) -# pragma warning(disable: 4244) // possible loss of data -#endif - // Copy Row Indications - std::copy(matrix.rowIndications.begin(), matrix.rowIndications.end(), (result->outerIndexPtr())); - // Copy Columns Indications - std::copy(matrix.columnIndications.begin(), matrix.columnIndications.end(), (result->innerIndexPtr())); - // And do the same thing with the actual values. - std::copy(matrix.valueStorage.begin(), matrix.valueStorage.end(), (result->valuePtr())); - -#ifdef WINDOWS -# pragma warning(pop) -#endif - - LOG4CPLUS_DEBUG(logger, "Done converting matrix to Eigen format."); - - return result; - } -}; - -} //namespace adapters - -} //namespace storm - -#endif /* STORM_ADAPTERS_EIGENADAPTER_H_ */ diff --git a/src/adapters/ExplicitModelAdapter.h b/src/adapters/ExplicitModelAdapter.h index 4bc5bc28c..270928779 100644 --- a/src/adapters/ExplicitModelAdapter.h +++ b/src/adapters/ExplicitModelAdapter.h @@ -480,10 +480,7 @@ namespace storm { // requested and issue an error otherwise. if (totalNumberOfChoices == 0) { if (storm::settings::Settings::getInstance()->isSet("fixDeadlocks")) { - transitionMatrix.insertNextValue(currentRow, currentState, storm::utility::constantOne(), true); - if (transitionRewards.size() > 0) { - transitionRewardMatrix.insertEmptyRow(true); - } + transitionMatrix.addNextValue(currentRow, currentState, storm::utility::constantOne()); ++currentRow; } else { LOG4CPLUS_ERROR(logger, "Error while creating sparse matrix from probabilistic program: found deadlock state. For fixing these, please provide the appropriate option."); @@ -531,16 +528,14 @@ namespace storm { choiceLabels.push_back(globalChoice.getChoiceLabels()); for (auto const& stateProbabilityPair : globalChoice) { - transitionMatrix.insertNextValue(currentRow, stateProbabilityPair.first, stateProbabilityPair.second, true); + transitionMatrix.addNextValue(currentRow, stateProbabilityPair.first, stateProbabilityPair.second); } // Add all transition rewards to the matrix and add dummy entry if there is none. if (stateToRewardMap.size() > 0) { for (auto const& stateRewardPair : stateToRewardMap) { - transitionRewardMatrix.insertNextValue(currentRow, stateRewardPair.first, stateRewardPair.second, true); + transitionRewardMatrix.addNextValue(currentRow, stateRewardPair.first, stateRewardPair.second); } - } else if (transitionRewards.size() > 0) { - transitionRewardMatrix.insertEmptyRow(true); } ++currentRow; @@ -554,7 +549,7 @@ namespace storm { choiceLabels.emplace_back(std::move(choice.getChoiceLabels())); for (auto const& stateProbabilityPair : choice) { - transitionMatrix.insertNextValue(currentRow, stateProbabilityPair.first, stateProbabilityPair.second, true); + transitionMatrix.addNextValue(currentRow, stateProbabilityPair.first, stateProbabilityPair.second); // Now add all rewards that match this choice. for (auto const& transitionReward : transitionRewards) { @@ -568,10 +563,8 @@ namespace storm { // Add all transition rewards to the matrix and add dummy entry if there is none. if (stateToRewardMap.size() > 0) { for (auto const& stateRewardPair : stateToRewardMap) { - transitionRewardMatrix.insertNextValue(currentRow, stateRewardPair.first, stateRewardPair.second, true); + transitionRewardMatrix.addNextValue(currentRow, stateRewardPair.first, stateRewardPair.second); } - } else if (transitionRewards.size() > 0) { - transitionRewardMatrix.insertEmptyRow(true); } ++currentRow; @@ -583,7 +576,7 @@ namespace storm { choiceLabels.emplace_back(std::move(choice.getChoiceLabels())); for (auto const& stateProbabilityPair : choice) { - transitionMatrix.insertNextValue(currentRow, stateProbabilityPair.first, stateProbabilityPair.second, true); + transitionMatrix.addNextValue(currentRow, stateProbabilityPair.first, stateProbabilityPair.second); // Now add all rewards that match this choice. for (auto const& transitionReward : transitionRewards) { @@ -597,10 +590,8 @@ namespace storm { // Add all transition rewards to the matrix and add dummy entry if there is none. if (stateToRewardMap.size() > 0) { for (auto const& stateRewardPair : stateToRewardMap) { - transitionRewardMatrix.insertNextValue(currentRow, stateRewardPair.first, stateRewardPair.second, true); + transitionRewardMatrix.addNextValue(currentRow, stateRewardPair.first, stateRewardPair.second); } - } else if (transitionRewards.size() > 0) { - transitionRewardMatrix.insertEmptyRow(true); } ++currentRow; @@ -629,10 +620,6 @@ namespace storm { VariableInformation variableInformation = createVariableInformation(program); - // Initialize the matrices. - modelComponents.transitionMatrix.initialize(); - modelComponents.transitionRewardMatrix.initialize(); - // Create the structure for storing the reachable state space. StateInformation stateInformation; @@ -649,8 +636,8 @@ namespace storm { modelComponents.choiceLabeling = std::move(nondeterministicChoiceIndicesAndChoiceLabelsPair.second); // Finalize the resulting matrices. - modelComponents.transitionMatrix.finalize(true); - modelComponents.transitionRewardMatrix.finalize(true); + modelComponents.transitionMatrix.finalize(); + modelComponents.transitionRewardMatrix.finalize(); // Now build the state labeling. modelComponents.stateLabeling = buildStateLabeling(program, variableInformation, stateInformation); diff --git a/src/adapters/GmmxxAdapter.h b/src/adapters/GmmxxAdapter.h index 14fc2cf30..5b20df4d9 100644 --- a/src/adapters/GmmxxAdapter.h +++ b/src/adapters/GmmxxAdapter.h @@ -32,11 +32,11 @@ public: */ template static gmm::csr_matrix* toGmmxxSparseMatrix(storm::storage::SparseMatrix const& matrix) { - uint_fast64_t realNonZeros = matrix.getNonZeroEntryCount(); + uint_fast64_t realNonZeros = matrix.getEntryCount(); LOG4CPLUS_DEBUG(logger, "Converting matrix with " << realNonZeros << " non-zeros to gmm++ format."); // Prepare the resulting matrix. - gmm::csr_matrix* result = new gmm::csr_matrix(matrix.rowCount, matrix.colCount); + gmm::csr_matrix* result = new gmm::csr_matrix(matrix.rowCount, matrix.columnCount); // Copy Row Indications std::copy(matrix.rowIndications.begin(), matrix.rowIndications.end(), result->jc.begin()); @@ -57,12 +57,12 @@ public: * @return A pointer to a row-major sparse matrix in gmm++ format. */ template - static gmm::csr_matrix* toGmmxxSparseMatrix(storm::storage::SparseMatrix && matrix) { - uint_fast64_t realNonZeros = matrix.getNonZeroEntryCount(); + static gmm::csr_matrix* toGmmxxSparseMatrix(storm::storage::SparseMatrix&& matrix) { + uint_fast64_t realNonZeros = matrix.getEntryCount(); LOG4CPLUS_DEBUG(logger, "Converting matrix with " << realNonZeros << " non-zeros to gmm++ format."); // Prepare the resulting matrix. - gmm::csr_matrix* result = new gmm::csr_matrix(matrix.rowCount, matrix.colCount); + gmm::csr_matrix* result = new gmm::csr_matrix(matrix.rowCount, matrix.columnCount); typedef unsigned long long IND_TYPE; typedef std::vector vectorType_ull_t; diff --git a/src/adapters/StormAdapter.h b/src/adapters/StormAdapter.h index 1f4dacd44..9fe348c00 100644 --- a/src/adapters/StormAdapter.h +++ b/src/adapters/StormAdapter.h @@ -33,30 +33,7 @@ public: 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(); + storm::storage::SparseMatrix* result = new storm::storage::SparseMatrix(matrix.ncols(), matrix.jc, matrix.ir, matrix.pr); LOG4CPLUS_DEBUG(logger, "Done converting matrix to storm format."); diff --git a/src/counterexamples/MILPMinimalLabelSetGenerator.h b/src/counterexamples/MILPMinimalLabelSetGenerator.h index 9b3c2b3e2..df5611577 100644 --- a/src/counterexamples/MILPMinimalLabelSetGenerator.h +++ b/src/counterexamples/MILPMinimalLabelSetGenerator.h @@ -129,9 +129,9 @@ namespace storm { for (uint_fast64_t row = nondeterministicChoiceIndices[state]; row < nondeterministicChoiceIndices[state + 1]; ++row) { bool currentChoiceRelevant = false; bool allSuccessorsProblematic = true; - for (typename storm::storage::SparseMatrix::ConstIndexIterator successorIt = transitionMatrix.constColumnIteratorBegin(row); successorIt != transitionMatrix.constColumnIteratorEnd(row); ++successorIt) { + for (auto const& successorEntry : transitionMatrix.getRow(row)) { // If there is a relevant successor, we need to add the labels of the current choice. - if (stateInformation.relevantStates.get(*successorIt) || psiStates.get(*successorIt)) { + if (stateInformation.relevantStates.get(successorEntry.column()) || psiStates.get(successorEntry.column())) { 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(*successorIt)) { + if (!stateInformation.problematicStates.get(successorEntry.column())) { allSuccessorsProblematic = false; } } @@ -303,12 +303,12 @@ namespace storm { std::list const& relevantChoicesForState = choiceInformation.relevantChoicesForRelevantStates.at(state); for (uint_fast64_t row : relevantChoicesForState) { - for (typename storm::storage::SparseMatrix::ConstIndexIterator successorIt = labeledMdp.getTransitionMatrix().constColumnIteratorBegin(row); successorIt != labeledMdp.getTransitionMatrix().constColumnIteratorEnd(row); ++successorIt) { - if (stateInformation.relevantStates.get(*successorIt)) { - if (resultingMap.find(*successorIt) == resultingMap.end()) { + for (auto const& successorEntry : labeledMdp.getTransitionMatrix().getRow(row)) { + if (stateInformation.relevantStates.get(successorEntry.column())) { + if (resultingMap.find(successorEntry.column()) == resultingMap.end()) { variableNameBuffer.str(""); variableNameBuffer.clear(); - variableNameBuffer << "r" << *successorIt; + variableNameBuffer << "r" << successorEntry.column(); resultingMap[state] = solver.createContinuousVariable(variableNameBuffer.str(), storm::solver::LpSolver::BOUNDED, 0, 1, 0); ++numberOfVariablesCreated; } @@ -337,12 +337,12 @@ namespace storm { for (auto state : stateInformation.problematicStates) { std::list const& relevantChoicesForState = choiceInformation.relevantChoicesForRelevantStates.at(state); for (uint_fast64_t row : relevantChoicesForState) { - for (typename storm::storage::SparseMatrix::ConstIndexIterator successorIt = labeledMdp.getTransitionMatrix().constColumnIteratorBegin(row); successorIt != labeledMdp.getTransitionMatrix().constColumnIteratorEnd(row); ++successorIt) { - if (stateInformation.relevantStates.get(*successorIt)) { + for (auto const& successorEntry : labeledMdp.getTransitionMatrix().getRow(row)) { + if (stateInformation.relevantStates.get(successorEntry.column())) { variableNameBuffer.str(""); variableNameBuffer.clear(); - variableNameBuffer << "t" << state << "to" << *successorIt; - resultingMap[std::make_pair(state, *successorIt)] = solver.createBinaryVariable(variableNameBuffer.str(), 0); + variableNameBuffer << "t" << state << "to" << successorEntry.column(); + resultingMap[std::make_pair(state, successorEntry.column())] = solver.createBinaryVariable(variableNameBuffer.str(), 0); ++numberOfVariablesCreated; } } @@ -550,13 +550,12 @@ namespace storm { coefficients.push_back(1.0); double rightHandSide = 1; - typename storm::storage::SparseMatrix::Rows rows = labeledMdp.getTransitionMatrix().getRows(choice, choice); - for (typename storm::storage::SparseMatrix::ConstIterator successorIt = rows.begin(), successorIte = rows.end(); successorIt != successorIte; ++successorIt) { - if (stateInformation.relevantStates.get(successorIt.column())) { - variables.push_back(static_cast(variableInformation.stateToProbabilityVariableIndexMap.at(successorIt.column()))); - coefficients.push_back(-successorIt.value()); - } else if (psiStates.get(successorIt.column())) { - rightHandSide += successorIt.value(); + for (auto const& successorEntry : labeledMdp.getTransitionMatrix().getRow(choice)) { + if (stateInformation.relevantStates.get(successorEntry.column())) { + variables.push_back(static_cast(variableInformation.stateToProbabilityVariableIndexMap.at(successorEntry.column()))); + coefficients.push_back(-successorEntry.value()); + } else if (psiStates.get(successorEntry.column())) { + rightHandSide += successorEntry.value(); } } @@ -609,8 +608,8 @@ namespace storm { variables.push_back(*choiceVariableIndicesIterator); coefficients.push_back(1); - for (typename storm::storage::SparseMatrix::ConstIndexIterator successorIt = labeledMdp.getTransitionMatrix().constColumnIteratorBegin(problematicChoice); successorIt != labeledMdp.getTransitionMatrix().constColumnIteratorEnd(problematicChoice); ++successorIt) { - variables.push_back(variableInformation.problematicTransitionToVariableIndexMap.at(std::make_pair(stateListPair.first, *successorIt))); + for (auto const& successorEntry : labeledMdp.getTransitionMatrix().getRow(problematicChoice)) { + variables.push_back(variableInformation.problematicTransitionToVariableIndexMap.at(std::make_pair(stateListPair.first, successorEntry.column()))); coefficients.push_back(-1); } @@ -621,15 +620,15 @@ namespace storm { for (auto state : stateInformation.problematicStates) { for (auto problematicChoice : choiceInformation.problematicChoicesForProblematicStates.at(state)) { - for (typename storm::storage::SparseMatrix::ConstIndexIterator successorIt = labeledMdp.getTransitionMatrix().constColumnIteratorBegin(problematicChoice); successorIt != labeledMdp.getTransitionMatrix().constColumnIteratorEnd(problematicChoice); ++successorIt) { + for (auto const& successorEntry : labeledMdp.getTransitionMatrix().getRow(state)) { std::vector variables; std::vector coefficients; variables.push_back(variableInformation.problematicStateToVariableIndexMap.at(state)); coefficients.push_back(1); - variables.push_back(variableInformation.problematicStateToVariableIndexMap.at(*successorIt)); + variables.push_back(variableInformation.problematicStateToVariableIndexMap.at(successorEntry.column())); coefficients.push_back(-1); - variables.push_back(variableInformation.problematicTransitionToVariableIndexMap.at(std::make_pair(state, *successorIt))); + variables.push_back(variableInformation.problematicTransitionToVariableIndexMap.at(std::make_pair(state, successorEntry.column()))); coefficients.push_back(1); solver.addConstraint("UnproblematicStateReachable" + std::to_string(numberOfConstraintsCreated), variables, coefficients, storm::solver::LpSolver::LESS, 1); @@ -684,8 +683,8 @@ namespace storm { std::list::const_iterator choiceVariableIndicesIterator = variableInformation.stateToChoiceVariablesIndexMap.at(state).begin(); for (auto choice : choiceInformation.relevantChoicesForRelevantStates.at(state)) { bool psiStateReachableInOneStep = false; - for (typename storm::storage::SparseMatrix::ConstIndexIterator successorIt = labeledMdp.getTransitionMatrix().constColumnIteratorBegin(choice); successorIt != labeledMdp.getTransitionMatrix().constColumnIteratorEnd(choice); ++successorIt) { - if (psiStates.get(*successorIt)) { + for (auto const& successorEntry : labeledMdp.getTransitionMatrix().getRow(choice)) { + if (psiStates.get(successorEntry.column())) { psiStateReachableInOneStep = true; } } @@ -697,9 +696,9 @@ namespace storm { variables.push_back(static_cast(*choiceVariableIndicesIterator)); coefficients.push_back(1); - for (typename storm::storage::SparseMatrix::ConstIndexIterator successorIt = labeledMdp.getTransitionMatrix().constColumnIteratorBegin(choice); successorIt != labeledMdp.getTransitionMatrix().constColumnIteratorEnd(choice); ++successorIt) { - if (state != *successorIt && stateInformation.relevantStates.get(*successorIt)) { - std::list const& successorChoiceVariableIndices = variableInformation.stateToChoiceVariablesIndexMap.at(*successorIt); + for (auto const& successorEntry : labeledMdp.getTransitionMatrix().getRow(choice)) { + if (state != successorEntry.column() && stateInformation.relevantStates.get(successorEntry.column())) { + std::list const& successorChoiceVariableIndices = variableInformation.stateToChoiceVariablesIndexMap.at(successorEntry.column()); for (auto choiceVariableIndex : successorChoiceVariableIndices) { variables.push_back(choiceVariableIndex); @@ -727,9 +726,9 @@ namespace storm { // Compute the set of predecessors. std::unordered_set predecessors; - for (typename storm::storage::SparseMatrix::ConstIndexIterator predecessorIt = backwardTransitions.constColumnIteratorBegin(state); predecessorIt != backwardTransitions.constColumnIteratorEnd(state); ++predecessorIt) { - if (state != *predecessorIt) { - predecessors.insert(*predecessorIt); + for (auto const& predecessorEntry : backwardTransitions.getRow(state)) { + if (state != predecessorEntry.column()) { + predecessors.insert(predecessorEntry.column()); } } @@ -744,8 +743,8 @@ namespace storm { bool choiceTargetsCurrentState = false; // Check if the current choice targets the current state. - for (typename storm::storage::SparseMatrix::ConstIndexIterator successorIt = labeledMdp.getTransitionMatrix().constColumnIteratorBegin(relevantChoice); successorIt != labeledMdp.getTransitionMatrix().constColumnIteratorEnd(relevantChoice); ++successorIt) { - if (state == *successorIt) { + for (auto const& successorEntry : labeledMdp.getTransitionMatrix().getRow(relevantChoice)) { + if (state == successorEntry.column()) { choiceTargetsCurrentState = true; break; } @@ -789,9 +788,9 @@ namespace storm { std::unordered_set predecessors; for (auto psiState : psiStates) { // Compute the set of predecessors. - for (typename storm::storage::SparseMatrix::ConstIndexIterator predecessorIt = backwardTransitions.constColumnIteratorBegin(psiState); predecessorIt != backwardTransitions.constColumnIteratorEnd(psiState); ++predecessorIt) { - if (psiState != *predecessorIt) { - predecessors.insert(*predecessorIt); + for (auto const& predecessorEntry : backwardTransitions.getRow(psiState)) { + if (psiState != predecessorEntry.column()) { + predecessors.insert(predecessorEntry.column()); } } } @@ -807,8 +806,8 @@ namespace storm { bool choiceTargetsPsiState = false; // Check if the current choice targets the current state. - for (typename storm::storage::SparseMatrix::ConstIndexIterator successorIt = labeledMdp.getTransitionMatrix().constColumnIteratorBegin(relevantChoice); successorIt != labeledMdp.getTransitionMatrix().constColumnIteratorEnd(relevantChoice); ++successorIt) { - if (psiStates.get(*successorIt)) { + for (auto const& successorEntry : labeledMdp.getTransitionMatrix().getRow(relevantChoice)) { + if (psiStates.get(successorEntry.column())) { choiceTargetsPsiState = true; break; } diff --git a/src/counterexamples/PathBasedSubsystemGenerator.h b/src/counterexamples/PathBasedSubsystemGenerator.h index bc4c43710..1676de7ef 100644 --- a/src/counterexamples/PathBasedSubsystemGenerator.h +++ b/src/counterexamples/PathBasedSubsystemGenerator.h @@ -67,8 +67,7 @@ public: distances[init].second = (T) 1; } - typename storm::storage::SparseMatrix::ConstRowIterator rowIt = transMat.begin(init); - for(auto trans = rowIt.begin() ; trans != rowIt.end(); ++trans) { + for(auto& trans : transMat.getRow(init)) { //save transition only if it's no 'virtual transition of prob 0 and it doesn't go from init state to init state. if(trans.value() != (T) 0 && !subSysStates.get(trans.column())) { //new state? @@ -114,8 +113,7 @@ public: // Same goes for forbidden states since they may not be used on a path, except as last node. if(!subSysStates.get(activeState.first) && allowedStates.get(activeState.first)) { // Look at all neighbors - typename storm::storage::SparseMatrix::ConstRowIterator rowIt = transMat.begin(activeState.first); - for(typename storm::storage::SparseMatrix::ConstIterator trans = rowIt.begin(); trans != rowIt.end(); ++trans) { + for(auto& trans : transMat.getRow(activeState.first)) { // Only consider the transition if it's not virtual if(trans.value() != (T) 0) { @@ -182,8 +180,7 @@ public: continue; } - typename storm::storage::SparseMatrix::ConstRowIterator rowIt = transMat.begin(init); - for(typename storm::storage::SparseMatrix::ConstIterator trans = rowIt.begin(); trans != rowIt.end(); ++trans) { + for(auto& trans : transMat.getRow(init)) { //save transition only if it's no 'virtual transition of prob 0 and it doesn't go from init state to init state. if(trans.value() != (T) 0 && !subSysStates.get(trans.column())) { //new state? @@ -234,8 +231,7 @@ public: // Same goes for forbidden states since they may not be used on a path, except as last node. if(!subSysStates.get(activeState.first) && allowedStates.get(activeState.first)) { // Look at all neighbors - typename storm::storage::SparseMatrix::ConstRowIterator rowIt = transMat.begin(activeState.first); - for(typename storm::storage::SparseMatrix::ConstIterator trans = rowIt.begin(); trans != rowIt.end(); ++trans) { + for(auto& trans : transMat.getRow(activeState.first)) { // Only consider the transition if it's not virtual if(trans.value() != (T) 0) { diff --git a/src/counterexamples/SMTMinimalCommandSetGenerator.h b/src/counterexamples/SMTMinimalCommandSetGenerator.h index de3f8fdb8..8e46f8da2 100644 --- a/src/counterexamples/SMTMinimalCommandSetGenerator.h +++ b/src/counterexamples/SMTMinimalCommandSetGenerator.h @@ -123,9 +123,9 @@ namespace storm { for (uint_fast64_t row = nondeterministicChoiceIndices[state]; row < nondeterministicChoiceIndices[state + 1]; ++row) { bool currentChoiceRelevant = false; - for (typename storm::storage::SparseMatrix::ConstIndexIterator successorIt = transitionMatrix.constColumnIteratorBegin(row); successorIt != transitionMatrix.constColumnIteratorEnd(row); ++successorIt) { + for (auto& entry : transitionMatrix.getRow(row)) { // If there is a relevant successor, we need to add the labels of the current choice. - if (relevancyInformation.relevantStates.get(*successorIt) || psiStates.get(*successorIt)) { + if (relevancyInformation.relevantStates.get(entry.column()) || psiStates.get(entry.column())) { for (auto const& label : choiceLabeling[row]) { relevancyInformation.relevantLabels.insert(label); } @@ -208,25 +208,25 @@ namespace storm { variableInformation.stateOrderVariables.push_back(context.real_const(variableName.str().c_str())); - for (auto const& relevantChoices : relevancyInformation.relevantChoicesForRelevantStates.at(state)) { - for (typename storm::storage::SparseMatrix::ConstIndexIterator successorIt = transitionMatrix.constColumnIteratorBegin(relevantChoices); successorIt != transitionMatrix.constColumnIteratorEnd(relevantChoices); ++successorIt) { + for (auto const& relevantChoice : relevancyInformation.relevantChoicesForRelevantStates.at(state)) { + for (auto const& entry : transitionMatrix.getRow(relevantChoice)) { // If the successor state is neither the state itself nor an irrelevant state, we need to add a variable for the transition. - if (state != *successorIt && (relevancyInformation.relevantStates.get(*successorIt) || psiStates.get(*successorIt))) { + if (state != entry.column() && (relevancyInformation.relevantStates.get(entry.column()) || psiStates.get(entry.column()))) { // Make sure that there is not already one variable for the state pair. This may happen because of several nondeterministic choices // targeting the same state. - if (variableInformation.statePairToIndexMap.find(std::make_pair(state, *successorIt)) != variableInformation.statePairToIndexMap.end()) { + if (variableInformation.statePairToIndexMap.find(std::make_pair(state, entry.column())) != variableInformation.statePairToIndexMap.end()) { continue; } // At this point we know that the state-pair does not have an associated variable. - variableInformation.statePairToIndexMap[std::make_pair(state, *successorIt)] = variableInformation.statePairVariables.size(); + variableInformation.statePairToIndexMap[std::make_pair(state, entry.column())] = variableInformation.statePairVariables.size(); // Clear contents of the stream to construct new expression name. variableName.clear(); variableName.str(""); - variableName << "t" << state << "_" << *successorIt; + variableName << "t" << state << "_" << entry.column(); variableInformation.statePairVariables.push_back(context.bool_const(variableName.str().c_str())); } @@ -315,12 +315,12 @@ namespace storm { // Iterate over successors and add relevant choices of relevant successors to the following label set. bool canReachTargetState = false; - for (typename storm::storage::SparseMatrix::ConstIndexIterator successorIt = transitionMatrix.constColumnIteratorBegin(currentChoice), successorIte = transitionMatrix.constColumnIteratorEnd(currentChoice); successorIt != successorIte; ++successorIt) { - if (relevancyInformation.relevantStates.get(*successorIt)) { - for (auto relevantChoice : relevancyInformation.relevantChoicesForRelevantStates.at(*successorIt)) { + for (auto const& entry : transitionMatrix.getRow(currentChoice)) { + if (relevancyInformation.relevantStates.get(entry.column())) { + for (auto relevantChoice : relevancyInformation.relevantChoicesForRelevantStates.at(entry.column())) { followingLabels[choiceLabeling[currentChoice]].insert(choiceLabeling[currentChoice]); } - } else if (psiStates.get(*successorIt)) { + } else if (psiStates.get(entry.column())) { canReachTargetState = true; } } @@ -334,12 +334,12 @@ namespace storm { // Iterate over predecessors and add all choices that target the current state to the preceding // label set of all labels of all relevant choices of the current state. - for (typename storm::storage::SparseMatrix::ConstIndexIterator predecessorIt = backwardTransitions.constColumnIteratorBegin(currentState), predecessorIte = backwardTransitions.constColumnIteratorEnd(currentState); predecessorIt != predecessorIte; ++predecessorIt) { - if (relevancyInformation.relevantStates.get(*predecessorIt)) { - for (auto predecessorChoice : relevancyInformation.relevantChoicesForRelevantStates.at(*predecessorIt)) { + for (auto const& predecessorEntry : backwardTransitions.getRow(currentState)) { + if (relevancyInformation.relevantStates.get(predecessorEntry.column())) { + for (auto predecessorChoice : relevancyInformation.relevantChoicesForRelevantStates.at(predecessorEntry.column())) { bool choiceTargetsCurrentState = false; - for (typename storm::storage::SparseMatrix::ConstIndexIterator successorIt = transitionMatrix.constColumnIteratorBegin(predecessorChoice), successorIte = transitionMatrix.constColumnIteratorEnd(predecessorChoice); successorIt != successorIte; ++successorIt) { - if (*successorIt == currentState) { + for (auto const& successorEntry : transitionMatrix.getRow(predecessorChoice)) { + if (successorEntry.column() == currentState) { choiceTargetsCurrentState = true; } } @@ -580,12 +580,12 @@ namespace storm { // Iterate over predecessors and add all choices that target the current state to the preceding // label set of all labels of all relevant choices of the current state. - for (typename storm::storage::SparseMatrix::ConstIndexIterator predecessorIt = backwardTransitions.constColumnIteratorBegin(currentState), predecessorIte = backwardTransitions.constColumnIteratorEnd(currentState); predecessorIt != predecessorIte; ++predecessorIt) { - if (relevancyInformation.relevantStates.get(*predecessorIt)) { - for (auto predecessorChoice : relevancyInformation.relevantChoicesForRelevantStates.at(*predecessorIt)) { + for (auto const& predecessorEntry : backwardTransitions.getRow(currentState)) { + if (relevancyInformation.relevantStates.get(predecessorEntry.column())) { + for (auto predecessorChoice : relevancyInformation.relevantChoicesForRelevantStates.at(predecessorEntry.column())) { bool choiceTargetsCurrentState = false; - for (typename storm::storage::SparseMatrix::ConstIndexIterator successorIt = transitionMatrix.constColumnIteratorBegin(predecessorChoice), successorIte = transitionMatrix.constColumnIteratorEnd(predecessorChoice); successorIt != successorIte; ++successorIt) { - if (*successorIt == currentState) { + for (auto const& successorEntry : transitionMatrix.getRow(predecessorChoice)) { + if (successorEntry.column() == currentState) { choiceTargetsCurrentState = true; } } @@ -912,17 +912,17 @@ namespace storm { if (!labeledMdp.getInitialStates().get(relevantState)) { // Assert the constraints (1). storm::storage::VectorSet relevantPredecessors; - for (typename storm::storage::SparseMatrix::ConstIndexIterator predecessorIt = backwardTransitions.constColumnIteratorBegin(relevantState), predecessorIte = backwardTransitions.constColumnIteratorEnd(relevantState); predecessorIt != predecessorIte; ++predecessorIt) { - if (relevantState != *predecessorIt && relevancyInformation.relevantStates.get(*predecessorIt)) { - relevantPredecessors.insert(*predecessorIt); + for (auto const& predecessorEntry : backwardTransitions.getRow(relevantState)) { + if (relevantState != predecessorEntry.column() && relevancyInformation.relevantStates.get(predecessorEntry.column())) { + relevantPredecessors.insert(predecessorEntry.column()); } } storm::storage::VectorSet relevantSuccessors; for (auto const& relevantChoice : relevancyInformation.relevantChoicesForRelevantStates.at(relevantState)) { - for (typename storm::storage::SparseMatrix::ConstIndexIterator successorIt = transitionMatrix.constColumnIteratorBegin(relevantChoice); successorIt != transitionMatrix.constColumnIteratorEnd(relevantChoice); ++successorIt) { - if (relevantState != *successorIt && (relevancyInformation.relevantStates.get(*successorIt) || psiStates.get(*successorIt))) { - relevantSuccessors.insert(*successorIt); + for (auto const& successorEntry : transitionMatrix.getRow(relevantChoice)) { + if (relevantState != successorEntry.column() && (relevancyInformation.relevantStates.get(successorEntry.column()) || psiStates.get(successorEntry.column()))) { + relevantSuccessors.insert(successorEntry.column()); } } } @@ -940,9 +940,9 @@ namespace storm { // Assert the constraints (2). storm::storage::VectorSet relevantSuccessors; for (auto const& relevantChoice : relevancyInformation.relevantChoicesForRelevantStates.at(relevantState)) { - for (typename storm::storage::SparseMatrix::ConstIndexIterator successorIt = transitionMatrix.constColumnIteratorBegin(relevantChoice); successorIt != transitionMatrix.constColumnIteratorEnd(relevantChoice); ++successorIt) { - if (relevantState != *successorIt && (relevancyInformation.relevantStates.get(*successorIt) || psiStates.get(*successorIt))) { - relevantSuccessors.insert(*successorIt); + for (auto const& successorEntry : transitionMatrix.getRow(relevantChoice)) { + if (relevantState != successorEntry.column() && (relevancyInformation.relevantStates.get(successorEntry.column()) || psiStates.get(successorEntry.column()))) { + relevantSuccessors.insert(successorEntry.column()); } } } @@ -964,8 +964,8 @@ namespace storm { // Assert constraint for (1). storm::storage::VectorSet choicesForStatePair; for (auto const& relevantChoice : relevancyInformation.relevantChoicesForRelevantStates.at(sourceState)) { - for (typename storm::storage::SparseMatrix::ConstIndexIterator successorIt = transitionMatrix.constColumnIteratorBegin(relevantChoice); successorIt != transitionMatrix.constColumnIteratorEnd(relevantChoice); ++successorIt) { - if (*successorIt == targetState) { + for (auto const& successorEntry : transitionMatrix.getRow(relevantChoice)) { + if (successorEntry.column() == targetState) { choicesForStatePair.insert(relevantChoice); } } @@ -1399,14 +1399,14 @@ namespace storm { for (uint_fast64_t currentChoice = nondeterministicChoiceIndices[currentState]; currentChoice < nondeterministicChoiceIndices[currentState + 1]; ++currentChoice) { bool choiceTargetsRelevantState = false; - for (typename storm::storage::SparseMatrix::ConstIndexIterator successorIt = transitionMatrix.constColumnIteratorBegin(currentChoice), successorIte = transitionMatrix.constColumnIteratorEnd(currentChoice); successorIt != successorIte; ++successorIt) { - if (relevancyInformation.relevantStates.get(*successorIt) && currentState != *successorIt) { + for (auto const& successorEntry : transitionMatrix.getRow(currentChoice)) { + if (relevancyInformation.relevantStates.get(successorEntry.column()) && currentState != successorEntry.column()) { choiceTargetsRelevantState = true; - if (!reachableStates.get(*successorIt)) { - reachableStates.set(*successorIt, true); - stack.push_back(*successorIt); + if (!reachableStates.get(successorEntry.column())) { + reachableStates.set(successorEntry.column()); + stack.push_back(successorEntry.column()); } - } else if (psiStates.get(*successorIt)) { + } else if (psiStates.get(successorEntry.column())) { targetStateIsReachable = true; } } @@ -1442,8 +1442,8 @@ namespace storm { bool isBorderChoice = false; // Determine whether the state has the option to leave the reachable state space and go to the unreachable relevant states. - for (typename storm::storage::SparseMatrix::ConstIndexIterator successorIt = originalMdp.getTransitionMatrix().constColumnIteratorBegin(currentChoice), successorIte = originalMdp.getTransitionMatrix().constColumnIteratorEnd(currentChoice); successorIt != successorIte; ++successorIt) { - if (unreachableRelevantStates.get(*successorIt)) { + for (auto const& successorEntry : originalMdp.getTransitionMatrix().getRow(currentChoice)) { + if (unreachableRelevantStates.get(successorEntry.column())) { isBorderChoice = true; } } @@ -1525,14 +1525,14 @@ namespace storm { for (uint_fast64_t currentChoice = nondeterministicChoiceIndices[currentState]; currentChoice < nondeterministicChoiceIndices[currentState + 1]; ++currentChoice) { bool choiceTargetsRelevantState = false; - for (typename storm::storage::SparseMatrix::ConstIndexIterator successorIt = transitionMatrix.constColumnIteratorBegin(currentChoice), successorIte = transitionMatrix.constColumnIteratorEnd(currentChoice); successorIt != successorIte; ++successorIt) { - if (relevancyInformation.relevantStates.get(*successorIt) && currentState != *successorIt) { + for (auto const& successorEntry : transitionMatrix.getRow(currentChoice)) { + if (relevancyInformation.relevantStates.get(successorEntry.column()) && currentState != successorEntry.column()) { choiceTargetsRelevantState = true; - if (!reachableStates.get(*successorIt)) { - reachableStates.set(*successorIt, true); - stack.push_back(*successorIt); + if (!reachableStates.get(successorEntry.column())) { + reachableStates.set(successorEntry.column(), true); + stack.push_back(successorEntry.column()); } - } else if (psiStates.get(*successorIt)) { + } else if (psiStates.get(successorEntry.column())) { targetStateIsReachable = true; } } diff --git a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h index 96f71648c..3edfba9b8 100644 --- a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h +++ b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h @@ -94,8 +94,7 @@ namespace storm { // Digitize aMarkovian. Based on whether the transition is a self-loop or not, we apply the two digitization rules. uint_fast64_t rowIndex = 0; for (auto state : markovianNonGoalStates) { - typename storm::storage::SparseMatrix::MutableRows row = aMarkovian.getMutableRow(rowIndex); - for (auto element : row) { + 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; @@ -109,8 +108,7 @@ namespace storm { // Digitize aMarkovianToProbabilistic. As there are no self-loops in this case, we only need to apply the digitization formula for regular successors. rowIndex = 0; for (auto state : markovianNonGoalStates) { - typename storm::storage::SparseMatrix::MutableRows row = aMarkovianToProbabilistic.getMutableRow(rowIndex); - for (auto element : row) { + for (auto element : aMarkovianToProbabilistic.getRow(rowIndex)) { element.value() = (1 - std::exp(-exitRates[state] * delta)) * element.value(); } ++rowIndex; @@ -121,14 +119,13 @@ namespace storm { std::vector bMarkovian(markovianNonGoalStates.getNumberOfSetBits()); // Compute the two fixed right-hand side vectors, one for Markovian states and one for the probabilistic ones. - std::vector bProbabilisticFixed = transitionMatrix.getConstrainedRowSumVector(probabilisticNonGoalStates, nondeterministicChoiceIndices, goalStates, aProbabilistic.getRowCount()); + std::vector bProbabilisticFixed = transitionMatrix.getConstrainedRowSumVector(probabilisticNonGoalStates, nondeterministicChoiceIndices, goalStates); std::vector bMarkovianFixed; bMarkovianFixed.reserve(markovianNonGoalStates.getNumberOfSetBits()); for (auto state : markovianNonGoalStates) { bMarkovianFixed.push_back(storm::utility::constantZero()); - typename storm::storage::SparseMatrix::Rows row = transitionMatrix.getRow(nondeterministicChoiceIndices[state]); - for (auto element : row) { + for (auto element : transitionMatrix.getRow(nondeterministicChoiceIndices[state])) { if (goalStates.get(element.column())) { bMarkovianFixed.back() += (1 - std::exp(-exitRates[state] * delta)) * element.value(); } diff --git a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h index acef76037..98e1c2e73 100644 --- a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h +++ b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h @@ -104,7 +104,6 @@ public: * checker. If the qualitative flag is set, exact probabilities might not be computed. */ virtual std::vector checkBoundedUntil(storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, uint_fast64_t stepBound, bool qualitative) const { - std::vector result(this->getModel().getNumberOfStates()); // If we identify the states that have probability 0 of reaching the target states, we can exclude them in the @@ -122,7 +121,7 @@ public: storm::utility::vector::setVectorValues(result, statesWithProbabilityGreater0, Type(0.5)); } else { // In this case we have have to compute the probabilities. - + // We can eliminate the rows and columns from the original transition probability matrix that have probability 0. storm::storage::SparseMatrix submatrix = this->getModel().getTransitionMatrix().getSubmatrix(statesWithProbabilityGreater0); @@ -192,9 +191,7 @@ public: * checker. If the qualitative flag is set, exact probabilities might not be computed. */ virtual std::vector checkBoundedEventually(storm::property::prctl::BoundedEventually const& formula, bool qualitative) const { - // Create equivalent temporary bounded until formula and check it. - storm::property::prctl::BoundedUntil temporaryBoundedUntilFormula(new storm::property::prctl::Ap("true"), formula.getChild().clone(), formula.getBound()); - return this->checkBoundedUntil(temporaryBoundedUntilFormula, qualitative); + return this->checkBoundedUntil(storm::storage::BitVector(this->getModel().getNumberOfStates(), true), formula.getChild().check(*this), formula.getBound(), qualitative); } /*! diff --git a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h index a03b9d080..7659bd091 100644 --- a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h +++ b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h @@ -323,7 +323,7 @@ namespace storm { // Prepare the right-hand side of the equation system. For entry i this corresponds to // the accumulated probability of going from state i to some 'yes' state. - std::vector b = transitionMatrix.getConstrainedRowSumVector(maybeStates, nondeterministicChoiceIndices, statesWithProbability1, submatrix.getRowCount()); + std::vector b = transitionMatrix.getConstrainedRowSumVector(maybeStates, nondeterministicChoiceIndices, statesWithProbability1); // Create vector for results for maybe states. std::vector x(maybeStates.getNumberOfSetBits()); diff --git a/src/models/AbstractDeterministicModel.h b/src/models/AbstractDeterministicModel.h index 7d4564280..926dd484b 100644 --- a/src/models/AbstractDeterministicModel.h +++ b/src/models/AbstractDeterministicModel.h @@ -71,18 +71,10 @@ class AbstractDeterministicModel: public AbstractModel { // Intentionally left empty. } - virtual typename storm::storage::SparseMatrix::Rows getRows(uint_fast64_t state) const override { + virtual typename storm::storage::SparseMatrix::const_rows getRows(uint_fast64_t state) const override { return this->transitionMatrix.getRows(state, state); } - virtual typename storm::storage::SparseMatrix::ConstRowIterator rowIteratorBegin(uint_fast64_t state) const override { - return this->transitionMatrix.begin(state); - } - - virtual typename storm::storage::SparseMatrix::ConstRowIterator rowIteratorEnd(uint_fast64_t state) const override { - return this->transitionMatrix.end(state); - } - /*! * Calculates a hash over all values contained in this Model. * @return size_t A Hash Value @@ -97,10 +89,11 @@ class AbstractDeterministicModel: public AbstractModel { // Simply iterate over all transitions and draw the arrows with probability information attached. auto rowIt = this->transitionMatrix.begin(); for (uint_fast64_t i = 0; i < this->transitionMatrix.getRowCount(); ++i, ++rowIt) { - for (auto transitionIt = rowIt.begin(), transitionIte = rowIt.end(); transitionIt != transitionIte; ++transitionIt) { - if (transitionIt.value() != storm::utility::constantZero()) { - if (subsystem == nullptr || subsystem->get(transitionIt.column())) { - outStream << "\t" << i << " -> " << transitionIt.column() << " [ label= \"" << transitionIt.value() << "\" ];" << std::endl; + 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; } } } diff --git a/src/models/AbstractModel.h b/src/models/AbstractModel.h index 8e2cc9730..f8ab02fd8 100644 --- a/src/models/AbstractModel.h +++ b/src/models/AbstractModel.h @@ -208,23 +208,7 @@ class AbstractModel: public std::enable_shared_from_this> { * @param state The state for which to retrieve the rows. * @return An object representing the matrix rows associated with the given state. */ - virtual typename storm::storage::SparseMatrix::Rows getRows(uint_fast64_t state) const = 0; - - /*! - * Returns an iterator to the successors of the given state. - * - * @param state The state for which to return the iterator. - * @return An iterator to the successors of the given state. - */ - virtual typename storm::storage::SparseMatrix::ConstRowIterator rowIteratorBegin(uint_fast64_t state) const = 0; - - /*! - * Returns an iterator pointing to the element past the successors of the given state. - * - * @param state The state for which to return the iterator. - * @return An iterator pointing to the element past the successors of the given state. - */ - virtual typename storm::storage::SparseMatrix::ConstRowIterator rowIteratorEnd(uint_fast64_t state) const = 0; + virtual typename storm::storage::SparseMatrix::const_rows getRows(uint_fast64_t state) const = 0; /*! * Returns the state space size of the model. @@ -239,7 +223,7 @@ class AbstractModel: public std::enable_shared_from_this> { * @return The number of (non-zero) transitions of the model. */ virtual uint_fast64_t getNumberOfTransitions() const { - return this->getTransitionMatrix().getNonZeroEntryCount(); + return this->getTransitionMatrix().getEntryCount(); } /*! @@ -383,13 +367,13 @@ class AbstractModel: public std::enable_shared_from_this> { */ virtual size_t getHash() const { std::size_t result = 0; - boost::hash_combine(result, transitionMatrix.getHash()); + boost::hash_combine(result, transitionMatrix.hash()); boost::hash_combine(result, stateLabeling.getHash()); if (stateRewardVector) { boost::hash_combine(result, storm::utility::Hash::getHash(stateRewardVector.get())); } if (transitionRewardMatrix) { - boost::hash_combine(result, transitionRewardMatrix.get().getHash()); + boost::hash_combine(result, transitionRewardMatrix.get().hash()); } return result; } diff --git a/src/models/AbstractNondeterministicModel.h b/src/models/AbstractNondeterministicModel.h index 6cc713fda..344109f44 100644 --- a/src/models/AbstractNondeterministicModel.h +++ b/src/models/AbstractNondeterministicModel.h @@ -110,18 +110,10 @@ namespace storm { return nondeterministicChoiceIndices; } - virtual typename storm::storage::SparseMatrix::Rows getRows(uint_fast64_t state) const override { + virtual typename storm::storage::SparseMatrix::const_rows getRows(uint_fast64_t state) const override { return this->transitionMatrix.getRows(nondeterministicChoiceIndices[state], nondeterministicChoiceIndices[state + 1] - 1); } - virtual typename storm::storage::SparseMatrix::ConstRowIterator rowIteratorBegin(uint_fast64_t state) const override { - return this->transitionMatrix.begin(nondeterministicChoiceIndices[state]); - } - - virtual typename storm::storage::SparseMatrix::ConstRowIterator rowIteratorEnd(uint_fast64_t state) const override { - return this->transitionMatrix.end(nondeterministicChoiceIndices[state + 1] - 1); - } - /*! * Retrieves the backward transition relation of the model, i.e. a set of transitions * between states that correspond to the reversed transition relation of this model. @@ -140,7 +132,7 @@ namespace storm { // First, we need to count how many backward transitions each state has. for (uint_fast64_t i = 0; i < numberOfStates; ++i) { - typename storm::storage::SparseMatrix::Rows rows = this->getRows(i); + typename storm::storage::SparseMatrix::const_rows rows = this->getRows(i); for (auto const& transition : rows) { if (transition.value() > 0) { ++rowIndications[transition.column() + 1]; @@ -160,7 +152,7 @@ namespace storm { // Now we are ready to actually fill in the list of predecessors for // every state. Again, we start by considering all but the last row. for (uint_fast64_t i = 0; i < numberOfStates; ++i) { - typename storm::storage::SparseMatrix::Rows rows = this->getRows(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(); @@ -169,11 +161,7 @@ namespace storm { } } - storm::storage::SparseMatrix backwardTransitionMatrix(numberOfStates, numberOfStates, - numberOfTransitions, - std::move(rowIndications), - std::move(columnIndications), - std::move(values)); + storm::storage::SparseMatrix backwardTransitionMatrix(numberOfStates, std::move(rowIndications), std::move(columnIndications), std::move(values)); return backwardTransitionMatrix; } @@ -209,16 +197,17 @@ namespace storm { AbstractModel::writeDotToStream(outStream, includeLabeling, subsystem, firstValue, secondValue, stateColoring, colors, scheduler, false); // Write the probability distributions for all the states. - auto rowIt = this->transitionMatrix.begin(); for (uint_fast64_t state = 0, highestStateIndex = this->getNumberOfStates() - 1; state <= highestStateIndex; ++state) { uint_fast64_t rowCount = nondeterministicChoiceIndices[state + 1] - nondeterministicChoiceIndices[state]; bool highlightChoice = true; // For this, we need to iterate over all available nondeterministic choices in the current state. - for (uint_fast64_t row = 0; row < rowCount; ++row, ++rowIt) { + for (uint_fast64_t choice = 0; choice < rowCount; ++choice) { + typename storm::storage::SparseMatrix::const_rows row = this->transitionMatrix.getRow(nondeterministicChoiceIndices[state] + choice); + if (scheduler != nullptr) { // If the scheduler picked the current choice, we will not make it dotted, but highlight it. - if ((*scheduler)[state] == row) { + if ((*scheduler)[state] == choice) { highlightChoice = true; } else { highlightChoice = false; @@ -227,7 +216,7 @@ namespace storm { // For each nondeterministic choice, we draw an arrow to an intermediate node to better display // the grouping of transitions. - outStream << "\t\"" << state << "c" << row << "\" [shape = \"point\""; + outStream << "\t\"" << state << "c" << choice << "\" [shape = \"point\""; // If we were given a scheduler to highlight, we do so now. if (scheduler != nullptr) { @@ -237,7 +226,7 @@ namespace storm { } outStream << "];" << std::endl; - outStream << "\t" << state << " -> \"" << state << "c" << row << "\""; + outStream << "\t" << state << " -> \"" << state << "c" << choice << "\""; // If we were given a scheduler to highlight, we do so now. if (scheduler != nullptr) { @@ -250,9 +239,9 @@ namespace storm { outStream << ";" << std::endl; // Now draw all probabilitic arcs that belong to this nondeterminstic choice. - for (auto transitionIt = rowIt.begin(), transitionIte = rowIt.end(); transitionIt != transitionIte; ++transitionIt) { - if (subsystem == nullptr || subsystem->get(transitionIt.column())) { - outStream << "\t\"" << state << "c" << row << "\" -> " << transitionIt.column() << " [ label= \"" << transitionIt.value() << "\" ]"; + for (auto const& transition : row) { + if (subsystem == nullptr || subsystem->get(transition.column())) { + outStream << "\t\"" << state << "c" << choice << "\" -> " << transition.column() << " [ label= \"" << transition.value() << "\" ]"; // If we were given a scheduler to highlight, we do so now. if (scheduler != nullptr) { diff --git a/src/models/Dtmc.h b/src/models/Dtmc.h index 563eee78e..e56e6e1c1 100644 --- a/src/models/Dtmc.h +++ b/src/models/Dtmc.h @@ -159,19 +159,18 @@ public: } // 1. Get all necessary information from the old transition matrix - storm::storage::SparseMatrix const & origMat = this->getTransitionMatrix(); + storm::storage::SparseMatrix const& origMat = this->getTransitionMatrix(); // Iterate over all rows. Count the number of all transitions from the old system to be // transfered to the new one. Also build a mapping from the state number of the old system // to the state number of the new system. uint_fast64_t subSysTransitionCount = 0; - uint_fast64_t row = 0; uint_fast64_t newRow = 0; std::vector stateMapping; - for(auto iter = origMat.begin(); iter != origMat.end(); ++iter) { + for(uint_fast64_t row = 0; row < origMat.getRowCount(); ++row) { if(subSysStates.get(row)){ - for(auto colIter = iter.begin(); colIter != iter.end(); ++colIter) { - if(subSysStates.get(colIter.column())) { + for(auto& entry : origMat.getRow(row)) { + if(subSysStates.get(entry.column())) { subSysTransitionCount++; } } @@ -180,7 +179,6 @@ public: } else { stateMapping.push_back((uint_fast64_t) -1); } - row++; } // 2. Construct transition matrix @@ -188,40 +186,37 @@ public: // Take all states indicated by the vector as well as one additional state s_b as target of // all transitions that target a state that is not kept. uint_fast64_t const newStateCount = subSysStates.getNumberOfSetBits() + 1; - storm::storage::SparseMatrix newMat(newStateCount); - // The number of transitions of the new Dtmc is the number of transitions transfered + // The number of transitions of the new Dtmc is the number of transitions transfered // from the old one plus one transition for each state to s_b. - newMat.initialize(subSysTransitionCount + newStateCount); + storm::storage::SparseMatrix newMat(newStateCount, subSysTransitionCount + newStateCount); // Now fill the matrix. newRow = 0; - row = 0; T rest = 0; - for(auto iter = origMat.begin(); iter != origMat.end(); ++iter) { + for(uint_fast64_t row = 0; row < origMat.getRowCount(); ++row) { if(subSysStates.get(row)){ // Transfer transitions - for(auto colIter = iter.begin(); colIter != iter.end(); ++colIter) { - if(subSysStates.get(colIter.column())) { - newMat.addNextValue(newRow, stateMapping[colIter.column()], colIter.value()); + for(auto& entry : origMat.getRow(row)) { + if(subSysStates.get(entry.column())) { + newMat.addNextValue(newRow, stateMapping[entry.column()], entry.value()); } else { - rest += colIter.value(); + rest += entry.value(); } } // Insert the transition taking care of the remaining outgoing probability. newMat.addNextValue(newRow, newStateCount - 1, rest); - rest = (T) 0; + rest = storm::utility::constantZero(); newRow++; } - row++; } // Insert last transition: self loop on s_b - newMat.addNextValue(newStateCount - 1, newStateCount - 1, (T) 1); + newMat.addNextValue(newStateCount - 1, newStateCount - 1, storm::utility::constantOne()); - newMat.finalize(false); + newMat.finalize(); // 3. Take care of the labeling. storm::models::AtomicPropositionsLabeling newLabeling = storm::models::AtomicPropositionsLabeling(this->getStateLabeling(), subSysStates); @@ -250,27 +245,24 @@ public: boost::optional> newTransitionRewards; if(this->hasTransitionRewards()) { - storm::storage::SparseMatrix newTransRewards(newStateCount); - newTransRewards.initialize(subSysTransitionCount + newStateCount); + storm::storage::SparseMatrix newTransRewards(newStateCount, subSysTransitionCount + newStateCount); // Copy the rewards for the kept states newRow = 0; - row = 0; - for(auto iter = this->getTransitionRewardMatrix().begin(); iter != this->getTransitionRewardMatrix().end(); ++iter) { + for(uint_fast64_t row = 0; row < this->getTransitionRewardMatrix().getRowCount(); ++row) { if(subSysStates.get(row)){ // Transfer transition rewards - for(auto colIter = iter.begin(); colIter != iter.end(); ++colIter) { - if(subSysStates.get(colIter.column())) { - newTransRewards.addNextValue(newRow, stateMapping[colIter.column()], colIter.value()); + for(auto& entry : this->getTransitionRewardMatrix().getRow(row)) { + if(subSysStates.get(entry.column())) { + newTransRewards.addNextValue(newRow, stateMapping[entry.column()], entry.value()); } } // Insert the reward (e.g. 0) for the transition taking care of the remaining outgoing probability. - newTransRewards.addNextValue(newRow, newStateCount - 1, (T) 0); + newTransRewards.addNextValue(newRow, newStateCount - 1, storm::utility::constantZero()); newRow++; } - row++; } newTransitionRewards = newTransRewards; diff --git a/src/models/MarkovAutomaton.h b/src/models/MarkovAutomaton.h index fa21aa9a5..b52cc9701 100644 --- a/src/models/MarkovAutomaton.h +++ b/src/models/MarkovAutomaton.h @@ -127,8 +127,7 @@ namespace storm { uint_fast64_t newNumberOfRows = this->getNumberOfChoices() - numberOfHybridStates; // Create the matrix for the new transition relation and the corresponding nondeterministic choice vector. - storm::storage::SparseMatrix newTransitionMatrix(newNumberOfRows, this->getNumberOfStates()); - newTransitionMatrix.initialize(); + storm::storage::SparseMatrix newTransitionMatrix; std::vector newNondeterministicChoiceIndices(this->getNumberOfStates() + 1); // Now copy over all choices that need to be kept. @@ -142,19 +141,15 @@ namespace storm { // Record the new beginning of choices of this state. newNondeterministicChoiceIndices[state] = currentChoice; - typename storm::storage::SparseMatrix::ConstRowIterator rowIt = this->transitionMatrix.begin(this->nondeterministicChoiceIndices[state]), rowIte = this->transitionMatrix.end(this->nondeterministicChoiceIndices[state + 1] - 1); - // If we are currently treating a hybrid state, we need to skip its first choice. if (this->isHybridState(state)) { - ++rowIt; - // Remove the Markovian state marking. this->markovianStates.set(state, false); } - for (; rowIt != rowIte; ++rowIt) { - for (typename storm::storage::SparseMatrix::ConstIterator succIt = rowIt.begin(), succIte = rowIt.end(); succIt != succIte; ++succIt) { - newTransitionMatrix.insertNextValue(currentChoice, succIt.column(), succIt.value()); + for (uint_fast64_t row = this->nondeterministicChoiceIndices[state] + (this->isHybridState(state) ? 1 : 0); row < this->nondeterministicChoiceIndices[state + 1]; ++row) { + for (auto const& entry : this->transitionMatrix.getRow(row)) { + newTransitionMatrix.addNextValue(currentChoice, entry.column(), entry.value()); } ++currentChoice; } @@ -194,16 +189,17 @@ namespace storm { AbstractModel::writeDotToStream(outStream, includeLabeling, subsystem, firstValue, secondValue, stateColoring, colors, scheduler, false); // Write the probability distributions for all the states. - auto rowIt = this->transitionMatrix.begin(); for (uint_fast64_t state = 0, highestStateIndex = this->getNumberOfStates() - 1; state <= highestStateIndex; ++state) { uint_fast64_t rowCount = this->getNondeterministicChoiceIndices()[state + 1] - this->getNondeterministicChoiceIndices()[state]; bool highlightChoice = true; // For this, we need to iterate over all available nondeterministic choices in the current state. - for (uint_fast64_t row = 0; row < rowCount; ++row, ++rowIt) { + for (uint_fast64_t choice = 0; choice < rowCount; ++choice) { + typename storm::storage::SparseMatrix::const_rows row = this->transitionMatrix.getRow(choice); + if (scheduler != nullptr) { // If the scheduler picked the current choice, we will not make it dotted, but highlight it. - if ((*scheduler)[state] == row) { + if ((*scheduler)[state] == choice) { highlightChoice = true; } else { highlightChoice = false; @@ -212,10 +208,10 @@ namespace storm { // If it's not a Markovian state or the current row is the first choice for this state, then we // are dealing with a probabilitic choice. - if (!markovianStates.get(state) || row != 0) { + if (!markovianStates.get(state) || choice != 0) { // For each nondeterministic choice, we draw an arrow to an intermediate node to better display // the grouping of transitions. - outStream << "\t\"" << state << "c" << row << "\" [shape = \"point\""; + outStream << "\t\"" << state << "c" << choice << "\" [shape = \"point\""; // If we were given a scheduler to highlight, we do so now. if (scheduler != nullptr) { @@ -225,7 +221,7 @@ namespace storm { } outStream << "];" << std::endl; - outStream << "\t" << state << " -> \"" << state << "c" << row << "\""; + outStream << "\t" << state << " -> \"" << state << "c" << choice << "\""; // If we were given a scheduler to highlight, we do so now. if (scheduler != nullptr) { @@ -238,9 +234,9 @@ namespace storm { outStream << ";" << std::endl; // Now draw all probabilitic arcs that belong to this nondeterminstic choice. - for (auto transitionIt = rowIt.begin(), transitionIte = rowIt.end(); transitionIt != transitionIte; ++transitionIt) { - if (subsystem == nullptr || subsystem->get(transitionIt.column())) { - outStream << "\t\"" << state << "c" << row << "\" -> " << transitionIt.column() << " [ label= \"" << transitionIt.value() << "\" ]"; + for (auto& transition : row) { + if (subsystem == nullptr || subsystem->get(transition.column())) { + outStream << "\t\"" << state << "c" << choice << "\" -> " << transition.column() << " [ label= \"" << transition.value() << "\" ]"; // If we were given a scheduler to highlight, we do so now. if (scheduler != nullptr) { @@ -255,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 transitionIt = rowIt.begin(), transitionIte = rowIt.end(); transitionIt != transitionIte; ++transitionIt) { - if (subsystem == nullptr || subsystem->get(transitionIt.column())) { - outStream << "\t\"" << state << "\" -> " << transitionIt.column() << " [ label= \"" << transitionIt.value() << " (" << this->exitRates[state] << ")\" ]"; + for (auto& transition : row) { + if (subsystem == nullptr || subsystem->get(transition.column())) { + outStream << "\t\"" << state << "\" -> " << transition.column() << " [ label= \"" << transition.value() << " (" << this->exitRates[state] << ")\" ]"; } } } @@ -276,8 +272,8 @@ namespace storm { */ void turnRatesToProbabilities() { for (auto state : this->markovianStates) { - for (typename storm::storage::SparseMatrix::ValueIterator valIt = this->transitionMatrix.valueIteratorBegin(this->getNondeterministicChoiceIndices()[state]), valIte = this->transitionMatrix.valueIteratorEnd(this->getNondeterministicChoiceIndices()[state]); valIt != valIte; ++valIt) { - *valIt = *valIt / this->exitRates[state]; + for (typename storm::storage::SparseMatrix::iterator it = this->transitionMatrix.begin(this->getNondeterministicChoiceIndices()[state]), ite = this->transitionMatrix.begin(this->getNondeterministicChoiceIndices()[state + 1]); it != ite; ++it) { + it.value() /= this->exitRates[state]; } } } diff --git a/src/models/Mdp.h b/src/models/Mdp.h index 6ecea851a..66165c8f2 100644 --- a/src/models/Mdp.h +++ b/src/models/Mdp.h @@ -144,7 +144,6 @@ public: std::vector> const& choiceLabeling = this->getChoiceLabeling(); storm::storage::SparseMatrix transitionMatrix; - transitionMatrix.initialize(); std::vector nondeterministicChoiceIndices; std::vector> newChoiceLabeling; @@ -161,9 +160,8 @@ public: nondeterministicChoiceIndices.push_back(currentRow); } stateHasValidChoice = true; - typename storm::storage::SparseMatrix::Rows row = this->getTransitionMatrix().getRows(choice, choice); - for (typename storm::storage::SparseMatrix::ConstIterator rowIt = row.begin(), rowIte = row.end(); rowIt != rowIte; ++rowIt) { - transitionMatrix.insertNextValue(currentRow, rowIt.column(), rowIt.value(), true); + for (auto const& entry : this->getTransitionMatrix().getRow(choice)) { + transitionMatrix.addNextValue(currentRow, entry.column(), entry.value()); } newChoiceLabeling.emplace_back(choiceLabeling[choice]); ++currentRow; @@ -173,12 +171,12 @@ public: // If no choice of the current state may be taken, we insert a self-loop to the state instead. if (!stateHasValidChoice) { nondeterministicChoiceIndices.push_back(currentRow); - transitionMatrix.insertNextValue(currentRow, state, storm::utility::constantOne(), true); + transitionMatrix.addNextValue(currentRow, state, storm::utility::constantOne()); newChoiceLabeling.emplace_back(); ++currentRow; } } - transitionMatrix.finalize(true); + transitionMatrix.finalize(); nondeterministicChoiceIndices.push_back(currentRow); Mdp restrictedMdp(std::move(transitionMatrix), storm::models::AtomicPropositionsLabeling(this->getStateLabeling()), std::move(nondeterministicChoiceIndices), this->hasStateRewards() ? boost::optional>(this->getStateRewardVector()) : boost::optional>(), this->hasTransitionRewards() ? boost::optional>(this->getTransitionRewardMatrix()) : boost::optional>(), boost::optional>>(newChoiceLabeling)); diff --git a/src/parser/DeterministicSparseTransitionParser.cpp b/src/parser/DeterministicSparseTransitionParser.cpp index e270c7a44..f824dcd28 100644 --- a/src/parser/DeterministicSparseTransitionParser.cpp +++ b/src/parser/DeterministicSparseTransitionParser.cpp @@ -201,12 +201,7 @@ storm::storage::SparseMatrix DeterministicSparseTransitionParser(std::st * The number of non-zero elements is computed by firstPass(). */ LOG4CPLUS_INFO(logger, "Attempting to create matrix of size " << (maxStateId+1) << " x " << (maxStateId+1) << "."); - storm::storage::SparseMatrix resultMatrix(maxStateId + 1); - resultMatrix.initialize(nonZeroEntryCount); - if (!resultMatrix.isInitialized()) { - LOG4CPLUS_ERROR(logger, "Could not create matrix of size " << (maxStateId+1) << " x " << (maxStateId+1) << "."); - throw std::bad_alloc(); - } + storm::storage::SparseMatrix resultMatrix(maxStateId + 1, nonZeroEntryCount); int_fast64_t row, lastRow = -1, col; double val; diff --git a/src/parser/MarkovAutomatonSparseTransitionParser.h b/src/parser/MarkovAutomatonSparseTransitionParser.h index 0792b9c97..94542b64e 100644 --- a/src/parser/MarkovAutomatonSparseTransitionParser.h +++ b/src/parser/MarkovAutomatonSparseTransitionParser.h @@ -39,8 +39,7 @@ namespace storm { */ struct ResultType { - ResultType(FirstPassResult const& firstPassResult) : transitionMatrix(firstPassResult.numberOfChoices, firstPassResult.highestStateIndex + 1), nondeterministicChoiceIndices(firstPassResult.highestStateIndex + 2), markovianChoices(firstPassResult.numberOfChoices), markovianStates(firstPassResult.highestStateIndex + 1), exitRates(firstPassResult.highestStateIndex + 1) { - transitionMatrix.initialize(firstPassResult.numberOfNonzeroEntries); + ResultType(FirstPassResult const& firstPassResult) : transitionMatrix(firstPassResult.numberOfChoices, firstPassResult.highestStateIndex + 1, firstPassResult.numberOfNonzeroEntries), nondeterministicChoiceIndices(firstPassResult.highestStateIndex + 2), markovianChoices(firstPassResult.numberOfChoices), markovianStates(firstPassResult.highestStateIndex + 1), exitRates(firstPassResult.highestStateIndex + 1) { // Intentionally left empty. } diff --git a/src/parser/NondeterministicSparseTransitionParser.cpp b/src/parser/NondeterministicSparseTransitionParser.cpp index 31492f51e..1a44cffab 100644 --- a/src/parser/NondeterministicSparseTransitionParser.cpp +++ b/src/parser/NondeterministicSparseTransitionParser.cpp @@ -264,13 +264,7 @@ NondeterministicSparseTransitionParserResult_t NondeterministicSparseTransitionP * Those two values, as well as the number of nonzero elements, was been calculated in the first run. */ LOG4CPLUS_INFO(logger, "Attempting to create matrix of size " << choices << " x " << (maxnode+1) << " with " << nonzero << " entries."); - storm::storage::SparseMatrix matrix(choices, maxnode + 1); - matrix.initialize(nonzero); - if (!matrix.isInitialized()) { - LOG4CPLUS_ERROR(logger, "Could not create matrix of size " << choices << " x " << (maxnode+1) << "."); - throw std::bad_alloc(); - } - + storm::storage::SparseMatrix matrix(choices, maxnode + 1, nonzero); /* * Create row mapping. diff --git a/src/solver/AbstractNondeterministicLinearEquationSolver.h b/src/solver/AbstractNondeterministicLinearEquationSolver.h index 2929bb695..8d6b41acc 100644 --- a/src/solver/AbstractNondeterministicLinearEquationSolver.h +++ b/src/solver/AbstractNondeterministicLinearEquationSolver.h @@ -80,8 +80,7 @@ namespace storm { * @returns The solution vector x of the system of linear equations as the content of the parameter x. */ virtual void solveEquationSystem(bool minimize, storm::storage::SparseMatrix const& A, std::vector& x, std::vector const& b, std::vector const& nondeterministicChoiceIndices, std::vector* multiplyResult = nullptr, std::vector* newX = nullptr) const { -// LOG4CPLUS_INFO(logger, "Starting iterative solver."); - + // Set up the environment for the power method. bool multiplyResultMemoryProvided = true; if (multiplyResult == nullptr) { @@ -137,14 +136,6 @@ namespace storm { if (!multiplyResultMemoryProvided) { delete multiplyResult; } - -// // Check if the solver converged and issue a warning otherwise. -// if (converged) { -// LOG4CPLUS_INFO(logger, "Iterative solver converged after " << iterations << " iterations."); -// } else { -// LOG4CPLUS_WARN(logger, "Iterative solver did not converge."); -// } - } protected: diff --git a/src/storage/MaximalEndComponentDecomposition.cpp b/src/storage/MaximalEndComponentDecomposition.cpp index 2f9b8eba2..ed329c6ba 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 (typename storm::storage::SparseMatrix::ConstIndexIterator successorIt = transitionMatrix.constColumnIteratorBegin(choice), successorIte = transitionMatrix.constColumnIteratorEnd(choice); successorIt != successorIte; ++successorIt) { - if (!scc.contains(*successorIt)) { + for (auto& entry : transitionMatrix.getRow(choice)) { + if (!scc.contains(entry.column())) { choiceContainedInMEC = false; 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 (typename storm::storage::SparseMatrix::ConstIndexIterator predIt = backwardTransitions.constColumnIteratorBegin(state), predIte = backwardTransitions.constColumnIteratorEnd(state); predIt != predIte; ++predIt) { - if (scc.contains(*predIt)) { - statesToCheck.set(*predIt); + for (auto& entry : transitionMatrix.getRow(state)) { + if (scc.contains(entry.column())) { + statesToCheck.set(entry.column()); } } } @@ -144,8 +144,8 @@ namespace storm { std::vector containedChoices; for (uint_fast64_t choice = nondeterministicChoiceIndices[state]; choice < nondeterministicChoiceIndices[state + 1]; ++choice) { bool choiceContained = true; - for (typename storm::storage::SparseMatrix::ConstIndexIterator successorIt = transitionMatrix.constColumnIteratorBegin(choice), successorIte = transitionMatrix.constColumnIteratorEnd(choice); successorIt != successorIte; ++successorIt) { - if (!mecStateSet.contains(*successorIt)) { + for (auto& entry : transitionMatrix.getRow(choice)) { + if (!mecStateSet.contains(entry.column())) { choiceContained = false; break; } diff --git a/src/storage/SparseMatrix.cpp b/src/storage/SparseMatrix.cpp index 97b0849ea..b148c4b99 100644 --- a/src/storage/SparseMatrix.cpp +++ b/src/storage/SparseMatrix.cpp @@ -101,7 +101,7 @@ namespace storm { } template - SparseMatrix::SparseMatrix(uint_fast64_t rows, uint_fast64_t columns, uint_fast64_t entries) : rowCount(rows), columnCount(columns), entryCount(entries), internalStatus(UNINITIALIZED), valueStorage(), columnIndications(), rowIndications(), currentEntryCount(0), lastRow(0), lastColumn(0) { + SparseMatrix::SparseMatrix(uint_fast64_t rows, uint_fast64_t columns, uint_fast64_t entries) : rowCount(rows), columnCount(columns), entryCount(entries), valueStorage(), columnIndications(), rowIndications(), internalStatus(UNINITIALIZED), currentEntryCount(0), lastRow(0), lastColumn(0) { storagePreallocated = rows != 0 && columns != 0 && entries != 0; prepareInternalStorage(); } @@ -128,6 +128,11 @@ namespace storm { other.lastRow = 0; other.lastColumn = 0; } + + template + SparseMatrix::SparseMatrix(uint_fast64_t columnCount, std::vector const& rowIndications, std::vector const& columnIndications, std::vector const& values) : rowCount(rowIndications.size() - 1), columnCount(columnCount), entryCount(values.size()), valueStorage(values), columnIndications(columnIndications), rowIndications(rowIndications), internalStatus(INITIALIZED), currentEntryCount(0), lastRow(0), lastColumn(0) { + // Intentionally left empty. + } template SparseMatrix::SparseMatrix(uint_fast64_t columnCount, std::vector&& rowIndications, std::vector&& columnIndications, std::vector&& values) : rowCount(rowIndications.size() - 1), columnCount(columnCount), entryCount(values.size()), valueStorage(std::move(values)), columnIndications(std::move(columnIndications)), rowIndications(std::move(rowIndications)), internalStatus(INITIALIZED), currentEntryCount(0), lastRow(0), lastColumn(0) { @@ -155,6 +160,27 @@ namespace storm { return *this; } + template + SparseMatrix& SparseMatrix::operator=(SparseMatrix&& other) { + // Only perform assignment if source and target are not the same. + if (this != &other) { + rowCount = other.rowCount; + columnCount = other.columnCount; + entryCount = other.entryCount; + + valueStorage = std::move(other.valueStorage); + columnIndications = std::move(other.columnIndications); + rowIndications = std::move(other.rowIndications); + + internalStatus = other.internalStatus; + currentEntryCount = other.currentEntryCount; + lastRow = other.lastRow; + lastColumn = other.lastColumn; + } + + return *this; + } + template void SparseMatrix::addNextValue(uint_fast64_t row, uint_fast64_t column, T const& value) { // Depending on whether the internal data storage was preallocated or not, adding the value is done somewhat @@ -168,12 +194,12 @@ namespace storm { // Check that we did not move backwards wrt. the row. if (row < lastRow) { - throw storm::exceptions::InvalidArgumentException() << "Illegal call to SparseMatrix::addNextValue: adding an element in row " << row << ", but an element in row " << lastRow << " has already been added." << std::endl; + throw storm::exceptions::InvalidArgumentException() << "Illegal call to SparseMatrix::addNextValue: adding an element in row " << row << ", but an element in row " << lastRow << " has already been added."; } // Check that we did not move backwards wrt. to column. if (row == lastRow && column < lastColumn) { - throw storm::exceptions::InvalidArgumentException() << "Illegal call to SparseMatrix::addNextValue: adding an element in column " << column << " in row " << row << ", but an element in column " << lastColumn << " has already been added in that row." << std::endl; + throw storm::exceptions::InvalidArgumentException() << "Illegal call to SparseMatrix::addNextValue: adding an element in column " << column << " in row " << row << ", but an element in column " << lastColumn << " has already been added in that row."; } // If we switched to another row, we have to adjust the missing entries in the row indices vector. @@ -203,6 +229,8 @@ namespace storm { } else { valueStorage.push_back(value); columnIndications.push_back(column); + columnCount = column + 1; + rowCount = row + 1; } } @@ -295,6 +323,8 @@ namespace storm { // one given by the parameter and set all subsequent elements of this row to zero. *valuePtr = storm::utility::constantOne(); *columnPtr = column; + ++valuePtr; + ++columnPtr; for (; valuePtr != valuePtrEnd; ++valuePtr) { *valuePtr = storm::utility::constantZero(); *columnPtr = 0; @@ -531,7 +561,7 @@ namespace storm { uint_fast64_t rowCount = this->columnCount; uint_fast64_t columnCount = this->rowCount; - uint_fast64_t entryCount = this->nonZeroEntryCount; + uint_fast64_t entryCount = this->entryCount; std::vector rowIndications(rowCount + 1); std::vector columnIndications(entryCount); @@ -539,8 +569,7 @@ namespace storm { // First, we need to count how many entries each column has. for (uint_fast64_t i = 0; i < this->rowCount; ++i) { - typename storm::storage::SparseMatrix::Rows rows = this->getRow(i); - for (auto const& transition : rows) { + for (auto const& transition : this->getRow(i)) { if (transition.value() > 0) { ++rowIndications[transition.column() + 1]; } @@ -559,8 +588,7 @@ namespace storm { // Now we are ready to actually fill in the values of the transposed matrix. for (uint_fast64_t i = 0; i < this->rowCount; ++i) { - typename storm::storage::SparseMatrix::Rows rows = this->getRow(i); - for (auto& transition : rows) { + for (auto& transition : this->getRow(i)) { if (transition.value() > 0) { values[nextIndices[transition.column()]] = transition.value(); columnIndications[nextIndices[transition.column()]++] = i; @@ -568,11 +596,7 @@ namespace storm { } } - storm::storage::SparseMatrix transposedMatrix(rowCount, colCount, - nonZeroEntryCount, - std::move(rowIndications), - std::move(columnIndications), - std::move(values)); + storm::storage::SparseMatrix transposedMatrix(columnCount, std::move(rowIndications), std::move(columnIndications), std::move(values)); return transposedMatrix; } @@ -616,11 +640,10 @@ namespace storm { } template - void SparseMatrix::negateAllNonDiagonalElements() { - // Check if the matrix is square, because only then it makes sense to perform this - // transformation. + void SparseMatrix::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() << "SparseMatrix::invertDiagonal requires the Matrix to be square!"; + throw storm::exceptions::InvalidArgumentException() << "Illegal call to SparseMatrix::invertDiagonal: matrix is non-square."; } // Iterate over all rows and negate all the elements that are not on the diagonal. @@ -629,7 +652,27 @@ namespace storm { uint_fast64_t rowEnd = rowIndications[row + 1]; while (rowStart < rowEnd) { if (columnIndications[rowStart] != row) { - valueStorage[rowStart] = - valueStorage[rowStart]; + valueStorage[rowStart] = -valueStorage[rowStart]; + } + ++rowStart; + } + } + } + + template + void SparseMatrix::deleteDiagonalEntries() { + // Check if the matrix is square, because only then it makes sense to perform this transformation. + if (this->getRowCount() != this->getColumnCount()) { + throw storm::exceptions::InvalidArgumentException() << "Illegal call to SparseMatrix::deleteDiagonalEntries: matrix is non-square."; + } + + // Iterate over all rows and negate all the elements that are not on the diagonal. + for (uint_fast64_t row = 0; row < rowCount; ++row) { + uint_fast64_t rowStart = rowIndications[row]; + uint_fast64_t rowEnd = rowIndications[row + 1]; + while (rowStart < rowEnd) { + if (columnIndications[rowStart] == row) { + valueStorage[rowStart] = storm::utility::constantZero(); } ++rowStart; } @@ -638,23 +681,28 @@ namespace storm { template typename std::pair, storm::storage::SparseMatrix> SparseMatrix::getJacobiDecomposition() const { - uint_fast64_t rowCount = this->getRowCount(); - uint_fast64_t colCount = this->getColumnCount(); - if (rowCount != colCount) { - throw storm::exceptions::InvalidArgumentException() << "SparseMatrix::getJacobiDecomposition requires the Matrix to be square."; + if (rowCount != columnCount) { + throw storm::exceptions::InvalidArgumentException() << "Illegal call to SparseMatrix::invertDiagonal: matrix is non-square."; } storm::storage::SparseMatrix resultLU(*this); - storm::storage::SparseMatrix resultDinv(rowCount, colCount); - // no entries apart from those on the diagonal (rowCount) - resultDinv.initialize(rowCount); + resultLU.deleteDiagonalEntries(); - // constant 1 for diagonal inversion - T constOne = storm::utility::constantOne(); + storm::storage::SparseMatrix resultDinv(rowCount, columnCount, rowCount); - // copy diagonal entries to other matrix - for (uint_fast64_t i = 0; i < rowCount; ++i) { - resultDinv.addNextValue(i, i, constOne / resultLU.getValue(i, i)); - resultLU.getValue(i, i) = storm::utility::constantZero(); + // Copy entries to the appropriate matrices. + for (uint_fast64_t rowNumber = 0; rowNumber < rowCount; ++rowNumber) { + + // Because the matrix may have several entries on the diagonal, we need to sum them before we are able + // to invert the entry. + T diagonalValue = storm::utility::constantZero(); + for (const_iterator rowIt = this->begin(rowNumber), rowIte = this->end(rowNumber); rowIt != rowIte; ++rowIt) { + if (rowIt.column() == rowNumber) { + diagonalValue += rowIt.value(); + } else if (rowIt.column() > rowNumber) { + break; + } + } + resultDinv.addNextValue(rowNumber, rowNumber, storm::utility::constantOne() / diagonalValue); } resultDinv.finalize(); @@ -663,12 +711,11 @@ namespace storm { template std::vector SparseMatrix::getPointwiseProductRowSumVector(storm::storage::SparseMatrix const& otherMatrix) const { - // Prepare result. 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 given matrix does not have a non-zero element at this column position, or - // multiply the two entries and add the result to the corresponding position in the vector. + // Iterate over all elements of the current matrix and either continue with the next element in case the + // given matrix does not have a non-zero element at this column position, or multiply the two entries and + // add the result to the corresponding position in the vector. for (uint_fast64_t row = 0; row < rowCount && row < otherMatrix.rowCount; ++row) { for (uint_fast64_t element = rowIndications[row], nextOtherElement = otherMatrix.rowIndications[row]; element < rowIndications[row + 1] && nextOtherElement < otherMatrix.rowIndications[row + 1]; ++element) { if (columnIndications[element] < otherMatrix.columnIndications[nextOtherElement]) { @@ -692,13 +739,19 @@ namespace storm { #ifdef STORM_HAVE_INTELTBB tbb::parallel_for(tbb::blocked_range(0, result.size()), tbbHelper_MatrixRowVectorScalarProduct, std::vector, T>(this, &vector, &result)); #else - ConstRowIterator rowIt = this->begin(); - - for (auto resultIt = result.begin(), resultIte = result.end(); resultIt != resultIte; ++resultIt, ++rowIt) { - *resultIt = storm::utility::constantZero(); + typename std::vector::const_iterator valueIterator = valueStorage.begin(); + typename std::vector::const_iterator valueIteratorEnd; + typename std::vector::const_iterator columnIterator = columnIndications.begin(); + typename std::vector::const_iterator rowIterator = rowIndications.begin(); + typename std::vector::const_iterator rowIteratorEnd = rowIndications.end(); + typename std::vector::iterator resultIterator = result.begin(); + typename std::vector::iterator resultIteratorEnd = result.end(); + + for (; resultIterator != resultIteratorEnd; ++rowIterator, ++resultIterator) { + *resultIterator = storm::utility::constantZero(); - for (auto elementIt = rowIt.begin(), elementIte = rowIt.end(); elementIt != elementIte; ++elementIt) { - *resultIt += elementIt.value() * vector[elementIt.column()]; + for (valueIteratorEnd = valueIterator + (*(rowIterator + 1) - *rowIterator); valueIterator != valueIteratorEnd; ++valueIterator, ++columnIterator) { + *resultIterator += *valueIterator * vector[*columnIterator]; } } #endif @@ -707,95 +760,74 @@ namespace storm { template uint_fast64_t SparseMatrix::getSizeInMemory() const { uint_fast64_t size = sizeof(*this); + // Add value_storage size. size += sizeof(T) * valueStorage.capacity(); + // Add column_indications size. size += sizeof(uint_fast64_t) * columnIndications.capacity(); + // Add row_indications size. size += sizeof(uint_fast64_t) * rowIndications.capacity(); + return size; } template - typename SparseMatrix::Rows SparseMatrix::getRows(uint_fast64_t startRow, uint_fast64_t endRow) const { - return Rows(this->valueStorage.data() + this->rowIndications[startRow], this->columnIndications.data() + this->rowIndications[startRow], this->rowIndications[endRow + 1] - this->rowIndications[startRow]); - } - - template - typename SparseMatrix::MutableRows SparseMatrix::getMutableRows(uint_fast64_t startRow, uint_fast64_t endRow) { - return MutableRows(this->valueStorage.data() + this->rowIndications[startRow], this->columnIndications.data() + this->rowIndications[startRow], this->rowIndications[endRow + 1] - this->rowIndications[startRow]); + typename SparseMatrix::const_rows SparseMatrix::getRows(uint_fast64_t startRow, uint_fast64_t endRow) const { + return const_rows(this->valueStorage.data() + this->rowIndications[startRow], this->columnIndications.data() + this->rowIndications[startRow], this->rowIndications[endRow + 1] - this->rowIndications[startRow]); } - + template - typename SparseMatrix::MutableRows SparseMatrix::getMutableRow(uint_fast64_t row) { - return getMutableRows(row, row); + typename SparseMatrix::rows SparseMatrix::getRows(uint_fast64_t startRow, uint_fast64_t endRow) { + return rows(this->valueStorage.data() + this->rowIndications[startRow], this->columnIndications.data() + this->rowIndications[startRow], this->rowIndications[endRow + 1] - this->rowIndications[startRow]); } - + template - typename SparseMatrix::Rows SparseMatrix::getRow(uint_fast64_t row) const { + typename SparseMatrix::const_rows SparseMatrix::getRow(uint_fast64_t row) const { return getRows(row, row); } - - template - typename SparseMatrix::ConstRowIterator SparseMatrix::begin(uint_fast64_t initialRow) const { - return ConstRowIterator(this->valueStorage.data(), this->columnIndications.data(), this->rowIndications.data() + initialRow); - } - - template - typename SparseMatrix::ConstRowIterator SparseMatrix::end() const { - return ConstRowIterator(this->valueStorage.data(), this->columnIndications.data(), this->rowIndications.data() + rowCount); - } - - template - typename SparseMatrix::ConstRowIterator SparseMatrix::end(uint_fast64_t row) const { - return ConstRowIterator(this->valueStorage.data(), this->columnIndications.data(), this->rowIndications.data() + row + 1); - } - - template - typename SparseMatrix::ConstIndexIterator SparseMatrix::constColumnIteratorBegin(uint_fast64_t row) const { - return &(this->columnIndications[0]) + this->rowIndications[row]; - } - + template - typename SparseMatrix::ConstIndexIterator SparseMatrix::constColumnIteratorEnd() const { - return &(this->columnIndications[0]) + this->rowIndications[rowCount]; + typename SparseMatrix::rows SparseMatrix::getRow(uint_fast64_t row) { + return getRows(row, row); } - + template - typename SparseMatrix::ConstIndexIterator SparseMatrix::constColumnIteratorEnd(uint_fast64_t row) const { - return &(this->columnIndications[0]) + this->rowIndications[row + 1]; + typename SparseMatrix::const_iterator SparseMatrix::begin(uint_fast64_t row) const { + return const_iterator(this->valueStorage.data() + this->rowIndications[row], this->columnIndications.data() + this->rowIndications[row]); } - + template - typename SparseMatrix::ConstValueIterator SparseMatrix::constValueIteratorBegin(uint_fast64_t row) const { - return &(this->valueStorage[0]) + this->rowIndications[row]; + typename SparseMatrix::iterator SparseMatrix::begin(uint_fast64_t row) { + return iterator(this->valueStorage.data() + this->rowIndications[row], this->columnIndications.data() + this->rowIndications[row]); } template - typename SparseMatrix::ConstValueIterator SparseMatrix::constValueIteratorEnd() const { - return &(this->valueStorage[0]) + this->rowIndications[rowCount]; + typename SparseMatrix::const_iterator SparseMatrix::end(uint_fast64_t row) const { + return const_iterator(this->valueStorage.data() + this->rowIndications[row + 1], this->columnIndications.data() + this->rowIndications[row + 1]); } template - typename SparseMatrix::ConstValueIterator SparseMatrix::constValueIteratorEnd(uint_fast64_t row) const { - return &(this->valueStorage[0]) + this->rowIndications[row + 1]; + typename SparseMatrix::iterator SparseMatrix::end(uint_fast64_t row) { + return iterator(this->valueStorage.data() + this->rowIndications[row + 1], this->columnIndications.data() + this->rowIndications[row + 1]); } - + template - typename SparseMatrix::ValueIterator SparseMatrix::valueIteratorBegin(uint_fast64_t row) { - return &(this->valueStorage[0]) + this->rowIndications[row]; + typename SparseMatrix::const_iterator SparseMatrix::end() const { + return const_iterator(this->valueStorage.data() + this->rowIndications[rowCount], this->columnIndications.data() + this->rowIndications[rowCount]); } template - typename SparseMatrix::ValueIterator SparseMatrix::valueIteratorEnd(uint_fast64_t row) { - return &(this->valueStorage[0]) + this->rowIndications[row + 1]; + typename SparseMatrix::iterator SparseMatrix::end() { + return iterator(this->valueStorage.data() + this->rowIndications[rowCount], this->columnIndications.data() + this->rowIndications[rowCount]); } - + template T SparseMatrix::getRowSum(uint_fast64_t row) const { T sum = storm::utility::constantZero(); - for (auto it = this->constValueIteratorBegin(row), ite = this->constValueIteratorEnd(row); it != ite; ++it) { - sum += *it; + for (typename std::vector::const_iterator valueIterator = valueStorage.begin() + rowIndications[row], valueIteratorEnd = valueStorage.begin() + rowIndications[row + 1]; valueIterator != valueIteratorEnd; ++valueIterator) { + sum += *valueIterator; } return sum; } @@ -809,8 +841,7 @@ namespace storm { // Check the subset property for all rows individually. for (uint_fast64_t row = 0; row < this->getRowCount(); ++row) { for (uint_fast64_t elem = rowIndications[row], elem2 = matrix.rowIndications[row]; elem < rowIndications[row + 1] && elem < matrix.rowIndications[row + 1]; ++elem) { - // Skip over all entries of the other matrix that are before the current entry in - // the current matrix. + // Skip over all entries of the other matrix that are before the current entry in the current matrix. while (elem2 < matrix.rowIndications[row + 1] && matrix.columnIndications[elem2] < columnIndications[elem]) { ++elem2; } @@ -823,73 +854,51 @@ namespace storm { } template - std::string SparseMatrix::toString(std::vector const* rowGroupIndices) const { - std::stringstream result; - uint_fast64_t currentNondeterministicChoiceIndex = 0; - + std::ostream& operator<<(std::ostream& out, SparseMatrix const& matrix) { // Print column numbers in header. - result << "\t\t"; - for (uint_fast64_t i = 0; i < colCount; ++i) { - result << i << "\t"; + out << "\t\t"; + for (uint_fast64_t i = 0; i < matrix.columnCount; ++i) { + out << i << "\t"; } - result << std::endl; + out << std::endl; // Iterate over all rows. - for (uint_fast64_t i = 0; i < rowCount; ++i) { - uint_fast64_t nextIndex = rowIndications[i]; - - // If we need to group rows, print a dashed line in case we have moved to the next group of rows. - if (rowGroupIndices != nullptr) { - if (i == (*rowGroupIndices)[currentNondeterministicChoiceIndex]) { - if (i != 0) { - result << "\t(\t"; - for (uint_fast64_t j = 0; j < colCount - 2; ++j) { - result << "----"; - if (j == 1) { - result << "\t" << currentNondeterministicChoiceIndex << "\t"; - } - } - result << "\t)" << std::endl; - } - ++currentNondeterministicChoiceIndex; - } - } + for (uint_fast64_t i = 0; i < matrix.rowCount; ++i) { + uint_fast64_t nextIndex = matrix.rowIndications[i]; // Print the actual row. - result << i << "\t(\t"; + out << i << "\t(\t"; uint_fast64_t currentRealIndex = 0; - while (currentRealIndex < colCount) { - if (nextIndex < rowIndications[i + 1] && currentRealIndex == columnIndications[nextIndex]) { - result << std::setprecision(8) << valueStorage[nextIndex] << "\t"; + while (currentRealIndex < matrix.columnCount) { + if (nextIndex < matrix.rowIndications[i + 1] && currentRealIndex == matrix.columnIndications[nextIndex]) { + out << matrix.valueStorage[nextIndex] << "\t"; ++nextIndex; } else { - result << "0\t"; + out << "0\t"; } ++currentRealIndex; } - result << "\t)\t" << i << std::endl; + out << "\t)\t" << i << std::endl; } // Print column numbers in footer. - result << "\t\t"; - for (uint_fast64_t i = 0; i < colCount; ++i) { - result << i << "\t"; + out << "\t\t"; + for (uint_fast64_t i = 0; i < matrix.columnCount; ++i) { + out << i << "\t"; } - result << std::endl; + out << std::endl; - // Return final result. - return result.str(); + return out; } template - std::size_t SparseMatrix::getHash() const { + std::size_t SparseMatrix::hash() const { std::size_t result = 0; boost::hash_combine(result, rowCount); - boost::hash_combine(result, colCount); - boost::hash_combine(result, nonZeroEntryCount); - boost::hash_combine(result, currentSize); - boost::hash_combine(result, lastRow); + boost::hash_combine(result, columnCount); + boost::hash_combine(result, entryCount); + boost::hash_combine(result, internalStatus); boost::hash_combine(result, boost::hash_range(valueStorage.begin(), valueStorage.end())); boost::hash_combine(result, boost::hash_range(columnIndications.begin(), columnIndications.end())); boost::hash_combine(result, boost::hash_range(rowIndications.begin(), rowIndications.end())); @@ -898,44 +907,23 @@ namespace storm { } template - void SparseMatrix::triggerErrorState() { - setState(MatrixStatus::Error); - } - - template - void SparseMatrix::setState(const MatrixStatus new_state) { - internalStatus = (internalStatus == MatrixStatus::Error) ? internalStatus : new_state; - } - - template - bool SparseMatrix::prepareInternalStorage(bool initializeElements) { - if (initializeElements) { - // Set up the arrays for the elements that are not on the diagonal. - valueStorage.resize(nonZeroEntryCount, storm::utility::constantZero()); - columnIndications.resize(nonZeroEntryCount, 0); - - // Set up the rowIndications vector and reserve one element more than there are rows in - // order to put a sentinel element at the end, which eases iteration process. - rowIndications.resize(rowCount + 1, 0); - - // Return whether all the allocations could be made without error. - return ((valueStorage.capacity() >= nonZeroEntryCount) && (columnIndications.capacity() >= nonZeroEntryCount) - && (rowIndications.capacity() >= (rowCount + 1))); - } else { - // If it was not requested to initialize the elements, we simply reserve the space. - valueStorage.reserve(nonZeroEntryCount); - columnIndications.reserve(nonZeroEntryCount); - rowIndications.reserve(rowCount + 1); - return true; + void SparseMatrix::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); + rowIndications = std::vector(rowCount + 1, 0); } } - // Explicit instantiations of specializations of this template here. + // Explicitly instantiate the matrix and the nested classes. + template class SparseMatrix::BaseIterator; + template class SparseMatrix::BaseIterator; template class SparseMatrix; + template class SparseMatrix::BaseIterator; + template class SparseMatrix::BaseIterator; template class SparseMatrix; - // Functions of the tbbHelper_MatrixRowVectorScalarProduct friend class. - #ifdef STORM_HAVE_INTELTBB template diff --git a/src/storage/SparseMatrix.h b/src/storage/SparseMatrix.h index 36413c08a..7b7a908b3 100644 --- a/src/storage/SparseMatrix.h +++ b/src/storage/SparseMatrix.h @@ -269,6 +269,16 @@ namespace storm { */ SparseMatrix(SparseMatrix&& other); + /*! + * Constructs a sparse matrix by copying the given contents. + * + * @param columnCount The number of columns of the matrix. + * @param rowIndications The row indications vector of the matrix to be constructed. + * @param columnIndications The column indications vector of the matrix to be constructed. + * @param values The vector containing the values of the entries in the matrix. + */ + SparseMatrix(uint_fast64_t columnCount, std::vector const& rowIndications, std::vector const& columnIndications, std::vector const& values); + /*! * Constructs a sparse matrix by moving the given contents. * @@ -468,6 +478,11 @@ namespace storm { */ void negateAllNonDiagonalEntries(); + /*! + * Sets all diagonal elements to zero. + */ + void deleteDiagonalEntries(); + /*! * Calculates the Jacobi decomposition of this sparse matrix. For this operation, the matrix must be square. * @@ -592,8 +607,9 @@ namespace storm { * @return True iff the current matrix is a submatrix of the given matrix. */ bool isSubmatrixOf(SparseMatrix const& matrix) const; - - friend std::ostream& operator<<(std::ostream& out, BitVector const& bitVector); + + template + friend std::ostream& operator<<(std::ostream& out, SparseMatrix const& matrix); /*! * Returns the size of the matrix in memory measured in bytes. diff --git a/src/storage/StronglyConnectedComponentDecomposition.cpp b/src/storage/StronglyConnectedComponentDecomposition.cpp index 2d3e462e7..4a43a6d44 100644 --- a/src/storage/StronglyConnectedComponentDecomposition.cpp +++ b/src/storage/StronglyConnectedComponentDecomposition.cpp @@ -91,7 +91,7 @@ namespace storm { // all successors of a particular state are considered. std::vector recursionStateStack; recursionStateStack.reserve(lowlinks.size()); - std::vector::ConstIterator> recursionIteratorStack; + std::vector::const_iterator> recursionIteratorStack; recursionIteratorStack.reserve(lowlinks.size()); std::vector statesInStack(lowlinks.size()); @@ -114,7 +114,7 @@ namespace storm { recursionStepForward: while (!recursionStateStack.empty()) { uint_fast64_t currentState = recursionStateStack.back(); - typename storm::storage::SparseMatrix::ConstIterator successorIt = recursionIteratorStack.back(); + typename storm::storage::SparseMatrix::const_iterator successorIt = recursionIteratorStack.back(); // Perform the treatment of newly discovered state as defined by Tarjan's algorithm. visitedStates.set(currentState, true); diff --git a/src/utility/counterexamples.h b/src/utility/counterexamples.h index bd441a048..23996aaed 100644 --- a/src/utility/counterexamples.h +++ b/src/utility/counterexamples.h @@ -34,9 +34,9 @@ namespace storm { // Initially, put all predecessors of target states in the worklist and empty the analysis information them. for (auto state : psiStates) { analysisInformation[state] = std::set(); - for (typename storm::storage::SparseMatrix::ConstIndexIterator predecessorIt = backwardTransitions.constColumnIteratorBegin(state), predecessorIte = backwardTransitions.constColumnIteratorEnd(state); predecessorIt != predecessorIte; ++predecessorIt) { - if (*predecessorIt != state) { - worklist.push(std::make_pair(*predecessorIt, state)); + for (auto& predecessorEntry : backwardTransitions.getRow(state)) { + if (predecessorEntry.column() != state) { + worklist.push(std::make_pair(predecessorEntry.column(), state)); } } } @@ -56,8 +56,8 @@ namespace storm { storm::storage::VectorSet tmpIntersection; bool choiceTargetsTargetState = false; - for (typename storm::storage::SparseMatrix::ConstIndexIterator successorIt = transitionMatrix.constColumnIteratorBegin(currentChoice), successorIte = transitionMatrix.constColumnIteratorEnd(currentChoice); successorIt != successorIte; ++successorIt) { - if (*successorIt == targetState) { + for (auto& entry : transitionMatrix.getRow(currentChoice)) { + if (entry.column() == targetState) { choiceTargetsTargetState = true; break; } @@ -76,10 +76,10 @@ namespace storm { // If the analysis information changed, we need to update it and put all the predecessors of this // state in the worklist. if (analysisInformation[currentState].size() != analysisInformationSizeBefore) { - for (typename storm::storage::SparseMatrix::ConstIndexIterator predecessorIt = backwardTransitions.constColumnIteratorBegin(currentState), predecessorIte = backwardTransitions.constColumnIteratorEnd(currentState); predecessorIt != predecessorIte; ++predecessorIt) { + for (auto& predecessorEntry : backwardTransitions.getRow(currentState)) { // Only put the predecessor in the worklist if it's not already a target state. - if (!psiStates.get(*predecessorIt)) { - worklist.push(std::make_pair(*predecessorIt, currentState)); + if (!psiStates.get(predecessorEntry.column())) { + worklist.push(std::make_pair(predecessorEntry.column(), currentState)); } } } diff --git a/src/utility/graph.h b/src/utility/graph.h index 3fd0c6693..dfcb19e4a 100644 --- a/src/utility/graph.h +++ b/src/utility/graph.h @@ -81,17 +81,17 @@ namespace storm { stepStack.pop_back(); } - for (auto predecessorIt = backwardTransitions.constColumnIteratorBegin(currentState), predecessorIte = backwardTransitions.constColumnIteratorEnd(currentState); predecessorIt != predecessorIte; ++predecessorIt) { - if (phiStates.get(*predecessorIt) && (!statesWithProbabilityGreater0.get(*predecessorIt) || (useStepBound && remainingSteps[*predecessorIt] < currentStepBound - 1))) { + for (auto& entry : backwardTransitions.getRow(currentState)) { + if (phiStates.get(entry.column()) && (!statesWithProbabilityGreater0.get(entry.column()) || (useStepBound && remainingSteps[entry.column()] < currentStepBound - 1))) { // If we don't have a bound on the number of steps to take, just add the state to the stack. if (!useStepBound) { - statesWithProbabilityGreater0.set(*predecessorIt, true); - stack.push_back(*predecessorIt); + statesWithProbabilityGreater0.set(entry.column(), true); + stack.push_back(entry.column()); } 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[*predecessorIt] = currentStepBound - 1; - statesWithProbabilityGreater0.set(*predecessorIt, true); - stack.push_back(*predecessorIt); + remainingSteps[entry.column()] = currentStepBound - 1; + statesWithProbabilityGreater0.set(entry.column(), true); + stack.push_back(entry.column()); stepStack.push_back(currentStepBound - 1); } } @@ -212,17 +212,17 @@ namespace storm { stepStack.pop_back(); } - for (auto predecessorIt = backwardTransitions.constColumnIteratorBegin(currentState), predecessorIte = backwardTransitions.constColumnIteratorEnd(currentState); predecessorIt != predecessorIte; ++predecessorIt) { - if (phiStates.get(*predecessorIt) && (!statesWithProbabilityGreater0.get(*predecessorIt) || (useStepBound && remainingSteps[*predecessorIt] < currentStepBound - 1))) { + for (auto& entry : backwardTransitions.getRow(currentState)) { + if (phiStates.get(entry.column()) && (!statesWithProbabilityGreater0.get(entry.column()) || (useStepBound && remainingSteps[entry.column()] < currentStepBound - 1))) { // If we don't have a bound on the number of steps to take, just add the state to the stack. if (!useStepBound) { - statesWithProbabilityGreater0.set(*predecessorIt, true); - stack.push_back(*predecessorIt); + statesWithProbabilityGreater0.set(entry.column(), true); + stack.push_back(entry.column()); } 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[*predecessorIt] = currentStepBound - 1; - statesWithProbabilityGreater0.set(*predecessorIt, true); - stack.push_back(*predecessorIt); + remainingSteps[entry.column()] = currentStepBound - 1; + statesWithProbabilityGreater0.set(entry.column(), true); + stack.push_back(entry.column()); stepStack.push_back(currentStepBound - 1); } } @@ -291,14 +291,14 @@ namespace storm { currentState = stack.back(); stack.pop_back(); - for(auto predecessorIt = backwardTransitions.constColumnIteratorBegin(currentState), predecessorIte = backwardTransitions.constColumnIteratorEnd(currentState); predecessorIt != predecessorIte; ++predecessorIt) { - if (phiStates.get(*predecessorIt) && !nextStates.get(*predecessorIt)) { + for (auto& predecessorEntry : backwardTransitions.getRow(currentState)) { + if (phiStates.get(predecessorEntry.column()) && !nextStates.get(predecessorEntry.column())) { // Check whether the predecessor has only successors in the current state set for one of the // nondeterminstic choices. - for (auto row = nondeterministicChoiceIndices[*predecessorIt]; row < nondeterministicChoiceIndices[*predecessorIt + 1]; ++row) { + for (auto row = nondeterministicChoiceIndices[predecessorEntry.column()]; row < nondeterministicChoiceIndices[predecessorEntry.column() + 1]; ++row) { bool allSuccessorsInCurrentStates = true; - for (auto targetIt = transitionMatrix.constColumnIteratorBegin(row), targetIte = transitionMatrix.constColumnIteratorEnd(row); targetIt != targetIte; ++targetIt) { - if (!currentStates.get(*targetIt)) { + for (auto& targetEntry : transitionMatrix.getRow(row)) { + if (!currentStates.get(targetEntry.column())) { allSuccessorsInCurrentStates = false; 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(*predecessorIt, true); - stack.push_back(*predecessorIt); + nextStates.set(predecessorEntry.column(), true); + stack.push_back(predecessorEntry.column()); break; } } @@ -402,15 +402,15 @@ namespace storm { stepStack.pop_back(); } - for(auto predecessorIt = backwardTransitions.constColumnIteratorBegin(currentState), predecessorIte = backwardTransitions.constColumnIteratorEnd(currentState); predecessorIt != predecessorIte; ++predecessorIt) { - if (phiStates.get(*predecessorIt) && (!statesWithProbabilityGreater0.get(*predecessorIt) || (useStepBound && remainingSteps[*predecessorIt] < currentStepBound - 1))) { + for(auto& predecessorEntry : backwardTransitions.getRow(currentState)) { + if (phiStates.get(predecessorEntry.column()) && (!statesWithProbabilityGreater0.get(predecessorEntry.column()) || (useStepBound && remainingSteps[predecessorEntry.column()] < currentStepBound - 1))) { // Check whether the predecessor has at least one successor in the current state set for every // nondeterministic choice. bool addToStatesWithProbabilityGreater0 = true; - for (auto row = nondeterministicChoiceIndices[*predecessorIt]; row < nondeterministicChoiceIndices[*predecessorIt + 1]; ++row) { + for (auto row = nondeterministicChoiceIndices[predecessorEntry.column()]; row < nondeterministicChoiceIndices[predecessorEntry.column() + 1]; ++row) { bool hasAtLeastOneSuccessorWithProbabilityGreater0 = false; - for (auto successorIt = transitionMatrix.constColumnIteratorBegin(row), successorIte = transitionMatrix.constColumnIteratorEnd(row); successorIt != successorIte; ++successorIt) { - if (statesWithProbabilityGreater0.get(*successorIt)) { + for (auto& successorEntry : transitionMatrix.getRow(row)) { + if (statesWithProbabilityGreater0.get(successorEntry.column())) { hasAtLeastOneSuccessorWithProbabilityGreater0 = true; 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(*predecessorIt, true); - stack.push_back(*predecessorIt); + statesWithProbabilityGreater0.set(predecessorEntry.column(), true); + stack.push_back(predecessorEntry.column()); } 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[*predecessorIt] = currentStepBound - 1; - statesWithProbabilityGreater0.set(*predecessorIt, true); - stack.push_back(*predecessorIt); + remainingSteps[predecessorEntry.column()] = currentStepBound - 1; + statesWithProbabilityGreater0.set(predecessorEntry.column(), true); + stack.push_back(predecessorEntry.column()); stepStack.push_back(currentStepBound - 1); } } @@ -502,17 +502,15 @@ namespace storm { currentState = stack.back(); stack.pop_back(); - for(auto predecessorIt = backwardTransitions.constColumnIteratorBegin(currentState), predecessorIte = backwardTransitions.constColumnIteratorEnd(currentState); predecessorIt != predecessorIte; ++predecessorIt) { - if (phiStates.get(*predecessorIt) && !nextStates.get(*predecessorIt)) { + for(auto& predecessorEntry : backwardTransitions.getRow(currentState)) { + if (phiStates.get(predecessorEntry.column()) && !nextStates.get(predecessorEntry.column())) { // Check whether the predecessor has only successors in the current state set for all of the // nondeterminstic choices. bool allSuccessorsInCurrentStatesForAllChoices = true; - for (auto row = nondeterministicChoiceIndices[*predecessorIt]; row < nondeterministicChoiceIndices[*predecessorIt + 1]; ++row) { - for (auto successorIt = transitionMatrix.constColumnIteratorBegin(row), successorIte = transitionMatrix.constColumnIteratorEnd(row); successorIt != successorIte; ++successorIt) { - if (!currentStates.get(*successorIt)) { - allSuccessorsInCurrentStatesForAllChoices = false; - goto afterCheckLoop; - } + for (auto& successorEntry : transitionMatrix.getRows(nondeterministicChoiceIndices[predecessorEntry.column()], nondeterministicChoiceIndices[predecessorEntry.column() + 1] - 1)) { + if (!currentStates.get(successorEntry.column())) { + allSuccessorsInCurrentStatesForAllChoices = false; + goto afterCheckLoop; } } @@ -521,8 +519,8 @@ namespace storm { // add it to the set of states for the next iteration and perform a backward search from // that state. if (allSuccessorsInCurrentStatesForAllChoices) { - nextStates.set(*predecessorIt, true); - stack.push_back(*predecessorIt); + nextStates.set(predecessorEntry.column(), true); + stack.push_back(predecessorEntry.column()); } } } @@ -541,7 +539,6 @@ namespace storm { template std::pair performProb01Min(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { std::pair result; - result.first = performProb0E(transitionMatrix, nondeterministicChoiceIndices, backwardTransitions, phiStates, psiStates); result.second = performProb1A(transitionMatrix, nondeterministicChoiceIndices, backwardTransitions, phiStates, psiStates); return result; @@ -584,7 +581,7 @@ namespace storm { // Prepare the stacks needed for recursion. std::vector recursionStack; recursionStack.reserve(matrix.getRowCount()); - std::vector::ConstIndexIterator> iteratorRecursionStack; + std::vector::const_iterator> iteratorRecursionStack; iteratorRecursionStack.reserve(numberOfStates); // Perform a depth-first search over the given transitions and record states in the reverse order they were visited. @@ -592,27 +589,23 @@ namespace storm { for (uint_fast64_t state = 0; state < numberOfStates; ++state) { if (!visitedStates.get(state)) { recursionStack.push_back(state); - iteratorRecursionStack.push_back(matrix.constColumnIteratorBegin(state)); + iteratorRecursionStack.push_back(matrix.begin(state)); recursionStepForward: while (!recursionStack.empty()) { uint_fast64_t currentState = recursionStack.back(); - typename storm::storage::SparseMatrix::ConstIndexIterator successorIt = iteratorRecursionStack.back(); + typename storm::storage::SparseMatrix::const_iterator successorIterator = iteratorRecursionStack.back(); visitedStates.set(currentState, true); recursionStepBackward: - for (; successorIt != matrix.constColumnIteratorEnd(currentState); ++successorIt) { - if (!visitedStates.get(*successorIt)) { + for (; successorIterator != matrix.end(currentState); ++successorIterator) { + if (!visitedStates.get(successorIterator.column())) { // Put unvisited successor on top of our recursion stack and remember that. - recursionStack.push_back(*successorIt); - - // Save current iterator position so we can continue where we left off later. - iteratorRecursionStack.pop_back(); - iteratorRecursionStack.push_back(successorIt + 1); + recursionStack.push_back(successorIterator.column()); // Also, put initial value for iterator on corresponding recursion stack. - iteratorRecursionStack.push_back(matrix.constColumnIteratorBegin(*successorIt)); + iteratorRecursionStack.push_back(matrix.begin(successorIterator.column())); goto recursionStepForward; } @@ -630,7 +623,7 @@ namespace storm { // original recursive call. if (recursionStack.size() > 0) { currentState = recursionStack.back(); - successorIt = iteratorRecursionStack.back(); + successorIterator = iteratorRecursionStack.back(); goto recursionStepBackward; } @@ -674,7 +667,7 @@ namespace storm { // Set the probability to 1 for all starting states. #ifdef LINUX - boost::container::set, DistanceCompare> probabilityStateSet; + boost::container::set, DistanceCompare> probabilityStateSet; #else std::set, DistanceCompare> probabilityStateSet; #endif @@ -690,7 +683,7 @@ namespace storm { probabilityStateSet.erase(probabilityStateSet.begin()); // Now check the new distances for all successors of the current state. - typename storm::storage::SparseMatrix::Rows row = transitions.getRows(probabilityStatePair.second, probabilityStatePair.second); + typename storm::storage::SparseMatrix::Rows row = transitions.getRow(probabilityStatePair.second); for (auto& transition : row) { // Only follow the transition if it lies within the filtered states. if (filterStates != nullptr && filterStates->get(transition.column())) { diff --git a/src/utility/matrix.h b/src/utility/matrix.h index e5520ac35..47e36fb44 100644 --- a/src/utility/matrix.h +++ b/src/utility/matrix.h @@ -31,13 +31,13 @@ namespace storm { } // If a valid choice for this state is defined, we copy over the corresponding entries. - typename storm::storage::SparseMatrix::Rows selectedRow = transitionMatrix.getRow(choice); + typename storm::storage::SparseMatrix::const_rows selectedRow = transitionMatrix.getRow(choice); for (auto entry : selectedRow) { - result.insertNextValue(state, entry.column(), entry.value()); + result.addNextValue(state, entry.column(), entry.value()); } } else { // If no valid choice for the state is defined, we insert a self-loop. - result.insertNextValue(state, state, storm::utility::constantOne()); + result.addNextValue(state, state, storm::utility::constantOne()); } } diff --git a/src/utility/vector.h b/src/utility/vector.h index 7a8902b2d..ee0c96f41 100644 --- a/src/utility/vector.h +++ b/src/utility/vector.h @@ -1,7 +1,6 @@ #ifndef STORM_UTILITY_VECTOR_H_ #define STORM_UTILITY_VECTOR_H_ -#include "Eigen/Core" #include "constants.h" #include #include @@ -43,21 +42,7 @@ namespace storm { vector[position] = value; } } - - /*! - * Sets the provided value at the provided positions in the given vector. - * - * @param vector The vector in which the value is to be set. - * @param positions The positions at which the value is to be set. - * @param value The value that is to be set. - */ - template - void setVectorValues(Eigen::Matrix& eigenVector, storm::storage::BitVector const& positions, T value) { - for (auto position : positions) { - eigenVector(position, 0) = value; - } - } - + /*! * Selects the elements from a vector at the specified positions and writes them consecutively into another vector. * @param vector The vector into which the selected elements are to be written. diff --git a/test/functional/eigen/EigenSparseMatrixTest.cpp b/test/functional/eigen/EigenSparseMatrixTest.cpp deleted file mode 100644 index b03ada475..000000000 --- a/test/functional/eigen/EigenSparseMatrixTest.cpp +++ /dev/null @@ -1,79 +0,0 @@ -#include "gtest/gtest.h" - -#include "Eigen/Sparse" -#include "src/exceptions/InvalidArgumentException.h" -#include - -TEST(EigenSparseMatrixTest, BasicReadWriteTest) { - // 25 rows, 50 non zero entries - Eigen::SparseMatrix esm(25, 25); - - int values[50] = { - 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, - 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, - 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, - 30, 31, 32, 33, 34, 35, 36, 37, 38, 39, - 40, 41, 42, 43, 44, 45, 46, 47, 48, 49 - }; - int position_row[50] = { - 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, - 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, - 2, 2, 2, 2, /* first row empty, one full row 25 minus the diagonal entry */ - 4, 4, /* one empty row, then first and last column */ - 13, 13, 13, 13, /* a few empty rows, middle columns */ - 24, 24, 24, 24, 24, 24, 24, 24, 24, 24, - 24, 24, 24, 24, 24, 24, 24, 24, 24, 24 /* second to last row */ - }; - int position_col[50] = { - 1, 3, 4, 5, 6, 7, 8, 9, 10, - 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, - 21, 22, 23, 24, 25, /* first row empty, one full row a 25 */ - 1, 25, /* one empty row, then first and last column */ - 16, 17, 18, 19, /* a few empty rows, middle columns */ - 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, - 14, 15, 16, 17, 18, 19, 20, 21, 22, 23 /* second to last row */ - }; - - typedef Eigen::Triplet ETd; - std::vector tripletList; - tripletList.reserve(50); - - for (int i = 0; i < 50; ++i) { - ASSERT_NO_THROW(tripletList.push_back(ETd(position_row[i] - 1, position_col[i] - 1, values[i]))); - } - - ASSERT_NO_THROW(esm.setFromTriplets(tripletList.begin(), tripletList.end())); - - for (int i = 0; i < 50; ++i) { - Eigen::SparseMatrix::InnerIterator it(esm, position_row[i] - 1); - ASSERT_EQ(values[i], esm.coeff(position_row[i] - 1, position_col[i] - 1)); - } - - // test for a few of the empty rows - for (int row = 15; row < 24; ++row) { - for (int col = 1; col <= 25; ++col) { - ASSERT_EQ(0, esm.coeff(row - 1, col - 1)); - } - } -} - -TEST(EigenSparseMatrixTest, BoundaryTest) { - Eigen::SparseMatrix esm(10, 10); - esm.reserve(100); - int values[100]; - for (uint_fast32_t i = 0; i < 100; ++i) { - values[i] = i; - } - - for (uint_fast32_t row = 0; row < 10; ++row) { - for (uint_fast32_t col = 0; col < 10; ++col) { - ASSERT_NO_THROW(esm.insert(row, col) = values[row * 10 + col]); - } - } - - for (uint_fast32_t row = 0; row < 10; ++row) { - for (uint_fast32_t col = 0; col < 10; ++col) { - ASSERT_EQ(values[row * 10 + col], esm.coeff(row, col)); - } - } -} diff --git a/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp index 228791409..d724ef23d 100644 --- a/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp @@ -116,7 +116,6 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, SynchronousLeader) { storm::parser::AutoParser parser(STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader4_8.tra", STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader4_8.lab", "", STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader4_8.pick.trans.rew"); ASSERT_EQ(parser.getType(), storm::models::DTMC); - std::shared_ptr> dtmc = parser.getModel>(); ASSERT_EQ(dtmc->getNumberOfStates(), 12400ull); diff --git a/test/functional/parser/ReadTraFileTest.cpp b/test/functional/parser/ReadTraFileTest.cpp deleted file mode 100644 index e6ff86456..000000000 --- a/test/functional/parser/ReadTraFileTest.cpp +++ /dev/null @@ -1,77 +0,0 @@ -/* - * ReadTraFileTest.cpp - * - * Created on: 16.08.2012 - * Author: Thomas Heinemann - */ - -#include "gtest/gtest.h" -#include "storm-config.h" -#include "src/storage/SparseMatrix.h" -#include "src/parser/DeterministicSparseTransitionParser.h" -#include "src/exceptions/FileIoException.h" -#include "src/exceptions/WrongFormatException.h" - -TEST(ReadTraFileTest, NonExistingFileTest) { - //No matter what happens, please don't create a file with the name "nonExistingFile.not"! :-) - ASSERT_THROW(storm::parser::DeterministicSparseTransitionParser(STORM_CPP_TESTS_BASE_PATH "/nonExistingFile.not"), storm::exceptions::FileIoException); -} - -/* The following test case is based on one of the original MRMC test cases - */ -TEST(ReadTraFileTest, ParseFileTest1) { - storm::storage::SparseMatrix result = storm::parser::DeterministicSparseTransitionParser(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/csl_general_input_01.tra"); - - double val = 0.0; - ASSERT_TRUE(result.getValue(0, 0, &val)); - ASSERT_EQ(val, 0.0); - - ASSERT_TRUE(result.getValue(0, 1, &val)); - ASSERT_EQ(val, 1.0); - - ASSERT_TRUE(result.getValue(1, 1, &val)); - ASSERT_EQ(val, 0.080645161290322580645161290322581); - - ASSERT_TRUE(result.getValue(1, 2, &val)); - ASSERT_EQ(val, 0.080645161290322580645161290322581); - - //Transition 1->3 was not set in the file, so it is not to appear in the matrix! - ASSERT_FALSE(result.getValue(1, 3, &val)); - ASSERT_EQ(val, 0); - - ASSERT_TRUE(result.getValue(2, 1, &val)); - ASSERT_EQ(val, 0.04032258064516129032258064516129); - - ASSERT_TRUE(result.getValue(2, 2, &val)); - ASSERT_EQ(val, 0.04032258064516129032258064516129); - - ASSERT_TRUE(result.getValue(2, 3, &val)); - ASSERT_EQ(val, 0.04032258064516129032258064516129); - - ASSERT_TRUE(result.getValue(2, 4, &val)); - ASSERT_EQ(val, 0.04032258064516129032258064516129); - - ASSERT_TRUE(result.getValue(3, 2, &val)); - ASSERT_EQ(val, 0.0806451612903225806451612903225812); - - ASSERT_TRUE(result.getValue(3, 3, &val)); - ASSERT_EQ(val, 0.0); - - ASSERT_TRUE(result.getValue(3, 4, &val)); - ASSERT_EQ(val, 0.080645161290322580645161290322581); - - ASSERT_TRUE(result.getValue(4, 4, &val)); - ASSERT_EQ(val, 0.0); -} - -TEST(ReadTraFileTest, WrongFormatTestHeader1) { - ASSERT_THROW(storm::parser::DeterministicSparseTransitionParser(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/wrong_format_header1.tra"), storm::exceptions::WrongFormatException); -} - -TEST(ReadTraFileTest, WrongFormatTestHeader2) { - ASSERT_THROW(storm::parser::DeterministicSparseTransitionParser(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/wrong_format_header2.tra"), storm::exceptions::WrongFormatException); -} - -TEST(ReadTraFileTest, WrongFormatTestTransition) { - ASSERT_THROW(storm::parser::DeterministicSparseTransitionParser(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/wrong_format_transition.tra"), storm::exceptions::WrongFormatException); -} diff --git a/test/functional/storage/SparseMatrixTest.cpp b/test/functional/storage/SparseMatrixTest.cpp deleted file mode 100644 index 17ab1fffb..000000000 --- a/test/functional/storage/SparseMatrixTest.cpp +++ /dev/null @@ -1,386 +0,0 @@ -#include "gtest/gtest.h" -#include "src/storage/SparseMatrix.h" -#include "src/exceptions/InvalidArgumentException.h" -#include "src/exceptions/OutOfRangeException.h" -#include "src/adapters/EigenAdapter.h" -#include "src/adapters/StormAdapter.h" - -TEST(SparseMatrixTest, ZeroRowsTest) { - storm::storage::SparseMatrix *ssm = new storm::storage::SparseMatrix(0); - ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix::MatrixStatus::UnInitialized); - - ASSERT_THROW(ssm->initialize(50), storm::exceptions::InvalidArgumentException); - ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix::MatrixStatus::Error); - - delete ssm; -} - -TEST(SparseMatrixTest, TooManyEntriesTest) { - storm::storage::SparseMatrix *ssm = new storm::storage::SparseMatrix(2); - ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix::MatrixStatus::UnInitialized); - - ASSERT_THROW(ssm->initialize(10), storm::exceptions::InvalidArgumentException); - ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix::MatrixStatus::Error); - - delete ssm; -} - -TEST(SparseMatrixTest, addNextValueTest) { - storm::storage::SparseMatrix *ssm = new storm::storage::SparseMatrix(5); - ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix::MatrixStatus::UnInitialized); - - ASSERT_NO_THROW(ssm->initialize(1)); - ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix::MatrixStatus::Initialized); - - ASSERT_THROW(ssm->addNextValue(-1, 1, 1), storm::exceptions::OutOfRangeException); - ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix::MatrixStatus::Error); - - ASSERT_THROW(ssm->addNextValue(1, -1, 1), storm::exceptions::OutOfRangeException); - ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix::MatrixStatus::Error); - - ASSERT_THROW(ssm->addNextValue(6, 1, 1), storm::exceptions::OutOfRangeException); - ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix::MatrixStatus::Error); - - ASSERT_THROW(ssm->addNextValue(1, 6, 1), storm::exceptions::OutOfRangeException); - ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix::MatrixStatus::Error); - - delete ssm; -} - -TEST(SparseMatrixTest, finalizeTest) { - storm::storage::SparseMatrix *ssm = new storm::storage::SparseMatrix(5); - ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix::MatrixStatus::UnInitialized); - - ASSERT_NO_THROW(ssm->initialize(5)); - ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix::MatrixStatus::Initialized); - - ASSERT_NO_THROW(ssm->addNextValue(1, 2, 1)); - ASSERT_NO_THROW(ssm->addNextValue(1, 3, 1)); - ASSERT_NO_THROW(ssm->addNextValue(1, 4, 1)); - ASSERT_NO_THROW(ssm->addNextValue(1, 5, 1)); - ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix::MatrixStatus::Initialized); - - ASSERT_THROW(ssm->finalize(), storm::exceptions::InvalidStateException); - ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix::MatrixStatus::Error); - - delete ssm; -} - -TEST(SparseMatrixTest, Test) { - // 25 rows, 50 non zero entries - storm::storage::SparseMatrix *ssm = new storm::storage::SparseMatrix(25); - ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix::MatrixStatus::UnInitialized); - - int values[50] = { - 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, - 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, - 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, - 30, 31, 32, 33, 34, 35, 36, 37, 38, 39, - 40, 41, 42, 43, 44, 45, 46, 47, 48, 49 - }; - int position_row[50] = { - 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, - 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, - 2, 2, 2, 2, /* first row empty, one full row 25 minus the diagonal entry */ - 4, 4, /* one empty row, then first and last column */ - 13, 13, 13, 13, /* a few empty rows, middle columns */ - 24, 24, 24, 24, 24, 24, 24, 24, 24, 24, - 24, 24, 24, 24, 24, 24, 24, 24, 24, 24 /* second to last row */ - }; - int position_col[50] = { - 1, 3, 4, 5, 6, 7, 8, 9, 10, - 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, - 21, 22, 23, 24, 25, /* first row empty, one full row a 25 */ - 1, 25, /* one empty row, then first and last column */ - 16, 17, 18, 19, /* a few empty rows, middle columns */ - 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, - 14, 15, 16, 17, 18, 19, 20, 21, 22, 23 /* second to last row */ - }; - int row_sums[25] = {}; - for (int i = 0; i < 50; ++i) { - row_sums[position_row[i]] += values[i]; - } - - ASSERT_NO_THROW(ssm->initialize(50)); - ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix::MatrixStatus::Initialized); - - for (int i = 0; i < 50; ++i) { - ASSERT_NO_THROW(ssm->addNextValue(position_row[i], position_col[i], values[i])); - } - ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix::MatrixStatus::Initialized); - - ASSERT_NO_THROW(ssm->finalize()); - ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix::MatrixStatus::ReadReady); - - int target; - for (int i = 0; i < 50; ++i) { - ASSERT_TRUE(ssm->getValue(position_row[i], position_col[i], &target)); - ASSERT_EQ(values[i], target); - } - - // test for a few of the empty rows - for (int row = 15; row < 24; ++row) { - for (int col = 1; col <= 25; ++col) { - target = 1; - ASSERT_FALSE(ssm->getValue(row, col, &target)); - - ASSERT_EQ(0, target); - } - } - ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix::MatrixStatus::ReadReady); - - // Test Row Sums - for (int row = 0; row < 25; ++row) { - ASSERT_EQ(row_sums[row], ssm->getRowSum(row)); - } - - delete ssm; -} - -TEST(SparseMatrixTest, ConversionFromDenseEigen_ColMajor_SparseMatrixTest) { - // 10 rows, 100 non zero entries - Eigen::SparseMatrix esm(10, 10); - for (int row = 0; row < 10; ++row) { - for (int col = 0; col < 10; ++col) { - esm.insert(row, col) = row * 10 + col; - } - } - - // make compressed, important for initialize() - esm.makeCompressed(); - - storm::storage::SparseMatrix *ssm = nullptr; - ASSERT_NO_THROW(ssm = storm::adapters::StormAdapter::toStormSparseMatrix(esm)); - - ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix::MatrixStatus::ReadReady); - - int target = -1; - for (int row = 0; row < 10; ++row) { - for (int col = 0; col < 10; ++col) { - ASSERT_TRUE(ssm->getValue(row, col, &target)); - ASSERT_EQ(target, row * 10 + col); - } - } - - delete ssm; -} - -TEST(SparseMatrixTest, ConversionFromDenseEigen_RowMajor_SparseMatrixTest) { - // 10 rows, 100 non zero entries - Eigen::SparseMatrix esm(10, 10); - for (int row = 0; row < 10; ++row) { - for (int col = 0; col < 10; ++col) { - esm.insert(row, col) = row * 10 + col; - } - } - - // make compressed, important for initialize() - esm.makeCompressed(); - - storm::storage::SparseMatrix *ssm = nullptr; - ASSERT_NO_THROW(ssm = storm::adapters::StormAdapter::toStormSparseMatrix(esm)); - - ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix::MatrixStatus::ReadReady); - - int target = -1; - for (int row = 0; row < 10; ++row) { - for (int col = 0; col < 10; ++col) { - ASSERT_TRUE(ssm->getValue(row, col, &target)); - ASSERT_EQ(target, row * 10 + col); - } - } - - delete ssm; -} - -TEST(SparseMatrixTest, ConversionFromSparseEigen_ColMajor_SparseMatrixTest) { - // 10 rows, 15 non zero entries - Eigen::SparseMatrix esm(10, 10); - - typedef Eigen::Triplet IntTriplet; - std::vector tripletList; - tripletList.reserve(15); - tripletList.push_back(IntTriplet(1, 0, 0)); - tripletList.push_back(IntTriplet(1, 1, 1)); - tripletList.push_back(IntTriplet(1, 2, 2)); - tripletList.push_back(IntTriplet(1, 3, 3)); - tripletList.push_back(IntTriplet(1, 4, 4)); - tripletList.push_back(IntTriplet(1, 5, 5)); - tripletList.push_back(IntTriplet(1, 6, 6)); - tripletList.push_back(IntTriplet(1, 7, 7)); - tripletList.push_back(IntTriplet(1, 8, 8)); - tripletList.push_back(IntTriplet(1, 9, 9)); - - tripletList.push_back(IntTriplet(4, 3, 10)); - tripletList.push_back(IntTriplet(4, 6, 11)); - tripletList.push_back(IntTriplet(4, 9, 12)); - - tripletList.push_back(IntTriplet(6, 0, 13)); - tripletList.push_back(IntTriplet(8, 9, 14)); - - esm.setFromTriplets(tripletList.begin(), tripletList.end()); - - // make compressed, important for initialize() - esm.makeCompressed(); - - storm::storage::SparseMatrix *ssm = nullptr; - ASSERT_NO_THROW(ssm = storm::adapters::StormAdapter::toStormSparseMatrix(esm)); - - ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix::MatrixStatus::ReadReady); - - int target = -1; - - for (auto &coeff: tripletList) { - ASSERT_TRUE(ssm->getValue(coeff.row(), coeff.col(), &target)); - ASSERT_EQ(target, coeff.value()); - } - - delete ssm; -} - -TEST(SparseMatrixTest, ConversionFromSparseEigen_RowMajor_SparseMatrixTest) { - // 10 rows, 15 non zero entries - Eigen::SparseMatrix esm(10, 10); - - typedef Eigen::Triplet IntTriplet; - std::vector tripletList; - tripletList.reserve(15); - tripletList.push_back(IntTriplet(1, 0, 15)); - tripletList.push_back(IntTriplet(1, 1, 1)); - tripletList.push_back(IntTriplet(1, 2, 2)); - tripletList.push_back(IntTriplet(1, 3, 3)); - tripletList.push_back(IntTriplet(1, 4, 4)); - tripletList.push_back(IntTriplet(1, 5, 5)); - tripletList.push_back(IntTriplet(1, 6, 6)); - tripletList.push_back(IntTriplet(1, 7, 7)); - tripletList.push_back(IntTriplet(1, 8, 8)); - tripletList.push_back(IntTriplet(1, 9, 9)); - - tripletList.push_back(IntTriplet(4, 3, 10)); - tripletList.push_back(IntTriplet(4, 6, 11)); - tripletList.push_back(IntTriplet(4, 9, 12)); - - tripletList.push_back(IntTriplet(6, 0, 13)); - tripletList.push_back(IntTriplet(8, 9, 14)); - - esm.setFromTriplets(tripletList.begin(), tripletList.end()); - - // make compressed, important for initialize() - esm.makeCompressed(); - - storm::storage::SparseMatrix *ssm = nullptr; - ASSERT_NO_THROW(ssm = storm::adapters::StormAdapter::toStormSparseMatrix(esm)); - - ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix::MatrixStatus::ReadReady); - - int target = -1; - for (auto &coeff: tripletList) { - bool retVal = ssm->getValue(coeff.row(), coeff.col(), &target); - ASSERT_TRUE(retVal); - ASSERT_EQ(target, coeff.value()); - } - - delete ssm; -} - -TEST(SparseMatrixTest, ConversionToSparseEigen_RowMajor_SparseMatrixTest) { - int values[100]; - storm::storage::SparseMatrix *ssm = new storm::storage::SparseMatrix(10); - - for (uint_fast32_t i = 0; i < 100; ++i) { - values[i] = i; - } - - ASSERT_NO_THROW(ssm->initialize(100)); - ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix::MatrixStatus::Initialized); - - for (uint_fast32_t row = 0; row < 10; ++row) { - for (uint_fast32_t col = 0; col < 10; ++col) { - ASSERT_NO_THROW(ssm->addNextValue(row, col, values[row * 10 + col])); - } - } - ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix::MatrixStatus::Initialized); - - ASSERT_NO_THROW(ssm->finalize()); - ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix::MatrixStatus::ReadReady); - - Eigen::SparseMatrix* esm = storm::adapters::EigenAdapter::toEigenSparseMatrix(*ssm); - - for (uint_fast32_t row = 0; row < 10; ++row) { - for (uint_fast32_t col = 0; col < 10; ++col) { - ASSERT_EQ(values[row * 10 + col], esm->coeff(row, col)); - } - } - - delete esm; - delete ssm; -} - -#ifdef STORM_USE_TBB -TEST(SparseMatrixTest, TBBMatrixMultTest) { - storm::storage::SparseMatrix matrix(10, 10); - ASSERT_NO_THROW(matrix.initialize(100)); - double values[100]; - std::vector x; - x.resize(10); - for (uint_fast64_t i = 0; i < 100; ++i) { - values[i] = i + 1.0; - if (i < 10) { - x[i] = 1.0; - } - matrix.addNextValue(i / 10, i % 10, values[i]); - } - ASSERT_NO_THROW(matrix.finalize()); - ASSERT_EQ(matrix.getState(), storm::storage::SparseMatrix::MatrixStatus::ReadReady); - - std::vector result; - result.resize(10); - - matrix.multiplyWithVector(x, result); - - for (uint_fast64_t i = 0; i < 10; ++i) { - double rowSum = 0.0; - for (uint_fast64_t j = 0; j < 10; ++j) { - rowSum += values[10 * i + j]; - } - ASSERT_EQ(rowSum, result.at(i)); - } -} - -TEST(SparseMatrixTest, TBBSparseMatrixMultTest) { - storm::storage::SparseMatrix matrix(10, 10); - ASSERT_NO_THROW(matrix.initialize(50)); - double values[100]; - std::vector x; - x.resize(10); - for (uint_fast64_t i = 0; i < 100; ++i) { - if (i % 2 == 0) { - values[i] = i + 1.0; - matrix.addNextValue(i / 10, i % 10, i + 1.0); - } else { - values[i] = 0.0; - } - - if (i < 10) { - x[i] = 1.0; - } - - } - ASSERT_NO_THROW(matrix.finalize()); - ASSERT_EQ(matrix.getState(), storm::storage::SparseMatrix::MatrixStatus::ReadReady); - - std::vector result; - result.resize(10); - - matrix.multiplyWithVector(x, result); - - for (uint_fast64_t i = 0; i < 10; ++i) { - double rowSum = 0.0; - for (uint_fast64_t j = 0; j < 10; ++j) { - rowSum += values[10 * i + j]; - } - ASSERT_EQ(rowSum, result.at(i)); - } -} - -#endif // STORM_USE_TBB diff --git a/test/functional/storage/adapters/EigenAdapterTest.cpp b/test/functional/storage/adapters/EigenAdapterTest.cpp deleted file mode 100644 index 6428c6493..000000000 --- a/test/functional/storage/adapters/EigenAdapterTest.cpp +++ /dev/null @@ -1,100 +0,0 @@ -#include "gtest/gtest.h" - -#include "Eigen/Sparse" -#include "src/adapters/EigenAdapter.h" -#include "src/exceptions/InvalidArgumentException.h" -#include - -#define STORM_EIGENADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE 5 -#define STORM_EIGENADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE 5 - -TEST(EigenAdapterTest, SimpleDenseSquareCopy) { - // 5 rows - storm::storage::SparseMatrix sm(STORM_EIGENADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE); - - double values[STORM_EIGENADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE * STORM_EIGENADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE]; - sm.initialize(STORM_EIGENADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE * STORM_EIGENADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE); - - int row = 0; - int col = 0; - for (int i = 0; i < STORM_EIGENADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE * STORM_EIGENADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE; ++i) { - values[i] = static_cast(i + 1); - - sm.addNextValue(row, col, values[i]); - ++col; - if (col == STORM_EIGENADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE) { - ++row; - col = 0; - } - } - sm.finalize(); - - auto esm = storm::adapters::EigenAdapter::toEigenSparseMatrix(sm); - - ASSERT_EQ(esm->rows(), STORM_EIGENADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE); - ASSERT_EQ(esm->cols(), STORM_EIGENADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE); - ASSERT_EQ(esm->nonZeros(), STORM_EIGENADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE * STORM_EIGENADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE); - - row = 0; - col = 0; - for (int i = 0; i < STORM_EIGENADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE * STORM_EIGENADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE; ++i) { - ASSERT_EQ(values[i], esm->coeff(row, col)); - ++col; - if (col == STORM_EIGENADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE) { - ++row; - col = 0; - } - } - - delete esm; -} - -TEST(EigenAdapterTest, SimpleSparseSquareCopy) { - // 5 rows - storm::storage::SparseMatrix sm(STORM_EIGENADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE); - - double values[STORM_EIGENADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE * STORM_EIGENADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE]; - sm.initialize((STORM_EIGENADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE * STORM_EIGENADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE + 1) / 2); - - int row = 0; - int col = 0; - - bool everySecondElement = true; - - for (int i = 0; i < STORM_EIGENADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE * STORM_EIGENADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE; ++i) { - values[i] = static_cast(i + 1); - if (everySecondElement) { - sm.addNextValue(row, col, values[i]); - } - everySecondElement = !everySecondElement; - ++col; - if (col == STORM_EIGENADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE) { - ++row; - col = 0; - } - } - sm.finalize(); - - auto esm = storm::adapters::EigenAdapter::toEigenSparseMatrix(sm); - - ASSERT_EQ(esm->rows(), STORM_EIGENADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE); - ASSERT_EQ(esm->cols(), STORM_EIGENADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE); - ASSERT_EQ(esm->nonZeros(), (STORM_EIGENADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE * STORM_EIGENADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE + 1) / 2); - - row = 0; - col = 0; - everySecondElement = true; - for (int i = 0; i < STORM_EIGENADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE * STORM_EIGENADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE; ++i) { - if (everySecondElement) { - ASSERT_EQ(values[i], esm->coeff(row, col)); - } - everySecondElement = !everySecondElement; - ++col; - if (col == STORM_EIGENADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE) { - ++row; - col = 0; - } - } - - delete esm; -} diff --git a/test/functional/storage/adapters/GmmAdapterTest.cpp b/test/functional/storage/adapters/GmmAdapterTest.cpp deleted file mode 100644 index 8377792d7..000000000 --- a/test/functional/storage/adapters/GmmAdapterTest.cpp +++ /dev/null @@ -1,111 +0,0 @@ -#include "gtest/gtest.h" - -#include "gmm/gmm_matrix.h" -#include "src/adapters/GmmxxAdapter.h" -#include "src/exceptions/InvalidArgumentException.h" -#include - -#define STORM_GMMADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE 5 -#define STORM_GMMADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE 5 - -double getValue(gmm::csr_matrix const& gmmSparseMatrix, uint_fast64_t row, uint_fast64_t col) { - uint_fast64_t rowStart = gmmSparseMatrix.jc.at(row); - uint_fast64_t rowEnd = gmmSparseMatrix.jc.at(row + 1); - while (rowStart < rowEnd) { - if (gmmSparseMatrix.ir.at(rowStart) == col) { - return gmmSparseMatrix.pr.at(rowStart); - } - if (gmmSparseMatrix.ir.at(rowStart) > col) { - break; - } - ++rowStart; - } - - return 0.0; -} - -TEST(GmmAdapterTest, SimpleDenseSquareCopy) { - // 5 rows - storm::storage::SparseMatrix sm(STORM_GMMADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE); - - double values[STORM_GMMADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE * STORM_GMMADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE]; - sm.initialize(STORM_GMMADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE * STORM_GMMADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE); - - int row = 0; - int col = 0; - for (int i = 0; i < STORM_GMMADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE * STORM_GMMADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE; ++i) { - values[i] = static_cast(i + 1); - - sm.addNextValue(row, col, values[i]); - ++col; - if (col == STORM_GMMADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE) { - ++row; - col = 0; - } - } - sm.finalize(); - - auto gsm = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix(sm); - - ASSERT_EQ(gsm->nrows(), STORM_GMMADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE); - ASSERT_EQ(gsm->ncols(), STORM_GMMADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE); - ASSERT_EQ(gmm::nnz(*gsm), STORM_GMMADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE * STORM_GMMADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE); - row = 0; - col = 0; - for (int i = 0; i < STORM_GMMADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE * STORM_GMMADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE; ++i) { - ASSERT_EQ(values[i], getValue(*gsm, row, col)); - ++col; - if (col == STORM_GMMADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE) { - ++row; - col = 0; - } - } -} - -TEST(GmmAdapterTest, SimpleSparseSquareCopy) { - // 5 rows - storm::storage::SparseMatrix sm(STORM_GMMADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE); - - double values[STORM_GMMADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE * STORM_GMMADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE]; - sm.initialize((STORM_GMMADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE * STORM_GMMADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE + 1) / 2); - - int row = 0; - int col = 0; - - bool everySecondElement = true; - - for (int i = 0; i < STORM_GMMADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE * STORM_GMMADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE; ++i) { - values[i] = static_cast(i + 1); - if (everySecondElement) { - sm.addNextValue(row, col, values[i]); - } - everySecondElement = !everySecondElement; - ++col; - if (col == STORM_GMMADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE) { - ++row; - col = 0; - } - } - sm.finalize(); - - auto gsm = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix(sm); - - ASSERT_EQ(gsm->nrows(), STORM_GMMADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE); - ASSERT_EQ(gsm->ncols(), STORM_GMMADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE); - ASSERT_EQ(gmm::nnz(*gsm), (STORM_GMMADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE * STORM_GMMADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE + 1) / 2); - - row = 0; - col = 0; - everySecondElement = true; - for (int i = 0; i < STORM_GMMADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE * STORM_GMMADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE; ++i) { - if (everySecondElement) { - ASSERT_EQ(values[i], getValue(*gsm, row, col)); - } - everySecondElement = !everySecondElement; - ++col; - if (col == STORM_GMMADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE) { - ++row; - col = 0; - } - } -} diff --git a/test/functional/storage/adapters/StormAdapterTest.cpp b/test/functional/storage/adapters/StormAdapterTest.cpp deleted file mode 100644 index c3d341a43..000000000 --- a/test/functional/storage/adapters/StormAdapterTest.cpp +++ /dev/null @@ -1,104 +0,0 @@ -#include "gtest/gtest.h" - -#include "gmm/gmm_matrix.h" -#include "src/adapters/StormAdapter.h" -#include "src/exceptions/InvalidArgumentException.h" -#include - -#define STORM_STORMADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE 5 -#define STORM_STORMADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE 5 - -TEST(StormAdapterTest, SimpleDenseSquareCopy) { - // 5 rows - gmm::csr_matrix gmmSparseMatrix; - - /* - * As CSR_Matrix is read-only we have to prepare the data in this row_matrix and then do a copy. - */ - gmm::row_matrix> gmmPreMatrix(STORM_STORMADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE, STORM_STORMADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE); - - double values[STORM_STORMADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE * STORM_STORMADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE]; - - int row = 0; - int col = 0; - for (int i = 0; i < STORM_STORMADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE * STORM_STORMADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE; ++i) { - values[i] = static_cast(i + 1); - - gmmPreMatrix(row, col) = values[i]; - ++col; - if (col == STORM_STORMADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE) { - ++row; - col = 0; - } - } - gmm::copy(gmmPreMatrix, gmmSparseMatrix); - - auto stormSparseMatrix = storm::adapters::StormAdapter::toStormSparseMatrix(gmmSparseMatrix); - - ASSERT_EQ(stormSparseMatrix->getRowCount(), STORM_STORMADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE); - ASSERT_EQ(stormSparseMatrix->getColumnCount(), STORM_STORMADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE); - ASSERT_EQ(stormSparseMatrix->getNonZeroEntryCount(), STORM_STORMADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE * STORM_STORMADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE); - row = 0; - col = 0; - for (int i = 0; i < STORM_STORMADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE * STORM_STORMADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE; ++i) { - ASSERT_EQ(values[i], stormSparseMatrix->getValue(row, col)); - ++col; - if (col == STORM_STORMADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE) { - ++row; - col = 0; - } - } -} - -TEST(StormAdapterTest, SimpleSparseSquareCopy) { - // 5 rows - gmm::csr_matrix gmmSparseMatrix; - - /* - * As CSR_Matrix is read-only we have to prepare the data in this row_matrix and then do a copy. - */ - gmm::row_matrix> gmmPreMatrix(STORM_STORMADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE, STORM_STORMADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE); - - double values[STORM_STORMADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE * STORM_STORMADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE]; - - int row = 0; - int col = 0; - - bool everySecondElement = true; - - for (int i = 0; i < STORM_STORMADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE * STORM_STORMADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE; ++i) { - values[i] = static_cast(i + 1); - if (everySecondElement) { - gmmPreMatrix(row, col) = values[i]; - } - everySecondElement = !everySecondElement; - ++col; - if (col == STORM_STORMADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE) { - ++row; - col = 0; - } - } - gmm::copy(gmmPreMatrix, gmmSparseMatrix); - - auto stormSparseMatrix = storm::adapters::StormAdapter::toStormSparseMatrix(gmmSparseMatrix); - - ASSERT_EQ(stormSparseMatrix->getRowCount(), STORM_STORMADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE); - ASSERT_EQ(stormSparseMatrix->getColumnCount(), STORM_STORMADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE); - ASSERT_EQ(stormSparseMatrix->getNonZeroEntryCount(), (STORM_STORMADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE * STORM_STORMADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE + 1) / 2); - - - row = 0; - col = 0; - everySecondElement = true; - for (int i = 0; i < STORM_STORMADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE * STORM_STORMADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE; ++i) { - if (everySecondElement) { - ASSERT_EQ(values[i], stormSparseMatrix->getValue(row, col)); - } - everySecondElement = !everySecondElement; - ++col; - if (col == STORM_STORMADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE) { - ++row; - col = 0; - } - } -} diff --git a/util/checklist/storage.ods b/util/checklist/storage.ods index 43080d6c57b5d6aea8e7e513c66c28dc7c78e624..d05761496281c3533609fc6a2e759dbb72e6be50 100644 GIT binary patch delta 3603 zcmZ8k2{aU38y;g{#@MpWWXV#QkYp^y7|U29!jNq+5n)31LH3ZX z6rs_4$P%(=-}*oQ_b>hbJ?Gx%-1k23d*5^3bKa#XnI<8HhRwp5mW~GiU;+R*!jjpn zfPbC0&tiSPitt439-rau9c4ID-BfETj)#||K2CMSO}~Fz#t7%{8O9=yvP`n<(2Jdc zYTto!Yi2Q{!HmN&dv6X9)20ryETndl_$_IRCRueS zATHdU+H;Tq^=3+kHziZw)DZ!s_t^ZGxU>oiF-reG$*tnMxbF3R*E}X>jHcFqw zIL&5KBY}5Diw-`HFbKW;;tL%TVd5ZENL=75_PBT4E!OqYZA4~3k$G6*aX>TW zxTcBFie^&L-wGV=-_iJSy#CaWFjx#W3k!t;ZM~U|7Ge zs%vOeUm{JEX>AJRtdXRt%_J7iJRS*Pi6R6=otfd*IQFhp5({(~u8l@$dm*twxl#t& z6l>j#y`nTtGZV-y`@-rMuODq@*@*8t%;y>{De^Om+<5Y8CEs2j`zZMV3iR~DO1cOm z&19QNrtV1$!(B@{s>WhY?r3x?@G_Do>!f^Q64G)urP%Z#;3>zfO?&BHlB&|>H*X&a zM>_kToqd&Rw7~Q_+VBdRy-I~<@Qb%i^%!u7YZ5LO;BrCaU}UPSPb>yIIYO}r?afK?4fbB$pjVpb zw0smF`0MDbYpv@=%lpscGh+}mhA<0WALS0WE@jh^5ZZ9a;oLM$Gx&thx`;?ZO?$p$ zUg8&sgQ|3j$6Tg{R!nHFT)JP*@aDnw7pj`<`*gOpIzTFc-}0LrAhk%4c42JO^A-9U zeB{y|(}4hR_N4G*L)rAYKFM0Dv^1|4S5D z24Sq7--Ieh=vu|p1!YV@ac8>qM5b!9&~m29jN1WAvJ4A1#}t5=cyh41$t4xf;{Voi z=|EQq7#wnI*>G`ZMTzS@v}W4qPyYj|QxDA|DXf3J{O87E;BL{+os$>@Ea!o6clair z>4iT=LiQvu36bSn7d&QI1C?)fT0KgrvQ%1hF%R;4&2HoMm^?=v?48I`VSTg<1?%a?^1I`aT~zTpE7 zY431-;z=|b1D0~g!1t%?>P0JnuxzyQ6LODDhb|nf^~8Wr*v{2S&LbrQ8dRS3)}mA# zug)0CYl132)u{~BU^crZ1XIV|Rk;RBA_G`ISunQWw8ANGDJ0zHX!2u^zf}9RaY7jG zWMn<~QbXWC^XVUbNpF8RoyVSiw(U{MCE(^EqRep7b%;=xVeq9J#$5YqKo`sN+D>GvFL3A({_RY#hY(qD_uWW?z7s!w}v7kZ(;Om z{MB6g@{PVIDPDA7U&wvh^{9r{L9Pc4%WfZVhvh%3=h@EE`k{0=d@JoMZ0$UHK)T;_ z6$1t%AU6tP8@3gj1_d@#WP-4=)*8YRJwo(^9x%e<=$#8Hlp;QGGcXb%!1_^fA$Q!w za#p+3`W}=-^=zyN$&uhaW4GE=LfAYv{6X+0a@!cC-lxJ}dGuI3B`2b~aiM!5ohZvV zWAZsDKO7TqK1?nSXy`AhcpkYPW;90B5Oe^OO~4lI)vRBq3fs0D)3Jx5kQQiFeD=q| z&?z}5manfT))Ed5!<$0X`>9`_?6enUN9dBe7!({z^84!k@MX9{ursRZB>fP*JDH%S zI8{2n8OvPXr-kZh(|QLvHwTz)zW1vUi&1z$!fS>h>Zr3_E;wbHKQ6h8k_CDy6i|;} zLtd5=Ed8-`M)byK(H+_NNSww%x3c6k&E zwyt%Q47%W0z-2nKl`79VJ-$jK)3X|fPi?d-w!1PBn_g>inXdMXXD+(JESL98=PzCA zF=>4CE~jkMxRcVC8beon7^(Cxt=N0@jv7&2oKQ$ItY#fOtTg?GYtIi!oz~feCNQ%1z!EFm-KFa9s@1_|D0Y_2FP@`>5pw1i(KeAi7WVOs#HT1WgoCW^(V7_^d2B)5^79bNZR(@! zy9l6w5NP)4F8F;OzdrG)zMrp3*6P5I1K(x3koSxJW9qlRed03&gew~lx`|EaQs{KsYujC z@`th;?O6W^ao;PiV`Ud*b)$_tq?E=sh$dH$2rVtqgxc(}oxQA4ar2`6OSSvz?P0`FueJ;=Yne9;Q5nvUcZQXUi8Zgr{f`SVlf?G~2A2 zYE+IqdoAiUCdy6;h>a{T-(aoJn^H+z>|c5KOB$QgZFUDQ2L2^81Sn&xXH*TJ95fUj zr=z3Gi=8Dd?B6px$bfOS_D-FpmR(Wk#eVpX(Y$w@>(QS{M0U|VR`Vhs-D5vAG80ht zo=TqH+-${IkkZ(?mU2?KWE9?X?_sQVYV~|ZQJ65lQn>%3fh{++iQMo;P_;gPkXUZ+ zrE@^LZDY$)^5Xn`XG86iLR)Onrc4Qi6k4%^(%Gol$L}0sX-(bh4PaN^7gVY{@n`xz5x`-cO5^i$A>R8;9v-bpBnlHE`5Dc delta 3547 zcmZ8kcQoAF79P@Af*7Jj8NL0q=)FV)3DJo%L>m!ZlpxWP zFuKby7!gq>5s!P{d-vV9|2W?{-&t$#z1Ci9?{6oileDFgK#XpZk}-ooU=WDXEDd6E z;q0`z1fX)InV%eh&@zaM^IPja^Ly};|8MJ!$O%k)V|ZujRk=*- zegZATPsFkb@L7Z)@EghUm0n^+P+gwbtIrDUqDtXN_|jM=b$WuhA$1egFq4LUa1UVY zEcp12sgQ^vyRh;~hELy`*~cV$HXi)^Ef>T>#6~!}OmOApu}&_r#1dDzFBO>PcmSe^ z_=?$dF;()<^Gy!W$dI#r$x|E{92lVDe&y5D(T~+FdL!<2dwQRm1U|=Hm9HKj>({u_ z2diH<=anah4SBV$p2j^dl1gd*UKj$bbFtjQWc$#d>)XFAX?zqHdo+u97|iIVGJOXb z;elAD_lt2q5uS24x=9Hph3ezVNkAYZDG2meHNjx;Sv8|>fd0oIXLl6R+uP}}BTCZW z&2{_kebkI1LkOYP=GW~bU42f&f*X%eH*%Xe494eycT_t0_F#REF3>@V-d=luoQJUq z!bPikOl1~i&hv3u=G|1X-nmz}sBlrQWF(G$+`J}Yn{0T&OPA>NIv9MztgEd6H7#H2;EE<}#L3gi%AmtH0+2&*vU6 zjMp-C89usZF_b(5L#4n{(HxA&*+(0v0NngqKOZ?8=4opOBLfR*z&8b9gQv<9x+8`R zEsYPjxj$;{cD#}yzb{GiKqJ{mXTYeqfJ6J*n{$O4RzvZwN_k@o^&5o8ud8keI19s&WEjdJs{EP zS=i)y{yo4?U)GaTwGCVgCPc}m)Rcda?-1HmREk9>F2&HBDRS*dl6w(ptZSiP_(`M_P1=FfCXYT#?X`lAI3ZetHoZwXLn=l&s)V^KR>(>OJZdSdD@ zQ5TnQWpul@-}#aPdy6K#=mll)8$ckUMT~E;@?nI_oXC^afZ8`zn_=0m_3*@f$0CP! zzLf}ph>I_T)|dC#>I!~YGKDxrrC@&+1y7L$>77cOUFG{gI}(Mv6Z&OD?9wHJV~8p5 zgep;XSJDUZGAPaBwInS9aJb13^LkN|8y~vDA3cseajVz(VvMyoDe{ir_yu56Hm(BC ze5|~fnaNyHuYxeQr>#xj z(KhUbJm6HupOdQ8@VVLNP$3A%gd>;djBs8O*f0E~gmxe1^YXNBN37Y=N#*Cto2p}0Z{M&H&L?+4DSvtJTi0UMK*2UKXq1`5DI~ABK=j=MdkZF73f>kg>JN{ZrhGWRHO4CHeCBiZY*2H= zpz@H54&{lFJB2cIn;3Y*_opZA2izXgKLc78db5(-X82rt5bxIX){$#C%sZ3HSNhb) zwqv+tibxtMpr$Z8XzAvN1dbECKy#S03rnf;&z@kovd^&89ij0~QF9dxOuUlb+gqY` zjhL=D4Qx4G9piQ2l0NmT8!kZ`JXS7pVzRUd+;Gy(Y|47ry)($>=VIoWJA3C%86BrY zVH#aTzEQF4fppR$uP+<)sXJ$@51?%D7GgG57Q_-wnj$@w*1J6~09-=+5H+iS?8&7n zk(yIIx_!gI-g%-QlJxoma6MC}vA)BF(|)s`!jF#MOmO14uk0Y+f67fUUY{juR`zke z(ZVzITq9!&5Gc21lGGz^eW!Bjz?e`YzIxmxZ!HK$7qszy@1pHwTiX#b9LV}I_%iO$ zjo>)KK|!%Lbddpto*%$h$}MYO_AK=G9ZBb!P#3@wpUtsCd_j)0wSYFfPAosBOV7 z*+4#dw8ejgXue8u0u1*&OX|4PfX5H=V!dadIyYkZqSFe%`@NvS7r-=>1OD6PdcPM*v5 z6?ONjDyv009LTT&5!E!ReXf&qOM=}=@UppsDBta^uz@E{04e>ep&6ZtuP(sSn+AM z$#*Fm1cYZ1+Z6Q!I$EM`uGp#mT-2okou#i)E5ybyQ)ZGM zv)}ZkQb1`j4)965sO&KhsRv@jn5<@NGBSwPENJt_A+WU&u*RdHI}7p~-LV%nlbzdoy#OpM%{ z9?+z&xi6ffB!2)^DSHbeu=gB03A6@DJ%eAd{^q^nmbUQXs*2&@hF7EBlSKcq%?u{CQzwIn7_%NJj%Hb6t`oF^Rl+c zBF#Kj{Ssze&zVPSV(RqYecKWGnigiSySc(qK%hFMYO) zG~}zOkep!#R#oX7IMfj5tcMz!{2ckU?En0Y)0U$>7rg(K!Wl!_qPpkI-!lyaI+wtI zo6LoO3Sy(1Bo~-L%%J~>=f6|SP||^&2Y;jkz3?59VN1)IQJ@1kXKHkyBx)JMI$Y-u z+}U@iYQ~l-zt}%LoyR;2_NNK|8~=hf)eKQJ(Trf-KfT54LKQEnon_@6;EMcHr2l_T e@rklayk}Bh>ugH1{KHe9X2znfFomf0Ir}e?Fm!