diff --git a/src/builder/ExplicitDFTModelBuilder.cpp b/src/builder/ExplicitDFTModelBuilder.cpp index 91a16f2d2..a7284cb9c 100644 --- a/src/builder/ExplicitDFTModelBuilder.cpp +++ b/src/builder/ExplicitDFTModelBuilder.cpp @@ -114,22 +114,22 @@ namespace storm { } std::shared_ptr<storm::models::sparse::Model<ValueType>> model; - // Turn the probabilities into rates by multiplying each row with the exit rate of the state. - // TODO Matthias: avoid transforming back and forth - storm::storage::SparseMatrix<ValueType> rateMatrix(modelComponents.transitionMatrix); - for (uint_fast64_t row = 0; row < rateMatrix.getRowCount(); ++row) { - assert(row < modelComponents.markovianStates.size()); - if (modelComponents.markovianStates.get(row)) { - for (auto& entry : rateMatrix.getRow(row)) { - entry.setValue(entry.getValue() * modelComponents.exitRates[row]); - } - } - } if (deterministic) { + // Turn the probabilities into rates by multiplying each row with the exit rate of the state. + // TODO Matthias: avoid transforming back and forth + storm::storage::SparseMatrix<ValueType> rateMatrix(modelComponents.transitionMatrix); + for (uint_fast64_t row = 0; row < rateMatrix.getRowCount(); ++row) { + assert(row < modelComponents.markovianStates.size()); + if (modelComponents.markovianStates.get(row)) { + for (auto& entry : rateMatrix.getRow(row)) { + entry.setValue(entry.getValue() * modelComponents.exitRates[row]); + } + } + } model = std::make_shared<storm::models::sparse::Ctmc<ValueType>>(std::move(rateMatrix), std::move(modelComponents.stateLabeling)); } else { - model = std::make_shared<storm::models::sparse::MarkovAutomaton<ValueType>>(std::move(rateMatrix), std::move(modelComponents.stateLabeling), std::move(modelComponents.markovianStates), std::move(modelComponents.exitRates)); + model = std::make_shared<storm::models::sparse::MarkovAutomaton<ValueType>>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), std::move(modelComponents.markovianStates), std::move(modelComponents.exitRates), true); } model->printModelInformationToStream(std::cout); diff --git a/src/models/sparse/MarkovAutomaton.cpp b/src/models/sparse/MarkovAutomaton.cpp index c757af1a0..8276f519d 100644 --- a/src/models/sparse/MarkovAutomaton.cpp +++ b/src/models/sparse/MarkovAutomaton.cpp @@ -34,6 +34,19 @@ namespace storm { this->turnRatesToProbabilities(); } + template <typename ValueType, typename RewardModelType> + MarkovAutomaton<ValueType, RewardModelType>::MarkovAutomaton(storm::storage::SparseMatrix<ValueType>&& transitionMatrix, + storm::models::sparse::StateLabeling&& stateLabeling, + storm::storage::BitVector const& markovianStates, + std::vector<ValueType> const& exitRates, + bool probabilities, + std::unordered_map<std::string, RewardModelType>&& rewardModels, + boost::optional<std::vector<LabelSet>>&& optionalChoiceLabeling) + : NondeterministicModel<ValueType, RewardModelType>(storm::models::ModelType::MarkovAutomaton, std::move(transitionMatrix), std::move(stateLabeling), std::move(rewardModels), std::move(optionalChoiceLabeling)), markovianStates(markovianStates), exitRates(std::move(exitRates)), closed(false) { + assert(probabilities); + assert(this->getTransitionMatrix().isProbabilistic()); + } + template <typename ValueType, typename RewardModelType> bool MarkovAutomaton<ValueType, RewardModelType>::isClosed() const { return closed; diff --git a/src/models/sparse/MarkovAutomaton.h b/src/models/sparse/MarkovAutomaton.h index ed807ab84..e335f5050 100644 --- a/src/models/sparse/MarkovAutomaton.h +++ b/src/models/sparse/MarkovAutomaton.h @@ -49,6 +49,25 @@ namespace storm { std::unordered_map<std::string, RewardModelType>&& rewardModels = std::unordered_map<std::string, RewardModelType>(), boost::optional<std::vector<LabelSet>>&& optionalChoiceLabeling = boost::optional<std::vector<LabelSet>>()); + /*! + * Constructs a model by moving the given data. + * + * @param transitionMatrix The matrix representing the transitions in the model in terms of rates. + * @param stateLabeling The labeling of the states. + * @param markovianStates A bit vector indicating the Markovian states of the automaton. + * @param exitRates A vector storing the exit rates 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. + * @param probabilities Flag if transitions matrix contains probabilities or rates + */ + MarkovAutomaton(storm::storage::SparseMatrix<ValueType>&& transitionMatrix, + storm::models::sparse::StateLabeling&& stateLabeling, + storm::storage::BitVector const& markovianStates, + std::vector<ValueType> const& exitRates, + bool probabilities, + std::unordered_map<std::string, RewardModelType>&& rewardModels = std::unordered_map<std::string, RewardModelType>(), + boost::optional<std::vector<LabelSet>>&& optionalChoiceLabeling = boost::optional<std::vector<LabelSet>>()); + MarkovAutomaton(MarkovAutomaton<ValueType, RewardModelType> const& other) = default; MarkovAutomaton& operator=(MarkovAutomaton<ValueType, RewardModelType> const& other) = default;