diff --git a/src/builder/ExplicitDFTModelBuilder.cpp b/src/builder/ExplicitDFTModelBuilder.cpp index fa8be6e1a..820dee6a4 100644 --- a/src/builder/ExplicitDFTModelBuilder.cpp +++ b/src/builder/ExplicitDFTModelBuilder.cpp @@ -120,7 +120,7 @@ namespace storm { } } } - model = std::make_shared>(std::move(rateMatrix), std::move(modelComponents.stateLabeling)); + model = std::make_shared>(std::move(rateMatrix), std::move(modelComponents.exitRates), std::move(modelComponents.stateLabeling)); } else { std::shared_ptr> ma = std::make_shared>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), std::move(modelComponents.markovianStates), std::move(modelComponents.exitRates), true); if (ma->hasOnlyTrivialNondeterminism()) { diff --git a/src/models/sparse/Ctmc.cpp b/src/models/sparse/Ctmc.cpp index 62347c81b..1d07c48a9 100644 --- a/src/models/sparse/Ctmc.cpp +++ b/src/models/sparse/Ctmc.cpp @@ -24,6 +24,13 @@ namespace storm { exitRates = createExitRateVector(this->getTransitionMatrix()); } + template + Ctmc::Ctmc(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRates, storm::models::sparse::StateLabeling const& stateLabeling, + std::unordered_map const& rewardModels, + boost::optional> const& optionalChoiceLabeling) + : DeterministicModel(storm::models::ModelType::Ctmc, std::move(rateMatrix), std::move(stateLabeling), std::move(rewardModels), std::move(optionalChoiceLabeling)), exitRates(exitRates) { + } + template std::vector const& Ctmc::getExitRateVector() const { return exitRates; diff --git a/src/models/sparse/Ctmc.h b/src/models/sparse/Ctmc.h index 716b80373..fc933ae7d 100644 --- a/src/models/sparse/Ctmc.h +++ b/src/models/sparse/Ctmc.h @@ -38,6 +38,20 @@ namespace storm { std::unordered_map&& rewardModels = std::unordered_map(), boost::optional>&& optionalChoiceLabeling = boost::optional>()); + /*! + * Constructs a model from the given data. + * + * @param rateMatrix The matrix representing the transitions in the model. + * @param exitRates The exit rates of all states. + * @param stateLabeling The labeling of the states. + * @param rewardModels A mapping of reward model names to reward models. + * @param optionalChoiceLabeling A vector that represents the labels associated with the choices of each state. + */ + Ctmc(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRates, storm::models::sparse::StateLabeling const& stateLabeling, + std::unordered_map const& rewardModels = std::unordered_map(), + boost::optional> const& optionalChoiceLabeling = boost::optional>()); + + Ctmc(Ctmc const& ctmc) = default; Ctmc& operator=(Ctmc const& ctmc) = default;