Browse Source

Quick fix for CTMC instantiation

tempestpy_adaptions
Matthias Volk 8 years ago
parent
commit
a18161b6e3
  1. 7
      src/storm/models/sparse/Ctmc.cpp
  2. 9
      src/storm/models/sparse/Ctmc.h
  3. 19
      src/storm/utility/ModelInstantiator.h

7
src/storm/models/sparse/Ctmc.cpp

@ -35,7 +35,12 @@ namespace storm {
std::vector<ValueType> const& Ctmc<ValueType, RewardModelType>::getExitRateVector() const { std::vector<ValueType> const& Ctmc<ValueType, RewardModelType>::getExitRateVector() const {
return exitRates; return exitRates;
} }
template <typename ValueType, typename RewardModelType>
std::vector<ValueType>& Ctmc<ValueType, RewardModelType>::getExitRateVector() {
return exitRates;
}
template <typename ValueType, typename RewardModelType> template <typename ValueType, typename RewardModelType>
std::vector<ValueType> Ctmc<ValueType, RewardModelType>::createExitRateVector(storm::storage::SparseMatrix<ValueType> const& rateMatrix) { std::vector<ValueType> Ctmc<ValueType, RewardModelType>::createExitRateVector(storm::storage::SparseMatrix<ValueType> const& rateMatrix) {
std::vector<ValueType> exitRates(rateMatrix.getRowCount()); std::vector<ValueType> exitRates(rateMatrix.getRowCount());

9
src/storm/models/sparse/Ctmc.h

@ -65,7 +65,14 @@ namespace storm {
* @return The exit rate vector. * @return The exit rate vector.
*/ */
std::vector<ValueType> const& getExitRateVector() const; 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: private:
/*! /*!
* Computes the exit rate vector based on the given rate matrix. * Computes the exit rate vector based on the given rate matrix.

19
src/storm/utility/ModelInstantiator.h

@ -67,15 +67,28 @@ namespace storm {
template<typename PMT = ParametricSparseModelType> template<typename PMT = ParametricSparseModelType>
typename std::enable_if< typename std::enable_if<
std::is_same<PMT,storm::models::sparse::Dtmc<typename ParametricSparseModelType::ValueType>>::value || 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 >::type
initializeModelSpecificData(PMT const& parametricModel) { initializeModelSpecificData(PMT const& parametricModel) {
auto stateLabelingCopy = parametricModel.getStateLabeling(); auto stateLabelingCopy = parametricModel.getStateLabeling();
auto choiceLabelingCopy = parametricModel.getOptionalChoiceLabeling(); auto choiceLabelingCopy = parametricModel.getOptionalChoiceLabeling();
this->instantiatedModel = std::make_shared<ConstantSparseModelType>(buildDummyMatrix(parametricModel.getTransitionMatrix()), std::move(stateLabelingCopy), buildDummyRewardModels(parametricModel.getRewardModels()), std::move(choiceLabelingCopy)); 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> template<typename PMT = ParametricSparseModelType>
typename std::enable_if< typename std::enable_if<
std::is_same<PMT,storm::models::sparse::MarkovAutomaton<typename ParametricSparseModelType::ValueType>>::value std::is_same<PMT,storm::models::sparse::MarkovAutomaton<typename ParametricSparseModelType::ValueType>>::value

Loading…
Cancel
Save