diff --git a/src/storm/models/sparse/Ctmc.cpp b/src/storm/models/sparse/Ctmc.cpp index 884eb359d..a43aded44 100644 --- a/src/storm/models/sparse/Ctmc.cpp +++ b/src/storm/models/sparse/Ctmc.cpp @@ -35,7 +35,12 @@ namespace storm { std::vector<ValueType> const& Ctmc<ValueType, RewardModelType>::getExitRateVector() const { return exitRates; } - + + template <typename ValueType, typename RewardModelType> + std::vector<ValueType>& Ctmc<ValueType, RewardModelType>::getExitRateVector() { + return exitRates; + } + template <typename ValueType, typename RewardModelType> std::vector<ValueType> Ctmc<ValueType, RewardModelType>::createExitRateVector(storm::storage::SparseMatrix<ValueType> const& rateMatrix) { std::vector<ValueType> exitRates(rateMatrix.getRowCount()); diff --git a/src/storm/models/sparse/Ctmc.h b/src/storm/models/sparse/Ctmc.h index 417a899a4..8bb1f37ed 100644 --- a/src/storm/models/sparse/Ctmc.h +++ b/src/storm/models/sparse/Ctmc.h @@ -65,7 +65,14 @@ namespace storm { * @return The exit rate vector. */ std::vector<ValueType> const& getExitRateVector() const; - + + /*! + * Retrieves the vector of exit rates of the model. + * + * @return The exit rate vector. + */ + std::vector<ValueType>& getExitRateVector(); + private: /*! * Computes the exit rate vector based on the given rate matrix. diff --git a/src/storm/utility/ModelInstantiator.h b/src/storm/utility/ModelInstantiator.h index 17de0ea21..ce5154a2b 100644 --- a/src/storm/utility/ModelInstantiator.h +++ b/src/storm/utility/ModelInstantiator.h @@ -67,15 +67,28 @@ namespace storm { template<typename PMT = ParametricSparseModelType> typename std::enable_if< std::is_same<PMT,storm::models::sparse::Dtmc<typename ParametricSparseModelType::ValueType>>::value || - std::is_same<PMT,storm::models::sparse::Mdp<typename ParametricSparseModelType::ValueType>>::value || - std::is_same<PMT,storm::models::sparse::Ctmc<typename ParametricSparseModelType::ValueType>>::value + std::is_same<PMT,storm::models::sparse::Mdp<typename ParametricSparseModelType::ValueType>>::value >::type initializeModelSpecificData(PMT const& parametricModel) { auto stateLabelingCopy = parametricModel.getStateLabeling(); auto choiceLabelingCopy = parametricModel.getOptionalChoiceLabeling(); this->instantiatedModel = std::make_shared<ConstantSparseModelType>(buildDummyMatrix(parametricModel.getTransitionMatrix()), std::move(stateLabelingCopy), buildDummyRewardModels(parametricModel.getRewardModels()), std::move(choiceLabelingCopy)); } - + + template<typename PMT = ParametricSparseModelType> + typename std::enable_if< + std::is_same<PMT,storm::models::sparse::Ctmc<typename ParametricSparseModelType::ValueType>>::value + >::type + initializeModelSpecificData(PMT const& parametricModel) { + auto stateLabelingCopy = parametricModel.getStateLabeling(); + auto choiceLabelingCopy = parametricModel.getOptionalChoiceLabeling(); + std::vector<ConstantType> exitRates(parametricModel.getExitRateVector().size(), storm::utility::one<ConstantType>()); + this->instantiatedModel = std::make_shared<ConstantSparseModelType>(buildDummyMatrix(parametricModel.getTransitionMatrix()), std::move(exitRates), std::move(stateLabelingCopy), buildDummyRewardModels(parametricModel.getRewardModels()), std::move(choiceLabelingCopy)); + + initializeVectorMapping(this->instantiatedModel->getExitRateVector(), this->functions, this->vectorMapping, parametricModel.getExitRateVector()); + } + + template<typename PMT = ParametricSparseModelType> typename std::enable_if< std::is_same<PMT,storm::models::sparse::MarkovAutomaton<typename ParametricSparseModelType::ValueType>>::value