Browse Source

modelMemoryProduct can now return the considered model and memory structure

tempestpy_adaptions
TimQu 7 years ago
parent
commit
2bccb7af78
  1. 10
      src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp
  2. 2
      src/storm/storage/memorystructure/SparseModelMemoryProduct.h

10
src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp

@ -495,6 +495,16 @@ namespace storm {
return storm::utility::builder::buildModelFromComponents(resultType, std::move(components));
}
template <typename ValueType, typename RewardModelType>
storm::models::sparse::Model<ValueType, RewardModelType> const& SparseModelMemoryProduct<ValueType, RewardModelType>::getOriginalModel() const {
return model;
}
template <typename ValueType, typename RewardModelType>
storm::storage::MemoryStructure const& SparseModelMemoryProduct<ValueType, RewardModelType>::getMemory() const {
return memory;
}
template class SparseModelMemoryProduct<double>;
template class SparseModelMemoryProduct<double, storm::models::sparse::StandardRewardModel<storm::Interval>>;
template class SparseModelMemoryProduct<storm::RationalNumber>;

2
src/storm/storage/memorystructure/SparseModelMemoryProduct.h

@ -41,6 +41,8 @@ namespace storm {
// An invalid index is returned, if the specifyied state does not exist (i.e., if it is not part of product).
uint64_t const& getResultState(uint64_t const& modelState, uint64_t const& memoryState) const;
storm::models::sparse::Model<ValueType, RewardModelType> const& getOriginalModel() const;
storm::storage::MemoryStructure const& getMemory() const;
private:
// Computes for each pair of memory state and model transition index the successor memory state

Loading…
Cancel
Save