From 21d9e91586c1223b518c969c1cf0991fec91bf65 Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 28 Aug 2015 23:13:24 +0200 Subject: [PATCH] work towards interval reward model Former-commit-id: 24f7e9684fe3daed42af70c57191f2645f985e7b --- CMakeLists.txt | 2 +- .../helper/SparseMarkovAutomatonCslHelper.cpp | 2 +- .../prctl/helper/SparseMdpPrctlHelper.cpp | 41 +++++++++++-------- .../prctl/helper/SparseMdpPrctlHelper.h | 7 ++-- src/models/sparse/StandardRewardModel.cpp | 15 +++++-- src/models/sparse/StandardRewardModel.h | 2 +- src/storage/SparseMatrix.cpp | 25 ++++++++--- src/storage/SparseMatrix.h | 3 +- src/utility/vector.h | 36 ++++++++-------- 9 files changed, 83 insertions(+), 50 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 5d67dcefa..afd5fa66e 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -164,7 +164,7 @@ else(CLANG) endif() add_definitions(-DBOOST_RESULT_OF_USE_DECLTYPE) - set (CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -std=c++11 -stdlib=${CLANG_STDLIB} -Wall -pedantic -Wno-newline-eof -Wno-mismatched-tags -ftemplate-depth=1024") + set (CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -std=c++14 -stdlib=${CLANG_STDLIB} -Wall -pedantic -Wno-newline-eof -Wno-mismatched-tags -ftemplate-depth=1024") set (CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -Wall -pedantic") # Turn on popcnt instruction if desired (yes by default) diff --git a/src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp b/src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp index c8138d908..5157e1eb4 100644 --- a/src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp +++ b/src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp @@ -178,7 +178,7 @@ namespace storm { template std::vector SparseMarkovAutomatonCslHelper::computeUntilProbabilities(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { - return storm::modelchecker::helper::SparseMdpPrctlHelper::computeUntilProbabilities(minimize, transitionMatrix, backwardTransitions, phiStates, psiStates, qualitative, minMaxLinearEquationSolverFactory); + return storm::modelchecker::helper::SparseMdpPrctlHelper::computeUntilProbabilities(minimize, transitionMatrix, backwardTransitions, phiStates, psiStates, qualitative, minMaxLinearEquationSolverFactory); } template diff --git a/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp index f771ceea3..9af12ad97 100644 --- a/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp +++ b/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp @@ -1,5 +1,7 @@ #include "src/modelchecker/prctl/helper/SparseMdpPrctlHelper.h" +#include "src/models/sparse/StandardRewardModel.h" + #include "src/storage/MaximalEndComponentDecomposition.h" #include "src/utility/macros.h" @@ -18,8 +20,8 @@ namespace storm { namespace modelchecker { namespace helper { - template - std::vector SparseMdpPrctlHelper::computeBoundedUntilProbabilities(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, uint_fast64_t stepBound, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { + template + std::vector SparseMdpPrctlHelper::computeBoundedUntilProbabilities(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, uint_fast64_t stepBound, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { std::vector result(transitionMatrix.getRowCount(), storm::utility::zero()); // Determine the states that have 0 probability of reaching the target states. @@ -52,8 +54,8 @@ namespace storm { return result; } - template - std::vector SparseMdpPrctlHelper::computeNextProbabilities(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& nextStates, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { + template + std::vector SparseMdpPrctlHelper::computeNextProbabilities(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& nextStates, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { // Create the vector with which to multiply and initialize it correctly. std::vector result(transitionMatrix.getRowCount()); storm::utility::vector::setVectorValues(result, nextStates, storm::utility::one()); @@ -64,8 +66,8 @@ namespace storm { return result; } - template - std::vector SparseMdpPrctlHelper::computeUntilProbabilities(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { + template + std::vector SparseMdpPrctlHelper::computeUntilProbabilities(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { uint_fast64_t numberOfStates = transitionMatrix.getRowCount(); // We need to identify the states which have to be taken out of the matrix, i.e. @@ -121,8 +123,9 @@ namespace storm { return result; } - template - std::vector SparseMdpPrctlHelper::computeInstantaneousRewards(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepCount, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { + template + template + std::vector SparseMdpPrctlHelper::computeInstantaneousRewards(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepCount, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { // Only compute the result if the model has a state-based reward this->getModel(). STORM_LOG_THROW(rewardModel.hasStateRewards(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); @@ -135,8 +138,9 @@ namespace storm { return result; } - template - std::vector SparseMdpPrctlHelper::computeCumulativeRewards(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { + template + template + std::vector SparseMdpPrctlHelper::computeCumulativeRewards(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { // Only compute the result if the model has at least one reward this->getModel(). STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); @@ -157,8 +161,9 @@ namespace storm { return result; } - template - std::vector SparseMdpPrctlHelper::computeReachabilityRewards(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, RewardModelType const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { + template + template + std::vector SparseMdpPrctlHelper::computeReachabilityRewards(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, RewardModelType const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { // Only compute the result if the model has at least one reward this->getModel(). STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); @@ -214,8 +219,8 @@ namespace storm { return result; } - template - std::vector SparseMdpPrctlHelper::computeLongRunAverage(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { + template + std::vector SparseMdpPrctlHelper::computeLongRunAverage(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { // If there are no goal states, we avoid the computation and directly return zero. uint_fast64_t numberOfStates = transitionMatrix.getRowGroupCount(); if (psiStates.empty()) { @@ -364,8 +369,8 @@ namespace storm { return result; } - template - ValueType SparseMdpPrctlHelper::computeLraForMaximalEndComponent(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& psiStates, storm::storage::MaximalEndComponent const& mec) { + template + ValueType SparseMdpPrctlHelper::computeLraForMaximalEndComponent(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& psiStates, storm::storage::MaximalEndComponent const& mec) { std::shared_ptr solver = storm::utility::solver::getLpSolver("LRA for MEC"); solver->setModelSense(minimize ? storm::solver::LpSolver::ModelSense::Maximize : storm::solver::LpSolver::ModelSense::Minimize); @@ -409,6 +414,10 @@ namespace storm { } template class SparseMdpPrctlHelper; + template std::vector SparseMdpPrctlHelper::computeInstantaneousRewards(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, storm::models::sparse::StandardRewardModel const& rewardModel, uint_fast64_t stepCount, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + template std::vector SparseMdpPrctlHelper::computeCumulativeRewards(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, storm::models::sparse::StandardRewardModel const& rewardModel, uint_fast64_t stepBound, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + template std::vector SparseMdpPrctlHelper::computeReachabilityRewards(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::models::sparse::StandardRewardModel const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + } } } diff --git a/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.h b/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.h index 518e0e118..b584e5d28 100644 --- a/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.h +++ b/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.h @@ -3,8 +3,6 @@ #include -#include "src/models/sparse/StandardRewardModel.h" - #include "src/storage/SparseMatrix.h" #include "src/storage/BitVector.h" #include "src/storage/MaximalEndComponent.h" @@ -15,7 +13,7 @@ namespace storm { namespace modelchecker { namespace helper { - template > + template class SparseMdpPrctlHelper { public: static std::vector computeBoundedUntilProbabilities(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, uint_fast64_t stepBound, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); @@ -24,10 +22,13 @@ namespace storm { static std::vector computeUntilProbabilities(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + template static std::vector computeInstantaneousRewards(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepCount, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + template static std::vector computeCumulativeRewards(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + template static std::vector computeReachabilityRewards(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, RewardModelType const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); static std::vector computeLongRunAverage(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); diff --git a/src/models/sparse/StandardRewardModel.cpp b/src/models/sparse/StandardRewardModel.cpp index 0ba437c96..b8fa2e3be 100644 --- a/src/models/sparse/StandardRewardModel.cpp +++ b/src/models/sparse/StandardRewardModel.cpp @@ -141,7 +141,7 @@ namespace storm { template template - std::vector StandardRewardModel::getTotalRewardVector(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& weights) const { + std::vector StandardRewardModel::getTotalRewardVector(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& weights) const { std::vector result = this->hasTransitionRewards() ? transitionMatrix.getPointwiseProductRowSumVector(this->getTransitionRewardMatrix()) : (this->hasStateActionRewards() ? this->getStateActionRewardVector() : std::vector(transitionMatrix.getRowCount())); if (!this->hasTransitionRewards() && this->hasStateActionRewards()) { // If we initialized the result with the state-action rewards we can scale the result in place. @@ -150,7 +150,7 @@ namespace storm { if (this->hasStateActionRewards() && this->hasTransitionRewards()) { // If we initialized the result with the transition rewards and still have state-action rewards, // we need to add the scaled vector directly. - storm::utility::vector::applyPointwise(weights, this->getStateActionRewardVector(), result, [] (ValueType const& a, ValueType const& b, ValueType const& c) { return c + a * b; } ); + storm::utility::vector::applyPointwise(weights, this->getStateActionRewardVector(), result, [] (MatrixValueType const& weight, ValueType const& rewardElement, ValueType const& resultElement) { return resultElement + weight * rewardElement; } ); } if (this->hasStateRewards()) { storm::utility::vector::addVectorToGroupedVector(result, this->getStateRewardVector(), transitionMatrix.getRowGroupIndices()); @@ -243,7 +243,7 @@ namespace storm { template std::vector StandardRewardModel::getTotalRewardVector(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& weights) const; template void StandardRewardModel::reduceToStateBasedRewards(storm::storage::SparseMatrix const& transitionMatrix, bool reduceToStateRewards); template class StandardRewardModel; -// template std::ostream& operator<<(std::ostream& out, StandardRewardModel const& rewardModel); + template std::ostream& operator<<(std::ostream& out, StandardRewardModel const& rewardModel); #ifdef STORM_HAVE_CARL template std::vector StandardRewardModel::getTotalRewardVector(uint_fast64_t numberOfRows, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& filter) const; @@ -251,7 +251,14 @@ namespace storm { template std::vector StandardRewardModel::getTotalRewardVector(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& weights) const; template void StandardRewardModel::reduceToStateBasedRewards(storm::storage::SparseMatrix const& transitionMatrix, bool reduceToStateRewards); template class StandardRewardModel; -// template std::ostream& operator<<(std::ostream& out, StandardRewardModel const& rewardModel); + template std::ostream& operator<<(std::ostream& out, StandardRewardModel const& rewardModel); + + template std::vector StandardRewardModel::getTotalRewardVector(uint_fast64_t numberOfRows, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& filter) const; + template std::vector StandardRewardModel::getTotalRewardVector(storm::storage::SparseMatrix const& transitionMatrix) const; + template std::vector StandardRewardModel::getTotalRewardVector(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& weights) const; + template void StandardRewardModel::reduceToStateBasedRewards(storm::storage::SparseMatrix const& transitionMatrix, bool reduceToStateRewards); + template class StandardRewardModel; + template std::ostream& operator<<(std::ostream& out, StandardRewardModel const& rewardModel); #endif } diff --git a/src/models/sparse/StandardRewardModel.h b/src/models/sparse/StandardRewardModel.h index 7bf8afe19..457d4df5b 100644 --- a/src/models/sparse/StandardRewardModel.h +++ b/src/models/sparse/StandardRewardModel.h @@ -178,7 +178,7 @@ namespace storm { * @return The full state-action reward vector. */ template - std::vector getTotalRewardVector(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& weights) const; + std::vector getTotalRewardVector(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& weights) const; /*! * Creates a vector representing the complete reward vector based on the state-, state-action- and diff --git a/src/storage/SparseMatrix.cpp b/src/storage/SparseMatrix.cpp index eee581ebc..21ecfd931 100644 --- a/src/storage/SparseMatrix.cpp +++ b/src/storage/SparseMatrix.cpp @@ -825,21 +825,24 @@ namespace storm { #endif template - std::vector SparseMatrix::getPointwiseProductRowSumVector(storm::storage::SparseMatrix const& otherMatrix) const { - std::vector result(rowCount, storm::utility::zero()); + template + std::vector SparseMatrix::getPointwiseProductRowSumVector(storm::storage::SparseMatrix const& otherMatrix) const { + std::vector result(rowCount, storm::utility::zero()); // 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 (index_type row = 0; row < rowCount && row < otherMatrix.rowCount; ++row) { - for (const_iterator it1 = this->begin(row), ite1 = this->end(row), it2 = otherMatrix.begin(row), ite2 = otherMatrix.end(row); it1 != ite1 && it2 != ite2; ++it1) { + for (index_type row = 0; row < rowCount && row < otherMatrix.getRowCount(); ++row) { + typename storm::storage::SparseMatrix::const_iterator it2 = otherMatrix.begin(row); + typename storm::storage::SparseMatrix::const_iterator ite2 = otherMatrix.end(row); + for (const_iterator it1 = this->begin(row), ite1 = this->end(row); it1 != ite1 && it2 != ite2; ++it1) { if (it1->getColumn() < it2->getColumn()) { continue; } else { // If the precondition of this method (i.e. that the given matrix is a submatrix // of the current one) was fulfilled, we know now that the two elements are in // the same column, so we can multiply and add them to the row sum vector. - result[row] += it2->getValue() * it1->getValue(); + result[row] += it2->getValue() * OtherValueType(it1->getValue()); ++it2; } } @@ -1161,18 +1164,27 @@ namespace storm { template class SparseMatrixBuilder; template class SparseMatrix; template std::ostream& operator<<(std::ostream& out, SparseMatrix const& matrix); + template std::vector SparseMatrix::getPointwiseProductRowSumVector(storm::storage::SparseMatrix const& otherMatrix) const; + template std::vector SparseMatrix::getPointwiseProductRowSumVector(storm::storage::SparseMatrix const& otherMatrix) const; + template std::vector SparseMatrix::getPointwiseProductRowSumVector(storm::storage::SparseMatrix const& otherMatrix) const; + //float template class MatrixEntry::index_type, float>; template std::ostream& operator<<(std::ostream& out, MatrixEntry const& entry); template class SparseMatrixBuilder; template class SparseMatrix; template std::ostream& operator<<(std::ostream& out, SparseMatrix const& matrix); + template std::vector SparseMatrix::getPointwiseProductRowSumVector(storm::storage::SparseMatrix const& otherMatrix) const; + template std::vector SparseMatrix::getPointwiseProductRowSumVector(storm::storage::SparseMatrix const& otherMatrix) const; + //int template class MatrixEntry::index_type, int>; template std::ostream& operator<<(std::ostream& out, MatrixEntry const& entry); template class SparseMatrixBuilder; template class SparseMatrix; template std::ostream& operator<<(std::ostream& out, SparseMatrix const& matrix); + template std::vector SparseMatrix::getPointwiseProductRowSumVector(storm::storage::SparseMatrix const& otherMatrix) const; + #ifdef STORM_HAVE_CARL // Rat Function template class MatrixEntry::index_type, RationalFunction>; @@ -1180,12 +1192,15 @@ namespace storm { template class SparseMatrixBuilder; template class SparseMatrix; template std::ostream& operator<<(std::ostream& out, SparseMatrix const& matrix); + template std::vector SparseMatrix::getPointwiseProductRowSumVector(storm::storage::SparseMatrix const& otherMatrix) const; + // Intervals template class MatrixEntry::index_type, Interval>; template std::ostream& operator<<(std::ostream& out, MatrixEntry const& entry); template class SparseMatrixBuilder; template class SparseMatrix; template std::ostream& operator<<(std::ostream& out, SparseMatrix const& matrix); + template std::vector SparseMatrix::getPointwiseProductRowSumVector(storm::storage::SparseMatrix const& otherMatrix) const; #endif diff --git a/src/storage/SparseMatrix.h b/src/storage/SparseMatrix.h index 71fe4078e..03de1bd6b 100644 --- a/src/storage/SparseMatrix.h +++ b/src/storage/SparseMatrix.h @@ -678,7 +678,8 @@ namespace storm { * @return A vector containing the sum of the entries in each row of the matrix resulting from pointwise * multiplication of the current matrix with the given matrix. */ - std::vector getPointwiseProductRowSumVector(storm::storage::SparseMatrix const& otherMatrix) const; + template + std::vector getPointwiseProductRowSumVector(storm::storage::SparseMatrix const& otherMatrix) const; /*! * Multiplies the matrix with the given vector and writes the result to the given result vector. If a diff --git a/src/utility/vector.h b/src/utility/vector.h index dd0ac7cf3..92c4a4265 100644 --- a/src/utility/vector.h +++ b/src/utility/vector.h @@ -200,8 +200,8 @@ namespace storm { * @param secondOperand The second operand. * @param target The target vector. */ - template - void applyPointwise(std::vector const& firstOperand, std::vector const& secondOperand, std::vector& target, std::function const& function) { + template + void applyPointwise(std::vector const& firstOperand, std::vector const& secondOperand, std::vector& target, std::function const& function) { #ifdef STORM_HAVE_INTELTBB tbb::parallel_for(tbb::blocked_range(0, target.size()), [&](tbb::blocked_range const& range) { @@ -238,8 +238,8 @@ namespace storm { * @param secondOperand The second operand. * @param target The target vector. */ - template - void applyPointwise(std::vector const& firstOperand, std::vector const& secondOperand, std::vector& target, std::function function) { + template + void applyPointwise(std::vector const& firstOperand, std::vector const& secondOperand, std::vector& target, std::function function) { #ifdef STORM_HAVE_INTELTBB tbb::parallel_for(tbb::blocked_range(0, target.size()), [&](tbb::blocked_range const& range) { @@ -257,8 +257,8 @@ namespace storm { * @param target The target vector. * @param function The function to apply. */ - template - void applyPointwise(std::vector const& operand, std::vector& target, std::function const& function) { + template + void applyPointwise(std::vector const& operand, std::vector& target, std::function const& function) { #ifdef STORM_HAVE_INTELTBB tbb::parallel_for(tbb::blocked_range(0, target.size()), [&](tbb::blocked_range const& range) { @@ -276,9 +276,9 @@ namespace storm { * @param secondOperand The second operand * @param target The target vector. */ - template - void addVectors(std::vector const& firstOperand, std::vector const& secondOperand, std::vector& target) { - applyPointwise(firstOperand, secondOperand, target, std::plus()); + template + void addVectors(std::vector const& firstOperand, std::vector const& secondOperand, std::vector& target) { + applyPointwise(firstOperand, secondOperand, target, std::plus<>()); } /*! @@ -288,9 +288,9 @@ namespace storm { * @param secondOperand The second operand * @param target The target vector. */ - template - void subtractVectors(std::vector const& firstOperand, std::vector const& secondOperand, std::vector& target) { - applyPointwise(firstOperand, secondOperand, target, std::minus()); + template + void subtractVectors(std::vector const& firstOperand, std::vector const& secondOperand, std::vector& target) { + applyPointwise(firstOperand, secondOperand, target, std::minus<>()); } /*! @@ -300,9 +300,9 @@ namespace storm { * @param secondOperand The second operand * @param target The target vector. */ - template - void multiplyVectorsPointwise(std::vector const& firstOperand, std::vector const& secondOperand, std::vector& target) { - applyPointwise(firstOperand, secondOperand, target, std::multiplies()); + template + void multiplyVectorsPointwise(std::vector const& firstOperand, std::vector const& secondOperand, std::vector& target) { + applyPointwise(firstOperand, secondOperand, target, std::multiplies<>()); } /*! @@ -311,9 +311,9 @@ namespace storm { * @param target The first summand and target vector. * @param summand The second summand. */ - template - void scaleVectorInPlace(std::vector& target, T const& factor) { - applyPointwise(target, target, [&] (T const& argument) { return argument * factor; }); + template + void scaleVectorInPlace(std::vector& target, ValueType2 const& factor) { + applyPointwise(target, target, [&] (ValueType1 const& argument) -> ValueType1 { return argument * factor; }); } /*!