sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

work towards interval reward model 

Former-commit-id: 24f7e9684f
tempestpy_adaptions
dehnert 9 years ago
parent
36b67a3a38
commit
21d9e91586
9 changed files with 83 additions and 50 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 2
      CMakeLists.txt
  2. 2
      src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp
  3. 41
      src/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp
  4. 7
      src/modelchecker/prctl/helper/SparseMdpPrctlHelper.h
  5. 15
      src/models/sparse/StandardRewardModel.cpp
  6. 2
      src/models/sparse/StandardRewardModel.h
  7. 25
      src/storage/SparseMatrix.cpp
  8. 3
      src/storage/SparseMatrix.h
  9. 36
      src/utility/vector.h

2
CMakeLists.txt
View File

@ -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)

2
src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp
View File

@ -178,7 +178,7 @@ namespace storm {
template<typename ValueType, typename RewardModelType>
std::vector<ValueType> SparseMarkovAutomatonCslHelper<ValueType, RewardModelType>::computeUntilProbabilities(bool minimize, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory) {
return storm::modelchecker::helper::SparseMdpPrctlHelper<ValueType, RewardModelType>::computeUntilProbabilities(minimize, transitionMatrix, backwardTransitions, phiStates, psiStates, qualitative, minMaxLinearEquationSolverFactory);
return storm::modelchecker::helper::SparseMdpPrctlHelper<ValueType>::computeUntilProbabilities(minimize, transitionMatrix, backwardTransitions, phiStates, psiStates, qualitative, minMaxLinearEquationSolverFactory);
}
template<typename ValueType, typename RewardModelType>

41
src/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp
View File

@ -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<typename ValueType, typename RewardModelType>
std::vector<ValueType> SparseMdpPrctlHelper<ValueType, RewardModelType>::computeBoundedUntilProbabilities(bool minimize, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, uint_fast64_t stepBound, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory) {
template<typename ValueType>
std::vector<ValueType> SparseMdpPrctlHelper<ValueType>::computeBoundedUntilProbabilities(bool minimize, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, uint_fast64_t stepBound, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory) {
std::vector<ValueType> result(transitionMatrix.getRowCount(), storm::utility::zero<ValueType>());
// Determine the states that have 0 probability of reaching the target states.
@ -52,8 +54,8 @@ namespace storm {
return result;
}
template<typename ValueType, typename RewardModelType>
std::vector<ValueType> SparseMdpPrctlHelper<ValueType, RewardModelType>::computeNextProbabilities(bool minimize, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector const& nextStates, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory) {
template<typename ValueType>
std::vector<ValueType> SparseMdpPrctlHelper<ValueType>::computeNextProbabilities(bool minimize, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector const& nextStates, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory) {
// Create the vector with which to multiply and initialize it correctly.
std::vector<ValueType> result(transitionMatrix.getRowCount());
storm::utility::vector::setVectorValues(result, nextStates, storm::utility::one<ValueType>());
@ -64,8 +66,8 @@ namespace storm {
return result;
}
template<typename ValueType, typename RewardModelType>
std::vector<ValueType> SparseMdpPrctlHelper<ValueType, RewardModelType>::computeUntilProbabilities(bool minimize, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory) {
template<typename ValueType>
std::vector<ValueType> SparseMdpPrctlHelper<ValueType>::computeUntilProbabilities(bool minimize, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> 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<typename ValueType, typename RewardModelType>
std::vector<ValueType> SparseMdpPrctlHelper<ValueType, RewardModelType>::computeInstantaneousRewards(bool minimize, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepCount, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory) {
template<typename ValueType>
template<typename RewardModelType>
std::vector<ValueType> SparseMdpPrctlHelper<ValueType>::computeInstantaneousRewards(bool minimize, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepCount, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> 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<typename ValueType, typename RewardModelType>
std::vector<ValueType> SparseMdpPrctlHelper<ValueType, RewardModelType>::computeCumulativeRewards(bool minimize, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory) {
template<typename ValueType>
template<typename RewardModelType>
std::vector<ValueType> SparseMdpPrctlHelper<ValueType>::computeCumulativeRewards(bool minimize, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> 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<typename ValueType, typename RewardModelType>
std::vector<ValueType> SparseMdpPrctlHelper<ValueType, RewardModelType>::computeReachabilityRewards(bool minimize, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, RewardModelType const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory) {
template<typename ValueType>
template<typename RewardModelType>
std::vector<ValueType> SparseMdpPrctlHelper<ValueType>::computeReachabilityRewards(bool minimize, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, RewardModelType const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> 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<typename ValueType, typename RewardModelType>
std::vector<ValueType> SparseMdpPrctlHelper<ValueType, RewardModelType>::computeLongRunAverage(bool minimize, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory) {
template<typename ValueType>
std::vector<ValueType> SparseMdpPrctlHelper<ValueType>::computeLongRunAverage(bool minimize, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> 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<typename ValueType, typename RewardModelType>
ValueType SparseMdpPrctlHelper<ValueType, RewardModelType>::computeLraForMaximalEndComponent(bool minimize, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector const& psiStates, storm::storage::MaximalEndComponent const& mec) {
template<typename ValueType>
ValueType SparseMdpPrctlHelper<ValueType>::computeLraForMaximalEndComponent(bool minimize, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector const& psiStates, storm::storage::MaximalEndComponent const& mec) {
std::shared_ptr<storm::solver::LpSolver> 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<double>;
template std::vector<double> SparseMdpPrctlHelper<double>::computeInstantaneousRewards(bool minimize, storm::storage::SparseMatrix<double> const& transitionMatrix, storm::models::sparse::StandardRewardModel<double> const& rewardModel, uint_fast64_t stepCount, storm::utility::solver::MinMaxLinearEquationSolverFactory<double> const& minMaxLinearEquationSolverFactory);
template std::vector<double> SparseMdpPrctlHelper<double>::computeCumulativeRewards(bool minimize, storm::storage::SparseMatrix<double> const& transitionMatrix, storm::models::sparse::StandardRewardModel<double> const& rewardModel, uint_fast64_t stepBound, storm::utility::solver::MinMaxLinearEquationSolverFactory<double> const& minMaxLinearEquationSolverFactory);
template std::vector<double> SparseMdpPrctlHelper<double>::computeReachabilityRewards(bool minimize, storm::storage::SparseMatrix<double> const& transitionMatrix, storm::storage::SparseMatrix<double> const& backwardTransitions, storm::models::sparse::StandardRewardModel<double> const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory<double> const& minMaxLinearEquationSolverFactory);
}
}
}

7
src/modelchecker/prctl/helper/SparseMdpPrctlHelper.h
View File

@ -3,8 +3,6 @@
#include <vector>
#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 <typename ValueType, typename RewardModelType = storm::models::sparse::StandardRewardModel<ValueType>>
template <typename ValueType>
class SparseMdpPrctlHelper {
public:
static std::vector<ValueType> computeBoundedUntilProbabilities(bool minimize, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, uint_fast64_t stepBound, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory);
@ -24,10 +22,13 @@ namespace storm {
static std::vector<ValueType> computeUntilProbabilities(bool minimize, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory);
template <typename RewardModelType>
static std::vector<ValueType> computeInstantaneousRewards(bool minimize, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepCount, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory);
template <typename RewardModelType>
static std::vector<ValueType> computeCumulativeRewards(bool minimize, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory);
template <typename RewardModelType>
static std::vector<ValueType> computeReachabilityRewards(bool minimize, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, RewardModelType const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory);
static std::vector<ValueType> computeLongRunAverage(bool minimize, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory);

15
src/models/sparse/StandardRewardModel.cpp
View File

@ -141,7 +141,7 @@ namespace storm {
template<typename ValueType>
template<typename MatrixValueType>
std::vector<ValueType> StandardRewardModel<ValueType>::getTotalRewardVector(storm::storage::SparseMatrix<MatrixValueType> const& transitionMatrix, std::vector<ValueType> const& weights) const {
std::vector<ValueType> StandardRewardModel<ValueType>::getTotalRewardVector(storm::storage::SparseMatrix<MatrixValueType> const& transitionMatrix, std::vector<MatrixValueType> const& weights) const {
std::vector<ValueType> result = this->hasTransitionRewards() ? transitionMatrix.getPointwiseProductRowSumVector(this->getTransitionRewardMatrix()) : (this->hasStateActionRewards() ? this->getStateActionRewardVector() : std::vector<ValueType>(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<ValueType>(weights, this->getStateActionRewardVector(), result, [] (ValueType const& a, ValueType const& b, ValueType const& c) { return c + a * b; } );
storm::utility::vector::applyPointwise<MatrixValueType, ValueType, ValueType>(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<float> StandardRewardModel<float>::getTotalRewardVector(storm::storage::SparseMatrix<float> const& transitionMatrix, std::vector<float> const& weights) const;
template void StandardRewardModel<float>::reduceToStateBasedRewards(storm::storage::SparseMatrix<float> const& transitionMatrix, bool reduceToStateRewards);
template class StandardRewardModel<float>;
// template std::ostream& operator<<<float>(std::ostream& out, StandardRewardModel<float> const& rewardModel);
template std::ostream& operator<<<float>(std::ostream& out, StandardRewardModel<float> const& rewardModel);
#ifdef STORM_HAVE_CARL
template std::vector<storm::RationalFunction> StandardRewardModel<storm::RationalFunction>::getTotalRewardVector(uint_fast64_t numberOfRows, storm::storage::SparseMatrix<storm::RationalFunction> const& transitionMatrix, storm::storage::BitVector const& filter) const;
@ -251,7 +251,14 @@ namespace storm {
template std::vector<storm::RationalFunction> StandardRewardModel<storm::RationalFunction>::getTotalRewardVector(storm::storage::SparseMatrix<storm::RationalFunction> const& transitionMatrix, std::vector<storm::RationalFunction> const& weights) const;
template void StandardRewardModel<storm::RationalFunction>::reduceToStateBasedRewards(storm::storage::SparseMatrix<storm::RationalFunction> const& transitionMatrix, bool reduceToStateRewards);
template class StandardRewardModel<storm::RationalFunction>;
// template std::ostream& operator<<<storm::RationalFunction>(std::ostream& out, StandardRewardModel<storm::RationalFunction> const& rewardModel);
template std::ostream& operator<<<storm::RationalFunction>(std::ostream& out, StandardRewardModel<storm::RationalFunction> const& rewardModel);
template std::vector<storm::Interval> StandardRewardModel<storm::Interval>::getTotalRewardVector(uint_fast64_t numberOfRows, storm::storage::SparseMatrix<double> const& transitionMatrix, storm::storage::BitVector const& filter) const;
template std::vector<storm::Interval> StandardRewardModel<storm::Interval>::getTotalRewardVector(storm::storage::SparseMatrix<double> const& transitionMatrix) const;
template std::vector<storm::Interval> StandardRewardModel<storm::Interval>::getTotalRewardVector(storm::storage::SparseMatrix<double> const& transitionMatrix, std::vector<double> const& weights) const;
template void StandardRewardModel<storm::Interval>::reduceToStateBasedRewards(storm::storage::SparseMatrix<double> const& transitionMatrix, bool reduceToStateRewards);
template class StandardRewardModel<storm::Interval>;
template std::ostream& operator<<<storm::Interval>(std::ostream& out, StandardRewardModel<storm::Interval> const& rewardModel);
#endif
}

2
src/models/sparse/StandardRewardModel.h
View File

@ -178,7 +178,7 @@ namespace storm {
* @return The full state-action reward vector.
*/
template<typename MatrixValueType>
std::vector<ValueType> getTotalRewardVector(storm::storage::SparseMatrix<MatrixValueType> const& transitionMatrix, std::vector<ValueType> const& weights) const;
std::vector<ValueType> getTotalRewardVector(storm::storage::SparseMatrix<MatrixValueType> const& transitionMatrix, std::vector<MatrixValueType> const& weights) const;
/*!
* Creates a vector representing the complete reward vector based on the state-, state-action- and

25
src/storage/SparseMatrix.cpp
View File

@ -825,21 +825,24 @@ namespace storm {
#endif
template<typename ValueType>
std::vector<ValueType> SparseMatrix<ValueType>::getPointwiseProductRowSumVector(storm::storage::SparseMatrix<ValueType> const& otherMatrix) const {
std::vector<ValueType> result(rowCount, storm::utility::zero<ValueType>());
template<typename OtherValueType, typename ResultValueType>
std::vector<ResultValueType> SparseMatrix<ValueType>::getPointwiseProductRowSumVector(storm::storage::SparseMatrix<OtherValueType> const& otherMatrix) const {
std::vector<ResultValueType> result(rowCount, storm::utility::zero<ResultValueType>());
// 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<OtherValueType>::const_iterator it2 = otherMatrix.begin(row);
typename storm::storage::SparseMatrix<OtherValueType>::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<double>;
template class SparseMatrix<double>;
template std::ostream& operator<<(std::ostream& out, SparseMatrix<double> const& matrix);
template std::vector<double> SparseMatrix<double>::getPointwiseProductRowSumVector(storm::storage::SparseMatrix<double> const& otherMatrix) const;
template std::vector<storm::RationalFunction> SparseMatrix<double>::getPointwiseProductRowSumVector(storm::storage::SparseMatrix<storm::RationalFunction> const& otherMatrix) const;
template std::vector<storm::Interval> SparseMatrix<double>::getPointwiseProductRowSumVector(storm::storage::SparseMatrix<storm::Interval> const& otherMatrix) const;
//float
template class MatrixEntry<typename SparseMatrix<float>::index_type, float>;
template std::ostream& operator<<(std::ostream& out, MatrixEntry<uint_fast64_t, float> const& entry);
template class SparseMatrixBuilder<float>;
template class SparseMatrix<float>;
template std::ostream& operator<<(std::ostream& out, SparseMatrix<float> const& matrix);
template std::vector<float> SparseMatrix<float>::getPointwiseProductRowSumVector(storm::storage::SparseMatrix<float> const& otherMatrix) const;
template std::vector<storm::RationalFunction> SparseMatrix<float>::getPointwiseProductRowSumVector(storm::storage::SparseMatrix<storm::RationalFunction> const& otherMatrix) const;
//int
template class MatrixEntry<typename SparseMatrix<int>::index_type, int>;
template std::ostream& operator<<(std::ostream& out, MatrixEntry<uint_fast64_t, int> const& entry);
template class SparseMatrixBuilder<int>;
template class SparseMatrix<int>;
template std::ostream& operator<<(std::ostream& out, SparseMatrix<int> const& matrix);
template std::vector<storm::RationalFunction> SparseMatrix<int>::getPointwiseProductRowSumVector(storm::storage::SparseMatrix<storm::RationalFunction> const& otherMatrix) const;
#ifdef STORM_HAVE_CARL
// Rat Function
template class MatrixEntry<typename SparseMatrix<RationalFunction>::index_type, RationalFunction>;
@ -1180,12 +1192,15 @@ namespace storm {
template class SparseMatrixBuilder<RationalFunction>;
template class SparseMatrix<RationalFunction>;
template std::ostream& operator<<(std::ostream& out, SparseMatrix<RationalFunction> const& matrix);
template std::vector<storm::RationalFunction> SparseMatrix<RationalFunction>::getPointwiseProductRowSumVector(storm::storage::SparseMatrix<storm::RationalFunction> const& otherMatrix) const;
// Intervals
template class MatrixEntry<typename SparseMatrix<Interval>::index_type, Interval>;
template std::ostream& operator<<(std::ostream& out, MatrixEntry<uint_fast64_t, Interval> const& entry);
template class SparseMatrixBuilder<Interval>;
template class SparseMatrix<Interval>;
template std::ostream& operator<<(std::ostream& out, SparseMatrix<Interval> const& matrix);
template std::vector<storm::Interval> SparseMatrix<Interval>::getPointwiseProductRowSumVector(storm::storage::SparseMatrix<storm::Interval> const& otherMatrix) const;
#endif

3
src/storage/SparseMatrix.h
View File

@ -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<value_type> getPointwiseProductRowSumVector(storm::storage::SparseMatrix<value_type> const& otherMatrix) const;
template<typename OtherValueType, typename ResultValueType = OtherValueType>
std::vector<ResultValueType> getPointwiseProductRowSumVector(storm::storage::SparseMatrix<OtherValueType> const& otherMatrix) const;
/*!
* Multiplies the matrix with the given vector and writes the result to the given result vector. If a

36
src/utility/vector.h
View File

@ -200,8 +200,8 @@ namespace storm {
* @param secondOperand The second operand.
* @param target The target vector.
*/
template<class T>
void applyPointwise(std::vector<T> const& firstOperand, std::vector<T> const& secondOperand, std::vector<T>& target, std::function<T (T const&, T const&, T const&)> const& function) {
template<class InValueType1, class InValueType2, class OutValueType>
void applyPointwise(std::vector<InValueType1> const& firstOperand, std::vector<InValueType2> const& secondOperand, std::vector<OutValueType>& target, std::function<OutValueType (InValueType1 const&, InValueType2 const&, OutValueType const&)> const& function) {
#ifdef STORM_HAVE_INTELTBB
tbb::parallel_for(tbb::blocked_range<uint_fast64_t>(0, target.size()),
[&](tbb::blocked_range<uint_fast64_t> const& range) {
@ -238,8 +238,8 @@ namespace storm {
* @param secondOperand The second operand.
* @param target The target vector.
*/
template<class T>
void applyPointwise(std::vector<T> const& firstOperand, std::vector<T> const& secondOperand, std::vector<T>& target, std::function<T (T const&, T const&)> function) {
template<class InValueType1, class InValueType2, class OutValueType>
void applyPointwise(std::vector<InValueType1> const& firstOperand, std::vector<InValueType2> const& secondOperand, std::vector<OutValueType>& target, std::function<OutValueType (InValueType1 const&, InValueType2 const&)> function) {
#ifdef STORM_HAVE_INTELTBB
tbb::parallel_for(tbb::blocked_range<uint_fast64_t>(0, target.size()),
[&](tbb::blocked_range<uint_fast64_t> const& range) {
@ -257,8 +257,8 @@ namespace storm {
* @param target The target vector.
* @param function The function to apply.
*/
template<class T>
void applyPointwise(std::vector<T> const& operand, std::vector<T>& target, std::function<T (T const&)> const& function) {
template<class InValueType, class OutValueType>
void applyPointwise(std::vector<InValueType> const& operand, std::vector<OutValueType>& target, std::function<OutValueType (InValueType const&)> const& function) {
#ifdef STORM_HAVE_INTELTBB
tbb::parallel_for(tbb::blocked_range<uint_fast64_t>(0, target.size()),
[&](tbb::blocked_range<uint_fast64_t> const& range) {
@ -276,9 +276,9 @@ namespace storm {
* @param secondOperand The second operand
* @param target The target vector.
*/
template<class T>
void addVectors(std::vector<T> const& firstOperand, std::vector<T> const& secondOperand, std::vector<T>& target) {
applyPointwise<T>(firstOperand, secondOperand, target, std::plus<T>());
template<class InValueType1, class InValueType2, class OutValueType>
void addVectors(std::vector<InValueType1> const& firstOperand, std::vector<InValueType2> const& secondOperand, std::vector<OutValueType>& target) {
applyPointwise<InValueType1, InValueType2, OutValueType>(firstOperand, secondOperand, target, std::plus<>());
}
/*!
@ -288,9 +288,9 @@ namespace storm {
* @param secondOperand The second operand
* @param target The target vector.
*/
template<class T>
void subtractVectors(std::vector<T> const& firstOperand, std::vector<T> const& secondOperand, std::vector<T>& target) {
applyPointwise<T>(firstOperand, secondOperand, target, std::minus<T>());
template<class InValueType1, class InValueType2, class OutValueType>
void subtractVectors(std::vector<InValueType1> const& firstOperand, std::vector<InValueType2> const& secondOperand, std::vector<OutValueType>& target) {
applyPointwise<InValueType1, InValueType2, OutValueType>(firstOperand, secondOperand, target, std::minus<>());
}
/*!
@ -300,9 +300,9 @@ namespace storm {
* @param secondOperand The second operand
* @param target The target vector.
*/
template<class T>
void multiplyVectorsPointwise(std::vector<T> const& firstOperand, std::vector<T> const& secondOperand, std::vector<T>& target) {
applyPointwise<T>(firstOperand, secondOperand, target, std::multiplies<T>());
template<class InValueType1, class InValueType2, class OutValueType>
void multiplyVectorsPointwise(std::vector<InValueType1> const& firstOperand, std::vector<InValueType2> const& secondOperand, std::vector<OutValueType>& target) {
applyPointwise<InValueType1, InValueType2, OutValueType>(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<class T>
void scaleVectorInPlace(std::vector<T>& target, T const& factor) {
applyPointwise<T>(target, target, [&] (T const& argument) { return argument * factor; });
template<class ValueType1, class ValueType2>
void scaleVectorInPlace(std::vector<ValueType1>& target, ValueType2 const& factor) {
applyPointwise<ValueType1, ValueType2>(target, target, [&] (ValueType1 const& argument) -> ValueType1 { return argument * factor; });
}
/*!

Write Preview
Loading…
Cancel
Save