One conversion less for MA

Former-commit-id: d0b47adf9b

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);

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;

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;