diff --git a/CMakeLists.txt b/CMakeLists.txt index 31d82172c..4efcb6e4f 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -45,14 +45,14 @@ set(CUSTOM_BOOST_ROOT "" CACHE STRING "A custom path to the Boost root directory ## ############################################################# -set(TBB_INSTALL_DIR "${PROJECT_SOURCE_DIR}/resources/3rdparty/tbb41_20130314_merged-win-lin-mac/") -if(MSVC) - set(ENV{TBB_ARCH_PLATFORM} "intel64/vc11") -elseif(CMAKE_COMPILER_IS_GNUCC) - set(ENV{TBB_ARCH_PLATFORM} "intel64/gcc4.4") -else(CLANG) - set(ENV{TBB_ARCH_PLATFORM} "intel64/clang3.2") -endif() +#set(TBB_INSTALL_DIR "${PROJECT_SOURCE_DIR}/resources/3rdparty/tbb41_20130314_merged-win-lin-mac/") +#if(MSVC) +# set(ENV{TBB_ARCH_PLATFORM} "intel64/vc11") +#elseif(CMAKE_COMPILER_IS_GNUCC) +# set(ENV{TBB_ARCH_PLATFORM} "intel64/gcc4.4") +#else(CLANG) +# set(ENV{TBB_ARCH_PLATFORM} "intel64/clang3.2") +#endif() # Add the resources/cmake folder to Module Search Path for FindTBB.cmake set(CMAKE_MODULE_PATH ${CMAKE_MODULE_PATH} "${PROJECT_SOURCE_DIR}/resources/cmake/") @@ -438,6 +438,7 @@ if (TBB_FOUND) message(STATUS "StoRM - Found Intel TBB with Interface Version ${TBB_INTERFACE_VERSION}") if (USE_INTELTBB) message(STATUS "StoRM - Linking with Intel TBB for activated Matrix/Vector MT") + message(${TBB_LIBRARY_DIRS}) include_directories(${TBB_INCLUDE_DIRS}) target_link_libraries(storm tbb tbbmalloc) target_link_libraries(storm-functional-tests tbb tbbmalloc) diff --git a/src/counterexamples/SMTMinimalCommandSetGenerator.h b/src/counterexamples/SMTMinimalCommandSetGenerator.h index 8e46f8da2..e8bedf243 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 (auto& entry : transitionMatrix.getRow(row)) { + for (auto const& entry : transitionMatrix.getRow(row)) { // If there is a relevant successor, we need to add the labels of the current choice. - if (relevancyInformation.relevantStates.get(entry.column()) || psiStates.get(entry.column())) { + if (relevancyInformation.relevantStates.get(entry.first) || psiStates.get(entry.first)) { for (auto const& label : choiceLabeling[row]) { relevancyInformation.relevantLabels.insert(label); } @@ -212,21 +212,21 @@ namespace storm { 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 != entry.column() && (relevancyInformation.relevantStates.get(entry.column()) || psiStates.get(entry.column()))) { + if (state != entry.first && (relevancyInformation.relevantStates.get(entry.first) || psiStates.get(entry.first))) { // 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, entry.column())) != variableInformation.statePairToIndexMap.end()) { + if (variableInformation.statePairToIndexMap.find(std::make_pair(state, entry.first)) != 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, entry.column())] = variableInformation.statePairVariables.size(); + variableInformation.statePairToIndexMap[std::make_pair(state, entry.first)] = variableInformation.statePairVariables.size(); // Clear contents of the stream to construct new expression name. variableName.clear(); variableName.str(""); - variableName << "t" << state << "_" << entry.column(); + variableName << "t" << state << "_" << entry.first; variableInformation.statePairVariables.push_back(context.bool_const(variableName.str().c_str())); } @@ -316,11 +316,11 @@ namespace storm { // Iterate over successors and add relevant choices of relevant successors to the following label set. bool canReachTargetState = false; for (auto const& entry : transitionMatrix.getRow(currentChoice)) { - if (relevancyInformation.relevantStates.get(entry.column())) { - for (auto relevantChoice : relevancyInformation.relevantChoicesForRelevantStates.at(entry.column())) { + if (relevancyInformation.relevantStates.get(entry.first)) { + for (auto relevantChoice : relevancyInformation.relevantChoicesForRelevantStates.at(entry.first)) { followingLabels[choiceLabeling[currentChoice]].insert(choiceLabeling[currentChoice]); } - } else if (psiStates.get(entry.column())) { + } else if (psiStates.get(entry.first)) { canReachTargetState = true; } } @@ -335,11 +335,11 @@ 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 (auto const& predecessorEntry : backwardTransitions.getRow(currentState)) { - if (relevancyInformation.relevantStates.get(predecessorEntry.column())) { - for (auto predecessorChoice : relevancyInformation.relevantChoicesForRelevantStates.at(predecessorEntry.column())) { + if (relevancyInformation.relevantStates.get(predecessorEntry.first)) { + for (auto predecessorChoice : relevancyInformation.relevantChoicesForRelevantStates.at(predecessorEntry.first)) { bool choiceTargetsCurrentState = false; for (auto const& successorEntry : transitionMatrix.getRow(predecessorChoice)) { - if (successorEntry.column() == currentState) { + if (successorEntry.first == currentState) { choiceTargetsCurrentState = true; } } @@ -581,11 +581,11 @@ 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 (auto const& predecessorEntry : backwardTransitions.getRow(currentState)) { - if (relevancyInformation.relevantStates.get(predecessorEntry.column())) { - for (auto predecessorChoice : relevancyInformation.relevantChoicesForRelevantStates.at(predecessorEntry.column())) { + if (relevancyInformation.relevantStates.get(predecessorEntry.first)) { + for (auto predecessorChoice : relevancyInformation.relevantChoicesForRelevantStates.at(predecessorEntry.first)) { bool choiceTargetsCurrentState = false; for (auto const& successorEntry : transitionMatrix.getRow(predecessorChoice)) { - if (successorEntry.column() == currentState) { + if (successorEntry.first == currentState) { choiceTargetsCurrentState = true; } } @@ -913,16 +913,16 @@ namespace storm { // Assert the constraints (1). storm::storage::VectorSet relevantPredecessors; for (auto const& predecessorEntry : backwardTransitions.getRow(relevantState)) { - if (relevantState != predecessorEntry.column() && relevancyInformation.relevantStates.get(predecessorEntry.column())) { - relevantPredecessors.insert(predecessorEntry.column()); + if (relevantState != predecessorEntry.first && relevancyInformation.relevantStates.get(predecessorEntry.first)) { + relevantPredecessors.insert(predecessorEntry.first); } } storm::storage::VectorSet relevantSuccessors; for (auto const& relevantChoice : relevancyInformation.relevantChoicesForRelevantStates.at(relevantState)) { for (auto const& successorEntry : transitionMatrix.getRow(relevantChoice)) { - if (relevantState != successorEntry.column() && (relevancyInformation.relevantStates.get(successorEntry.column()) || psiStates.get(successorEntry.column()))) { - relevantSuccessors.insert(successorEntry.column()); + if (relevantState != successorEntry.first && (relevancyInformation.relevantStates.get(successorEntry.first) || psiStates.get(successorEntry.first))) { + relevantSuccessors.insert(successorEntry.first); } } } @@ -941,8 +941,8 @@ namespace storm { storm::storage::VectorSet relevantSuccessors; for (auto const& relevantChoice : relevancyInformation.relevantChoicesForRelevantStates.at(relevantState)) { for (auto const& successorEntry : transitionMatrix.getRow(relevantChoice)) { - if (relevantState != successorEntry.column() && (relevancyInformation.relevantStates.get(successorEntry.column()) || psiStates.get(successorEntry.column()))) { - relevantSuccessors.insert(successorEntry.column()); + if (relevantState != successorEntry.first && (relevancyInformation.relevantStates.get(successorEntry.first) || psiStates.get(successorEntry.first))) { + relevantSuccessors.insert(successorEntry.first); } } } @@ -965,7 +965,7 @@ namespace storm { storm::storage::VectorSet choicesForStatePair; for (auto const& relevantChoice : relevancyInformation.relevantChoicesForRelevantStates.at(sourceState)) { for (auto const& successorEntry : transitionMatrix.getRow(relevantChoice)) { - if (successorEntry.column() == targetState) { + if (successorEntry.first == targetState) { choicesForStatePair.insert(relevantChoice); } } @@ -1400,13 +1400,13 @@ namespace storm { bool choiceTargetsRelevantState = false; for (auto const& successorEntry : transitionMatrix.getRow(currentChoice)) { - if (relevancyInformation.relevantStates.get(successorEntry.column()) && currentState != successorEntry.column()) { + if (relevancyInformation.relevantStates.get(successorEntry.first) && currentState != successorEntry.first) { choiceTargetsRelevantState = true; - if (!reachableStates.get(successorEntry.column())) { - reachableStates.set(successorEntry.column()); - stack.push_back(successorEntry.column()); + if (!reachableStates.get(successorEntry.first)) { + reachableStates.set(successorEntry.first); + stack.push_back(successorEntry.first); } - } else if (psiStates.get(successorEntry.column())) { + } else if (psiStates.get(successorEntry.first)) { targetStateIsReachable = true; } } @@ -1443,7 +1443,7 @@ namespace storm { // Determine whether the state has the option to leave the reachable state space and go to the unreachable relevant states. for (auto const& successorEntry : originalMdp.getTransitionMatrix().getRow(currentChoice)) { - if (unreachableRelevantStates.get(successorEntry.column())) { + if (unreachableRelevantStates.get(successorEntry.first)) { isBorderChoice = true; } } @@ -1526,13 +1526,13 @@ namespace storm { bool choiceTargetsRelevantState = false; for (auto const& successorEntry : transitionMatrix.getRow(currentChoice)) { - if (relevancyInformation.relevantStates.get(successorEntry.column()) && currentState != successorEntry.column()) { + if (relevancyInformation.relevantStates.get(successorEntry.first) && currentState != successorEntry.first) { choiceTargetsRelevantState = true; - if (!reachableStates.get(successorEntry.column())) { - reachableStates.set(successorEntry.column(), true); - stack.push_back(successorEntry.column()); + if (!reachableStates.get(successorEntry.first)) { + reachableStates.set(successorEntry.first, true); + stack.push_back(successorEntry.first); } - } else if (psiStates.get(successorEntry.column())) { + } else if (psiStates.get(successorEntry.first)) { targetStateIsReachable = true; } } diff --git a/src/models/Dtmc.h b/src/models/Dtmc.h index 4ccbda8b4..0e30f8753 100644 --- a/src/models/Dtmc.h +++ b/src/models/Dtmc.h @@ -139,7 +139,7 @@ public: // Is there any state in the subsystem? if(subSysStates.getNumberOfSetBits() == 0) { LOG4CPLUS_ERROR(logger, "No states in subsystem!"); - return storm::models::Dtmc(storm::storage::SparseMatrix(0), + return storm::models::Dtmc(storm::storage::SparseMatrix(), storm::models::AtomicPropositionsLabeling(this->getStateLabeling(), subSysStates), boost::optional>(), boost::optional>(), @@ -189,7 +189,7 @@ public: // 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. - storm::storage::SparseMatrix newMat(newStateCount, subSysTransitionCount + newStateCount); + storm::storage::SparseMatrixBuilder newMatBuilder(newStateCount, subSysTransitionCount + newStateCount); // Now fill the matrix. newRow = 0; @@ -199,14 +199,14 @@ public: // Transfer transitions for(auto& entry : origMat.getRow(row)) { if(subSysStates.get(entry.first)) { - newMat.addNextValue(newRow, stateMapping[entry.first], entry.second); + newMatBuilder.addNextValue(newRow, stateMapping[entry.first], entry.second); } else { rest += entry.second; } } // Insert the transition taking care of the remaining outgoing probability. - newMat.addNextValue(newRow, newStateCount - 1, rest); + newMatBuilder.addNextValue(newRow, newStateCount - 1, rest); rest = storm::utility::constantZero(); newRow++; @@ -214,9 +214,7 @@ public: } // Insert last transition: self loop on s_b - newMat.addNextValue(newStateCount - 1, newStateCount - 1, storm::utility::constantOne()); - - newMat.finalize(); + newMatBuilder.addNextValue(newStateCount - 1, newStateCount - 1, storm::utility::constantOne()); // 3. Take care of the labeling. storm::models::AtomicPropositionsLabeling newLabeling = storm::models::AtomicPropositionsLabeling(this->getStateLabeling(), subSysStates); @@ -245,7 +243,7 @@ public: boost::optional> newTransitionRewards; if(this->hasTransitionRewards()) { - storm::storage::SparseMatrix newTransRewards(newStateCount, subSysTransitionCount + newStateCount); + storm::storage::SparseMatrixBuilder newTransRewardsBuilder(newStateCount, subSysTransitionCount + newStateCount); // Copy the rewards for the kept states newRow = 0; @@ -254,18 +252,18 @@ public: // Transfer transition rewards for(auto& entry : this->getTransitionRewardMatrix().getRow(row)) { if(subSysStates.get(entry.first)) { - newTransRewards.addNextValue(newRow, stateMapping[entry.first], entry.second); + newTransRewardsBuilder.addNextValue(newRow, stateMapping[entry.first], entry.second); } } // Insert the reward (e.g. 0) for the transition taking care of the remaining outgoing probability. - newTransRewards.addNextValue(newRow, newStateCount - 1, storm::utility::constantZero()); + newTransRewardsBuilder.addNextValue(newRow, newStateCount - 1, storm::utility::constantZero()); newRow++; } } - newTransitionRewards = newTransRewards; + newTransitionRewards = newTransRewardsBuilder.build(); } boost::optional>> newChoiceLabels; @@ -283,12 +281,7 @@ public: } // 5. Make Dtmc from its parts and return it - return storm::models::Dtmc(newMat, - newLabeling, - newStateRewards, - newTransitionRewards, - newChoiceLabels - ); + return storm::models::Dtmc(newMatBuilder.build(), newLabeling, newStateRewards, std::move(newTransitionRewards), newChoiceLabels); } diff --git a/src/models/MarkovAutomaton.h b/src/models/MarkovAutomaton.h index 547bd7dce..8dce30e6b 100644 --- a/src/models/MarkovAutomaton.h +++ b/src/models/MarkovAutomaton.h @@ -127,7 +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; + storm::storage::SparseMatrixBuilder newTransitionMatrixBuilder; std::vector newNondeterministicChoiceIndices(this->getNumberOfStates() + 1); // Now copy over all choices that need to be kept. @@ -149,7 +149,7 @@ namespace storm { for (uint_fast64_t row = this->nondeterministicChoiceIndices[state] + (this->isHybridState(state) ? 1 : 0); row < this->nondeterministicChoiceIndices[state + 1]; ++row) { for (auto const& entry : this->transitionMatrix.getRow(row)) { - newTransitionMatrix.addNextValue(currentChoice, entry.first, entry.second); + newTransitionMatrixBuilder.addNextValue(currentChoice, entry.first, entry.second); } ++currentChoice; } @@ -159,8 +159,7 @@ namespace storm { newNondeterministicChoiceIndices.back() = currentChoice; // Finalize the matrix and put the new transition data in place. - newTransitionMatrix.finalize(); - this->transitionMatrix = std::move(newTransitionMatrix); + this->transitionMatrix = newTransitionMatrixBuilder.build(); this->nondeterministicChoiceIndices = std::move(newNondeterministicChoiceIndices); // Mark the automaton as closed. diff --git a/src/models/Mdp.h b/src/models/Mdp.h index aad76c1ef..bcb9d0eac 100644 --- a/src/models/Mdp.h +++ b/src/models/Mdp.h @@ -143,7 +143,7 @@ public: std::vector> const& choiceLabeling = this->getChoiceLabeling(); - storm::storage::SparseMatrix transitionMatrix; + storm::storage::SparseMatrixBuilder transitionMatrixBuilder; std::vector nondeterministicChoiceIndices; std::vector> newChoiceLabeling; @@ -161,7 +161,7 @@ public: } stateHasValidChoice = true; for (auto const& entry : this->getTransitionMatrix().getRow(choice)) { - transitionMatrix.addNextValue(currentRow, entry.column(), entry.value()); + transitionMatrixBuilder.addNextValue(currentRow, entry.first, entry.second); } newChoiceLabeling.emplace_back(choiceLabeling[choice]); ++currentRow; @@ -171,15 +171,15 @@ 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.addNextValue(currentRow, state, storm::utility::constantOne()); + transitionMatrixBuilder.addNextValue(currentRow, state, storm::utility::constantOne()); newChoiceLabeling.emplace_back(); ++currentRow; } } - 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)); + Mdp restrictedMdp(transitionMatrixBuilder.build(), 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)); return restrictedMdp; } diff --git a/src/solver/AbstractNondeterministicLinearEquationSolver.h b/src/solver/AbstractNondeterministicLinearEquationSolver.h index 8d6b41acc..d1cc8bbf2 100644 --- a/src/solver/AbstractNondeterministicLinearEquationSolver.h +++ b/src/solver/AbstractNondeterministicLinearEquationSolver.h @@ -99,21 +99,34 @@ namespace storm { // Proceed with the iterations as long as the method did not converge or reach the // user-specified maximum number of iterations. + std::chrono::nanoseconds multTime(0); + std::chrono::nanoseconds addTime(0); + std::chrono::nanoseconds reduceTime(0); + std::chrono::nanoseconds convergedTime(0); + auto clock = std::chrono::high_resolution_clock::now(); while (!converged && iterations < maxIterations) { // Compute x' = A*x + b. + clock = std::chrono::high_resolution_clock::now(); A.multiplyWithVector(*currentX, *multiplyResult); + multTime += std::chrono::high_resolution_clock::now() - clock; + clock = std::chrono::high_resolution_clock::now(); storm::utility::vector::addVectorsInPlace(*multiplyResult, b); + addTime += std::chrono::high_resolution_clock::now() - clock; // Reduce the vector x' by applying min/max for all non-deterministic choices as given by the topmost // element of the min/max operator stack. + clock = std::chrono::high_resolution_clock::now(); if (minimize) { storm::utility::vector::reduceVectorMin(*multiplyResult, *newX, nondeterministicChoiceIndices); } else { storm::utility::vector::reduceVectorMax(*multiplyResult, *newX, nondeterministicChoiceIndices); } + reduceTime += std::chrono::high_resolution_clock::now() - clock; // Determine whether the method converged. + clock = std::chrono::high_resolution_clock::now(); converged = storm::utility::vector::equalModuloPrecision(*currentX, *newX, precision, relative); + convergedTime += std::chrono::high_resolution_clock::now() - clock; // Update environment variables. swap = currentX; @@ -121,6 +134,11 @@ namespace storm { newX = swap; ++iterations; } + + std::cout << std::chrono::duration_cast(multTime).count() << "ms" << std::endl; + std::cout << std::chrono::duration_cast(addTime).count() << "ms" << std::endl; + std::cout << std::chrono::duration_cast(reduceTime).count() << "ms" << std::endl; + std::cout << std::chrono::duration_cast(convergedTime).count() << "ms" << std::endl; // If we performed an odd number of iterations, we need to swap the x and currentX, because the newest result // is currently stored in currentX, but x is the output vector. diff --git a/src/storage/SparseMatrix.cpp b/src/storage/SparseMatrix.cpp index 18db8363c..608fe92be 100644 --- a/src/storage/SparseMatrix.cpp +++ b/src/storage/SparseMatrix.cpp @@ -693,7 +693,7 @@ namespace storm { template void SparseMatrix::multiplyWithVector(std::vector const& vector, std::vector& result) const { #ifdef STORM_HAVE_INTELTBB - tbb::parallel_for(tbb::blocked_range(0, result.size()), tbbHelper_MatrixRowVectorScalarProduct, std::vector, T>(this, &vector, &result)); + tbb::parallel_for(tbb::blocked_range(0, result.size()), TbbMatrixRowVectorScalarProduct(*this, vector, result)); #else const_iterator it = this->begin(); const_iterator ite = this->begin(); @@ -865,30 +865,26 @@ namespace storm { template std::ostream& operator<<(std::ostream& out, SparseMatrix const& matrix); #ifdef STORM_HAVE_INTELTBB + template + TbbMatrixRowVectorScalarProduct::TbbMatrixRowVectorScalarProduct(SparseMatrix const& matrix, std::vector const& vector, std::vector& result) : result(result), vector(vector), matrix(matrix) { + // Intentionally left empty. + } - template - tbbHelper_MatrixRowVectorScalarProduct::tbbHelper_MatrixRowVectorScalarProduct(M const* matrixA, V const* vectorX, V * resultVector) : matrixA(matrixA), vectorX(vectorX), resultVector(resultVector) {} - - template - void tbbHelper_MatrixRowVectorScalarProduct::operator() (const tbb::blocked_range& r) const { - for (uint_fast64_t row = r.begin(); row < r.end(); ++row) { - uint_fast64_t index = matrixA->rowIndications.at(row); - uint_fast64_t indexEnd = matrixA->rowIndications.at(row + 1); - - // Initialize the result to be 0. - T element = storm::utility::constantZero(); - - for (; index != indexEnd; ++index) { - element += matrixA->valueStorage.at(index) * vectorX->at(matrixA->columnIndications.at(index)); + template + void TbbMatrixRowVectorScalarProduct::operator() (tbb::blocked_range const& range) const { + for (uint_fast64_t row = range.begin(); row < range.end(); ++row) { + ValueType element = storm::utility::constantZero(); + + for (typename SparseMatrix::const_iterator it = matrix.begin(row), ite = matrix.end(row); it != ite; ++it) { + element += it->second * vector[it->first]; } - // Write back to the result Vector - resultVector->at(row) = element; + result[row] = element; } } - // Explicit instanciations of specializations of this template here. - template class tbbHelper_MatrixRowVectorScalarProduct, std::vector, double>; + // Explicitly instantiate the helper class. + template class TbbMatrixRowVectorScalarProduct; #endif diff --git a/src/storage/SparseMatrix.h b/src/storage/SparseMatrix.h index d4f481e04..3654dc1b8 100644 --- a/src/storage/SparseMatrix.h +++ b/src/storage/SparseMatrix.h @@ -36,8 +36,8 @@ namespace storm { #ifdef STORM_HAVE_INTELTBB // Forward declaration of the TBB Helper class. - template - class tbbHelper_MatrixRowVectorScalarProduct; + template + class TbbMatrixRowVectorScalarProduct; #endif // Forward declare matrix class. @@ -642,20 +642,34 @@ namespace storm { #ifdef STORM_HAVE_INTELTBB /*! - * This function is a helper for the parallel execution of the multipliyWithVector method. - * It uses Intel's TBB parallel_for paradigm to split up the row/vector multiplication and summation. + * This class is a helper class for parallel matrix-vector multiplication using Intel TBB. */ - template - class tbbHelper_MatrixRowVectorScalarProduct { + template + class TbbMatrixRowVectorScalarProduct { public: - tbbHelper_MatrixRowVectorScalarProduct(M const* matrixA, V const* vectorX, V * resultVector); + /*! + * Constructs a helper object with which TBB can perform parallel matrix-vector multiplication. + * + * @param matrix The matrix to use for the multiplication. + * @param vector The vector with which to multiply the matrix. + * @param result The vector that is supposed to hold the result after performing the multiplication. + */ + TbbMatrixRowVectorScalarProduct(SparseMatrix const& matrix, std::vector const& vector, std::vector& result); - void operator() (const tbb::blocked_range& r) const; + /*! + * Performs the actual multiplication of a row with the vector. + */ + void operator() (tbb::blocked_range const& range) const; private: - V * resultVector; - V const* vectorX; - M const* matrixA; + // The vector that is supposed to hold the result after performing the multiplication. + std::vector& result; + + // The vector with which to multiply the matrix. + std::vector const& vector; + + // The matrix to use for the multiplication. + SparseMatrix const& matrix; }; #endif diff --git a/src/utility/vector.h b/src/utility/vector.h index ee0c96f41..018e36e88 100644 --- a/src/utility/vector.h +++ b/src/utility/vector.h @@ -135,8 +135,11 @@ namespace storm { LOG4CPLUS_ERROR(logger, "Lengths of vectors do not match, which makes operation impossible."); throw storm::exceptions::InvalidArgumentException() << "Length of vectors do not match, which makes operation impossible."; } - +#ifdef STORM_HAVE_INTELTBB + tbb::parallel_for(tbb::blocked_range(0, target.size(), target.size() / 4), [&](tbb::blocked_range& range) { for (uint_fast64_t current = range.begin(), end = range.end(); current < end; ++current) { target[current] += summand[current]; } }); +#else std::transform(target.begin(), target.end(), summand.begin(), target.begin(), std::plus()); +#endif } /*!