From f2ab549b36196fcf8a01df22294ff10391db04f2 Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@cs.rwth-aachen.de>
Date: Mon, 29 May 2017 11:41:04 +0200
Subject: [PATCH] fixed compiling storm-dft

---
 .../builder/ExplicitDFTModelBuilder.cpp       | 19 +++++--------------
 .../builder/ExplicitDFTModelBuilderApprox.cpp | 18 +++++++++++++++---
 2 files changed, 20 insertions(+), 17 deletions(-)

diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp b/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp
index bdee4eedc..25daedf7a 100644
--- a/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp
+++ b/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp
@@ -138,22 +138,13 @@ namespace storm {
             }
 
             std::shared_ptr<storm::models::sparse::Model<ValueType>> model;
-            
+            storm::storage::sparse::ModelComponents<ValueType> components(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling));
+                    components.exitRates = std::move(modelComponents.exitRates);
             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) {
-                    STORM_LOG_ASSERT(row < modelComponents.markovianStates.size(), "Row exceeds no. of markovian states.");
-                    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.exitRates), std::move(modelComponents.stateLabeling));
+                model = std::make_shared<storm::models::sparse::Ctmc<ValueType>>(std::move(components));
             } else {
-                std::shared_ptr<storm::models::sparse::MarkovAutomaton<ValueType>> ma = 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);
+                    components.markovianStates = std::move(modelComponents.markovianStates);
+                    std::shared_ptr<storm::models::sparse::MarkovAutomaton<ValueType>> ma = std::make_shared<storm::models::sparse::MarkovAutomaton<ValueType>>(std::move(components));
                 if (ma->hasOnlyTrivialNondeterminism()) {
                     // Markov automaton can be converted into CTMC
                     model = ma->convertToCTMC();
diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp b/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp
index 84eaa21a7..0c7d69628 100644
--- a/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp
+++ b/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp
@@ -525,7 +525,11 @@ namespace storm {
                     }
                     STORM_LOG_TRACE("Exit rates: " << modelComponents.exitRates);
 
-                    std::shared_ptr<storm::models::sparse::MarkovAutomaton<ValueType>> ma = std::make_shared<storm::models::sparse::MarkovAutomaton<ValueType>>(std::move(matrix), std::move(labeling), modelComponents.markovianStates, modelComponents.exitRates);
+                    storm::storage::sparse::ModelComponents<ValueType> maComponents(std::move(matrix), std::move(labeling));
+                    maComponents.rateTransitions = true;
+                    maComponents.markovianStates = modelComponents.markovianStates;
+                    maComponents.exitRates = modelComponents.exitRates;
+                    std::shared_ptr<storm::models::sparse::MarkovAutomaton<ValueType>> ma = std::make_shared<storm::models::sparse::MarkovAutomaton<ValueType>>(std::move(maComponents));
                     if (ma->hasOnlyTrivialNondeterminism()) {
                         // Markov automaton can be converted into CTMC
                         // TODO Matthias: change components which were not moved accordingly
@@ -573,9 +577,17 @@ namespace storm {
 
                 std::shared_ptr<storm::models::sparse::MarkovAutomaton<ValueType>> ma;
                 if (copy) {
-                    ma = std::make_shared<storm::models::sparse::MarkovAutomaton<ValueType>>(modelComponents.transitionMatrix, modelComponents.stateLabeling, modelComponents.markovianStates, modelComponents.exitRates);
+                    storm::storage::sparse::ModelComponents<ValueType> maComponents(modelComponents.transitionMatrix, modelComponents.stateLabeling);
+                    maComponents.rateTransitions = true;
+                    maComponents.markovianStates = modelComponents.markovianStates;
+                    maComponents.exitRates = modelComponents.exitRates;
+                    std::shared_ptr<storm::models::sparse::MarkovAutomaton<ValueType>> ma = std::make_shared<storm::models::sparse::MarkovAutomaton<ValueType>>(std::move(maComponents));
                 } else {
-                    ma = std::make_shared<storm::models::sparse::MarkovAutomaton<ValueType>>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), std::move(modelComponents.markovianStates), std::move(modelComponents.exitRates));
+                    storm::storage::sparse::ModelComponents<ValueType> maComponents(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling));
+                    maComponents.rateTransitions = true;
+                    maComponents.markovianStates = std::move(modelComponents.markovianStates);
+                    maComponents.exitRates = std::move(modelComponents.exitRates);
+                    std::shared_ptr<storm::models::sparse::MarkovAutomaton<ValueType>> ma = std::make_shared<storm::models::sparse::MarkovAutomaton<ValueType>>(std::move(maComponents));
                 }
                 if (ma->hasOnlyTrivialNondeterminism()) {
                     // Markov automaton can be converted into CTMC